Release Notes

v0.6.0

This minor release adds an end-to-end FBMCQ bounded model checking workflow, makes inspect reports useful to both people and LLM repair loops, expands the built-in runtime templates to Python, C, C Poll, C++, and C++ Poll, and ships substantially expanded bilingual documentation. It also contains public API and CLI compatibility changes that require callers to review the migration notes.

FBMCQ and Bounded Model Checking

  • Added the FBMCQ property language, parser, model binding, macro expansion, transition-relation compiler, Z3 solving pipeline, and public pyfcstm.bmc APIs. The language covers reachability, coverage, safety, bounded liveness, response, assumptions, and initial-state constraints.

  • Added pyfcstm bmc for one FCSTM model and one FBMCQ query. The default terminal report states whether the bounded property holds before showing the SAT/UNSAT solver diagnostic, supports optional ANSI color, and requires every decoded SAT witness to pass structural validation and simulator replay.

  • Added the stable bmc-cli/v1 JSON envelope for CI, tools, and LLM consumers, with a downloadable schema in the BMC result protocol reference. The envelope preserves polarity-aware outcomes, solver timing, witness and replay records, diagnostics, and the matching process exit code.

Inspect and Diagnostics

  • Changed pyfcstm inspect to default to a checker-style human report with aligned source spans, nearby source context, compact severity labels, and --color auto|always|never. Files, pipes, and machine formats remain free of ANSI escapes.

  • Kept the stable machine report under --format json and added --format llm-json and --format llm-md using schema pyfcstm.inspect.llm.v1. LLM reports carry source context, provenance, repair guidance, and explicit do-not notes.

  • Expanded static and verify-backed diagnostics, including numeric and guard reasoning, while keeping solver-backed inspect checks behind the existing explicit enablement and safety gates.

  • Added isolated multi-provider repair evaluations that test whether a consumer can locate, explain, repair, and replay real diagnostics without access to hidden repository context.

Simulation and Runtime Semantics

  • Hardened hot start, pseudo-state routing, DFS limits, stack stabilization, speculative rollback, expression short-circuiting, persistent-variable normalization, event ownership, history resizing, and terminal queries.

  • Added pyfcstm.simulate.CycleResult event accounting and strengthened abstract-handler registration, decorator scanning, execution context, named action references, warning metadata, and session-copy behavior.

  • Extended the shared semantic fixture corpus so the simulator and generated runtimes are checked against the same cycle-by-cycle state, variable, event, history, callback, and failure behavior.

Built-In Templates and DSL

  • Added the first-class cpp and cpp_poll built-in templates alongside python, c, and c_poll. C-family templates use CMake-driven native checks, simulator-alignment fixtures, wrapper smoke tests, and explicit deployment profiles without requiring heap allocation in the runtime core.

  • Added ordered combo-transition triggers that combine event and guard terms in one cycle. They expand into traceable pseudo relay states while preserving source metadata, guard/effect order, rollback, PlantUML output, inspect reports, simulation behavior, and generated-runtime alignment.

  • Added template-suite detection and dedicated representative/full-suite jobs so source-template dependencies and native toolchain coverage fail closed without forcing every ordinary change through every expensive native suite.

LLM Prompt Resources

  • Added the packaged FBMCQ authoring guide and integrity-checked public APIs: pyfcstm.llm.get_fbmcq_language_guide_prompt_for_llm(), pyfcstm.llm.get_fbmcq_language_guide_prompt_path_for_llm(), and pyfcstm.llm.get_fbmcq_language_guide_prompt_metadata_for_llm().

  • The FCSTM and FBMCQ guide APIs now live in dedicated modules while pyfcstm.llm remains the compact public import surface. Both Guide resources use adjacent SHA-256 sidecars generated by make sha256.

  • Added standalone FBMCQ Guide evaluation fixtures for seven property kinds, full-source and known-fact task forms, oracle checks, anti-vacuity checks, mutation discrimination, and trace replay. Provider transcripts remain repository evidence rather than package data.

Documentation and Release Artifacts

  • Reorganized the bilingual documentation around Tutorials, How-to Guides, Explanations, and Reference material, with runnable examples and dedicated coverage for the DSL, simulation, inspect, templates, and BMC workflows.

  • Added bilingual BMC Tutorial and How-to material, three mathematical Explanation pages, and exhaustive query/result Reference pages. The explanations derive 40 labelled, implementation-traceable equations and are verified in MathJax HTML and XeLaTeX PDF output.

  • Hardened the bilingual Sphinx PDF path with isolated builds, XeLaTeX/CJK font checks, structural/content validation, adversarial self-checks, and complete contents/index verification. GitHub Releases now attach validated English and Chinese PDF manuals in addition to package, CLI, and VSIX artifacts.

Verification and Inspect

  • Removed the unimplemented bounded_reachability, symbolic_bfs, bounded_safety, bounded_invariant, and path_witness entries from pyfcstm.verify.REGISTRY. The registry now contains only its 14 callable structural and SMT-local algorithms.

  • Removed the verify-only taxonomy values bmc_search, k_unrollings, k_unrollings_times_branching, and bmc_unrolled. BMC queries and witnesses are exposed by pyfcstm.bmc, not through verify or inspect.

