pyfcstm.verify.inspect_adapter

Inspect gating and execution helpers for verify algorithm metadata.

This module decides which raw verification algorithms are eligible for automatic inspect runs under a bounded complexity and call-count policy. It also executes eligible algorithms and normalizes their raw results without importing diagnostics presentation code.

Examples:

>>> from pyfcstm.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> from pyfcstm.verify.inspect_adapter import run_inspect_algorithms
>>> source = '''
... state Root {
...     state A;
...     [*] -> A;
... }
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> names = [result.algorithm_name for result in run_inspect_algorithms(machine)]
>>> "topological_reachable_set" in names
True
>>> "bounded_reachability" in names
False

Module map:

Entry	Purpose
`InspectRunResult`	Carries one normalized inspect-adapter result while preserving the raw verification payload.
`eligible_for_inspect()`	Decides whether one metadata entry is allowed by inspect policy.
`iter_inspect_eligible()`	Iterates eligible registry metadata entries in stable registry order.
`run_inspect_algorithms()`	Executes eligible algorithms and returns normalized results for later diagnostics conversion.

all

pyfcstm.verify.inspect_adapter.__all__ = ['InspectRunResult', 'InspectAccessForbiddenError', 'eligible_for_inspect', 'iter_inspect_eligible', 'run_inspect_algorithms']

Built-in mutable sequence.

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

InspectRunResult

class pyfcstm.verify.inspect_adapter.InspectRunResult(algorithm_name: str, complexity_tier: Literal['structural', 'smt_linear', 'smt_nonlinear_decidable', 'smt_undecidable_heuristic', 'bmc_search'], smt_logic: Literal['QF_UF', 'QF_LIA', 'QF_LRA', 'QF_LIRA', 'QF_UFLIA', 'QF_UFLRA', 'QF_BV', 'QF_FP', 'QF_NIA', 'QF_NRA', 'QF_UFNRA', 'QF_NIRA', 'transcendental'] | None, verification_scope: Literal['topological_only', 'smt_local', 'bmc_unrolled'] | None, diagnostic_codes: Tuple[str, ...], result_kind: Literal['sat', 'unsat', 'unknown', 'timeout', 'undecidable_skip'], diagnostics: Tuple[dict, ...], reason: str | None, raw_result: Any)[source]

Normalized output for one inspect-adapter algorithm run.

The adapter returns one instance per registry algorithm, not one instance per raw diagnostic. Structural algorithms keep their graph-oriented raw payload in raw_result; their result_kind records that the structural run completed rather than replacing the structural payload. SMT-local algorithms expose raw diagnostic dictionaries through diagnostics while preserving their original AlgorithmResult or per-element result tuple.

Parameters:

algorithm_name (str) – Registry name of the executed algorithm.
complexity_tier (ComplexityTier) – Algorithm complexity tier from registry metadata.
smt_logic (Optional[SMTLogic]) – SMT logic from registry metadata, or None for structural algorithms.
verification_scope (Optional[VerificationScope]) – Downstream boundary label from registry metadata.
diagnostic_codes (Tuple[str, ...]) – Diagnostic codes advertised by registry metadata.
result_kind (ResultKind) – Normalized result kind for the whole algorithm run.
diagnostics (Tuple[dict, ...]) – Raw verify diagnostic dictionaries collected from AlgorithmResult values.
reason (Optional[str]) – Optional reason from the raw result when the run is inconclusive or skipped.
raw_result (object) – Original raw algorithm return value kept for later inspect or diagnostics conversion.

Examples:

>>> result = InspectRunResult(
...     algorithm_name="topological_reachable_set",
...     complexity_tier="structural",
...     smt_logic=None,
...     verification_scope="topological_only",
...     diagnostic_codes=(),
...     result_kind="sat",
...     diagnostics=(),
...     reason=None,
...     raw_result={"Root.A": ()},
... )
>>> result.algorithm_name
'topological_reachable_set'

InspectAccessForbiddenError

class pyfcstm.verify.inspect_adapter.InspectAccessForbiddenError[source]

Raised when a forbidden inspect complexity tier is requested.

Examples:

>>> raise InspectAccessForbiddenError("blocked")
Traceback (most recent call last):
...
pyfcstm.verify.inspect_adapter.InspectAccessForbiddenError: blocked

eligible_for_inspect

pyfcstm.verify.inspect_adapter.eligible_for_inspect(meta: VerifyAlgorithmMeta, *, max_complexity_tier: Literal['structural', 'smt_linear', 'smt_nonlinear_decidable', 'smt_undecidable_heuristic', 'bmc_search'] = 'structural', max_call_count_scaling: Literal['none', 'one', 'linear_in_states', 'linear_in_transitions', 'linear_in_vars', 'linear_in_leaves', 'quadratic_in_outgoing_per_state', 'quadratic_in_states', 'vars_times_transitions', 'k_unrollings', 'k_unrollings_times_branching'] = 'linear_in_transitions') → bool[source]

Return whether meta may run automatically from inspect.

Parameters:

meta (VerifyAlgorithmMeta) – Algorithm metadata to evaluate.
max_complexity_tier (ComplexityTier) – Maximum allowed non-BMC complexity tier.
max_call_count_scaling (CallCountScaling) – Maximum allowed inspect call-count scaling.

Returns:

True if the algorithm is eligible for inspect automation.

Return type:

bool

Raises:

InspectAccessForbiddenError – If max_complexity_tier is 'bmc_search' or if either inspect limit is outside the automatic inspect ordering.

Examples:

>>> from pyfcstm.verify.registry import REGISTRY
>>> eligible_for_inspect(REGISTRY["topological_reachable_set"])
True
>>> eligible_for_inspect(REGISTRY["bounded_reachability"])
False

iter_inspect_eligible

pyfcstm.verify.inspect_adapter.iter_inspect_eligible(*, max_complexity_tier: Literal['structural', 'smt_linear', 'smt_nonlinear_decidable', 'smt_undecidable_heuristic', 'bmc_search'] = 'structural', max_call_count_scaling: Literal['none', 'one', 'linear_in_states', 'linear_in_transitions', 'linear_in_vars', 'linear_in_leaves', 'quadratic_in_outgoing_per_state', 'quadratic_in_states', 'vars_times_transitions', 'k_unrollings', 'k_unrollings_times_branching'] = 'linear_in_transitions') → Iterator[VerifyAlgorithmMeta][source]

Iterate over registry algorithms eligible for inspect automation.

Parameters:

max_complexity_tier (ComplexityTier) – Maximum allowed non-BMC complexity tier.
max_call_count_scaling (CallCountScaling) – Maximum allowed inspect call-count scaling.

Returns:

Iterator over eligible metadata entries in registry order.

Yield:

Eligible metadata entries in registry order.

Return type:

Iterator[VerifyAlgorithmMeta]

Examples:

>>> names = [meta.name for meta in iter_inspect_eligible()]
>>> names[:2]
['topological_reachable_set', 'unreachable_states']

run_inspect_algorithms

pyfcstm.verify.inspect_adapter.run_inspect_algorithms(machine, *, max_complexity_tier: Literal['structural', 'smt_linear', 'smt_nonlinear_decidable', 'smt_undecidable_heuristic', 'bmc_search'] = 'structural', max_call_count_scaling: Literal['none', 'one', 'linear_in_states', 'linear_in_transitions', 'linear_in_vars', 'linear_in_leaves', 'quadratic_in_outgoing_per_state', 'quadratic_in_states', 'vars_times_transitions', 'k_unrollings', 'k_unrollings_times_branching'] = 'linear_in_transitions', smt_timeout_ms: int | None = None, registry: Mapping[str, VerifyAlgorithmMeta] | None = None) → Tuple[InspectRunResult, ...][source]

Run inspect-eligible verify algorithms and normalize their outputs.

The function is the execution half of the inspect adapter. It reuses eligible_for_inspect() as the only admission policy, runs algorithms in registry order, keeps planned impl=None entries as controlled skip results when they are otherwise eligible, and never emits diagnostics-layer objects directly.

Parameters:

machine (StateMachine) – State machine to verify.
max_complexity_tier (ComplexityTier, optional) – Maximum non-BMC complexity tier allowed by the inspect policy, defaults to "structural".
max_call_count_scaling (CallCountScaling, optional) – Maximum call-count scaling allowed by the inspect policy, defaults to "linear_in_transitions".
smt_timeout_ms (Optional[int], optional) – Optional solver timeout passed to SMT-local algorithms as smt_timeout_ms. None preserves the raw algorithm default of no configured solver timeout.
registry (Optional[Mapping[str, VerifyAlgorithmMeta]], optional) – Optional metadata registry for tests or alternate consumers. None uses pyfcstm.verify.registry.REGISTRY.

Returns:

Normalized results in registry order.

Return type:

Tuple[InspectRunResult, …]

Raises:

InspectAccessForbiddenError – If either inspect limit is outside the automatic inspect ordering.
TypeError – If an SMT-local algorithm returns an unexpected raw result payload.
ValueError – If an SMT-local algorithm has no inspect dispatch rule.

Examples:

>>> 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)
>>> [result.algorithm_name for result in run_inspect_algorithms(machine)][:2]
['topological_reachable_set', 'unreachable_states']

pyfcstm.verify.inspect_adapter

__all__

InspectRunResult

InspectAccessForbiddenError

eligible_for_inspect

iter_inspect_eligible

run_inspect_algorithms

all