pyfcstm.bmc.query

Top-level FCSTM BMC query data model.

The query model is intentionally parser-independent. It captures the shape of *.fbmcq files after syntax parsing but before model-aware semantic binding, state/event resolution, solver lowering, or witness replay. Parser and binder layers can construct these frozen dataclasses from ANTLR parse trees and then bind them against pyfcstm.model.StateMachine objects.

Design contracts:

Query objects are data-only and must not import pyfcstm.verify or solver internals.
str() on every concrete query object returns canonical .fbmcq DSL text that later parser work must accept for round-trip tests.
repr() remains the dataclass debugging representation and is not a DSL surface.
to_canonical() is the language-neutral golden shape for parser, binder, and compiler parity tests. Collection fields in canonical output use JSON-stable list values even when the frozen dataclass stores them as tuples internally.

The module contains:

InitialSpec - Cold, terminated, or state hot-start initial condition.
FrameAssumption, EventAssumption, and EventCardinalityAssumption - Environment assumptions.
BmcProperty - Skeleton for reachability, safety, response, and cover goals.
BmcQuery - Complete query root object.

Example:

>>> from pyfcstm.bmc.ast import Active
>>> from pyfcstm.bmc.query import BmcProperty, BmcQuery
>>> query = BmcQuery(property=BmcProperty("reach", 3, predicate=Active("Root.Done")))
>>> query.to_canonical()["property"]["kind"]
'reach'

all

pyfcstm.bmc.query.__all__ = ['InitialVariablePolicy', 'InitialSpec', 'BmcAssumption', 'FrameAssumption', 'EventAssumption', 'EventCardinalityAssumption', 'BmcProperty', 'BmcQuery']

Built-in mutable sequence.

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

InitialVariablePolicy

class pyfcstm.bmc.query.InitialVariablePolicy(havoc_all: bool = False, havoc_variables: Tuple[str, ...] = ())[source]

Initial-frame persistent-variable initializer policy.

The policy controls which FCSTM declaration initializers are skipped while constructing F_0. A skipped variable remains a free initial-frame symbol that can still be constrained by the surrounding initial where predicate.

Parameters:

havoc_all (bool, optional) – Whether havoc * skips every persistent-variable initializer, defaults to False.
havoc_variables (Tuple[str, ...], optional) – Specific variable names skipped by havoc { ... }, defaults to ().

Example:

>>> InitialVariablePolicy(havoc_variables=("x",)).to_canonical()["havoc_variables"]
['x']
>>> str(InitialVariablePolicy(havoc_all=True))
'havoc *'

__str__() → str[source]

Return the canonical havoc clause text.

Returns:: havoc clause text, or "" for the empty policy.
Return type:: str

Example:

>>> str(InitialVariablePolicy())
''
>>> str(InitialVariablePolicy(havoc_variables=("x", "event")))
'havoc { x, "event" }'

havoc_names(domain_or_names: object) → Tuple[str, ...][source]

Return variable names skipped by this policy.

Parameters:: domain_or_names (object) – Either a BMC domain-like object with a variables attribute or an iterable of variable names.
Returns:: Names whose declaration initializers are skipped.
Return type:: Tuple[str, …]
Raises:: pyfcstm.bmc.errors.InvalidBmcQuery – If domain_or_names does not provide names needed by havoc *.

Example:

>>> InitialVariablePolicy(havoc_variables=("x",)).havoc_names(("x", "y"))
('x',)

property is_empty: bool

Return whether the policy leaves all declaration initializers intact.

Returns:: True when no havoc clause is present.
Return type:: bool

Example:

>>> InitialVariablePolicy().is_empty
True

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

Return a stable canonical initial-variable-policy dictionary.

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

Example:

>>> InitialVariablePolicy(havoc_all=True).to_canonical()["havoc_all"]
True

InitialSpec

class pyfcstm.bmc.query.InitialSpec(mode: str = 'cold', state_path: str | None = None, predicate: ~pyfcstm.bmc.ast.BmcCondExpr | None = None, variable_policy: ~pyfcstm.bmc.query.InitialVariablePolicy = <factory>)[source]

Initial BMC frame specification.

Parameters:

mode (str, optional) – Initial mode: "cold", "terminated", or "state". Defaults to "cold".
state_path (Optional[str], optional) – State path for mode="state", defaults to None.
predicate (Optional[BmcCondExpr], optional) – Optional initial-state predicate that contributes only to the initial condition, defaults to None. The predicate is valid for all modes and renders as a where clause, for example init cold where active("Root.A");.
variable_policy (InitialVariablePolicy, optional) – Initial-frame variable initializer policy, defaults to an empty policy that keeps all declaration initializers.

Example:

>>> InitialSpec().to_canonical()["mode"]
'cold'
>>> InitialSpec(mode="state", state_path="Root.Active").state_path
'Root.Active'

__str__() → str[source]

Return the canonical .fbmcq DSL spelling for this initial clause.

Returns:: Initial clause text.
Return type:: str

Example:

>>> str(InitialSpec())
'init cold;'

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

Return a stable canonical initial-spec dictionary.

Returns:: Canonical initial specification.
Return type:: Dict[str, object]

Example:

>>> InitialSpec().to_canonical()["node"]
'initial_spec'

BmcAssumption

class pyfcstm.bmc.query.BmcAssumption[source]

Base class for BMC environment assumptions.

Variables:: _node_name – Canonical node tag emitted by BmcAssumption.to_canonical().

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> isinstance(FrameAssumption("always", BoolLiteral("true")), BmcAssumption)
True

__str__() → str[source]

