Skip to content

tutorial.md

Latest commit

 

History

History
145 lines (101 loc) · 5.52 KB

tutorial.md

File metadata and controls

145 lines (101 loc) · 5.52 KB
Raw

Tutorial

English | 日本語

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

The tools you need are listed in Requirements. If you do not have the Quint CLI yet, follow Setup before you start.

Where to start

Clone the repository:

git clone [email protected]:conjikidow/quint-connect-tutorial.git
cd quint-connect-tutorial

main holds the finished tutorial, so starting there would spoil it. Start from the first checkpoint instead, on a branch of your own:

git switch -c tutorial-work step-0

All four steps are done on that one branch, by editing the files in place. Each step has a tag holding the state it starts from, so nothing is lost if you get stuck. See Checkpoints.

Step 0: get to know the planner

Read the three files in this order.

Once you know what the planner is supposed to do, run the tests:

cargo test

Everything passes.

Step 1: connect the specification to the implementation

The model-based test does not exist yet. Bring in its skeleton, together with the dependencies it needs:

git restore --source=step-1 -- Cargo.toml Cargo.lock tests/model_based.rs

From here you only edit tests/model_based.rs. Leave src/lib.rs and spec/planner.qnt as they are.

Everything the skeleton leaves to you is marked with a TODO, and there are four of them.

  • The body of from_driver, which reads out of the implementation the values the trace records. This one is the oracle of the test: it decides what it means for the two sides to agree.
  • The specification variable whose contents config compares.
  • The switch! arms for the actions that are not handled yet.
  • The specification to run, and the test function returning the driver.

Refer to the Quint Connect README for the syntax of all of them.

The names in the switch! arms are matched against the specification, so they have to spell its action names and nondet names exactly.

The skeleton does not compile as it stands, so the compiler is your first list of what is missing. Run the test with:

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

By the end of this step, the example-based tests still pass and the model-based test fails. A failure reporting that the specification and the implementation diverge means your driver works, so move on. Anything else is still the driver: a compilation error, an unknown action, or a trace that cannot be deserialized.

Step 2: make the implementation agree with the specification

Now the opposite: only src/lib.rs changes. The specification is the reference here, so do not edit it to make the test pass. The model-based test stays as you wrote it too.

The failure report names the action that was replayed and shows both states. That is usually enough to locate the disagreement. Verbose output shows every step rather than only the last one, and QUINT_SEED replays the exact traces a previous run generated.

The test stops at the first divergence it finds, so run it again after every fix. The step is over once

cargo test -- --nocapture

is green.

Step 3: pin down what the model-based test found

The last step changes only tests/example_based.rs.

Add an example-based test for every case you had to fix in step 2. The model-based test found those cases by exploring the specification, and it will find them again; an example-based test names them, and says out loud what the planner is supposed to do about them. Model-based testing does not replace example-based testing. It finds the gaps and hands you the cases worth pinning down.

Then compare your work with the reference solution:

git diff main

From here, a few directions are worth taking.

  • Check the specification exhaustively rather than by simulation, as described in Checking the specification alone.
  • Extend the specification with a larger grid, several obstacles, or a new action, and let the model-based test tell you what the implementation still owes it.

Checkpoints

Each tag holds the state the corresponding step starts from.

Tag State
step-0 The specification, the implementation, and the example-based tests.
step-1 The same, plus the skeleton of the model-based test.
step-2 The same, plus the finished model-based test, which reports a divergence.
step-3 The same, plus an implementation that agrees with the specification.
main The same, plus the regression tests of step 3.

The answer to a step is therefore the tag of the step after it. To skip a step, or to recover a working tree you would rather forget, take that file back:

git restore --source=step-2 -- tests/model_based.rs    # skip step 1
git restore --source=step-3 -- src/lib.rs              # skip step 2
git restore --source=main -- tests/example_based.rs    # skip step 3