pyfcstm.bmc.expand

Runtime-aligned macro-step expansion for FCSTM BMC.

The expansion layer turns a pyfcstm.bmc.source.MacroStepSource into a solver-independent pyfcstm.bmc.macro.MacroStepFormal. It mirrors the cycle-level control flow of pyfcstm.simulate.SimulationRuntime while staying strictly below solver lowering: the output is a flat control-path plan with event atoms, anchored guard requirements, accepted-path priority masks, and ordered model action blocks. The expander does not build Z3 expressions, does not turn operations into writeback strings, and does not split action-local if blocks into separate cases.

The module contains:

Example:

>>> from pyfcstm.bmc import build_bmc_domain, stable_leaf_source
>>> from pyfcstm.bmc.expand import expand_macro_step_cases
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('def int x = 0; state Root { during { x = x + 1; } }')
>>> domain = build_bmc_domain(model, 1)
>>> formal = expand_macro_step_cases(stable_leaf_source(domain, 'Root'))
>>> formal.success_cases[0].kind
'fallback'

__all__

pyfcstm.bmc.expand.__all__ = ['MacroExpansionOptions', 'expand_macro_step_cases']

Built-in mutable sequence.

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

MacroExpansionOptions

class pyfcstm.bmc.expand.MacroExpansionOptions(max_micro_steps: int = 1000, max_stack_depth: int = 64, verify_partition: bool = True, partition_max_assignments: int = 4096)[source]

Options controlling macro-step expansion safety checks.

Parameters:

  • max_micro_steps (int, optional) – Maximum symbolic micro-steps explored before the build fails, defaults to 1000.

  • max_stack_depth (int, optional) – Maximum runtime stack depth, defaults to 64.

  • verify_partition (bool, optional) – Whether to run the source-local partition self-check after building cases, defaults to True.

  • partition_max_assignments (int, optional) – Assignment budget for the fallback truth-table checker, defaults to 4096. Structurally recognized accepted/fallback masks can validate without enumerating this budget.

Example:

>>> MacroExpansionOptions(max_micro_steps=10).max_stack_depth
64

expand_macro_step_cases

pyfcstm.bmc.expand.expand_macro_step_cases(source: MacroStepSource, options: MacroExpansionOptions | None = None) → MacroStepFormal[source]

Expand one macro-step source into runtime-aligned flat cases.

Parameters:
Returns:

Source-local macro-step formal.

Return type:

pyfcstm.bmc.macro.MacroStepFormal

Raises:

  • InvalidBmcEncoding – If the source is malformed or lacks a domain model reference.

  • BmcBuildError – If expansion cannot safely summarize a bounded runtime path.

Example:

>>> from pyfcstm.bmc import build_bmc_domain, stable_leaf_source
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> domain = build_bmc_domain(model, 1)
>>> expand_macro_step_cases(stable_leaf_source(domain, 'Root')).success_cases[0].kind
'fallback'