pyfcstm.bmc.witness

Decode and replay bounded model checking witnesses.

This module is the witness layer above pyfcstm.bmc.properties. It solves compiled BMC property formulas, decodes SAT models into JSON-stable macro-step traces, and replays those traces against pyfcstm.simulate.SimulationRuntime as a runtime-alignment oracle. The trace deliberately stays at the public cycle boundary: frames, sparse replay input events, selected BMC case metadata, delta/gamma progress flags, and abstract-call snapshots. Each step also records ordered consumed events and derived unconsumed inputs so replay checks the complete public cycle event accounting contract.

The module contains:

• BmcSolveResult - Structured solver status and optional Z3 model.

• BmcWitnessTrace - JSON-stable decoded witness root object.

• BmcReplayResult - Structured runtime replay result and mismatches.

• solve_bmc_property() - Solve a compiled property formula.

• decode_bmc_witness() - Decode one SAT model into a witness trace.

• replay_bmc_witness() - Replay a witness with SimulationRuntime.

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.bmc.witness import solve_bmc_property, decode_bmc_witness
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> core = build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: active("Root");'))
>>> formula = compile_bmc_property(core)
>>> result = solve_bmc_property(formula)
>>> result.status
'sat'
>>> decode_bmc_witness(formula, result.model).schema_version
'bmc-witness/v1'

BmcSolveStatus

pyfcstm.bmc.witness.BmcSolveStatus

Public solver statuses returned by BmcSolveResult.

alias of Literal[‘sat’, ‘unsat’, ‘unknown’, ‘timeout’]

__all__

