# Formal models

[Quint](https://quint-lang.org) models of designs where interleavings matter
more than any single code path. A model is a hand-written reading of the code:
it finds flaws the design and the code share, not places where the code
strays from the design. So every counterexample is also reproduced as a failing
test against the real code before anything is changed.

```sh
npm install -g @informalsystems/quint     # 0.33 or later
```

Exhaustive bounded checking (`quint verify`) uses Apalache and needs Java 17.

The gated state machine the agent ran before the switch-over (M2.8) had its
own model, `orchestrator.qnt`; it went with that code, and is in the history.

## `loop.qnt`: the agent loop, as the architecture describes it

Models the design in `docs/Architecture.md` rather than the code (it was
written before the loop was):
- work items from assigned issues and conversations;
- restatements and revision-bound go-aheads;
- park-and-switch, with branches pushed on parking;
- blocked dependencies;
- harness-owned milestones and waiting for merges;
- review follow-ups;
- record issues;
- crashes and build VM wipes at any point.

A counterexample here is a gap in the architecture, so it is fixed there,
and the model carries the fix (marked `FIX n`). `loop_scenarios.qnt` keeps each
counterexample as a trace of the fixed behaviour. Each trace fails if its fix
is reverted, and each property that never failed was checked against a
deliberately broken model.

```sh
quint run specs/loop.qnt --invariant=all_properties --max-steps=80 --max-samples=200000
quint test specs/loop_scenarios.qnt
```

Traces need about 80 steps to reach second milestones. The `w_*` values at the
end are reachability witnesses: each should be *violated*, which shows the
state it names is reachable.

**Against the real code.** `nisse-dev/tests/test_loop_properties.py` checks
the same properties against the loop itself: a seeded random walk over
what the operator and Gitea can do (go-aheads, answers, comments, merges,
closes, abandon, a crash and restart), checking every property after every
step. It found two bugs the design model couldn't, because they were in the
code: abandon left an open PR, and a review fix after a follow-up PR went to
the merged branch. Each also has its own regression test.

**Keeping it true.** When the architecture changes a rule this models, change
the model and the walk in the same PR.