pyfcstm.verify.topology

Topological verification algorithms for pyfcstm.verify.

This module implements the group-1 verification algorithms that work only on the hierarchical state topology. The algorithms project a pyfcstm.model.StateMachine into a leaf-level macro graph and then run structural graph queries over that projection. They intentionally ignore guard satisfiability, event availability, transition ordering, and runtime variable evolution; positive reachability results are therefore over-approximations of runtime behavior, while unreachable results describe structural topology facts.

The module contains:

LeafLevelGraph - Immutable container for the projected leaf graph.
FinitenessReport - Report object for topological_finite().
InevitabilityReport - Report object for topological_inevitable_terminator().
build_leaf_level_macro_graph() - Build the guard-agnostic projection.
topological_reachable_set() - Compute reachable leaf states.
unreachable_states() - Find structurally unreachable leaf states.
strongly_connected_components() - Find cyclic leaf-level regions.
topological_finite() - Detect reachable no-exit regions.
topological_inevitable_terminator() - Detect non-terminating topology.
event_emission_to_consumer_reachable() - Detect events whose consumers are all unreachable.

Note

The graph projection is independent from the diagnostics package. Diagnostic integration is expected to wrap these functions and translate their plain Python return values into diagnostic payloads.

Example:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> ast = parse_with_grammar_entry("state Root;", "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> graph = build_leaf_level_macro_graph(machine)
>>> graph.nodes
('Root',)
>>> graph.edges[EXIT_ROOT_SINK]
()

EXIT_ROOT_SINK

pyfcstm.verify.topology.EXIT_ROOT_SINK = '⊥_root': Synthetic sink used for transitions that exit the root state.

all

pyfcstm.verify.topology.__all__ = ['EXIT_ROOT_SINK', 'FinitenessReport', 'InevitabilityReport', 'LeafLevelGraph', 'build_leaf_level_macro_graph', 'event_emission_to_consumer_reachable', 'strongly_connected_components', 'topological_finite', 'topological_inevitable_terminator', 'topological_reachable_set', 'unreachable_states']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

LeafLevelGraph

class pyfcstm.verify.topology.LeafLevelGraph(nodes: Tuple[str, ...], edges: Mapping[str, Tuple[str, ...]])[source]

Leaf-level macro graph projected from a hierarchical state machine.

Each node is a dotted path for a leaf state in the source model. Edges describe guard-agnostic macro steps between leaf states after expanding composite targets through their initial transitions and bubbling leaf exits through parent transitions. The synthetic EXIT_ROOT_SINK key is present in edges so callers can query root termination uniformly.

Parameters:

nodes (Tuple[str, ...]) – Dotted paths of leaf states in stable sorted order.
edges (Mapping[str, Tuple[str, ...]]) – Mapping from each leaf path, and optionally EXIT_ROOT_SINK, to sorted successor paths. The mapping is copied into a read-only proxy during initialization.

Example:

>>> graph = LeafLevelGraph(
...     nodes=("Root.Idle",),
...     edges={"Root.Idle": (EXIT_ROOT_SINK,), EXIT_ROOT_SINK: ()},
... )
>>> graph.nodes
('Root.Idle',)
>>> graph.edges["Root.Idle"]
('⊥_root',)
>>> graph.edges["Root.Idle"] = ("Root.Other",)
Traceback (most recent call last):
...
TypeError: 'mappingproxy' object does not support item assignment

__post_init__() → None[source]

Freeze the edge mapping after dataclass initialization.

Returns:: None.
Return type:: None

Example:

>>> graph = LeafLevelGraph(nodes=("Root.A",), edges={"Root.A": ()})
>>> type(graph.edges).__name__
'mappingproxy'

FinitenessReport

class pyfcstm.verify.topology.FinitenessReport(finite: bool, counterexamples: Tuple[Tuple[Literal['trap_cycle', 'deadlock'], object], ...])[source]

Result for topological_finite().

The report is true when every root-reachable leaf can eventually reach the synthetic root-exit sink in the topology graph. Counterexamples are plain tuples so later diagnostic layers can choose their own payload shape without coupling the topology package to the diagnostics package.

Parameters:

finite (bool) – True when every root-reachable leaf can reach the root exit sink in the topological graph.
counterexamples (Tuple[Tuple[Literal['trap_cycle', 'deadlock'], object], ...]) – Counterexamples as ('trap_cycle', scc_tuple) or ('deadlock', state_path) entries.

Example:

>>> report = FinitenessReport(finite=False, counterexamples=(
...     ("deadlock", "Root.Stuck"),
... ))
>>> report.finite
False
>>> report.counterexamples[0][0]
'deadlock'

InevitabilityReport

class pyfcstm.verify.topology.InevitabilityReport(inevitable: bool, counterexample_path: Tuple[str, ...] | None)[source]

Result for topological_inevitable_terminator().

The report is true only when the topology has no root-reachable cycle or deadlock that could keep execution away from the root terminator forever. A false report contains one representative path or SCC; it is not intended to enumerate every possible non-terminating region.

Parameters:

inevitable (bool) – True when no root-reachable topological path can stay in a cycle or deadlock forever.
counterexample_path (Optional[Tuple[str, ...]]) – Representative non-terminating SCC or deadlock path, or None when inevitable is true.

Example:

>>> report = InevitabilityReport(
...     inevitable=False,
...     counterexample_path=("Root.Loop",),
... )
>>> report.inevitable
False
>>> report.counterexample_path
('Root.Loop',)

build_leaf_level_macro_graph

pyfcstm.verify.topology.build_leaf_level_macro_graph(machine: StateMachine) → LeafLevelGraph[source]

Build the guard-agnostic leaf-level macro graph for machine.

The projection follows normal leaf-to-leaf transitions, expands composite targets through their initial transitions, and bubbles Leaf -> [*] transitions through parent outgoing transitions. Parent-level transitions whose source is a composite state are therefore considered only after a descendant leaf explicitly exits to that parent; they are not copied onto every active descendant leaf. If a non-root parent has no outgoing transition, the bubble is an off-cliff exit and contributes no edge. A root leaf is treated as root-exit-capable by adding an edge to EXIT_ROOT_SINK.

Parameters:: machine (StateMachine) – State machine to project.
Returns:: Leaf-level macro graph.
Return type:: LeafLevelGraph
Raises:: TypeError – If a transition endpoint uses a model object type that is not produced by the FCSTM grammar pipeline.

Example:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> source = '''
... state Root {
...     state Idle;
...     [*] -> Idle;
...     Idle -> [*];
... }
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> graph = build_leaf_level_macro_graph(machine)
>>> graph.edges["Root.Idle"]
('⊥_root',)

topological_reachable_set

pyfcstm.verify.topology.topological_reachable_set(machine: StateMachine) → Dict[str, Tuple[str, ...]][source]

Compute guard-agnostic reachable leaf states for every model state.

Composite states are first projected through their initial descent and then closed over the leaf-level macro graph. Leaf-state results omit the leaf itself, matching the existing inspect reachability convention for cycles. The returned mapping is keyed by dotted state paths for all states, not only leaves.

Parameters:: machine (StateMachine) – State machine to inspect.
Returns:: Mapping from every state path to sorted reachable leaf paths.
Return type:: Dict[str, Tuple[str, …]]

Example:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> source = '''
... state Root {
...     state A;
...     state B;
...     [*] -> A;
...     A -> B;
... }
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> topological_reachable_set(machine)["Root.A"]
('Root.B',)

unreachable_states

pyfcstm.verify.topology.unreachable_states(machine: StateMachine) → Tuple[str, ...][source]

Return non-pseudo leaf states unreachable from the root topology.

The result uses topology reachability from the root initial descent and filters out pseudo leaf states. Composite states are not returned directly; their unreachable leaf descendants are reported instead.

Parameters:: machine (StateMachine) – State machine to inspect.
Returns:: Sorted unreachable leaf state paths.
Return type:: Tuple[str, …]

Example:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> source = '''
... state Root {
...     state A;
...     state Lost;
...     [*] -> A;
... }
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> unreachable_states(machine)
('Root.Lost',)

strongly_connected_components

pyfcstm.verify.topology.strongly_connected_components(machine: StateMachine) → Tuple[Tuple[str, ...], ...][source]

Return non-trivial SCCs in the leaf-level topology graph.

A non-trivial SCC is either a component with more than one leaf or a single leaf with a self-loop. The implementation is iterative so deeply nested or wide generated models are not limited by Python’s recursion depth.

Parameters:: machine (StateMachine) – State machine to inspect.
Returns:: Sorted non-trivial SCCs.
Return type:: Tuple[Tuple[str, …], …]

Example:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> source = '''
... state Root {
...     state A;
...     state B;
...     [*] -> A;
...     A -> B;
...     B -> A;
... }
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> strongly_connected_components(machine)
(('Root.A', 'Root.B'),)

topological_finite

pyfcstm.verify.topology.topological_finite(machine: StateMachine) → FinitenessReport[source]

Check whether all root-reachable leaves can reach the root exit sink.

This check accepts models where every reachable leaf has at least one topological route to termination, even if runtime guards could block that route. It reports closed trap cycles that cannot reach the root sink and deadlock leaves with no outgoing projected edge.

Parameters:: machine (StateMachine) – State machine to inspect.
Returns:: Finiteness report with trap-cycle and deadlock counterexamples.
Return type:: FinitenessReport

Example:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> source = '''
... state Root {
...     state A;
...     state B;
...     [*] -> A;
...     A -> B;
... }
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> report = topological_finite(machine)
>>> report.finite
False
>>> report.counterexamples
(('deadlock', 'Root.B'),)

topological_inevitable_terminator

pyfcstm.verify.topology.topological_inevitable_terminator(machine: StateMachine) → InevitabilityReport[source]

Check whether every topological path must eventually terminate.

This is an intentionally structural check: any root-reachable deadlock or cycle is enough to produce a non-inevitability counterexample, even when another outgoing edge could exit at runtime.

Parameters:: machine (StateMachine) – State machine to inspect.
Returns:: Inevitability report.
Return type:: InevitabilityReport

Example:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> source = '''
... state Root {
...     state A;
...     [*] -> A;
...     A -> A;
...     A -> [*];
... }
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> report = topological_inevitable_terminator(machine)
>>> report.inevitable
False
>>> report.counterexample_path
('Root.A',)

event_emission_to_consumer_reachable

pyfcstm.verify.topology.event_emission_to_consumer_reachable(machine: StateMachine) → Tuple[str, ...][source]

Return events whose consumer source states are all unreachable.

Unused declared events are ignored here; they remain the responsibility of the existing design-health unused-event check. A transition is treated as an event consumer at the point where its source can be selected. Leaf-source consumers are reachable when their leaf is root-reachable. Initial-transition consumers are reachable when the owning composite can be entered. Composite-source consumers are reachable only when a root-reachable descendant leaf can explicitly exit to the composite boundary, because parent-level transitions are considered after Leaf -> [*] bubble semantics rather than while any descendant leaf is merely active. If every consumer source for a used event is outside these root-reachable topology points, the event’s qualified name is returned.

Parameters:: machine (StateMachine) – State machine to inspect.
Returns:: Sorted qualified event names whose consumers are all unreachable.
Return type:: Tuple[str, …]

Example:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> source = '''
... state Root {
...     event Panic;
...     state A;
...     state Lost;
...     [*] -> A;
...     Lost -> A : Panic;
... }
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> event_emission_to_consumer_reachable(machine)
('Root.Panic',)

pyfcstm.verify.topology

EXIT_ROOT_SINK

__all__

LeafLevelGraph

FinitenessReport

InevitabilityReport

build_leaf_level_macro_graph

topological_reachable_set

unreachable_states

strongly_connected_components

topological_finite

topological_inevitable_terminator

event_emission_to_consumer_reachable

all