pyfcstm.bmc.witness.__all__ = ['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.

BmcSolveResult

class pyfcstm.bmc.witness.BmcSolveResult(formula: BmcPropertyFormula, status: Literal['sat', 'unsat', 'unknown', 'timeout'], model: ModelRef | None = None, reason: str | None = None, elapsed_ms: float = 0.0, timeout_ms: int | None = None, incomplete_status: Literal['sat', 'unsat', 'unknown', 'timeout'] | None = None, incomplete_model: ModelRef | None = None, incomplete_reason: str | None = None, diagnostics: Tuple[str, ...] = ())

Structured result for one BMC property solve.

The raw Z3 models are intentionally kept as Python attributes rather than JSON fields. Callers can pass model to decode_bmc_witness() when status is "sat" while to_canonical() remains JSON-stable for logs and tests. Verdict properties such as property_satisfied, witness_found, and counterexample_found translate solver objective satisfiability into user-facing bounded property results. Manually constructed SAT results must carry their SAT model, and non-SAT results must not carry a model, so the public status and replay payload cannot diverge.

Parameters:

• formula (pyfcstm.bmc.properties.BmcPropertyFormula) – Compiled BMC property formula that was solved.

• status (str) – Solver status for formula.solve_formula.

• model (z3.ModelRef, optional) – SAT model for formula.solve_formula, defaults to None.

• reason (str, optional) – Raw solver reason for "unknown" or "timeout" primary statuses, defaults to None.

• elapsed_ms (float, optional) – Objective solve wall time in milliseconds, defaults to 0.0.

• timeout_ms (int, optional) – Configured timeout in milliseconds, defaults to None.

• incomplete_status (str, optional) – Solver status for the incomplete-bound formula, defaults to None.

• incomplete_model (z3.ModelRef, optional) – SAT model for the incomplete-bound formula, defaults to None.

• incomplete_reason (str, optional) – Raw solver reason for an inconclusive incomplete-bound solve, or a diagnostic reason when that solve was not executed, defaults to None.

• diagnostics (Tuple[str, ...], optional) – Solver-level diagnostics, defaults to ().

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the solve result payload is malformed.

Example:

>>> import z3
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: active("Root");')))
>>> result = solve_bmc_property(formula)
>>> result.to_canonical()['status'] in {'sat', 'unsat', 'unknown', 'timeout'}
True

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

property counterexample_found: bool

Return whether the primary objective found a counterexample.

Returns:

True when SAT means a violation trace and the primary objective is satisfiable.

Return type:

bool

Example:

>>> import z3
>>> from pyfcstm.bmc.witness import BmcSolveResult
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check forbid <= 1: active("Root");')))
>>> solver = z3.Solver()
>>> solver.add(z3.BoolVal(True))
>>> solver.check() == z3.sat
True
>>> BmcSolveResult(formula, 'sat', model=solver.model()).counterexample_found
True

property incomplete: bool

Return whether the verdict is known to be horizon-incomplete.

Solver unknown and timeout statuses are always incomplete. A response property is also incomplete when the primary objective is "unsat" and its suffix diagnostic was not solved, was inconclusive, or can still contain an uncovered trigger window. If the primary response objective is "sat", the counterexample verdict is already decisive even when a separate suffix diagnostic would also be satisfiable.

Returns:

Whether the solve result carries an incomplete verdict.

Return type:

bool

Example:

>>> from pyfcstm.bmc.witness import BmcSolveResult
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: active("Root");')))
>>> BmcSolveResult(formula, 'timeout', reason='timeout').incomplete
True

property kind: str

Return the property kind.

Returns:

Property kind.

Return type:

str

Example:

>>> from pyfcstm.bmc.query import BmcProperty
>>> from pyfcstm.bmc.properties import BmcPropertyFormula, _lower_predicate
>>> # ``kind`` is copied from the solved formula.

property outcome: str

Return a stable user-facing outcome label.

Returns:

One of "property_satisfied", "property_violated", "witness_found", "no_witness", "incomplete", "timeout", or "unknown".

Return type:

str

Example:

>>> from pyfcstm.bmc.witness import BmcSolveResult
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: terminated();')))
>>> BmcSolveResult(formula, 'unsat').outcome
'no_witness'

property polarity: str

Return whether SAT is a witness or counterexample.

Returns:

Formula polarity.

Return type:

str

Example:

>>> # For reach properties, SAT is a witness.

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

property property_satisfied: bool | None

Return the user-facing bounded property verdict.

This verdict translates the solver objective status through polarity. Witness objectives are satisfied exactly when SAT finds a witness. Counterexample objectives are satisfied exactly when the counterexample search is UNSAT, except response properties whose suffix diagnostic is unsolved, satisfiable, or inconclusive remain incomplete.

Returns:

True if the bounded property is satisfied, False if it is violated or lacks a required witness, and None if the result is incomplete.

Return type:

Optional[bool]

Example:

>>> from pyfcstm.bmc.witness import BmcSolveResult
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: terminated();')))
>>> BmcSolveResult(formula, 'unsat').property_satisfied
False

to_canonical() → Dict[str, Any]

Return a JSON-stable solve summary.

Raw Z3 models are excluded because they are not JSON values. The decoded witness carries model assignments in stable frame and step fields after decode_bmc_witness() succeeds.

Returns:

Canonical solve result.

Return type:

Dict[str, object]

Example:

>>> import z3
>>> from pyfcstm.bmc.witness import BmcSolveResult
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: active("Root");')))
>>> BmcSolveResult(formula, 'unsat').to_canonical()['status']
'unsat'

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

property witness_found: bool

Return whether the primary objective found a positive witness.

Returns:

True when SAT means a witness and the primary objective is satisfiable.

Return type:

bool

Example:

>>> import z3
>>> from pyfcstm.bmc.witness import BmcSolveResult
>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: active("Root");')))
>>> solver = z3.Solver()
>>> solver.add(z3.BoolVal(True))
>>> solver.check() == z3.sat
True
>>> BmcSolveResult(formula, 'sat', model=solver.model()).witness_found
True

BmcEventDecodePolicy

class pyfcstm.bmc.witness.BmcEventDecodePolicy(include_debug_reads: bool = True, include_property_support: bool = True)

Policy for decoding sparse replay events from a SAT model.

The default policy emits the canonical replay-minimal event set plus debug reads for negative or false assumptions. It intentionally does not expose a mode that dumps every true Z3 event Boolean because model completion can make irrelevant event symbols true and pollute replay inputs.

Parameters:

• include_debug_reads (bool, optional) – Whether to include non-replay event reads in BmcWitnessStep.event_reads, defaults to True.

• include_property_support (bool, optional) – Whether response-trigger support events may be added when they are required to replay a response counterexample, defaults to True. If disabled, decoding still succeeds when support is unnecessary, but fails loudly rather than emitting a non-faithful trace when support is required.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If a policy flag is malformed.

Example:

>>> BmcEventDecodePolicy().include_debug_reads
True

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable event decode policy.

Returns:

Canonical event decode policy.

Return type:

Dict[str, object]

Example:

>>> BmcEventDecodePolicy().to_canonical()['include_debug_reads']
True

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcWitnessEvent

class pyfcstm.bmc.witness.BmcWitnessEvent(path: str, reason: str, model_value: bool = True)

Replay input event decoded for one BMC step.

Parameters:

• path (str) – Fully qualified event path.

• reason (str) – Decode reason such as "case_positive".

• model_value (bool) – Boolean value observed in the SAT model.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the event payload is malformed.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_canonical()['path']
'Root.Go'

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable event dictionary.

Returns:

Canonical event dictionary.

Return type:

Dict[str, object]

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_canonical()['reason']
'case_positive'

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcWitnessCallRecord

class pyfcstm.bmc.witness.BmcWitnessCallRecord(ordinal: int, action_name: str, stage: str, role: str, state: str, active_leaf: str, named_ref: str | None = None, snapshot: ~typing.Mapping[str, ~typing.Any] = <factory>)

Decoded abstract-call occurrence for one selected macro-step case.

Parameters:

• ordinal (int) – Call ordinal within the selected case.

• action_name (str) – Resolved abstract action path.

• stage (str) – Runtime call stage.

• role (str) – Runtime action-block role.

• state (str) – Calling state path.

• active_leaf (str) – Active leaf path visible to the handler.

• named_ref (str, optional) – Named ref callsite path, defaults to None.

• snapshot (Mapping[str, object], optional) – Persistent variable snapshot before the handler call, defaults to {}.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the call-record payload is malformed.

Example:

>>> rec = BmcWitnessCallRecord(0, 'Root.A.Hook', 'during', 'leaf_during', 'Root.A', 'Root.A')
>>> rec.to_canonical()['ordinal']
0

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable call record.

Returns:

Canonical call record.

Return type:

Dict[str, object]

Example:

>>> BmcWitnessCallRecord(0, 'Root.A.Hook', 'during', 'leaf_during', 'Root.A', 'Root.A').to_canonical()['action_name']
'Root.A.Hook'

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcWitnessFrame

class pyfcstm.bmc.witness.BmcWitnessFrame(index: int, state_id: int | None, state: str | None, sentinel: str | None, terminated: bool, vars: Mapping[str, Any])

Decoded public frame in a BMC witness trace.

Parameters:

• index (int) – Frame index.

• state_id (int, optional) – Normal state id or None for sentinels.

• state (str, optional) – Normal state path or None for sentinels.

• sentinel (str, optional) – "init", "terminated", or None.

• terminated (bool) – Whether this frame is terminated.

• vars (Mapping[str, object]) – Persistent variable values.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the frame payload is malformed.

Example:

>>> BmcWitnessFrame(0, None, None, 'init', False, {}).to_canonical()['sentinel']
'init'

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable frame dictionary.

Returns:

Canonical frame.

Return type:

Dict[str, object]

Example:

>>> BmcWitnessFrame(0, None, None, 'init', False, {}).to_canonical()['state'] is None
True

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcWitnessStep

class pyfcstm.bmc.witness.BmcWitnessStep(index: int, source_frame: int, target_frame: int, case_label: str, case_kind: str, progress: str, source_state: str | None, target_state: str | None, delta: bool, gamma: bool, input_events: Sequence[BmcWitnessEvent] = (), event_reads: Sequence[BmcWitnessEvent] = (), abstract_calls: Sequence[BmcWitnessCallRecord] = (), consumed_events: Sequence[str] = (), unconsumed_events: Sequence[str] | None = None)

Decoded macro-step witness entry.

Parameters:

• index (int) – Step index.

• source_frame (int) – Source frame index.

• target_frame (int) – Target frame index.

• case_label (str) – Selected BMC case label.

• case_kind (str) – Selected BMC case kind, such as "initial", "transition", "fallback", "delta", or "absorb".

• progress (str) – Replay-friendly progress classification.

• source_state (str, optional) – Source state path or None for sentinels.

• target_state (str, optional) – Target state path or None for sentinels.

• delta (bool) – Decoded Delta_i flag.

• gamma (bool) – Decoded Gamma_i flag.

• input_events (Sequence[BmcWitnessEvent], optional) – Sparse replay input events whose reasons are replay inputs and whose model values are True, defaults to ().

• event_reads (Sequence[BmcWitnessEvent], optional) – Debug-only event reads, defaults to ().

• abstract_calls (Sequence[BmcWitnessCallRecord], optional) – Decoded abstract-call records, defaults to ().

• consumed_events (Sequence[str], optional) – Event paths consumed by selected evented transitions in micro-step order, defaults to ().

• unconsumed_events (Sequence[str], optional) – Replay input event paths not consumed by the selected macro path. None derives the value from input_events and consumed_events, defaults to None.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the step payload is malformed.

Example:

>>> step = BmcWitnessStep(0, 0, 1, 'Root::fallback::Root::0', 'fallback', 'fallback_gamma', 'Root', 'Root', False, True)
>>> step.to_canonical()['progress']
'fallback_gamma'

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

property input_event_paths: Tuple[str, ...]

Return replay input event paths in witness order.

Returns:

Event paths.

Return type:

Tuple[str, …]

Example:

>>> step = BmcWitnessStep(0, 0, 1, 'c', 'fallback', 'fallback_gamma', 'Root', 'Root', False, True)
>>> step.input_event_paths
()

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable step dictionary.

Returns:

Canonical step.

Return type:

Dict[str, object]

Example:

>>> step = BmcWitnessStep(0, 0, 1, 'c', 'fallback', 'fallback_gamma', 'Root', 'Root', False, True)
>>> step.to_canonical()['delta']
False

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcWitnessTrace

class pyfcstm.bmc.witness.BmcWitnessTrace(property: Mapping[str, Any], solver: Mapping[str, Any], initial: Mapping[str, Any], frames: Sequence[BmcWitnessFrame], steps: Sequence[BmcWitnessStep], diagnostics: Sequence[str] = (), schema_version: str = 'bmc-witness/v1')

Decoded BMC witness trace.

The metadata dictionaries are public JSON-stable payloads. They may contain strings, booleans, None, finite numeric values, nested mappings, and lists, but not arbitrary Python objects or non-finite floating-point values. The bmc-witness/v1 step schema includes canonical replay input events, ordered consumed event paths, and presence-derived unconsumed event paths.

Parameters:

• property (Mapping[str, object]) – Property metadata.

• solver (Mapping[str, object]) – Solver metadata.

• initial (Mapping[str, object]) – Initial replay metadata.

• frames (Sequence[BmcWitnessFrame]) – Decoded frames.

• steps (Sequence[BmcWitnessStep]) – Decoded steps.

• diagnostics (Sequence[str], optional) – Witness diagnostics, defaults to ().

• schema_version (str, optional) – Witness schema version, defaults to "bmc-witness/v1".

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the trace payload is malformed or violates public witness invariants.

Example:

>>> trace = BmcWitnessTrace({'kind': 'reach'}, {'status': 'sat'}, {'mode': 'cold'}, (), ())
>>> trace.to_canonical()['schema_version']
'bmc-witness/v1'

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable witness dictionary.

Returns:

Canonical witness.

Return type:

Dict[str, object]

Example:

>>> trace = BmcWitnessTrace({'kind': 'reach'}, {'status': 'sat'}, {'mode': 'cold'}, (), ())
>>> trace.to_canonical()['steps']
[]

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcRuntimeFrame

class pyfcstm.bmc.witness.BmcRuntimeFrame(index: int, state: str | None, terminated: bool, vars: Mapping[str, Any])

Runtime frame captured during witness replay.

Parameters:

• index (int) – Frame index.

• state (str, optional) – Runtime state path or None when terminated.

• terminated (bool) – Whether the runtime is ended.

• vars (Mapping[str, object]) – Persistent runtime variables.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the runtime-frame payload is malformed.

Example:

>>> BmcRuntimeFrame(0, 'Root', False, {}).to_canonical()['state']
'Root'

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable runtime frame.

Returns:

Canonical runtime frame.

Return type:

Dict[str, object]

Example:

>>> BmcRuntimeFrame(0, None, True, {}).to_canonical()['terminated']
True

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcRuntimeStep

class pyfcstm.bmc.witness.BmcRuntimeStep(index: int, input_events: Sequence[str], consumed_events: Sequence[str], unconsumed_events: Sequence[str], abstract_calls: Sequence[BmcWitnessCallRecord])

Runtime step captured during witness replay.

Parameters:

• index (int) – Step index.

• input_events (Sequence[str]) – Runtime input events.

• consumed_events (Sequence[str]) – Runtime consumed events.

• unconsumed_events (Sequence[str]) – Runtime unconsumed events.

• abstract_calls (Sequence[BmcWitnessCallRecord]) – Handler call records captured in this step.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the runtime-step payload is malformed.

Example:

>>> BmcRuntimeStep(0, (), (), (), ()).to_canonical()['index']
0

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable runtime step.

Returns:

Canonical runtime step.

Return type:

Dict[str, object]

Example:

>>> BmcRuntimeStep(0, (), (), (), ()).to_canonical()['input_events']
[]

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcRuntimeTrace

class pyfcstm.bmc.witness.BmcRuntimeTrace(frames: Sequence[BmcRuntimeFrame], steps: Sequence[BmcRuntimeStep])

Runtime replay trace.

Parameters:

• frames (Sequence[BmcRuntimeFrame]) – Runtime frames.

• steps (Sequence[BmcRuntimeStep]) – Runtime steps.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the runtime-trace payload is malformed.

Example:

>>> BmcRuntimeTrace((), ()).to_canonical()['frames']
[]

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable runtime trace.

Returns:

Canonical runtime trace.

Return type:

Dict[str, object]

Example:

>>> BmcRuntimeTrace((), ()).to_canonical()['steps']
[]

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcReplayMismatch

class pyfcstm.bmc.witness.BmcReplayMismatch(path: str, expected: Any, actual: Any, message: str, tolerance: float | None = None)

Structured replay mismatch.

Parameters:

• path (str) – Dotted or indexed mismatch path.

• expected (object) – Expected value from the witness.

• actual (object) – Actual value observed from runtime replay.

• message (str) – Human-readable mismatch summary.

• tolerance (float, optional) – Float tolerance used for comparison, defaults to None.

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the mismatch payload is malformed.

Example:

>>> BmcReplayMismatch('frames[1].state', 'A', 'B', 'state mismatch').path
'frames[1].state'

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable mismatch dictionary.

Returns:

Canonical mismatch.

Return type:

Dict[str, object]

Example:

>>> BmcReplayMismatch('x', 1, 2, 'bad').to_canonical()['actual']
2

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

BmcReplayResult

class pyfcstm.bmc.witness.BmcReplayResult(witness: BmcWitnessTrace, runtime_trace: BmcRuntimeTrace, mismatches: Sequence[BmcReplayMismatch] = ())

Result of replaying a BMC witness through SimulationRuntime.

Parameters:

• witness (BmcWitnessTrace) – Witness that was replayed.

• runtime_trace (BmcRuntimeTrace) – Captured runtime trace.

• mismatches (Sequence[BmcReplayMismatch], optional) – Structured replay mismatches, defaults to ().

Raises:

pyfcstm.bmc.errors.BmcBuildError – If the replay result payload is malformed.

Example:

>>> trace = BmcWitnessTrace({'kind': 'reach'}, {'status': 'sat'}, {'mode': 'cold'}, (), ())
>>> BmcReplayResult(trace, BmcRuntimeTrace((), ())).ok
True

__str__() → str

Return the default terminal-friendly representation.

Trace-like objects cap this implicit display at the first 50 rows so a direct print(obj) remains practical in terminals. Use to_text() or pretty_print() with max_rows=None when the full table is required.

Returns:

Rendered text.

Return type:

str

Example:

>>> str(BmcWitnessEvent('Root.Go', 'case_positive')).splitlines()[0]
'BmcWitnessEvent'

property ok: bool

Return whether replay had no mismatches.

Returns:

True when replay matched the witness.

Return type:

bool

Example:

>>> trace = BmcWitnessTrace({'kind': 'reach'}, {'status': 'sat'}, {'mode': 'cold'}, (), ())
>>> BmcReplayResult(trace, BmcRuntimeTrace((), ())).ok
True

pretty_print(*, file: Any | None = None, tablefmt: str = 'simple', verbose: bool = False, max_rows: int | None = None, max_events: int | None = 6, max_call_groups: int | None = 6, max_cell_width: int | None = 72, max_var_columns: int | None = None, vars_order: str = 'domain', events_mode: str = 'input', event_reason: str = 'auto', calls_mode: str = 'summary', call_path: str = 'full', call_details: str = 'state_vars', via_mode: str = 'endpoint', show_case: bool = False, show_ids: bool = False, show_legend: bool = True, end: str = '\n') → None

Print a human-readable representation.

Parameters:

• file (object, optional) – File-like object to write to, defaults to sys.stdout.

• tablefmt (str, optional) – tabulate table format, defaults to "simple".

• verbose (bool, optional) – Whether to enable the verbose audit view, defaults to False.

• max_rows (int, optional) – Maximum trace rows to show, defaults to None.

• max_events (int, optional) – Maximum event lines per step, defaults to 6.

• max_call_groups (int, optional) – Maximum call lines per step, defaults to 6.

• max_cell_width (int, optional) – Maximum logical cell-line width, defaults to 72.

• max_var_columns (int, optional) – Maximum variable columns, defaults to None.

• vars_order (str, optional) – Variable column order, defaults to "domain".

• events_mode (str, optional) – Event display mode, defaults to "input".

• event_reason (str, optional) – Event reason tag mode, defaults to "auto".

• calls_mode (str, optional) – Abstract-call display mode, defaults to "summary".

• call_path (str, optional) – Abstract-call path display mode, defaults to "full".

• call_details (str, optional) – Expanded call detail mode, defaults to "state_vars".

• via_mode (str, optional) – Transition path display mode, defaults to "endpoint".

• show_case (bool, optional) – Whether to show selected BMC case labels, defaults to False.

• show_ids (bool, optional) – Whether to show debug id columns, defaults to False.

• show_legend (bool, optional) – Whether to append the extra legend, defaults to True.

• end (str, optional) – String appended after output, defaults to a newline.

Returns:

None.

Return type:

None

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().splitlines()[0]
'BmcWitnessEvent'

to_canonical() → Dict[str, Any]

Return a JSON-stable replay result.

Returns:

Canonical replay result.

Return type:

Dict[str, object]

Example:

>>> trace = BmcWitnessTrace({'kind': 'reach'}, {'status': 'sat'}, {'mode': 'cold'}, (), ())
>>> BmcReplayResult(trace, BmcRuntimeTrace((), ())).to_canonical()['ok']
True

to_text(**kwargs: Any) → str

Return a human-readable representation as text.

Parameters:

kwargs (object) – Pretty-print options except file and end.

Returns:

Rendered text.

Return type:

str

Raises:

pyfcstm.bmc.errors.BmcBuildError – If file or end is passed to this string-returning helper.

Example:

>>> BmcWitnessEvent('Root.Go', 'case_positive').to_text().startswith('BmcWitnessEvent')
True

solve_bmc_property

pyfcstm.bmc.witness.solve_bmc_property(formula: BmcPropertyFormula, *, timeout_ms: int | None = None, check_incomplete: bool = True) → BmcSolveResult

Solve a compiled BMC property formula.

The primary status always comes from BmcPropertyFormula.solve_formula. When check_incomplete is true and the formula has a non-false incomplete-bound observation, the incomplete formula is solved separately and reported without changing the primary status.

Parameters:

• formula (pyfcstm.bmc.properties.BmcPropertyFormula) – Compiled BMC property formula.

• timeout_ms (int, optional) – Optional Z3 timeout in milliseconds, defaults to None.

• check_incomplete (bool, optional) – Whether to solve incomplete-bound diagnostics, defaults to True.

Returns:

Structured solve result.

Return type:

BmcSolveResult

Raises:

pyfcstm.bmc.errors.BmcBuildError – If arguments are malformed.

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: active("Root");')))
>>> solve_bmc_property(formula).status
'sat'

decode_bmc_witness

pyfcstm.bmc.witness.decode_bmc_witness(formula: BmcPropertyFormula, model: ModelRef, *, event_policy: BmcEventDecodePolicy | None = None) → BmcWitnessTrace

Decode a SAT model into a macro-step witness trace.

The decoder consumes selected case relations and trace symbols produced by earlier BMC layers. It does not re-expand macro paths, and it intentionally emits only sparse replay input events instead of every true event Boolean in the Z3 model.

Parameters:

• formula (pyfcstm.bmc.properties.BmcPropertyFormula) – Compiled BMC property formula whose solve formula was SAT.

• model (z3.ModelRef) – Z3 model returned for formula.solve_formula.

• event_policy (BmcEventDecodePolicy, optional) – Optional sparse event decode policy, defaults to None which uses BmcEventDecodePolicy.

Returns:

Decoded witness trace.

Return type:

BmcWitnessTrace

Raises:

pyfcstm.bmc.errors.BmcBuildError – If inputs are malformed or the model violates internal witness consistency assumptions.

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.bmc.witness import solve_bmc_property, decode_bmc_witness
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: active("Root");')))
>>> result = solve_bmc_property(formula)
>>> decode_bmc_witness(formula, result.model).frames[0].sentinel
'init'

replay_bmc_witness

pyfcstm.bmc.witness.replay_bmc_witness(state_machine: StateMachine, witness: BmcWitnessTrace, *, abstract_handlers: Mapping[str, Callable[[ReadOnlyExecutionContext], None]] | None = None) → BmcReplayResult

Replay a decoded witness with SimulationRuntime.

Replay compares only macro-observable runtime data: states, termination, persistent variables, event accounting, and abstract handler contexts. BMC case labels remain witness-side debug metadata because the runtime does not expose selected case labels.

Parameters:

• state_machine (pyfcstm.model.StateMachine) – State machine used for replay.

• witness (BmcWitnessTrace) – Decoded BMC witness trace.

• abstract_handlers (Mapping[str, Callable], optional) – Optional user handlers wrapped after the recorder, defaults to None.

Returns:

Replay result with structured mismatches.

Return type:

BmcReplayResult

Raises:

pyfcstm.bmc.errors.BmcBuildError – If inputs are malformed.

Example:

>>> from pyfcstm.bmc import BmcEngine, build_bmc_core_formula, compile_bmc_property
>>> from pyfcstm.bmc.witness import solve_bmc_property, decode_bmc_witness, replay_bmc_witness
>>> from pyfcstm.model import load_state_machine_from_text
>>> sm = load_state_machine_from_text('state Root;')
>>> formula = compile_bmc_property(build_bmc_core_formula(BmcEngine(sm).prepare('check reach <= 1: active("Root");')))
>>> result = solve_bmc_property(formula)
>>> replay_bmc_witness(sm, decode_bmc_witness(formula, result.model)).ok
True