pyfcstm.bmc.relation

Build solver-level BMC core trace relations.

This module lowers the solver-independent BMC preparation and macro-step handoff objects into the first SMT formula layer. The public entry point build_bmc_core_formula() consumes a pyfcstm.bmc.engine.BmcPreparedContext, allocates bounded frame / step symbols, expands macro-step cases, and constructs the core formula Core_N = D_N ∧ I_0 ∧ T_N ∧ ENV_N.

The relation builder deliberately stops before property compilation. It does not decide whether a query is reachable, forbidden, covered, or healthy; later layers can add objective predicates, witness decoding, and optional health or runtime-error observations on top of the returned core formula. Semantic no-progress observations that are part of the core transition relation are exposed directly as Delta_i and Gamma_i symbols.

Public concepts:

BmcTraceSymbols - Z3 symbols for frames, event inputs, and case selectors.
BmcCaseRelation - One lowered macro-step case implication.
BmcStepRelation - All case implications for one symbolic step.
BmcCoreFormula - The complete D_N / I_0 / T_N / ENV_N bundle.

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;')
>>> context = BmcEngine(model).prepare('check reach <= 1: terminated();')
>>> core = build_bmc_core_formula(context)
>>> core.to_canonical()['node']
'bmc_core_formula'

all

pyfcstm.bmc.relation.__all__ = ['BmcAbstractCallRecord', 'BmcTraceSymbols', 'BmcCaseRelation', 'BmcStepRelation', 'BmcCoreFormula', 'build_bmc_core_formula']

Built-in mutable sequence.

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

BmcAbstractCallRecord

class pyfcstm.bmc.relation.BmcAbstractCallRecord(ordinal: int, action_name: str, stage: str, role: str, state_path: str, active_leaf_path: str, named_ref: str | None, snapshot: Mapping[str, ArithRef])[source]

Lowered abstract-call occurrence with call-time symbolic snapshot.

Parameters:

ordinal (int) – Zero-based call order within the lowered case.
action_name (str) – Resolved abstract action name.
stage (str) – Coarse public call stage, one of enter, during, or exit. Transition effects are intentionally grouped under during at this coarse layer; use role for exact runtime-role filtering.
role (str) – Runtime role that produced the call.
state_path (str) – Runtime public state path approximation.
active_leaf_path (str) – Runtime active leaf approximation.
named_ref (str, optional) – Named reference callsite, defaults to None.
snapshot (Mapping[str, z3.ArithRef]) – Mapping from persistent variable names to call-time Z3 expressions.

Example:

>>> import z3
>>> BmcAbstractCallRecord(0, 'A', 'during', 'leaf_during', 'Root', 'Root', None, {'x': z3.Int('x')}).to_canonical()['action_name']
'A'

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

Return a JSON-stable call-record summary.

Returns:: Canonical call record.
Return type:: Dict[str, object]

BmcTraceSymbols

class pyfcstm.bmc.relation.BmcTraceSymbols(domain: ~pyfcstm.bmc.domain.BmcDomain, frame_states: ~typing.Tuple[~z3.z3.ArithRef, ...], frame_vars: ~typing.Tuple[~typing.Mapping[str, ~z3.z3.ArithRef], ...], event_inputs: ~typing.Tuple[~typing.Mapping[str, ~z3.z3.BoolRef], ...], delta_flags: ~typing.Tuple[~z3.z3.BoolRef, ...], gamma_flags: ~typing.Tuple[~z3.z3.BoolRef, ...], case_selectors: ~typing.Tuple[~typing.Mapping[str, ~z3.z3.BoolRef], ...] = <factory>)[source]

Z3 symbols for one bounded BMC trace.

Parameters:

domain (pyfcstm.bmc.domain.BmcDomain) – Domain snapshot that owns the symbols.
frame_states (Tuple[z3.ArithRef, ...]) – State-id symbols for F_0..F_N.
frame_vars (Tuple[Mapping[str, z3.ArithRef], ...]) – Per-frame persistent-variable symbols.
event_inputs (Tuple[Mapping[str, z3.BoolRef], ...]) – Per-step event-input symbols.
delta_flags (Tuple[z3.BoolRef, ...]) – Per-step semantic-delta observation symbols.
gamma_flags (Tuple[z3.BoolRef, ...]) – Per-step fallback observation symbols.
case_selectors (Tuple[Mapping[str, z3.BoolRef], ...]) – Per-step case-selector symbols.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> symbols = BmcTraceSymbols.allocate(domain, {0: ('case0',)})
>>> symbols.frame_state(0).sort().name()
'Int'
>>> 'case0' in symbols.case_selectors[0]
True

