dongarandClaude Opus 5.5
d79e399933
CI / checks (push) Skipped
CI / checks (pull_request) Successful in 1m14s
specs/orchestrator.qnt models control.py: states, gate, pending
questions, comment cursors, publish intents and the worker queue, with
operator messages, Gitea comments, work outcomes (exceptions included)
and a crash at any point interleaving freely. Eight properties.
Seven counterexamples, each written out as a trace in
specs/orchestrator_scenarios.qnt and reproduced against the real code in
nisse-dev/tests/test_quint_counterexamples.py (xfail, strict, until
fixed):
1-4 an approval or feedback lands on a plan the operator had not seen:
a double 'approve', 'approve rev-1' meant for the architecture,
approving on both channels, and 'approve' plus an afterthought;
5 a crash after the PR opens but before PR_OPEN publishes again and
cannot get back to PR_OPEN;
6 a crash while answering a review comment loses it silently;
7 'project complete' leaves the plan issue open.
no_stranding, await_input_has_a_question and execution_needs_approval
held over 200,000 random traces of 40 steps, and under Apalache's
exhaustive check to depth 8, which does find counterexample 1 at that
depth. No behaviour changes here.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
39 lines
1.7 KiB
Markdown
39 lines
1.7 KiB
Markdown
# 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.
|