pyfcstm.bmc.properties

Compile BMC query properties into solver objectives.

This module is the property layer above pyfcstm.bmc.relation. It consumes a pyfcstm.bmc.relation.BmcCoreFormula, keeps the core trace relation unchanged, and adds the query objective for the bound check clause. The compiler does not solve the formula, decode witnesses, replay traces, or connect to pyfcstm.verify; those stages can consume the returned BmcPropertyFormula later.

The module contains:

• BmcPropertyFormula - Compiled objective and diagnostic formulas.

• compile_bmc_property() - Public entry point for lowering a bound query property against an existing core trace formula.

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula
>>> from pyfcstm.bmc.properties import compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> core = build_bmc_core_formula(BmcEngine(model).prepare('check reach <= 1: active("Root");'))
>>> compile_bmc_property(core).kind
'reach'

__all__

pyfcstm.bmc.properties.__all__ = ['BmcPropertyFormula', 'compile_bmc_property']

Built-in mutable sequence.

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

BmcPropertyFormula

class pyfcstm.bmc.properties.BmcPropertyFormula(core: BmcCoreFormula, kind: str, polarity: str, objective_formula: BoolRef, solve_formula: BoolRef, incomplete_formula: BoolRef, incomplete_solve_formula: BoolRef, diagnostics: Tuple[str, ...] = (), case_label: str | None = None, response_window: int | None = None)

Compiled BMC property objective.

Parameters:

• core (pyfcstm.bmc.relation.BmcCoreFormula) – Core trace formula consumed by this property objective.

• kind (str) – Property kind from the bound query.

• polarity (str) – "witness" when SAT means a desired witness, or "counterexample" when SAT means a violation trace.

• objective_formula (z3.BoolRef) – Property objective Phi_q.

• solve_formula (z3.BoolRef) – Core_N conjoined with objective_formula.

• incomplete_formula (z3.BoolRef) – Optional bounded-horizon incompleteness observation Omega_q. Currently non-trivial for response properties.

• incomplete_solve_formula (z3.BoolRef) – Core_N conjoined with incomplete_formula for later solver/report layers.

• diagnostics (Tuple[str, ...], optional) – Static compiler diagnostics, defaults to ().

• case_label (Optional[str], optional) – Cover case label, defaults to None.

• response_window (Optional[int], optional) – Response window, defaults to None.

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> core = build_bmc_core_formula(BmcEngine(model).prepare('check reach <= 1: active("Root");'))
>>> formula = compile_bmc_property(core)
>>> formula.to_canonical()['polarity']
'witness'

property bound: int

Return the compiled query bound.

Returns:

Query bound.

Return type:

int

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> core = build_bmc_core_formula(BmcEngine(model).prepare('check reach <= 1: active("Root");'))
>>> compile_bmc_property(core).bound
1

to_canonical() → Dict[str, Any]

Return a JSON-stable compiled-property summary.

Formula fields use Z3 sexpr() text so downstream snapshots receive SMT-LIB-style expressions instead of Python pretty-printer output.

Returns:

Canonical property formula summary.

Return type:

Dict[str, object]

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> core = build_bmc_core_formula(BmcEngine(model).prepare('check reach <= 1: active("Root");'))
>>> compile_bmc_property(core).to_canonical()['node']
'bmc_property_formula'

compile_bmc_property

pyfcstm.bmc.properties.compile_bmc_property(core: BmcCoreFormula) → BmcPropertyFormula

Compile the prepared query property into a solver objective.

The returned formula keeps pyfcstm.bmc.relation.BmcCoreFormula.core intact and adds only the objective requested by the bound check clause. SAT means a witness for reach / exists_always / cover and a counterexample for forbid / invariant / must_reach / response.

Parameters:

core (pyfcstm.bmc.relation.BmcCoreFormula) – Core trace formula to extend with the query objective.

Returns:

Compiled property objective bundle.

Return type:

BmcPropertyFormula

Raises:

• pyfcstm.bmc.errors.BmcBuildError – If core or bound property metadata is internally inconsistent.

• pyfcstm.bmc.errors.InvalidBmcQuery – If a query-level cover label or property shape is invalid for property compilation.

• pyfcstm.bmc.errors.UnsupportedBmcQuery – If the property uses a parsed but unsupported expression shape or unsupported arithmetic operation.

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> core = build_bmc_core_formula(BmcEngine(model).prepare('check reach <= 1: active("Root");'))
>>> compile_bmc_property(core).solve_formula.sort().name()
'Bool'