active_state(frame_index: int, state_path: str) → BoolRef[source]

Return the ancestor-or-self active predicate for state_path.

Parameters:

frame_index (int) – Frame index in 0..N.
state_path (str) – Model state path queried by active(...).

Returns:

Z3 predicate for public active-path observation.

Return type:

z3.BoolRef

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the frame is invalid.
pyfcstm.bmc.errors.InvalidBmcDomain – If state_path is unknown.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> BmcTraceSymbols.allocate(domain).active_state(0, 'Root').sort().name()
'Bool'

classmethod allocate(domain: BmcDomain, case_labels_by_step: Mapping[int, Sequence[str]] | None = None) → BmcTraceSymbols[source]

Allocate trace symbols for domain.

Parameters:

domain (pyfcstm.bmc.domain.BmcDomain) – Domain snapshot to allocate for.
case_labels_by_step (Optional[Mapping[int, Sequence[str]]], optional) – Optional mapping from step index to case labels that need selector symbols, defaults to None.

Returns:

Allocated symbol bundle.

Return type:

BmcTraceSymbols

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the domain is malformed.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> BmcTraceSymbols.allocate(domain).to_canonical()['node']
'bmc_trace_symbols'

case_selector(step_index: int, label: str) → BoolRef[source]

Return a case-selector symbol for a step.

Parameters:

step_index (int) – Step index in 0..N-1.
label (str) – Macro-step case label.

Returns:

Case-selector symbol.

Return type:

z3.BoolRef

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the selector is unknown.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> symbols = BmcTraceSymbols.allocate(domain, {0: ('Root::fallback::Root::0',)})
>>> symbols.case_selector(0, 'Root::fallback::Root::0').sort().name()
'Bool'

delta_flag(step_index: int) → BoolRef[source]

Return the semantic-delta observation symbol for a step.

Parameters:: step_index (int) – Step index in 0..N-1.
Returns:: Delta_i observation symbol.
Return type:: z3.BoolRef
Raises:: pyfcstm.bmc.errors.BmcBuildError – If step_index is invalid.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> BmcTraceSymbols.allocate(domain).delta_flag(0).sort().name()
'Bool'

event_input(step_index: int, event_path: str) → BoolRef[source]

Return an event-input symbol for a step.

Parameters:

step_index (int) – Step index in 0..N-1.
event_path (str) – Fully resolved event path.

Returns:

Event-input symbol.

Return type:

z3.BoolRef

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the step or event is unknown.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root { event Go; state A; [*] -> A; }')
>>> domain = build_bmc_domain(model, 1)
>>> BmcTraceSymbols.allocate(domain).event_input(0, 'Root.Go').sort().name()
'Bool'

frame_state(frame_index: int) → ArithRef[source]

Return the state symbol for a frame.

Parameters:: frame_index (int) – Frame index in 0..N.
Returns:: State-id symbol.
Return type:: z3.ArithRef
Raises:: pyfcstm.bmc.errors.BmcBuildError – If frame_index is invalid.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> BmcTraceSymbols.allocate(domain).frame_state(0).decl().name()
'F_0_state'

frame_var(frame_index: int, name: str) → ArithRef[source]

Return a persistent-variable symbol for a frame.

Parameters:

frame_index (int) – Frame index in 0..N.
name (str) – Persistent variable name.

Returns:

Variable symbol.

Return type:

z3.ArithRef

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the frame or variable is unknown.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('def int x = 0; state Root;'), 1)
>>> BmcTraceSymbols.allocate(domain).frame_var(0, 'x').sort().name()
'Int'

gamma_flag(step_index: int) → BoolRef[source]

Return the fallback observation symbol for a step.

Parameters:: step_index (int) – Step index in 0..N-1.
Returns:: Gamma_i observation symbol.
Return type:: z3.BoolRef
Raises:: pyfcstm.bmc.errors.BmcBuildError – If step_index is invalid.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> BmcTraceSymbols.allocate(domain).gamma_flag(0).sort().name()
'Bool'

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

