pyfcstm.verify.registry

Algorithm registry for pyfcstm.verify.

The registry maps stable algorithm names to pyfcstm.verify.taxonomy.VerifyAlgorithmMeta entries. Implemented structural and SMT-local algorithms carry callables; planned bounded-search entries stay present with impl=None so downstream policy can expose the future surface without running it automatically.

Example:

>>> from pyfcstm.verify.registry import REGISTRY
>>> REGISTRY["dead_guard"].impl.__name__
'dead_guard'
>>> REGISTRY["bounded_reachability"].impl is None
True

REGISTRY

pyfcstm.verify.registry.REGISTRY: Mapping[str, VerifyAlgorithmMeta] = mappingproxy({'topological_reachable_set': VerifyAlgorithmMeta(name='topological_reachable_set', description='Compute guard-agnostic reachable states over the transition topology.', closedness='closed', complexity_tier='structural', smt_logic=None, formula_size_scaling='none', call_count_scaling='linear_in_states', incremental=False, fallback_unknown_risk='none', recommended_tactic=None, quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=(), verification_scope='topological_only', dominant_dim=('V', 'E', 'depth'), diagnostic_codes=(), impl=<function topological_reachable_set>), 'unreachable_states': VerifyAlgorithmMeta(name='unreachable_states', description='Report states unreachable from the root entry topology.', closedness='closed', complexity_tier='structural', smt_logic=None, formula_size_scaling='none', call_count_scaling='linear_in_states', incremental=False, fallback_unknown_risk='none', recommended_tactic=None, quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=(), verification_scope='topological_only', dominant_dim=('V_leaf', 'depth'), diagnostic_codes=('W_UNREACHABLE_STATE',), impl=<function unreachable_states>), 'strongly_connected_components': VerifyAlgorithmMeta(name='strongly_connected_components', description='Find non-trivial strongly connected components in the topology graph.', closedness='closed', complexity_tier='structural', smt_logic=None, formula_size_scaling='none', call_count_scaling='linear_in_states', incremental=False, fallback_unknown_risk='none', recommended_tactic=None, quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=(), verification_scope='topological_only', dominant_dim=('V', 'E'), diagnostic_codes=('I_NONTRIVIAL_SCC',), impl=<function strongly_connected_components>), 'topological_finite': VerifyAlgorithmMeta(name='topological_finite', description='Check whether topology has an exit path rather than a closed no-exit region.', closedness='closed', complexity_tier='structural', smt_logic=None, formula_size_scaling='none', call_count_scaling='linear_in_states', incremental=False, fallback_unknown_risk='none', recommended_tactic=None, quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=(), verification_scope='topological_only', dominant_dim=('V', 'E'), diagnostic_codes=('W_TOPOLOGICAL_NOEXIT',), impl=<function topological_finite>), 'topological_inevitable_terminator': VerifyAlgorithmMeta(name='topological_inevitable_terminator', description='Identify topology regions that are not forced to reach a terminator.', closedness='closed', complexity_tier='structural', smt_logic=None, formula_size_scaling='none', call_count_scaling='linear_in_states', incremental=False, fallback_unknown_risk='none', recommended_tactic=None, quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=(), verification_scope='topological_only', dominant_dim=('V', 'E'), diagnostic_codes=('I_TOPOLOGICAL_NON_TERMINATING',), impl=<function topological_inevitable_terminator>), 'event_emission_to_consumer_reachable': VerifyAlgorithmMeta(name='event_emission_to_consumer_reachable', description='Check whether each used event has a topologically reachable consumer source.', closedness='closed', complexity_tier='structural', smt_logic=None, formula_size_scaling='none', call_count_scaling='linear_in_transitions', incremental=False, fallback_unknown_risk='none', recommended_tactic=None, quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=(), verification_scope='topological_only', dominant_dim=('events', 'E'), diagnostic_codes=('W_EVENT_UNREACHABLE_EMIT',), impl=<function event_emission_to_consumer_reachable>), 'dead_guard': VerifyAlgorithmMeta(name='dead_guard', description='Detect guards that are unsatisfiable under variable constraints.', closedness='closed', complexity_tier='smt_linear', smt_logic='QF_LIRA', formula_size_scaling='constant', call_count_scaling='linear_in_transitions', incremental=False, fallback_unknown_risk='medium', recommended_tactic='qflia', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='smt_local', dominant_dim=('E', 'vars'), diagnostic_codes=('W_DEAD_GUARD',), impl=<function dead_guard>), 'guard_tautology': VerifyAlgorithmMeta(name='guard_tautology', description='Detect guards that are always true under variable constraints.', closedness='closed', complexity_tier='smt_linear', smt_logic='QF_LIRA', formula_size_scaling='constant', call_count_scaling='linear_in_transitions', incremental=False, fallback_unknown_risk='medium', recommended_tactic='qflia', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='smt_local', dominant_dim=('E', 'vars'), diagnostic_codes=('W_GUARD_TAUTOLOGY',), impl=<function guard_tautology>), 'forced_guard_unsat_under_init': VerifyAlgorithmMeta(name='forced_guard_unsat_under_init', description='Detect forced-transition guards unsatisfiable under initial variable values.', closedness='closed', complexity_tier='smt_linear', smt_logic='QF_LIRA', formula_size_scaling='constant', call_count_scaling='linear_in_transitions', incremental=False, fallback_unknown_risk='low', recommended_tactic='qflia', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='smt_local', dominant_dim=('forced_transitions', 'vars'), diagnostic_codes=('W_FORCED_GUARD_UNSAT',), impl=<function forced_guard_unsat_under_init>), 'effect_no_op_under_guard': VerifyAlgorithmMeta(name='effect_no_op_under_guard', description='Detect transition effects that are no-ops whenever the guard holds.', closedness='closed', complexity_tier='smt_linear', smt_logic='QF_LIRA', formula_size_scaling='constant', call_count_scaling='linear_in_transitions', incremental=False, fallback_unknown_risk='medium', recommended_tactic='qflia', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='smt_local', dominant_dim=('E', 'vars'), diagnostic_codes=('W_EFFECT_SMT_NO_OP',), impl=<function effect_no_op_under_guard>), 'effect_contradicts_guard': VerifyAlgorithmMeta(name='effect_contradicts_guard', description='Detect effects whose post-state contradicts their transition guard.', closedness='closed', complexity_tier='smt_linear', smt_logic='QF_LIRA', formula_size_scaling='constant', call_count_scaling='linear_in_transitions', incremental=False, fallback_unknown_risk='medium', recommended_tactic='qflia', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='smt_local', dominant_dim=('E', 'vars'), diagnostic_codes=('I_EFFECT_GUARD_CONTRADICT',), impl=<function effect_contradicts_guard>), 'transition_shadowed_by_predecessor': VerifyAlgorithmMeta(name='transition_shadowed_by_predecessor', description='Detect outgoing transitions fully shadowed by earlier same-domain transitions.', closedness='closed', complexity_tier='smt_linear', smt_logic='QF_LIRA', formula_size_scaling='constant', call_count_scaling='linear_in_transitions', incremental=True, fallback_unknown_risk='medium', recommended_tactic='qflia', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='smt_local', dominant_dim=('E', 'vars'), diagnostic_codes=('W_TRANSITION_SHADOWED',), impl=<function transition_shadowed_by_predecessor>), 'enter_postcondition_implies_during_precondition': VerifyAlgorithmMeta(name='enter_postcondition_implies_during_precondition', description='Compare entry postconditions with first-cycle during preconditions.', closedness='closed', complexity_tier='smt_linear', smt_logic='QF_LIRA', formula_size_scaling='constant', call_count_scaling='linear_in_leaves', incremental=True, fallback_unknown_risk='medium', recommended_tactic='qflia', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='smt_local', dominant_dim=('V_leaf', 'vars'), diagnostic_codes=('I_ENTER_DURING_CONTRADICT',), impl=<function enter_postcondition_implies_during_precondition>), 'composite_init_guards_incomplete': VerifyAlgorithmMeta(name='composite_init_guards_incomplete', description='Detect composite states whose initial transitions do not jointly cover all variable and event inputs.', closedness='closed', complexity_tier='smt_linear', smt_logic='QF_LIRA', formula_size_scaling='linear', call_count_scaling='linear_in_states', incremental=True, fallback_unknown_risk='medium', recommended_tactic='qflia', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='smt_local', dominant_dim=('V', 'vars', 'events'), diagnostic_codes=('W_COMPOSITE_INIT_INCOMPLETE',), impl=<function composite_init_guards_incomplete>), 'bounded_reachability': VerifyAlgorithmMeta(name='bounded_reachability', description='Query whether a target state is reachable from a source within a bound.', closedness='queried', complexity_tier='bmc_search', smt_logic='QF_LIRA', formula_size_scaling='linear', call_count_scaling='k_unrollings', incremental=True, fallback_unknown_risk='medium', recommended_tactic='smt', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='bmc_unrolled', dominant_dim=('depth', 'vars', 'events', 'branching'), diagnostic_codes=(), impl=None), 'symbolic_bfs': VerifyAlgorithmMeta(name='symbolic_bfs', description='Build bounded symbolic BFS spaces for queried reachability algorithms.', closedness='queried', complexity_tier='bmc_search', smt_logic='QF_LIRA', formula_size_scaling='linear', call_count_scaling='k_unrollings_times_branching', incremental=True, fallback_unknown_risk='medium', recommended_tactic='smt', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='bmc_unrolled', dominant_dim=('depth', 'vars', 'events', 'branching'), diagnostic_codes=(), impl=None), 'bounded_safety': VerifyAlgorithmMeta(name='bounded_safety', description='Query whether bounded executions avoid bad states or bad conditions.', closedness='queried', complexity_tier='bmc_search', smt_logic='QF_LIRA', formula_size_scaling='linear', call_count_scaling='k_unrollings', incremental=True, fallback_unknown_risk='medium', recommended_tactic='smt', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='bmc_unrolled', dominant_dim=('depth', 'vars', 'events', 'branching'), diagnostic_codes=(), impl=None), 'bounded_invariant': VerifyAlgorithmMeta(name='bounded_invariant', description='Query whether an invariant holds over all bounded reachable frames.', closedness='queried', complexity_tier='bmc_search', smt_logic='QF_LIRA', formula_size_scaling='linear', call_count_scaling='k_unrollings_times_branching', incremental=True, fallback_unknown_risk='high', recommended_tactic='smt', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='bmc_unrolled', dominant_dim=('depth', 'vars', 'events', 'branching'), diagnostic_codes=(), impl=None), 'path_witness': VerifyAlgorithmMeta(name='path_witness', description='Decode a concrete path witness from a satisfiable symbolic frame.', closedness='queried', complexity_tier='bmc_search', smt_logic='QF_LIRA', formula_size_scaling='linear', call_count_scaling='one', incremental=False, fallback_unknown_risk='medium', recommended_tactic='smt', quantifier_alternation_depth=0, max_bitwidth=None, theory_combination=('LIA', 'LRA'), verification_scope='bmc_unrolled', dominant_dim=('depth',), diagnostic_codes=(), impl=None)})

__all__

pyfcstm.verify.registry.__all__ = ['REGISTRY']

Built-in mutable sequence.

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