pyfcstm.entry.bmc

Command-line bounded model checking for FCSTM models.

This module composes the public BMC pipeline into the pyfcstm bmc command. It keeps query compilation, solving, witness decoding, and runtime replay explicit while providing stable human and JSON process contracts.

The normative bmc-cli/v1 JSON Schema is published as a download from the BMC result protocol reference rather than shipped as a runtime package resource.

Module map:

Entry

Purpose

build_bmc_output()

Run one model/query pair and return report text plus its exit status.

write_bmc_output()

Atomically replace an output file with a completed report.

_add_bmc_subcommand()

Register the bmc command on a Click group.

Examples:

>>> import os
>>> from tempfile import TemporaryDirectory
>>> with TemporaryDirectory() as td:
...     model_path = os.path.join(td, "machine.fcstm")
...     query_path = os.path.join(td, "property.fbmcq")
...     with open(model_path, "w", encoding="utf-8") as f:
...         _ = f.write("state Root;")
...     with open(query_path, "w", encoding="utf-8") as f:
...         _ = f.write('check reach <= 1: active("Root");')
...     report, exit_code = build_bmc_output(model_path, query_path)
>>> exit_code
0
>>> report.startswith("BMC reach <= 1: PROPERTY HOLDS")
True

__all__

pyfcstm.entry.bmc.__all__ = ['build_bmc_output', 'write_bmc_output']

Built-in mutable sequence.

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

build_bmc_output

pyfcstm.entry.bmc.build_bmc_output(input_code_file: str, query_file: str, *, json_output: bool = False, timeout_ms: int | None = None, max_bound: int | None = None) → Tuple[str, int][source]

Run one bounded query and build its complete CLI report.

Parameters:

  • input_code_file (str) – FCSTM model file path.

  • query_file (str) – FBMCQ query file path.

  • json_output (bool, optional) –

    Whether to emit bmc-cli/v1 JSON, defaults to False. Its normative JSON Schema is linked from the BMC result protocol reference.

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

  • max_bound (int, optional) – Maximum accepted query bound, defaults to None.

Returns:

Completed report text and matching process exit status.

Return type:

Tuple[str, int]

Raises:

  • pyfcstm.entry.base.ClickErrorException – If model/query input is invalid or unsupported.

  • RuntimeError – If solving, witness decoding, or replay encounters an internal consistency failure.

Examples:

>>> # See the module example for a complete temporary-file invocation.
>>> callable(build_bmc_output)
True

write_bmc_output

pyfcstm.entry.bmc.write_bmc_output(output_file: str, text: str) → None[source]

Atomically replace one output file with a completed BMC report.

The temporary file is created beside the target so os.replace() remains an atomic same-filesystem operation. Parent directories are not created.

Parameters:

  • output_file (str) – Destination file path.

  • text (str) – Complete UTF-8 report text.

Returns:

None.

Return type:

None

Raises:

  • OSError – If temporary-file creation, writing, synchronization, or replacement fails.

  • UnicodeError – If text cannot be encoded as UTF-8.

Examples:

>>> import os
>>> from tempfile import TemporaryDirectory
>>> with TemporaryDirectory() as td:
...     path = os.path.join(td, "result.txt")
...     write_bmc_output(path, "ok\n")
...     open(path, encoding="utf-8").read()
'ok\n'