Quint Connect Tutorial

English | 日本語

A tutorial for Quint Connect, a model-based testing framework connecting Quint specifications with Rust implementations.

The subject is a tiny rover path planner on a 3x3 grid. The planner looks for a path from a start position to a goal position while avoiding at most one obstacle. The same behavior is described twice: once as a Quint specification and once as a Rust implementation. Quint Connect generates traces from the specification, replays them against the implementation, and compares both states after every step.

The tutorial is hands-on. You write the model-based test yourself, let it disagree with the implementation, and then fix what it finds.

Layout

• spec/planner.qnt: the Quint specification, with the planner state, the two candidate paths, the selection rule, and the invariants.
• src/lib.rs: the Rust implementation, with Position, PlanResult, and the Planner itself.
• tests/example_based.rs: example-based tests, with hand-written inputs and the results they are expected to produce.
• tests/model_based.rs: the Quint Connect driver and the model-based test that replays the generated traces. This is the file you write in step 1.
• docs/tutorial.md: the tutorial itself, from the first checkpoint to the reference solution.

Requirements

• Rust, as pinned by rust-toolchain.toml.
• The Quint CLI, which must be executable from PATH, as Quint Connect runs it as a subprocess to generate traces. This tutorial is tested with Quint 0.32.0.
• A JDK 17 or later, but only to model check the specification with quint verify, which runs the Apalache model checker on the JVM.

Setup

Install the Quint CLI with npm, which requires Node.js:

npm i @informalsystems/quint@0.32.0 -g

Homebrew, Nix, and prebuilt binaries are also available; see the Quint installation guide for the up-to-date instructions.

Check that the CLI is reachable:

quint --version

The crate dependencies are fetched by Cargo on the first build. Quint 0.31 and later simulate with a Rust evaluator that is downloaded into ~/.quint on the first simulation, so the first run of the model-based test needs network access and takes a little longer.

Tutorial

The tutorial itself is in docs/tutorial.md. It starts from a tagged checkpoint rather than from main, which already holds the finished work.

Running tests

Run every test:

cargo test -- --nocapture

--nocapture is what makes the progress of the model-based test visible.

Run only the hand-written tests:

cargo test --test example_based

Run only the model-based test:

cargo test --test model_based -- --nocapture

Verbose output

Quint Connect can print the action, the nondeterministic choices, and the resulting state of every step:

QUINT_VERBOSE=1 cargo test --test model_based -- --nocapture

QUINT_VERBOSE=2 additionally prints the raw states read from the traces.

Replaying the same traces

When the model-based test fails, it reports the random seed used to generate the traces. Set QUINT_SEED to that value to replay exactly the same traces:

QUINT_SEED=0x659f147f cargo test --test model_based -- --nocapture

Checking the specification alone

The specification can be checked without Rust. Type checking and simulation take well under a second:

quint typecheck spec/planner.qnt
quint run spec/planner.qnt --max-samples=100 --max-steps=20 --invariant=inv

quint run simulates random traces, so it only checks the invariants on the executions it happens to generate. quint verify checks them exhaustively up to a bounded number of steps instead, using the Apalache model checker:

quint verify spec/planner.qnt --invariant=inv

That takes about half a minute, as Apalache runs on the JVM and is downloaded on the first run.

Model behavior

The planner considers exactly two candidate paths from the start position to the goal position.

• The XY path first moves along the X axis and then along the Y axis.
• The YX path first moves along the Y axis and then along the X axis.

A path lists every position the rover reaches, one step at a time. It does not contain the start position, and it always ends at the goal. For a start of (0, 0) and a goal of (2, 1), the XY path is [(1, 0), (2, 0), (2, 1)] and the YX path is [(0, 1), (1, 1), (2, 1)].

A candidate path is valid when it does not contain the obstacle, and the result is chosen as follows.

1. If the XY path is valid, the plan is the XY path.
2. Otherwise, if the YX path is valid, the plan is the YX path.
3. Otherwise, there is no plan at all.

Three consequences are worth pointing out. An obstacle sitting on the start position never invalidates a path, as the start position is not part of any path. An obstacle sitting on the goal position invalidates every path, as every path ends at the goal. When the start position is the goal position, both paths are empty, so the result is the empty plan rather than no plan.

License

Licensed under the Apache License, Version 2.0, the same license as Quint Connect itself.