Return the canonical .fbmcq DSL spelling for this assumption.

Returns:: Assumption clause text.
Return type:: str

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> str(FrameAssumption("always", BoolLiteral("true")))
'assume always: true;'

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

Return a stable canonical assumption dictionary.

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

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> FrameAssumption("always", BoolLiteral("true")).to_canonical()["node"]
'frame_assumption'

FrameAssumption

class pyfcstm.bmc.query.FrameAssumption(kind: str, predicate: BmcCondExpr, frame: int | None = None)[source]

Assumption over frame predicates.

Parameters:

kind (str) – "always" for all frames or "at" for one frame.
predicate (BmcCondExpr) – Condition predicate constrained by this assumption.
frame (Optional[int], optional) – Required non-negative frame index for kind="at", defaults to None.

Example:

>>> from pyfcstm.bmc.ast import BoolLiteral
>>> FrameAssumption("at", BoolLiteral("true"), frame=0).to_canonical()["frame"]
0

EventAssumption

class pyfcstm.bmc.query.EventAssumption(event_path: str, selector: int | Literal['*'] | str = '*', expected: bool = True)[source]

Assumption over one event selection expression.

Parameters:

event_path (str) – Event path referenced by the query.
selector (int or str, optional) – Frame selector such as "*", 0, or "0..3". Defaults to "*".
expected (bool, optional) – Whether the event is expected to be true, defaults to True.

Example:

>>> EventAssumption("Root.Start", selector="0..2").to_canonical()["selector"]
'0..2'

EventCardinalityAssumption

class pyfcstm.bmc.query.EventCardinalityAssumption(kind: str, event_paths: Tuple[str, ...] = ())[source]

Cardinality assumption over a group of event paths.

Parameters:

kind (str) – Cardinality kind, either "any" or "at_most_one".
event_paths (Tuple[str, ...], optional) – Event paths for "at_most_one". "any" uses an empty tuple internally because it is equivalent to omitting the cardinality assumption, defaults to (). "at_most_one" paths must be unique.

Example:

>>> EventCardinalityAssumption("at_most_one", ("A.Go", "A.Stop")).to_canonical()["kind"]
'at_most_one'
>>> EventCardinalityAssumption("any").to_canonical()["event_paths"]
[]

BmcProperty

class pyfcstm.bmc.query.BmcProperty(kind: str, bound: int, predicate: BmcCondExpr | None = None, trigger: BmcCondExpr | None = None, response: BmcCondExpr | None = None, within: int | None = None)[source]

BMC query objective skeleton.

Parameters:

kind (str) – Property kind such as "reach", "forbid", "invariant", "must_reach", "exists_always", "response", or "cover".
bound (int) – Positive inclusive query bound.
predicate (Optional[BmcCondExpr], optional) – Predicate for single-body properties, including kind="cover" with a later binder-validated Case predicate, defaults to None.
trigger (Optional[BmcCondExpr], optional) – Trigger predicate for kind="response", defaults to None.
response (Optional[BmcCondExpr], optional) – Response predicate for kind="response", defaults to None.
within (Optional[int], optional) – Positive response window for kind="response", defaults to None.

Example:

>>> from pyfcstm.bmc.ast import Active
>>> BmcProperty("reach", 2, predicate=Active("Root.Done")).to_canonical()["bound"]
2

__str__() → str[source]

Return the canonical .fbmcq DSL spelling for this property.

Returns:: Check clause text.
Return type:: str

Example:

>>> from pyfcstm.bmc.ast import Active
>>> str(BmcProperty("reach", 2, predicate=Active("Root.Done")))
'check reach <= 2: active("Root.Done");'

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

Return a stable canonical property dictionary.

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

Example:

>>> from pyfcstm.bmc.ast import Active
>>> BmcProperty("forbid", 1, predicate=Active("Root.Bad")).to_canonical()["kind"]
'forbid'

BmcQuery

class pyfcstm.bmc.query.BmcQuery(property: ~pyfcstm.bmc.query.BmcProperty, initial: ~pyfcstm.bmc.query.InitialSpec = <factory>, assumptions: ~typing.Tuple[~pyfcstm.bmc.query.BmcAssumption, ...] = ())[source]

Complete FCSTM BMC query root object.

Parameters:

property (BmcProperty) – Query objective.
initial (InitialSpec, optional) – Initial frame specification, defaults to InitialSpec with mode="cold".
assumptions (Tuple[BmcAssumption, ...], optional) – Tuple of environment assumptions, defaults to empty. Canonical output renders assumptions as a JSON-stable list.

Example:

>>> from pyfcstm.bmc.ast import Active
>>> query = BmcQuery(property=BmcProperty("reach", 1, predicate=Active("Root.Done")))
>>> query.initial.mode
'cold'

__str__() → str[source]

Return the canonical .fbmcq DSL spelling for this query.

Returns:: Complete query file text.
Return type:: str

Example:

>>> from pyfcstm.bmc.ast import Active
>>> query = BmcQuery(property=BmcProperty("reach", 1, predicate=Active("Root.Done")))
>>> str(query).splitlines()[0]
'init cold;'

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

Return a stable canonical query dictionary.

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

Example:

>>> from pyfcstm.bmc.ast import Active
>>> query = BmcQuery(property=BmcProperty("reach", 1, predicate=Active("Root.Done")))
>>> query.to_canonical()["node"]
'bmc_query'

pyfcstm.bmc.query

__all__

InitialVariablePolicy

InitialSpec

BmcAssumption

FrameAssumption

EventAssumption

EventCardinalityAssumption

BmcProperty

BmcQuery

all