Return a JSON-stable symbol summary.

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

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> BmcTraceSymbols.allocate(domain).to_canonical()['frame_states'][0]
'F_0_state'

BmcCaseRelation

class pyfcstm.bmc.relation.BmcCaseRelation(step_index: int, case: CycleCase, selector: BoolRef, antecedent: BoolRef, consequent: BoolRef, implication: BoolRef, selector_constraint: BoolRef, post_var_exprs: Mapping[str, ArithRef], guard_terms: Mapping[str, BoolRef], definedness_constraints: Tuple[DomainConstraint, ...] = (), call_records: Tuple[BmcAbstractCallRecord, ...] = ())[source]

Lowered relation for one macro-step case.

Parameters:

step_index (int) – Step index owning this case.
case (pyfcstm.bmc.macro.CycleCase) – Macro-step case that was lowered.
selector (z3.BoolRef) – Case-selector symbol bound to antecedent. The relation builder treats macro-step partition validity as an upstream contract: selector equality exposes selected cases but does not independently diagnose malformed partitions.
antecedent (z3.BoolRef) – Source guard and lowered case condition.
consequent (z3.BoolRef) – Target-state, post-var, and definedness constraints.
implication (z3.BoolRef) – z3.Implies(antecedent, consequent).
selector_constraint (z3.BoolRef) – Equality between selector and antecedent.
post_var_exprs (Mapping[str, z3.ArithRef]) – Final expression for every persistent variable.
guard_terms (Mapping[str, z3.BoolRef]) – Lowered guard terms keyed by requirement id.
definedness_constraints (Tuple[pyfcstm.solver.domain.DomainConstraint, ...]) – Runtime-definedness constraints in source order.

Example:

>>> import z3
>>> from pyfcstm.bmc.macro import BoolTemplate, CycleCase
>>> case = CycleCase('fallback', 0, 'Root', 0, 'Root', 'Root::fallback::Root::0', BoolTemplate.true(), ())
>>> rel = BmcCaseRelation(0, case, z3.Bool('c'), z3.BoolVal(True), z3.BoolVal(True), z3.BoolVal(True), z3.BoolVal(True), {}, {}, ())
>>> rel.to_canonical()['case_label']
'Root::fallback::Root::0'

property formula: BoolRef

Return selector binding and implication for this case.

Returns:: Case formula.
Return type:: z3.BoolRef

Example:

>>> import z3
>>> from pyfcstm.bmc.macro import BoolTemplate, CycleCase
>>> case = CycleCase('fallback', 0, 'Root', 0, 'Root', 'Root::fallback::Root::0', BoolTemplate.true(), ())
>>> rel = BmcCaseRelation(0, case, z3.Bool('c'), z3.BoolVal(True), z3.BoolVal(True), z3.BoolVal(True), z3.BoolVal(True), {}, {}, ())
>>> rel.formula.sort().name()
'Bool'

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

Return a JSON-stable case-relation dictionary.

Returns:: Canonical case relation.
Return type:: Dict[str, object]

Example:

>>> import z3
>>> from pyfcstm.bmc.macro import BoolTemplate, CycleCase
>>> case = CycleCase('fallback', 0, 'Root', 0, 'Root', 'Root::fallback::Root::0', BoolTemplate.true(), ())
>>> rel = BmcCaseRelation(0, case, z3.Bool('c'), z3.BoolVal(True), z3.BoolVal(True), z3.BoolVal(True), z3.BoolVal(True), {}, {}, ())
>>> rel.to_canonical()['node']
'bmc_case_relation'

BmcStepRelation

class pyfcstm.bmc.relation.BmcStepRelation(step_index: int, formals: ~typing.Tuple[~pyfcstm.bmc.macro.MacroStepFormal, ...], case_relations: ~typing.Tuple[~pyfcstm.bmc.relation.BmcCaseRelation, ...], formula: ~z3.z3.BoolRef, delta_constraint: ~z3.z3.BoolRef = <factory>, gamma_constraint: ~z3.z3.BoolRef = <factory>, progress_mutex_constraint: ~z3.z3.BoolRef = <factory>)[source]

Lowered relation for one symbolic BMC step.

