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 in human-readable, full JSON, or stable LLM-oriented formats.

Module map:

Entry	Purpose
`build_inspect_json()`	Build full JSON text for one input file and inspect policy.
`build_inspect_output()`	Build text in the requested inspect output format.
`resolve_inspect_color_enabled()`	Resolve whether the human inspect renderer should emit ANSI color.
`_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 { state Idle; [*] -> Idle; }")
...     text = build_inspect_json(path)
>>> '"root_state_path": "Root"' in text
True

resolve_inspect_color_enabled

pyfcstm.entry.inspect.resolve_inspect_color_enabled(color_mode: str, *, output_format: str = 'human', output_file: str | None = None, stdout_isatty: bool | None = None, no_color: str | None = None, term: str | None = None) → bool[source]

Return whether inspect output should include ANSI color.

Color is a presentation feature for the human format only. Machine formats always stay ANSI-free so their JSON or Markdown can be consumed by scripts, editors, and LLM pipelines without escape-code cleanup.

Parameters:

color_mode (str) – Requested color mode: "auto", "always", or "never".
output_format (str, optional) – Inspect output format, defaults to "human".
output_file (Optional[str], optional) – Output path supplied to -o. A non-None value disables ANSI color even when color_mode is "always".
stdout_isatty (Optional[bool], optional) – Optional TTY probe result. None probes sys.stdout.
no_color (Optional[str], optional) – Optional NO_COLOR value. None reads from the environment; any non-empty value disables auto color.
term (Optional[str], optional) – Optional TERM value. None reads from the environment; "dumb" disables auto color.

Returns:

True if the human renderer should emit ANSI color.

Return type:

bool

Raises:

ValueError – If color_mode is unsupported.

Examples:

>>> resolve_inspect_color_enabled("never", stdout_isatty=True)
False
>>> resolve_inspect_color_enabled("always", stdout_isatty=False)
True
>>> resolve_inspect_color_enabled("always", output_format="json", stdout_isatty=True)
False
>>> resolve_inspect_color_enabled("auto", stdout_isatty=True, no_color="0")
False

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 { state Idle; [*] -> Idle; }")
...     payload = json.loads(build_inspect_json(path))
>>> payload["root_state_path"]
'Root'

build_inspect_output

pyfcstm.entry.inspect.build_inspect_output(input_code_file: str, *, output_format: str = 'human', color_enabled: bool = False, 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 inspect output text in the requested presentation format.

output_format="json" delegates to build_inspect_json() so the full JSON contract stays byte-for-byte aligned with the pre-existing machine-readable path. Human and stable LLM formats additionally read the top-level source file to render source excerpts.

Parameters:

input_code_file (str) – Path to the input FCSTM DSL file.
output_format (str, optional) – One of "human", "json", "llm-json", or "llm-md". Defaults to "human".
color_enabled (bool, optional) – Whether the human renderer should emit ANSI color. Ignored by machine-readable formats.
enable_verify (bool, optional) – Whether to run inspect-eligible verify algorithms.
max_complexity_tier (str, optional) – Maximum verify complexity tier accepted by inspect.
max_call_count_scaling (str, optional) – Maximum verify call-count scaling accepted by inspect.
smt_timeout_ms (Optional[int], optional) – Optional solver timeout in milliseconds.

Returns:

Rendered inspect output ending with a newline.

Return type:

str

Raises:

pyfcstm.entry.base.ClickErrorException – If reading, parsing, model validation, or inspect policy validation fails.
ValueError – If output_format is not supported.

Example:

>>> 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 { state Idle; [*] -> Idle; }")
...     text = build_inspect_output(path)
>>> "[WARN] FCSTM Inspect Report" in text
True