# 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.

## `orchestrator.qnt`: nisse-dev's control loop

Models `nisse-dev/src/nisse_dev/control.py`: the states, the gate, pending
questions, Gitea comment cursors, publish intents, and the worker queue.
Operator messages, Gitea comments, planner/executor/publisher outcomes
(exceptions included) and **a crash at any point** all interleave freely.
Each pure function is named after the method it mirrors.

The properties are at the end of the file (`all_properties` is their
conjunction). Counterexamples are written out as short traces in
`orchestrator_scenarios.qnt`, and replayed against the real code in
`nisse-dev/tests/test_quint_counterexamples.py`.

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

# Random simulation, one property at a time:
quint run specs/orchestrator.qnt --invariant=no_stranding \
    --max-steps=40 --max-samples=200000

# The counterexample traces (each expects its property to break):
quint test specs/orchestrator_scenarios.qnt
```

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

**Keeping it true.** When `control.py` changes how a state is entered or
left, change the matching function here in the same PR. When a
counterexample's fix lands, flip its scenario's `expect` to the property
holding, and drop the `xfail` from its Python reproduction.

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

Models the design in `docs/Architecture.md` rather than code, since the new
loop doesn't exist yet:
- 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.

**Keeping it true.** When the architecture changes a rule this models, change
the model in the same PR. When the new loop is built (Development Plan Phase 2),
each property gets a test against the real code, as `orchestrator.qnt`'s did.