Parameters:

step_index (int) – Step index in 0..N-1.
formals (Tuple[pyfcstm.bmc.macro.MacroStepFormal, ...]) – Macro-step formals consumed by this step.
case_relations (Tuple[BmcCaseRelation, ...]) – Lowered case relations.
formula (z3.BoolRef) – Conjunction of selector bindings, implications, and step observation constraints.
delta_constraint (z3.BoolRef) – Equality tying Delta_i to delta antecedents.
gamma_constraint (z3.BoolRef) – Equality tying Gamma_i to fallback antecedents.
progress_mutex_constraint (z3.BoolRef) – Mutual exclusion of delta and gamma.

Example:

>>> import z3
>>> step = BmcStepRelation(0, (), (), z3.BoolVal(True))
>>> step.to_canonical()['step_index']
0

property case_registry: Mapping[str, BmcCaseRelation]

Return lowered cases keyed by label for this step.

Returns:: Case-label mapping.
Return type:: Mapping[str, BmcCaseRelation]

Example:

>>> import z3
>>> BmcStepRelation(0, (), (), z3.BoolVal(True)).case_registry
{}

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

Return a JSON-stable step-relation dictionary.

Returns:: Canonical step relation.
Return type:: Dict[str, object]

Example:

>>> import z3
>>> BmcStepRelation(0, (), (), z3.BoolVal(True)).to_canonical()['node']
'bmc_step_relation'

BmcCoreFormula

class pyfcstm.bmc.relation.BmcCoreFormula(context: BmcPreparedContext, symbols: BmcTraceSymbols, domain_formula: BoolRef, initial_formula: BoolRef, transition_formula: BoolRef, environment_formula: BoolRef, core: BoolRef, steps: Tuple[BmcStepRelation, ...], diagnostics: Tuple[str, ...] = ())[source]

Complete solver-level core formula for a bounded trace.

Parameters:

context (pyfcstm.bmc.engine.BmcPreparedContext) – Prepared BMC context consumed by the builder.
symbols (BmcTraceSymbols) – Trace symbols used by the formulas.
domain_formula (z3.BoolRef) – D_N domain constraints.
initial_formula (z3.BoolRef) – I_0 initial-frame constraints.
transition_formula (z3.BoolRef) – T_N transition relation.
environment_formula (z3.BoolRef) – ENV_N environment assumptions.
core (z3.BoolRef) – D_N ∧ I_0 ∧ T_N ∧ ENV_N.
steps (Tuple[BmcStepRelation, ...]) – Lowered step relations.
diagnostics (Tuple[str, ...], optional) – Reserved build-time diagnostics, defaults to (). Relation-level semantic-delta information is currently exposed through case metadata, so this tuple is empty in the initial core-relation builder.

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;')
>>> context = BmcEngine(model).prepare('check reach <= 1: terminated();')
>>> build_bmc_core_formula(context).to_canonical()['bound']
1

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

Return a JSON-stable core-formula summary.

Returns:: Canonical core formula.
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: terminated();'))
>>> core.to_canonical()['node']
'bmc_core_formula'

build_bmc_core_formula

pyfcstm.bmc.relation.build_bmc_core_formula(context: BmcPreparedContext) → BmcCoreFormula[source]

Build Core_N for a prepared BMC context.

The returned formula is exactly the core relation layer: D_N ∧ I_0 ∧ T_N ∧ ENV_N. Health gates, objective predicates, solving, and witness replay are intentionally left to later layers.

Parameters:

context (pyfcstm.bmc.engine.BmcPreparedContext) – Prepared BMC context from pyfcstm.bmc.BmcEngine.

Returns:

Solver-level core formula bundle.

Return type:

BmcCoreFormula

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the prepared context or macro handoff data is internally inconsistent.
pyfcstm.bmc.errors.UnsupportedBmcQuery – If a well-formed query or action uses a solver feature not supported by this relation builder.

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;')
>>> context = BmcEngine(model).prepare('check reach <= 1: terminated();')
>>> build_bmc_core_formula(context).core.sort().name()
'Bool'

pyfcstm.bmc.relation

__all__

BmcAbstractCallRecord

BmcTraceSymbols

BmcCaseRelation

BmcStepRelation

BmcCoreFormula

build_bmc_core_formula

all