pyfcstm.bmc.engine

Preparation engine for FCSTM bounded model checking queries.

The engine layer is the first BMC handoff point that combines a pyfcstm.model.StateMachine with a parser-independent pyfcstm.bmc.query.BmcQuery. It parses query text when necessary, performs structure-only binding before any domain construction, builds the bounded domain, resolves query references against that domain, and returns a JSON-stable preparation context.

This module is intentionally a preparation layer only. It does not expand macro-step cases, lower formulas to Z3, compile property objectives, decode witnesses, expose CLI commands, or register anything under pyfcstm.verify.

The module contains:

BmcOptions - Prepare-time policy options.
BmcPreparedContext - Prepared query/domain handoff data.
BmcEngine - Reusable model-bound preparation entry point.
prepare_bmc_query() - Function-style convenience API.

Example:

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

all

pyfcstm.bmc.engine.__all__ = ['BmcOptions', 'BmcPreparedContext', 'BmcEngine', 'prepare_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.

BmcOptions

class pyfcstm.bmc.engine.BmcOptions(max_bound: int | None = None)[source]

Prepare-time policy options for BMC query preparation.

The first engine prototype keeps options deliberately small. max_bound is a policy guard for expensive accidental queries; solver tactics, timeouts, witness formatting, and CLI concerns belong to later layers.

Parameters:: max_bound (Optional[int], optional) – Maximum allowed query bound, or None for no limit, defaults to None.
Raises:: pyfcstm.bmc.errors.BmcBuildError – If max_bound is not None and not a positive integer.

Example:

>>> BmcOptions(max_bound=3).to_canonical()["max_bound"]
3

to_canonical() → Dict[str, Any][source]

Return a JSON-stable options dictionary.

Returns:: Canonical options dictionary.
Return type:: Dict[str, object]

Example:

>>> BmcOptions().to_canonical()
{'node': 'bmc_options', 'max_bound': None}

BmcPreparedContext

class pyfcstm.bmc.engine.BmcPreparedContext(model: StateMachine, query: BmcQuery, bound_query: BoundBmcQuery, domain: BmcDomain, options: BmcOptions, source_text: str | None = None)[source]

Prepared model, query, domain, and binding snapshot.

Prepared contexts are solver-independent handoff objects. The raw model is retained for future engine stages, while to_canonical() deliberately emits only JSON-stable query, bound-query, domain, option, and source-text data.

Parameters:

model (pyfcstm.model.StateMachine) – State machine used for domain numbering.
query (pyfcstm.bmc.query.BmcQuery) – Parser-independent BMC query object.
bound_query (pyfcstm.bmc.binding.BoundBmcQuery) – Model/domain-aware bound query snapshot.
domain (pyfcstm.bmc.domain.BmcDomain) – Bounded model domain.
options (BmcOptions) – Effective preparation options.
source_text (Optional[str], optional) – Original .fbmcq text for string inputs, defaults to None for AST inputs.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If fields are malformed or inconsistent.

Example:

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

property bound: int

Return the prepared query/domain bound.

Returns:: Positive BMC bound.
Return type:: int

Example:

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

property references: Tuple[BoundReference, ...]

Return references discovered during domain-aware query binding.

Returns:: Bound query references.
Return type:: Tuple[pyfcstm.bmc.binding.BoundReference, …]

Example:

>>> from pyfcstm.bmc.engine import BmcEngine
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> BmcEngine(model).prepare('check reach <= 1: active("Root");').references[0].kind
'state'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable prepared-context dictionary.

The state-machine object is intentionally omitted because it is not a JSON primitive and the domain snapshot contains the stable numbering data needed by later BMC stages.

Returns:: Canonical prepared context.
Return type:: Dict[str, object]

Example:

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

BmcEngine

class pyfcstm.bmc.engine.BmcEngine(model: StateMachine, options: BmcOptions | None = None)[source]

Model-bound entry point for BMC query preparation.

Parameters:

model (pyfcstm.model.StateMachine) – State machine to prepare queries against.
options (BmcOptions, optional) – Default preparation options, defaults to BmcOptions().

Raises:

pyfcstm.bmc.errors.BmcBuildError – If model or options is invalid.

Example:

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

__init__(model: StateMachine, options: BmcOptions | None = None) → None[source]

Initialize a BMC preparation engine.

Parameters:

model (pyfcstm.model.StateMachine) – State machine to prepare queries against.
options (BmcOptions, optional) – Default preparation options, defaults to BmcOptions().

Returns:

None.

Return type:

None

Raises:

pyfcstm.bmc.errors.BmcBuildError – If model or options is invalid.

Example:

>>> from pyfcstm.bmc.engine import BmcEngine
>>> from pyfcstm.model import load_state_machine_from_text
>>> isinstance(BmcEngine(load_state_machine_from_text('state Root;')), BmcEngine)
True

property model: StateMachine

Return the state machine held by this engine.

Returns:: State machine used for preparation.
Return type:: pyfcstm.model.StateMachine

Example:

>>> from pyfcstm.bmc.engine import BmcEngine
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> BmcEngine(model).model is model
True

property options: BmcOptions

Return the engine default preparation options.

Returns:: Default options.
Return type:: BmcOptions

Example:

>>> from pyfcstm.bmc.engine import BmcEngine, BmcOptions
>>> from pyfcstm.model import load_state_machine_from_text
>>> BmcEngine(load_state_machine_from_text('state Root;'), BmcOptions(max_bound=1)).options.max_bound
1

prepare(query: str | BmcQuery, options: BmcOptions | None = None) → BmcPreparedContext[source]

Prepare a BMC query text or AST against this engine’s model.

Per-call options completely replace the engine default options. When options is omitted, the engine default options are used.

Parameters:

query (Union[str, pyfcstm.bmc.query.BmcQuery]) – Query text or parser-independent query object.
options (BmcOptions, optional) – Per-call options, defaults to None.

Returns:

Prepared BMC context.

Return type:

BmcPreparedContext

Raises:

pyfcstm.bmc.errors.BmcQueryParseError – If query text cannot be parsed.
pyfcstm.bmc.errors.InvalidBmcQuery – If query binding fails.
pyfcstm.bmc.errors.InvalidBmcDomain – If domain construction fails.
pyfcstm.bmc.errors.BmcBuildError – If inputs or option policy are invalid.

Example:

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

prepare_bmc_query

pyfcstm.bmc.engine.prepare_bmc_query(model: StateMachine, query: str | BmcQuery, options: BmcOptions | None = None) → BmcPreparedContext[source]

Prepare a BMC query with a one-shot engine.

This function is an engine-level convenience wrapper. It performs the full prepare pipeline and returns a BmcPreparedContext, unlike pyfcstm.bmc.binding.bind_bmc_query(), which only returns a bound query snapshot.

Parameters:

model (pyfcstm.model.StateMachine) – State machine to prepare against.
query (Union[str, pyfcstm.bmc.query.BmcQuery]) – Query text or parser-independent query object.
options (BmcOptions, optional) – Preparation options, defaults to None.

Returns:

Prepared BMC context.

Return type:

BmcPreparedContext

Raises:

pyfcstm.bmc.errors.BmcError – If parsing, binding, domain construction, or option policy fails.

Example:

>>> from pyfcstm.bmc.engine import prepare_bmc_query
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> prepare_bmc_query(model, 'check reach <= 1: active("Root");').bound
1

pyfcstm.bmc.engine

__all__

BmcOptions

BmcPreparedContext

BmcEngine

prepare_bmc_query

all