pyfcstm.entry.inspect

Command-line model inspection for FCSTM DSL files.

This module registers the inspect CLI command. The command reads an FCSTM DSL file, builds a pyfcstm.model.StateMachine, runs pyfcstm.diagnostics.inspect_model(), and emits the inspection payload as stable JSON text.

Module map:

Entry

Purpose

build_inspect_json()

Build JSON text for one input file and inspect policy.

_add_inspect_subcommand()

Register the inspect subcommand on a Click group.

Examples:

>>> import os
>>> from tempfile import TemporaryDirectory
>>> with TemporaryDirectory() as td:
...     path = os.path.join(td, "demo.fcstm")
...     with open(path, "w", encoding="utf-8") as f:
...         _ = f.write("state Root;")
...     text = build_inspect_json(path)
>>> '"root_state_path": "Root"' in text
True

build_inspect_json

pyfcstm.entry.inspect.build_inspect_json(input_code_file: str, *, enable_verify: bool = False, max_complexity_tier: str = 'structural', max_call_count_scaling: str = 'linear_in_transitions', smt_timeout_ms: int | None = None) → str[source]

Build stable JSON text for an inspected FCSTM model.

The helper centralizes the CLI workflow: read and parse the DSL file, build the state-machine model, run pyfcstm.diagnostics.inspect_model(), and serialize the JSON-friendly dict returned by ModelInspect.to_json().

Parameters:

  • input_code_file (str) – Path to the input FCSTM DSL file.

  • enable_verify (bool, optional) – Whether to run inspect-eligible verify algorithms.

  • max_complexity_tier (str, optional) – Maximum verify complexity tier accepted by inspect. Forbidden tiers are rejected even when enable_verify is false.

  • max_call_count_scaling (str, optional) – Maximum verify call-count scaling accepted by inspect. Forbidden scaling labels are rejected even when enable_verify is false.

  • smt_timeout_ms (Optional[int], optional) – Optional solver timeout in milliseconds for SMT-local verify algorithms. None leaves the solver timeout unset. 0 is forwarded unchanged to the solver layer and follows Z3 semantics, where no finite timeout is configured.

Returns:

Pretty-printed JSON inspection report text ending with a newline.

Return type:

str

Raises:

pyfcstm.entry.base.ClickErrorException – If the input file is missing, cannot be read, cannot be decoded, fails parsing or model validation, or requests a forbidden inspect verify policy.

Examples:

>>> import json
>>> import os
>>> from tempfile import TemporaryDirectory
>>> with TemporaryDirectory() as td:
...     path = os.path.join(td, "demo.fcstm")
...     with open(path, "w", encoding="utf-8") as f:
...         _ = f.write("state Root;")
...     payload = json.loads(build_inspect_json(path))
>>> payload["root_state_path"]
'Root'