test

Test Z Specification with ProB

Validate and animate a Z specification using probcli (ProB command line interface).

Input

Arguments: $ARGUMENTS

Parse arguments:

• First positional argument: file path (or search in docs/)
• -v or --verbose: Append each check's detail field to its summary line. Without -v, render only <name>: <status>; with -v, render <name>: <status> — <detail> (display only — the tool returns structured JSON, not raw probcli stdout, so there is no raw output to surface)
• -s N or --setsize N: Default set size for model checking (default: 2)

-a and -v are not parameters of the test tool. run_full_suite animates a fixed 20 steps internally — custom step counts are the separate animate capability. The tool's max_ops (default 1000) bounds model-checking only, and stays at the default; -v merely changes how this command renders the returned JSON.

Process

1. Locate the Specification

If a file path is provided, use it directly. If no file specified, look in docs/ for .tex files.

2. Verify

Call mcp__plugin_z-spec_zspec__test with file, plus setsize from -s. Leave max_ops and timeout at the tool defaults — they are not wired to flags. -v is the verbose flag (see step 3), not a tool argument.

The tool runs the five checks — parse-and-init, animation, CBC assertions, CBC deadlock, model check — and returns:

{timestamp, probcli_version, setsize, ok, states_analysed,
 transitions_fired, checks:[{name, status, detail}],
 operations:[{name, times_fired, covered}], counter_example?}

It persists <stem>.report.json alongside the spec.

3. Report

If the returned JSON has an error field (e.g. the binary is not installed), show that message to the user and stop — do not render the normal result.

Render the JSON as text. Without -v, render each check as <check.name>: <check.status> (summary only). With -v, append the detail as <check.name>: <check.status> — <check.detail>: