quint_run
Simulate Quint specifications with random execution to verify invariants and detect violations through counterexample traces.
Instructions
Simulate a Quint specification with random execution. Runs the state machine and optionally checks an invariant. Returns pass/fail and a counterexample trace if the invariant is violated.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| source | No | Quint specification source code (.qnt content) | |
| file_path | No | Path to a .qnt file on disk | |
| init | No | Init action name (default: "init") | |
| step | No | Step action name (default: "step") | |
| invariant | No | Invariant to check during simulation | |
| max_samples | No | Number of simulation runs (default: 10000) | |
| max_steps | No | Max steps per run (default: 20) | |
| seed | No | Random seed for reproducibility |
Implementation Reference
- index.js:170-221 (handler)Tool definition and handler for 'quint_run'. It uses 'runWithSource' to invoke the 'quint run' command with the provided simulation arguments (init, step, invariant, max_samples, max_steps, seed).
server.tool( "quint_run", "Simulate a Quint specification with random execution. Runs the state machine and optionally checks an invariant. Returns pass/fail and a counterexample trace if the invariant is violated.", { ...sourceSchema, init: z.string().optional().describe('Init action name (default: "init")'), step: z.string().optional().describe('Step action name (default: "step")'), invariant: z .string() .optional() .describe("Invariant to check during simulation"), max_samples: z .number() .optional() .describe("Number of simulation runs (default: 10000)"), max_steps: z .number() .optional() .describe("Max steps per run (default: 20)"), seed: z.number().optional().describe("Random seed for reproducibility"), }, async ({ source, file_path, init, step, invariant, max_samples, max_steps, seed, }) => { try { const result = await runWithSource(source, file_path, (f) => { const args = ["run"]; if (init) args.push(`--init=${init}`); if (step) args.push(`--step=${step}`); if (invariant) args.push(`--invariant=${invariant}`); if (max_samples != null) args.push(`--max-samples=${max_samples}`); if (max_steps != null) args.push(`--max-steps=${max_steps}`); if (seed != null) args.push(`--seed=${seed}`); args.push(f); return args; }); return formatResult(result); } catch (err) { return { content: [{ type: "text", text: `Error: ${err.message}` }], isError: true, }; } }, );