pyfcstm.bmc

Public API for FCSTM bounded model checking data contracts.

The BMC package is an independent root package for the FCSTM bounded model checking workstream. It exposes parser-independent query and expression dataclasses, parser entry points, domain numbering snapshots, and macro-step source/case contracts while deliberately leaving semantic binding, solver lowering, witness replay, and verify-registry integration to separate layers.

Package contracts:

  • BMC query objects are parser-independent and data-only in this package.

  • Parser entry points build parser-independent query objects and remain separate from model-aware binding or solver lowering.

  • Domain-numbering and macro-step exports are resolved lazily so parser-only imports do not load pyfcstm.model.

  • Macro-step contracts and expansion are solver-independent and do not import z3 from the root package.

  • Engine exports are resolved lazily; importing pyfcstm.bmc does not prepare queries or load model-aware engine modules.

  • The root package must not depend on pyfcstm.verify or its registry.

  • The high-level query compilation facade remains compile-only; solving and witness decoding require a separate explicit call.

  • str() on exported query and expression dataclasses is reserved for the canonical .fbmcq query DSL spelling.

  • repr() remains the dataclass debugging representation; callers that need stable machine comparison should use to_canonical().

Public module structure:

Area

Public entry

Purpose

Error hierarchy

BmcError, BmcQueryParseError, InvalidBmcQuery, UnsupportedBmcQuery, InvalidBmcEncoding, InvalidBmcDomain, BmcBuildError

Provide stable BMC-specific exception types without importing pyfcstm.verify.

Query parser

parse_bmc_query(), parse_bmc_num_expression(), parse_bmc_cond_expression(), parse_with_bmc_grammar_entry(), build_bmc_ast_from_parse_tree()

Convert .fbmcq text or existing ANTLR parse trees into parser-independent AST/query nodes.

Query binding

BmcBindingDiagnostic, BoundBmcQuery, bind_bmc_query_structure(), bind_bmc_query()

Validate query semantic contexts and optionally resolve model/domain references without coupling parser-only imports to solver layers.

Typed expression bases

BmcExpr, BmcNumExpr, BmcCondExpr

Keep FCSTM numeric and condition expression categories explicit.

FCSTM-compatible numeric expressions

IntLiteral, FloatLiteral, NameRef, MathConst, NumUnaryOp, NumBinaryOp, NumConditionalOp, UFuncCall

Represent the current FCSTM num_expression shape.

FCSTM-compatible condition expressions

BoolLiteral, CondUnaryOp, NumericComparison, CondBinaryOp, CondConditionalOp

Represent the current FCSTM cond_expression shape.

BMC-only query atoms

FrameVar, Cycle, Active, Terminated, Event, Case, CallCount, Called

Represent frame variables, cycle counters, active state, selected event, selected macro-step case, termination, and abstract-call count/existence predicates.

BMC domain model

StateDomainEntry, EventDomainEntry, VarDomainEntry, FrameRef, StepRef, EventInputRef, BmcDomain, build_bmc_domain()

Lazily number model states, events, persistent variables, frames, steps, sentinel states, and event-input slots before solver lowering.

Macro-step sources

MacroStepSource, source_from_initial_spec(), init_source(), entry_source(), stable_leaf_source(), terminated_source()

Describe cold-init, hot-entry, stable-leaf, and terminated source profiles without reading initial where predicates or building solver relations.

Macro-step case data

BoolTemplate, EventUse, GuardRequirement, PriorityExclusion, ActionBlock, CycleCase, MacroStepFormal, PartitionCheckResult

Freeze case labels, control-path conditions, anchored guards, runtime action blocks, ordered event consumption, source-local buckets, and build-time partition summaries.

Macro-step case helpers

case_path_condition(), terminated_absorb_case(), build_fallback_case(), build_semantic_delta_case(), verify_boolean_partition(), verify_source_partition()

Construct terminated absorb, fallback, and semantic-delta cases while keeping partition self-checks outside formal trace formulas.

Macro-step expansion

MacroExpansionOptions, expand_macro_step_cases()

Expand source profiles into runtime-aligned, solver-independent macro-step cases consumed by later relation builders.

BMC engine preparation

BmcOptions, BmcPreparedContext, BmcEngine, prepare_bmc_query()

Prepare StateMachine + .fbmcq inputs into bound query and domain context without solver, witness, CLI, or verify-registry coupling.

BMC relation builder

BmcAbstractCallRecord, BmcTraceSymbols, BmcCaseRelation, BmcStepRelation, BmcCoreFormula, build_bmc_core_formula()

Lower prepared contexts and macro-step cases into Core_N while exposing selected-case abstract-call records and leaving health gates, objectives, solving, and witness replay to later modules.

BMC property compiler

BmcPropertyFormula, compile_bmc_property()

Compile the bound query check clause into a solver objective layered on top of Core_N without solving or witness replay.

BMC query compilation facade

compile_bmc_query()

Compose query preparation, Core_N construction, and property compilation into a solve-ready formula without starting a solver.

BMC solver and witness decoding