Compatibility Notes

BMC results are bounded by the query’s <= N and are not unbounded proofs. Scripts must consume --json instead of parsing human wording, color, or live timing. SAT means a witness for witness-polarity properties and a counterexample for counterexample-polarity properties; use the reported property verdict or result.outcome rather than treating SAT as success.

The default inspect output is now intended for humans. Existing scripts that parsed the former default JSON output must pass --format json. LLM automation should use llm-json or llm-md rather than parsing the human report.

Code that referenced the removed verify registry keys or taxonomy values must migrate to the public pyfcstm.bmc query APIs. The inspect CLI no longer accepts the removed BMC-only values merely to reject them in application code; Click now reports them as invalid choices with usage exit status 2 instead of the former policy-error status 1.

The five built-in templates remain marked experimental. The VSCode extension continues to use its own independent version line and is not versioned as 0.6.0 by this Python package release.

v0.5.0

This release is a minor release rather than a v0.4.2 patch release. It adds new user-facing APIs, CLI surfaces, packaged LLM resources, verification-backed diagnostics, DSL condition operators, and simulator semantic fixes. Existing models should review the compatibility notes before upgrading.

Verification and Inspect

  • Added the pyfcstm.verify package as the public entry point for raw verification algorithms, registry metadata, complexity taxonomy, and inspect gating helpers.

  • Added SMT-local verification algorithms for guards, effects, lifecycle relations, transition shadowing, and composite initialization checks.

  • Integrated inspect-eligible verification algorithms into pyfcstm.diagnostics.inspect_model() and the pyfcstm inspect CLI. Verify-backed checks stay opt-in through enable_verify=True or pyfcstm inspect --enable-verify.

  • Added inspect safety gates for complexity tier, call-count scaling, and SMT timeout forwarding. BMC-style search remains outside the automatic inspect path.

Diagnostics and CLI

  • Expanded the structured diagnostics catalog to 59 codes: 20 errors, 32 warnings, and 7 infos.

  • Added verify-backed diagnostic coverage while keeping the default inspect path static unless verification is explicitly enabled.

  • Added pyfcstm inspect for stable JSON output matching inspect_model(model).to_json().

  • Preserved Python / jsfcstm diagnostic-surface parity for normalized code, severity, and reference payloads used by editor integrations.

LLM Grammar Guide

  • Added pyfcstm.llm with pyfcstm.llm.get_grammar_guide_prompt_for_llm(), pyfcstm.llm.get_grammar_guide_prompt_path_for_llm(), and pyfcstm.llm.get_grammar_guide_prompt_metadata_for_llm().

  • Packaged the official LLM-facing FCSTM grammar guide as pyfcstm/llm/fcstm_grammar_guide.md.

  • Added a packaged SHA-256 sidecar and runtime integrity verification for the grammar guide prompt. Callers may downgrade integrity failures to warnings when they intentionally need to inspect a damaged or development resource.

  • Added standalone llm_eval/ fixtures and reports for prompt-quality validation. These files are repository evaluation assets and are not packaged into PyPI distributions.

Simulation and Built-In Templates

  • Hardened simulator semantics around speculative rollback, hot-start initialization, event normalization, lifecycle action references, abstract handler contracts, and cycle boundary behavior.

  • Added a semantic fixture corpus for simulator and generated-runtime alignment.

  • Stabilized generated Python runtime metadata, callback rollback behavior, and expression-error wrapping.

  • The packaged built-in template flow remains available through pyfcstm generate --template .... Current packaged templates are python, c, and c_poll; the VSCode extension has its own independent version line and is not versioned as 0.5.0 by this Python package release.

DSL Expression Operators

This release extends cond_expression with three boolean operators for guard conditions and other boolean expression sites:

  • A => B and A implies B express implication. The canonical DSL spelling is =>. Implication is right-associative, so A => B => C means A => (B => C).

  • A xor B expresses boolean exclusive-or. Chained xor is a left-associative boolean parity chain, not an exactly-one-of-many operator.

  • A iff B expresses boolean equivalence and is the readable spelling of boolean equality. Chained iff expressions use the same boolean equality precedence layer as == and !=.

Compatibility Notes

implies, xor, and iff are now reserved DSL keywords. Existing machines that used these names for variables, states, or events must rename those identifiers before using this release.

-> remains the state-transition arrow and is not an implication operator in guard conditions. Use => or implies instead.

^ remains the numeric bitwise XOR operator. It can be used inside arithmetic expressions that are compared in a guard, for example:

StateA -> StateB : if [(flags ^ 0xFF) == 0];

It is not a boolean XOR spelling:

StateA -> StateB : if [a > 0 xor b > 0];   // valid
StateA -> StateB : if [(a > 0) ^ (b > 0)]; // invalid
StateA -> StateB : if [true ^ false];      // invalid

The verification and inspect APIs are new public surfaces in this release. They are intended to be stable at the function and JSON-contract level, but callers should still treat precise diagnostic wording and solver evidence text as diagnostic payloads rather than hard-coded parsing targets.