pyfcstm.verify.registry

Algorithm registry for pyfcstm.verify.

The registry maps stable algorithm names to pyfcstm.verify.taxonomy.VerifyAlgorithmMeta entries. Every registered structural or SMT-local algorithm carries an executable callable.

Example:

>>> from pyfcstm.verify.registry import REGISTRY
>>> REGISTRY["dead_guard"].impl.__name__
'dead_guard'
>>> all(callable(meta.impl) for meta in REGISTRY.values())
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>)})

__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.