mcp-server-quint

Instructions

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,
        };
      }
    },
  );