BmcSolveResult, BmcWitnessTrace, BmcWitnessFrame, BmcWitnessStep, BmcWitnessEvent, BmcWitnessCallRecord, solve_bmc_property(), decode_bmc_witness()

Solve compiled property formulas and decode SAT models into JSON-stable macro-step witness traces with complete cycle event accounting.

BMC witness replay

BmcReplayResult, BmcReplayMismatch, replay_bmc_witness()

Replay decoded witnesses through SimulationRuntime and return structured mismatch diagnostics.

Query root model

InitialVariablePolicy, InitialSpec, BmcAssumption, FrameAssumption, EventAssumption, EventCardinalityAssumption, BmcProperty, BmcQuery

Capture top-level *.fbmcq query structure, including initial variable initializer policy, before parser, binder, or solver-specific phases.

Example:

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

__all__

pyfcstm.bmc.__all__ = ['BmcError', 'BmcQueryParseError', 'InvalidBmcQuery', 'UnsupportedBmcQuery', 'InvalidBmcEncoding', 'InvalidBmcDomain', 'BmcBuildError', 'parse_bmc_query', 'parse_bmc_num_expression', 'parse_bmc_cond_expression', 'parse_with_bmc_grammar_entry', 'build_bmc_ast_from_parse_tree', 'BmcExpr', 'BmcNumExpr', 'BmcCondExpr', 'IntLiteral', 'FloatLiteral', 'BoolLiteral', 'NameRef', 'MathConst', 'NumUnaryOp', 'NumBinaryOp', 'NumConditionalOp', 'UFuncCall', 'CondUnaryOp', 'NumericComparison', 'CondBinaryOp', 'CondConditionalOp', 'FrameVar', 'Cycle', 'CallStepPoint', 'CallStepSelector', 'CallFilter', 'CallCount', 'Active', 'Terminated', 'Event', 'Case', 'Called', 'InitialVariablePolicy', 'InitialSpec', 'BmcAssumption', 'FrameAssumption', 'EventAssumption', 'EventCardinalityAssumption', 'BmcProperty', 'BmcQuery', 'BmcBindingDiagnostic', 'BoundReference', 'BoundInitialSpec', 'BoundAssumption', 'BoundProperty', 'BoundBmcQuery', 'bind_bmc_query_structure', 'bind_bmc_query', 'STATE_INIT_ID', 'STATE_TERMINATE_ID', 'StateDomainEntry', 'EventDomainEntry', 'VarDomainEntry', 'FrameRef', 'StepRef', 'EventInputRef', 'BmcDomain', 'build_bmc_domain', 'INIT_CASE_PATH', 'TERMINATE_CASE_PATH', 'MacroStepSource', 'init_source', 'entry_source', 'stable_leaf_source', 'terminated_source', 'source_from_initial_spec', 'MacroExpansionOptions', 'expand_macro_step_cases', 'BoolTemplate', 'EventUse', 'GuardRequirement', 'PriorityExclusion', 'ActionBlock', 'CycleCase', 'PartitionCheckResult', 'MacroStepFormal', 'case_path_condition', 'terminated_absorb_case', 'build_fallback_case', 'build_semantic_delta_case', 'verify_boolean_partition', 'verify_source_partition', 'BmcOptions', 'BmcPreparedContext', 'BmcEngine', 'prepare_bmc_query', 'BmcAbstractCallRecord', 'BmcTraceSymbols', 'BmcCaseRelation', 'BmcStepRelation', 'BmcCoreFormula', 'build_bmc_core_formula', 'BmcPropertyFormula', 'compile_bmc_property', 'compile_bmc_query', 'BmcSolveStatus', 'BmcEventDecodePolicy', 'BmcSolveResult', 'BmcWitnessEvent', 'BmcWitnessCallRecord', 'BmcWitnessFrame', 'BmcWitnessStep', 'BmcWitnessTrace', 'BmcRuntimeFrame', 'BmcRuntimeStep', 'BmcRuntimeTrace', 'BmcReplayMismatch', 'BmcReplayResult', 'solve_bmc_property', 'decode_bmc_witness', 'replay_bmc_witness']

Built-in mutable sequence.

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

__getattr__

pyfcstm.bmc.__getattr__(name: str)[source]

Lazily resolve model-aware binding, compilation, and solver exports.

Binding, domain numbering, macro-step helpers, and the preparation engine are kept behind lazy exports so parser-only callers can import pyfcstm.bmc without loading model-aware or later BMC layers. This preserves the convenience API while keeping parse/query data structures independent from solver and verify-registry wiring.

Parameters:

name (str) – Attribute name requested from pyfcstm.bmc.

Returns:

The requested lazy export.

Return type:

object

Raises:

AttributeError – If name is not a public lazy export.

Example:

>>> import pyfcstm.bmc as bmc
>>> bmc.STATE_TERMINATE_ID
-1
>>> callable(bmc.bind_bmc_query_structure)
True

__dir__

pyfcstm.bmc.__dir__()[source]

Return public module attributes including lazy BMC layer exports.

Returns:

Sorted attribute names for interactive discovery.

Return type:

list

Example:

>>> import pyfcstm.bmc as bmc
>>> 'BmcDomain' in dir(bmc)
True