You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This commit was created on GitHub.com and signed with GitHub’s verified signature.
Model checker fixes
Function calls now work in every flow context — top-level funcs can be called from serial actions and from inside parallel and oneof blocks, at the top level or within roles. Previously calls were restricted to atomic context or roles, and role-method calls inside parallel blocks crashed the checker. (#379, #380)
Counterexample traces through parallel blocks render correctly — failures whose trace passes through a parallel block previously crashed the failure dump instead of printing the trace, error graph, and HTML. (#381)
exists assertions are now verified in --experimental_no_graph and simulation modes — previously they were silently reported as PASSED. Exhaustive no-graph runs now FAIL on unwitnessed exists assertions; simulation prints a named warning. (#376)
Clear error for require used directly inside a parallel block — parallel statements are unordered, so there is no defined point for the check. Place the require above the parallel block to guard the action, or inside an atomic:/serial: branch to guard that branch. (#382)
Other improvements
Official Docker image: ghcr.io/fizzbee-io/fizzbee — thin image wrapping the release tarball, rebuilt monthly on the current Debian trixie base. (#370, #374, #375)
MBT: per-process socket path for the Rust plugin server — fixes concurrent runs. (#372)
Explorer: failed runs supported via ?errors=1. (#378)