pyfcstm.bmc.pipeline

High-level compile-only pipeline for FCSTM BMC queries.

This module provides the convenient public handoff from a state machine and query text or query model to a solve-ready pyfcstm.bmc.properties.BmcPropertyFormula. It composes the existing preparation, core-relation, and property-compilation stages without starting a solver or decoding a witness.

Use compile_bmc_query() when the caller owns a model and query. Use the lower-level pyfcstm.bmc.properties.compile_bmc_property() when the caller already owns a pyfcstm.bmc.relation.BmcCoreFormula and needs to compile only its property objective.

The module contains:

• compile_bmc_query() - Compile a model and query into a solve-ready property formula without solving it.

Example:

>>> from pyfcstm.bmc.pipeline import compile_bmc_query
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_query(model, 'check reach <= 1: active("Root");')
>>> formula.kind, formula.polarity
('reach', 'witness')

__all__

pyfcstm.bmc.pipeline.__all__ = ['compile_bmc_query']

Built-in mutable sequence.

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

compile_bmc_query

pyfcstm.bmc.pipeline.compile_bmc_query(model: StateMachine, query: str | BmcQuery, *, options: BmcOptions | None = None) → BmcPropertyFormula

Compile a model and BMC query into a solve-ready formula without solving.

The function preserves the existing three-stage BMC truth source: pyfcstm.bmc.engine.prepare_bmc_query(), pyfcstm.bmc.relation.build_bmc_core_formula(), and pyfcstm.bmc.properties.compile_bmc_property(). It does not construct a property solver, call pyfcstm.bmc.witness.solve_bmc_property(), or decode a witness.

Parameters:

• model (pyfcstm.model.StateMachine) – State machine to compile against.

• query (Union[str, pyfcstm.bmc.query.BmcQuery]) – .fbmcq query text or a parsed query model.

• options (pyfcstm.bmc.engine.BmcOptions, optional) – Optional preparation policy, defaults to None.

Returns:

Compiled property formula ready for an explicit solver call.

Return type:

pyfcstm.bmc.properties.BmcPropertyFormula

Raises:

• pyfcstm.bmc.errors.BmcBuildError – If the model, query input, options, or generated BMC structures are invalid.

• pyfcstm.bmc.errors.BmcQueryParseError – If query text cannot be parsed.

• pyfcstm.bmc.errors.InvalidBmcQuery – If the query is structurally or semantically invalid for the model.

• pyfcstm.bmc.errors.InvalidBmcDomain – If the bounded model domain is invalid.

• pyfcstm.bmc.errors.UnsupportedBmcQuery – If a valid query construct cannot be lowered by the current BMC implementation.

Example:

>>> from pyfcstm.bmc.pipeline import compile_bmc_query
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_query(model, 'check reach <= 1: active("Root");')
>>> formula.kind, formula.polarity
('reach', 'witness')