dongarandClaude Opus 5.5
8bd1ac0fa2
Fixes counterexample 5 from specs/orchestrator.qnt. A crash after the PR was opened but before PR_OPEN was recorded left the agent in EXECUTING; the restart question's 'continue' and 'start' then published again, Gitea refused a second PR, and there was no way back to PR_OPEN. On the live run the executor model happened to notice the existing work; recovery must not depend on that. - Boot (A3 step 4): in EXECUTING, if Gitea shows the milestone's PR open, adopt it, watch it from the start, and resume in PR_OPEN with a notice. Gitea unreachable or the PR closed: the restart question, as before. - MilestonePublisher.publish is idempotent: after pushing, an open PR for the branch is adopted (and so updated) rather than a second one opened. This also covers a PR opened whose response was lost. - The model adopts too, gains the lost-response outcome, and now counts PRs opened per milestone (one_pr_per_milestone was a flag the fixed model could never set). A mutant without adoption fails the new scenario; the properties held over 200,000 traces each. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
Formal models
Quint 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.
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.