M2.8: switch over to the new loop
nisse-dev now runs only the conversational loop. The gated state machine it was built alongside is gone: - Removed control.py, planner.py, executor.py, approvals.py, gates.py (command_form moves to loop/reader.py), publish.py and poller.py, the old assembly in agent.py (its shared helpers move to loop/build.py), the store's state-machine view (get_state, transition), their tests, the old end-to-end and live planning/milestone/gate tests, and specs/orchestrator.qnt with its scenarios. - Roles are driver, helper, expert and classifier; driver is required. loop:, roles.planner, roles.executor and tuning.executor are refused with what to use instead; tuning.driver takes the turn cap and failure limit. - The benchmark and the capability matrix measure the driver: the loop's own system prompt and tools, the task's plan as the agreed restatement. Task plans end with finish_milestone, so earlier runs show as (old); stored runs' executor tuning reads as the driver's. - A delegation on the loop records what its helper's alias resolved to (L9), as the old path's did. - The dump shows a work item's revision and what it waits for. - Behaviour the old tests covered and the loop shares stays covered: driver runs that fail on a model call, stop mid-turn, reset the failure count; go-aheads ignoring case and punctuation; a request too big to fit is never sent; the assembly tests, now on build_loop_agent. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
This commit is contained in:
dongarandClaude Opus 5.5 committed
1 parent
09232dcbdd
commit
6ae2375194
89 files changed
+951
-8592
No files matched your search
+5
-27
@@ -6,41 +6,19 @@ 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.
|
||||
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 code, since the new
|
||||
loop doesn't exist yet:
|
||||
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;
|
||||
@@ -66,7 +44,7 @@ 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 new loop itself: a seeded random walk over
|
||||
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
|
||||
|
||||
@@ -1,488 +0,0 @@
|
||||
// A model of nisse-dev's orchestrator (nisse-dev/src/nisse_dev/control.py),
|
||||
// written to look for counterexamples: interleavings of operator messages,
|
||||
// Gitea comments, work outcomes and crashes that break a property the
|
||||
// design relies on.
|
||||
//
|
||||
// Everything lives in one record, `s`, and each handler is a pure function
|
||||
// named after the method it mirrors. The model keeps what matters for the
|
||||
// properties below and drops the rest (texts, transcripts, models, tools).
|
||||
//
|
||||
// Durable state (the state store) survives a crash; volatile state (the
|
||||
// worker queue, work in flight, pollers, the cancel flag) does not. Gitea is
|
||||
// the outside world and survives everything.
|
||||
//
|
||||
// Run: quint run specs/orchestrator.qnt --invariant=all_properties
|
||||
// quint run specs/orchestrator.qnt --invariant=<one property>
|
||||
module orchestrator {
|
||||
|
||||
// ---- bounds --------------------------------------------------------------
|
||||
|
||||
pure val MAX_MS = 2 // milestones per task
|
||||
pure val MAX_TASKS = 2 // tasks per run ('use' / 'abandon' / 'complete')
|
||||
pure val MAX_QUEUE = 3 // jobs waiting on the worker
|
||||
pure val MAX_IDS = 8 // Gitea comments per run
|
||||
|
||||
// ---- vocabulary ----------------------------------------------------------
|
||||
|
||||
pure val WORKING = Set("PLANNING_ARCH", "MILESTONE_PLANNING", "EXECUTING")
|
||||
pure val SIGNOFF = Set("AWAIT_ARCH_SIGNOFF", "AWAIT_MILESTONE_SIGNOFF")
|
||||
// Work that sets _working, so a message then gets "busy" (control._handle).
|
||||
pure val LONG_WORK = Set("plan", "exec", "review")
|
||||
|
||||
// What the operator had in front of them: the plan last put up for sign-off.
|
||||
type Plan = { g: str, rev: int }
|
||||
pure val NO_PLAN: Plan = { g: "", rev: 0 }
|
||||
|
||||
type Gate = { on: bool, g: str, rev: int, approved: bool }
|
||||
pure val NO_GATE: Gate = { on: false, g: "", rev: 0, approved: false }
|
||||
|
||||
type Pending = { kind: str, g: str, interrupted: str }
|
||||
pure val NO_PENDING: Pending = { kind: "", g: "", interrupted: "" }
|
||||
|
||||
// A message or comment waiting on the worker. `saw` is what the operator
|
||||
// had seen when they sent it; the agent never knows it, the properties do.
|
||||
type Job = { src: str, kind: str, saw: Plan, cid: int }
|
||||
|
||||
type PlanComment = { id: int, tid: int, kind: str, saw: Plan }
|
||||
type PrComment = { id: int, key: int }
|
||||
|
||||
type Watch = { on: bool, floor: int }
|
||||
pure val OFF: Watch = { on: false, floor: 0 }
|
||||
|
||||
type Sys = {
|
||||
// -- durable: the state store (control._data and the state) --
|
||||
st: str,
|
||||
tid: int, // task counter; a task's branches are its own
|
||||
task: bool, // a project is in use
|
||||
gate: Gate,
|
||||
revs: str -> int, // latest revision per gate
|
||||
lastRev: int, // revisions run across the task (L3)
|
||||
ms: int,
|
||||
pending: Pending,
|
||||
prOn: bool, prKey: int, prLast: int, // _data["pr"]
|
||||
reviewing: int, // pr["reviewing"]: the comment being answered, 0 if none
|
||||
boardOn: bool, boardPosted: bool, boardLast: int, // _data["board"]
|
||||
intents: Set[int], // pending open_pr intents, by PR key
|
||||
// -- Gitea --
|
||||
planThread: List[PlanComment],
|
||||
prThread: List[PrComment],
|
||||
nextId: int,
|
||||
giteaPr: int -> str, // PR key -> "open" / "closed"
|
||||
opened: int -> int, // PR key -> how many PRs Gitea ever opened for it
|
||||
openIssues: Set[int], // plan issues still open, by task
|
||||
// -- volatile: lost in a crash --
|
||||
queue: List[Job],
|
||||
work: str, // none / plan / exec / publish / review
|
||||
workGate: str,
|
||||
workCid: int,
|
||||
pubStage: int,
|
||||
cancel: bool,
|
||||
planWatch: Watch,
|
||||
prWatch: Watch,
|
||||
// -- the operator's view, and history the properties read --
|
||||
shown: Plan,
|
||||
taken: Set[int], // review comments the agent took up
|
||||
answered: Set[int], // ... and answered (pushed, asked, or reported)
|
||||
badApproval: bool,
|
||||
staleFeedback: bool,
|
||||
}
|
||||
|
||||
// ---- helpers ------------------------------------------------------------
|
||||
|
||||
pure def msGate(ms: int): str = if (ms == 1) "ms1" else "ms2"
|
||||
pure def prKeyOf(s: Sys): int = s.tid * 10 + s.ms
|
||||
pure def prState(s: Sys, key: int): str =
|
||||
if (s.giteaPr.keys().contains(key)) s.giteaPr.get(key) else "none"
|
||||
pure def planIds(s: Sys): int =
|
||||
s.planThread.foldl(0, (acc, c) => if (c.tid == s.tid and c.id > acc) c.id else acc)
|
||||
pure def prIds(s: Sys, key: int): int =
|
||||
s.prThread.foldl(0, (acc, c) => if (c.key == key and c.id > acc) c.id else acc)
|
||||
pure def max(a: int, b: int): int = if (a > b) a else b
|
||||
// Gitea opens a PR for a branch.
|
||||
pure def openPr(s: Sys, key: int): Sys =
|
||||
{ ...s, giteaPr: s.giteaPr.put(key, "open"),
|
||||
opened: s.opened.put(key, (if (s.opened.keys().contains(key)) s.opened.get(key) else 0) + 1) }
|
||||
|
||||
pure def queued(s: Sys, src: str): bool = s.queue.foldl(false, (acc, j) => acc or j.src == src)
|
||||
|
||||
// _await_input
|
||||
pure def awaitInput(s: Sys, p: Pending): Sys = { ...s, st: "AWAIT_INPUT", pending: p }
|
||||
|
||||
// _settled: a job that leaves a working state behind with nothing running
|
||||
// moves to AWAIT_INPUT with the restart choice.
|
||||
pure def settle(s: Sys): Sys =
|
||||
if (s.work == "none" and WORKING.contains(s.st))
|
||||
awaitInput(s, { kind: "boot", g: "", interrupted: s.st })
|
||||
else s
|
||||
|
||||
pure def endWork(s: Sys): Sys = { ...s, work: "none", workGate: "", workCid: 0, cancel: false }
|
||||
|
||||
// _run_planning_turn, first half: the turn is now in flight.
|
||||
pure def startPlanning(s: Sys, g: str): Sys =
|
||||
{ ...s, st: if (g == "arch") "PLANNING_ARCH" else "MILESTONE_PLANNING",
|
||||
work: "plan", workGate: g }
|
||||
|
||||
// _begin_project
|
||||
pure def beginProject(s: Sys, giteaUp: bool): Sys =
|
||||
val t = s.tid + 1
|
||||
startPlanning(
|
||||
{ ...s, tid: t, task: true, gate: NO_GATE,
|
||||
revs: Map("arch" -> 0, "ms1" -> 0, "ms2" -> 0), lastRev: 0, ms: 1, pending: NO_PENDING,
|
||||
prOn: false, prKey: 0, prLast: 0, reviewing: 0,
|
||||
boardOn: giteaUp, boardPosted: false, boardLast: 0,
|
||||
openIssues: if (giteaUp) s.openIssues.union(Set(t)) else s.openIssues,
|
||||
planWatch: OFF, prWatch: OFF },
|
||||
"arch")
|
||||
|
||||
// _run_planning_turn, second half: the planner submitted a plan.
|
||||
// _post_plan_to_board then watches the issue from here (a fresh watch
|
||||
// skips what is already there).
|
||||
pure def planSubmitted(s: Sys, giteaUp: bool): Sys =
|
||||
val g = s.workGate
|
||||
val rev = s.lastRev + 1
|
||||
val posted = s.boardOn and giteaUp
|
||||
val t = endWork({ ...s,
|
||||
revs: s.revs.set(g, rev), lastRev: rev,
|
||||
gate: { on: true, g: g, rev: rev, approved: false },
|
||||
st: if (g == "arch") "AWAIT_ARCH_SIGNOFF" else "AWAIT_MILESTONE_SIGNOFF",
|
||||
shown: { g: g, rev: rev } })
|
||||
if (posted)
|
||||
{ ...t, boardPosted: true, boardLast: planIds(t), planWatch: { on: true, floor: planIds(t) } }
|
||||
else t
|
||||
|
||||
// _execute_milestone: start
|
||||
pure def startExec(s: Sys): Sys = { ...s, st: "EXECUTING", work: "exec" }
|
||||
|
||||
// _apply_gate_reply and Gate.evaluate, for Matrix and Gitea alike.
|
||||
// A job's `saw` doubles as its arrival stamp: the revision up when it was
|
||||
// sent (Matrix) or the latest plan posted before it (Gitea). A reply that
|
||||
// names no revision applies only if that is the current one.
|
||||
pure def applyGate(s: Sys, j: Job): Sys =
|
||||
val current = { g: s.gate.g, rev: s.gate.rev }
|
||||
if (s.gate.approved)
|
||||
if (j.kind == "start") startExec(s) else s
|
||||
else if (j.kind == "approveRev" and j.saw.rev != s.gate.rev)
|
||||
s // names another revision: ignored with a notice
|
||||
else if (j.kind != "approveRev" and j.saw.rev != s.gate.rev)
|
||||
s // about another revision: not applied, the agent says so
|
||||
else if (j.kind == "approve" or j.kind == "approveRev")
|
||||
val s2 = { ...s, badApproval: s.badApproval or j.saw != current }
|
||||
if (s.gate.g == "arch")
|
||||
startPlanning({ ...s2, gate: NO_GATE }, msGate(s.ms))
|
||||
else
|
||||
{ ...s2, gate: { ...s.gate, approved: true }, st: "AWAIT_MILESTONE_SIGNOFF" }
|
||||
else
|
||||
// Anything else is rejection feedback, and the gate is planned again.
|
||||
startPlanning({ ...s, staleFeedback: s.staleFeedback or j.saw != current, gate: NO_GATE },
|
||||
s.gate.g)
|
||||
|
||||
// _return_to_pr_open / _watch_pr
|
||||
pure def returnToPrOpen(s: Sys): Sys =
|
||||
{ ...s, st: "PR_OPEN", prWatch: if (s.prOn) { on: true, floor: s.prLast } else OFF }
|
||||
|
||||
// _abandon: IDLE first, then close the issue and the PR, abort intents.
|
||||
pure def abandon(s: Sys): Sys =
|
||||
{ ...s, st: "IDLE", task: false, gate: NO_GATE, pending: NO_PENDING,
|
||||
prOn: false, reviewing: 0, boardOn: false, boardPosted: false, intents: Set(),
|
||||
openIssues: s.openIssues.exclude(Set(s.tid)),
|
||||
giteaPr: if (s.prOn) s.giteaPr.put(s.prKey, "closed") else s.giteaPr,
|
||||
planWatch: OFF, prWatch: OFF }
|
||||
|
||||
// _handle_pr_open: 'project complete' closes the plan issue; the PR is
|
||||
// the operator's to merge.
|
||||
pure def complete(s: Sys): Sys =
|
||||
{ ...s, st: "IDLE", task: false, gate: NO_GATE, pending: NO_PENDING,
|
||||
prOn: false, reviewing: 0, boardOn: false, boardPosted: false,
|
||||
openIssues: s.openIssues.exclude(Set(s.tid)), planWatch: OFF, prWatch: OFF }
|
||||
|
||||
// _resume_after_restart
|
||||
pure def resume(s: Sys, p: Pending, j: Job): Sys =
|
||||
if (j.kind != "continue" and j.kind != "replan")
|
||||
{ ...s, pending: p } // asked again
|
||||
else if (p.interrupted == "PR_OPEN")
|
||||
returnToPrOpen(s)
|
||||
else if (j.kind == "continue" and p.interrupted == "EXECUTING" and s.gate.approved)
|
||||
{ ...s, st: "AWAIT_MILESTONE_SIGNOFF" }
|
||||
else
|
||||
val g =
|
||||
if (p.interrupted == "PLANNING_ARCH") "arch"
|
||||
else if (p.interrupted == "MILESTONE_PLANNING" or p.interrupted == "EXECUTING") msGate(s.ms)
|
||||
else if (s.gate.g != "") s.gate.g
|
||||
else if (s.revs.get("arch") == 0) "arch"
|
||||
else msGate(s.ms)
|
||||
startPlanning({ ...s, gate: NO_GATE }, g)
|
||||
|
||||
// _handle_answer
|
||||
pure def answer(s: Sys, j: Job, giteaUp: bool): Sys =
|
||||
val p = s.pending
|
||||
val s0 = { ...s, pending: NO_PENDING }
|
||||
if (p.kind == "")
|
||||
if (j.kind == "use") beginProject({ ...s, planWatch: OFF, prWatch: OFF }, giteaUp) else s
|
||||
else if (p.kind == "question" or p.kind == "planning_failed") startPlanning(s0, p.g)
|
||||
else if (p.kind == "review_stopped") returnToPrOpen(s0)
|
||||
else if (p.kind == "milestone_stopped") { ...s0, st: "AWAIT_MILESTONE_SIGNOFF" }
|
||||
else if (p.kind == "boot") resume(s0, p, j)
|
||||
else s0
|
||||
|
||||
// _handle_now, for a Matrix message the worker has reached.
|
||||
pure def handleMatrix(s: Sys, j: Job, giteaUp: bool): Sys =
|
||||
if (j.kind == "abandon")
|
||||
if (s.st == "IDLE") s else abandon(s)
|
||||
else if (s.st == "IDLE")
|
||||
if (j.kind == "use") beginProject(s, giteaUp) else s
|
||||
else if (SIGNOFF.contains(s.st))
|
||||
if (not(s.gate.on))
|
||||
awaitInput(s, { kind: "boot", g: "",
|
||||
interrupted: if (s.st == "AWAIT_ARCH_SIGNOFF") "PLANNING_ARCH" else "MILESTONE_PLANNING" })
|
||||
else applyGate(s, j)
|
||||
else if (s.st == "PR_OPEN")
|
||||
if (j.kind == "next" and s.ms < MAX_MS)
|
||||
startPlanning({ ...s, ms: s.ms + 1, gate: NO_GATE, prOn: false, prWatch: OFF }, msGate(s.ms + 1))
|
||||
else if (j.kind == "complete") complete(s)
|
||||
else s
|
||||
else if (s.st == "AWAIT_INPUT") answer(s, j, giteaUp)
|
||||
else s // busy
|
||||
|
||||
// _handle_plan_comment_now
|
||||
pure def handlePlanComment(s: Sys, j: Job): Sys =
|
||||
if (not(SIGNOFF.contains(s.st))) s // not taken
|
||||
else applyGate({ ...s, boardLast: max(s.boardLast, j.cid) }, j)
|
||||
|
||||
// _handle_review_comment_now, first half: the executor starts on it,
|
||||
// with the comment marked (durably) until it returns.
|
||||
pure def handleReviewComment(s: Sys, j: Job): Sys =
|
||||
if (s.st != "PR_OPEN") s // not taken
|
||||
else { ...s, prLast: max(s.prLast, j.cid), taken: s.taken.union(Set(j.cid)),
|
||||
reviewing: j.cid, work: "review", workCid: j.cid }
|
||||
|
||||
pure def handleJob(s: Sys, j: Job, giteaUp: bool): Sys =
|
||||
if (j.src == "matrix") handleMatrix(s, j, giteaUp)
|
||||
else if (j.src == "plan") handlePlanComment(s, j)
|
||||
else handleReviewComment(s, j)
|
||||
|
||||
// Orchestrator.start, after a crash: reconcile intents against Gitea,
|
||||
// then resume, re-ask, or ask the restart question.
|
||||
pure def boot(s: Sys, giteaUp: bool): Sys =
|
||||
val unresolved = s.intents.size() > 0 and not(giteaUp)
|
||||
val s0 = { ...s, intents: if (giteaUp) Set() else s.intents }
|
||||
if (unresolved)
|
||||
awaitInput(s0, { kind: "boot", g: "", interrupted: s.st })
|
||||
else if (s.st == "AWAIT_INPUT" and s.pending.kind != "")
|
||||
s0
|
||||
else if (s.st == "EXECUTING" and giteaUp and prState(s, prKeyOf(s)) == "open")
|
||||
// L8 boot step 3: the milestone's PR is open, so it was published and only
|
||||
// PR_OPEN went unrecorded. Adopt it; nothing watched it, so from 0.
|
||||
{ ...s0, st: "PR_OPEN", prOn: true, prKey: prKeyOf(s), prLast: 0,
|
||||
prWatch: { on: true, floor: 0 }, planWatch: OFF }
|
||||
else if (s.st == "PR_OPEN")
|
||||
// A comment whose answer never finished is delivered again.
|
||||
{ ...s0, prWatch: if (s.prOn)
|
||||
{ on: true, floor: if (s.reviewing > 0) s.reviewing - 1 else s.prLast }
|
||||
else OFF }
|
||||
else if (s.st == "IDLE" or (SIGNOFF.contains(s.st) and s.gate.on))
|
||||
if (s.gate.on and s.boardPosted) { ...s0, planWatch: { on: true, floor: s.boardLast } } else s0
|
||||
else
|
||||
awaitInput(s0, { kind: "boot", g: "", interrupted: s.st })
|
||||
|
||||
// ---- the system ---------------------------------------------------------
|
||||
|
||||
var s: Sys
|
||||
|
||||
action init = s' = {
|
||||
st: "IDLE", tid: 0, task: false, gate: NO_GATE,
|
||||
revs: Map("arch" -> 0, "ms1" -> 0, "ms2" -> 0), lastRev: 0, ms: 1, pending: NO_PENDING,
|
||||
prOn: false, prKey: 0, prLast: 0, reviewing: 0,
|
||||
boardOn: false, boardPosted: false, boardLast: 0,
|
||||
intents: Set(),
|
||||
planThread: List(), prThread: List(), nextId: 1,
|
||||
giteaPr: Map(), opened: Map(), openIssues: Set(),
|
||||
queue: List(), work: "none", workGate: "", workCid: 0, pubStage: 0, cancel: false,
|
||||
planWatch: OFF, prWatch: OFF,
|
||||
shown: NO_PLAN, taken: Set(), answered: Set(),
|
||||
badApproval: false, staleFeedback: false,
|
||||
}
|
||||
|
||||
// Each action has a deterministic form taking its choices as parameters,
|
||||
// so scenarios (orchestrator_scenarios.qnt) can replay a trace exactly;
|
||||
// `step` picks the parameters at random.
|
||||
|
||||
pure val MATRIX_KINDS = Set("use", "approve", "approveRev", "text", "start", "next",
|
||||
"complete", "abandon", "continue", "replan", "stop")
|
||||
pure val COMMENT_KINDS = Set("approve", "approveRev", "text", "start")
|
||||
|
||||
// The operator sends a Matrix message (control._handle, on the
|
||||
// transport's thread). While long work runs it only gets "busy"; `stop`
|
||||
// reaches the cancel flag whenever the worker is busy.
|
||||
action send(kind: str): bool = all {
|
||||
s.tid < MAX_TASKS or kind != "use",
|
||||
if (kind == "stop")
|
||||
s' = { ...s, cancel: s.cancel or s.work != "none" }
|
||||
else if (LONG_WORK.contains(s.work))
|
||||
s' = s
|
||||
else all {
|
||||
s.queue.length() < MAX_QUEUE,
|
||||
s' = { ...s, queue: s.queue.append({ src: "matrix", kind: kind, saw: s.shown, cid: 0 }) },
|
||||
},
|
||||
}
|
||||
|
||||
// The operator comments on the plan issue.
|
||||
action commentPlan(kind: str): bool = all {
|
||||
s.task, s.openIssues.contains(s.tid), s.nextId <= MAX_IDS,
|
||||
s' = { ...s, nextId: s.nextId + 1,
|
||||
planThread: s.planThread.append({ id: s.nextId, tid: s.tid, kind: kind, saw: s.shown }) },
|
||||
}
|
||||
|
||||
// The operator comments on the open PR.
|
||||
action commentPr: bool = all {
|
||||
s.prOn, s.nextId <= MAX_IDS, prState(s, s.prKey) == "open",
|
||||
s' = { ...s, nextId: s.nextId + 1, prThread: s.prThread.append({ id: s.nextId, key: s.prKey }) },
|
||||
}
|
||||
|
||||
// A poller delivers the next new comment (CommentPoller.poll_once). It
|
||||
// waits on the worker, so one job per poller at a time.
|
||||
action pollPlan: bool = {
|
||||
val c = s.planThread.foldl({ id: 0, tid: 0, kind: "", saw: NO_PLAN },
|
||||
(acc, x) => if (x.tid == s.tid and x.id > s.planWatch.floor and (acc.id == 0 or x.id < acc.id)) x else acc)
|
||||
all {
|
||||
s.planWatch.on, c.id > 0, not(queued(s, "plan")), s.queue.length() < MAX_QUEUE,
|
||||
s' = { ...s, planWatch: { on: true, floor: c.id },
|
||||
queue: s.queue.append({ src: "plan", kind: c.kind, saw: c.saw, cid: c.id }) },
|
||||
}
|
||||
}
|
||||
|
||||
action pollPr: bool = {
|
||||
val c = s.prThread.foldl({ id: 0, key: 0 },
|
||||
(acc, x) => if (x.key == s.prKey and x.id > s.prWatch.floor and (acc.id == 0 or x.id < acc.id)) x else acc)
|
||||
all {
|
||||
s.prWatch.on, c.id > 0, not(queued(s, "pr")), s.queue.length() < MAX_QUEUE,
|
||||
s' = { ...s, prWatch: { on: true, floor: c.id },
|
||||
queue: s.queue.append({ src: "pr", kind: "review", saw: NO_PLAN, cid: c.id }) },
|
||||
}
|
||||
}
|
||||
|
||||
// The worker takes the next job, one at a time, and settles it.
|
||||
action runJob(giteaUp: bool): bool = all {
|
||||
s.work == "none", s.queue.length() > 0,
|
||||
s' = settle(handleJob({ ...s, queue: s.queue.tail() }, s.queue.head(), giteaUp)),
|
||||
}
|
||||
|
||||
// A planning turn ends.
|
||||
action finishPlanning(outcome: str, giteaUp: bool): bool = all {
|
||||
s.work == "plan", outcome != "stopped" or s.cancel,
|
||||
s' =
|
||||
if (outcome == "submit") planSubmitted(s, giteaUp)
|
||||
else if (outcome == "ask" or outcome == "stopped")
|
||||
awaitInput(endWork(s), { kind: "question", g: s.workGate, interrupted: "" })
|
||||
else if (outcome == "error")
|
||||
awaitInput(endWork(s), { kind: "planning_failed", g: s.workGate, interrupted: "" })
|
||||
else settle(endWork(s)),
|
||||
}
|
||||
|
||||
// The executor finishes a milestone.
|
||||
action finishExec(outcome: str): bool = all {
|
||||
s.work == "exec", outcome != "stopped" or s.cancel,
|
||||
s' =
|
||||
if (outcome == "completed") { ...s, work: "publish", pubStage: 0, cancel: false }
|
||||
else if (outcome == "exception") settle(endWork(s))
|
||||
else awaitInput(endWork(s), { kind: "milestone_stopped", g: "", interrupted: "" }),
|
||||
}
|
||||
|
||||
// Publishing, one step at a time, so a crash can land between them
|
||||
// (MilestonePublisher.publish and control._publish_milestone):
|
||||
// 0 commit, begin_intent; 1 push, then adopt an open PR for the branch or
|
||||
// open one ("lost": Gitea opened it but the response never came back);
|
||||
// 2 commit_intent; 3 record the PR, watch it, PR_OPEN.
|
||||
action publishStep(outcome: str): bool = {
|
||||
val key = prKeyOf(s)
|
||||
all {
|
||||
s.work == "publish",
|
||||
s' =
|
||||
if (s.pubStage == 0)
|
||||
if (outcome == "nochanges" or outcome == "fail")
|
||||
awaitInput(endWork(s), { kind: "milestone_stopped", g: "", interrupted: "" })
|
||||
else if (outcome == "exception") settle(endWork(s))
|
||||
else { ...s, intents: s.intents.union(Set(key)), pubStage: 1 }
|
||||
else if (s.pubStage == 1)
|
||||
if (outcome == "exception") settle(endWork(s))
|
||||
else if (outcome == "fail" or outcome == "nochanges")
|
||||
awaitInput(endWork(s), { kind: "milestone_stopped", g: "", interrupted: "" })
|
||||
else if (prState(s, key) == "open")
|
||||
{ ...s, pubStage: 2 } // adopted, never a second
|
||||
else if (outcome == "lost")
|
||||
awaitInput(endWork(openPr(s, key)),
|
||||
{ kind: "milestone_stopped", g: "", interrupted: "" })
|
||||
else { ...openPr(s, key), pubStage: 2 }
|
||||
else if (s.pubStage == 2)
|
||||
{ ...s, intents: s.intents.exclude(Set(key)), pubStage: 3 }
|
||||
else
|
||||
endWork({ ...s, prOn: true, prKey: key, prLast: prIds(s, key),
|
||||
prWatch: { on: true, floor: prIds(s, key) }, planWatch: OFF,
|
||||
st: "PR_OPEN" }),
|
||||
}
|
||||
}
|
||||
|
||||
// The executor finishes responding to a review comment.
|
||||
action finishReview(outcome: str): bool = all {
|
||||
s.work == "review", outcome != "stopped" or s.cancel,
|
||||
s' =
|
||||
val t = endWork({ ...s, answered: s.answered.union(Set(s.workCid)), reviewing: 0 })
|
||||
if (outcome == "stopped" or outcome == "escalate")
|
||||
awaitInput(t, { kind: "review_stopped", g: "", interrupted: "" })
|
||||
else t,
|
||||
}
|
||||
|
||||
// The process dies and starts again: volatile state is gone.
|
||||
action crash(giteaUp: bool): bool =
|
||||
s' = boot({ ...s, queue: List(), work: "none", workGate: "", workCid: 0, pubStage: 0,
|
||||
cancel: false, planWatch: OFF, prWatch: OFF }, giteaUp)
|
||||
|
||||
action step = {
|
||||
nondet kind = MATRIX_KINDS.oneOf()
|
||||
nondet ckind = COMMENT_KINDS.oneOf()
|
||||
nondet up = Set(true, false).oneOf()
|
||||
nondet planOutcome = Set("submit", "ask", "error", "stopped", "exception").oneOf()
|
||||
nondet workOutcome = Set("completed", "stopped", "escalate", "exception").oneOf()
|
||||
nondet pubOutcome = Set("ok", "nochanges", "fail", "lost", "exception").oneOf()
|
||||
any {
|
||||
send(kind), commentPlan(ckind), commentPr, pollPlan, pollPr, runJob(up),
|
||||
finishPlanning(planOutcome, up), finishExec(workOutcome), publishStep(pubOutcome),
|
||||
finishReview(workOutcome), crash(up),
|
||||
}
|
||||
}
|
||||
|
||||
// ---- properties ---------------------------------------------------------
|
||||
|
||||
// #66: a working state only while its work is running.
|
||||
val no_stranding = WORKING.contains(s.st) implies s.work != "none"
|
||||
|
||||
// Waiting on the operator always means a question to answer.
|
||||
val await_input_has_a_question = s.st == "AWAIT_INPUT" implies s.pending.kind != ""
|
||||
|
||||
// A milestone runs only on an approved plan for that milestone.
|
||||
val execution_needs_approval =
|
||||
s.st == "EXECUTING" implies (s.gate.on and s.gate.approved and s.gate.g == msGate(s.ms))
|
||||
|
||||
// An approval only ever approves the plan the operator was looking at.
|
||||
val approval_only_of_what_was_seen = not(s.badApproval)
|
||||
|
||||
// Rejection feedback only ever lands on the plan it was written about.
|
||||
val feedback_only_on_what_was_seen = not(s.staleFeedback)
|
||||
|
||||
// Never more than one PR opened for a milestone.
|
||||
val one_pr_per_milestone = s.opened.keys().forall(k => s.opened.get(k) <= 1)
|
||||
|
||||
// A review comment the agent took up is answered, being worked on, or
|
||||
// marked to be delivered again: never silently dropped.
|
||||
val review_comments_answered =
|
||||
s.taken.forall(id => s.answered.contains(id) or (s.work == "review" and s.workCid == id)
|
||||
or s.reviewing == id)
|
||||
|
||||
// With no task, no plan issue is left open.
|
||||
val no_open_issue_without_a_task = not(s.task) implies s.openIssues.size() == 0
|
||||
|
||||
val all_properties = and {
|
||||
no_stranding, await_input_has_a_question, execution_needs_approval,
|
||||
approval_only_of_what_was_seen, feedback_only_on_what_was_seen,
|
||||
one_pr_per_milestone, review_comments_answered, no_open_issue_without_a_task,
|
||||
}
|
||||
}
|
||||
@@ -1,125 +0,0 @@
|
||||
// Counterexamples found in orchestrator.qnt, written out as short traces.
|
||||
// Each ends by expecting the property it breaks to be false; once the design
|
||||
// is fixed, the expectation is flipped and the trace kept as a regression.
|
||||
// All fixed: 1-4 (replies bind to the revision up when they arrived), 5 (boot
|
||||
// and publishing adopt an open PR), 6 (redelivered), 7 (issue closed).
|
||||
//
|
||||
// Run: quint test specs/orchestrator_scenarios.qnt (runs every *Test)
|
||||
module orchestrator_scenarios {
|
||||
import orchestrator.* from "./orchestrator"
|
||||
|
||||
// Architecture plan rev-1 is up for sign-off, posted to Gitea.
|
||||
action toArchSignoff = init
|
||||
.then(send("use")).then(runJob(true))
|
||||
.then(finishPlanning("submit", true))
|
||||
|
||||
// The milestone plan is approved; the next word starts it.
|
||||
action toMilestoneApproved = toArchSignoff
|
||||
.then(send("approve")).then(runJob(true))
|
||||
.then(finishPlanning("submit", true))
|
||||
.then(send("approve")).then(runJob(true))
|
||||
|
||||
action toPrOpen = toMilestoneApproved
|
||||
.then(send("start")).then(runJob(true))
|
||||
.then(finishExec("completed"))
|
||||
.then(publishStep("ok")).then(publishStep("ok"))
|
||||
.then(publishStep("ok")).then(publishStep("ok"))
|
||||
|
||||
// 1. The operator sends "approve" twice, say a double tap or an impatient
|
||||
// repeat, while looking at the architecture plan. Both are queued
|
||||
// before either runs. The first approves the architecture; planning
|
||||
// the milestone runs; the second then approved the milestone plan,
|
||||
// which the operator had not seen. Fixed: it is about rev-1, not
|
||||
// applied.
|
||||
run doubleApproveApprovesAnUnseenPlanTest =
|
||||
toArchSignoff
|
||||
.then(send("approve")).then(send("approve"))
|
||||
.then(runJob(true)) // approves arch rev-1
|
||||
.then(finishPlanning("submit", true)) // milestone-1 rev-1 is up
|
||||
.then(runJob(true)) // the second "approve"
|
||||
.expect(s.gate.g == "ms1" and not(s.gate.approved) and approval_only_of_what_was_seen)
|
||||
|
||||
// 2. The same with the revision named: "approve rev-1" meant for the
|
||||
// architecture's rev-1 also matched the milestone's rev-1, because
|
||||
// revisions were numbered per gate. Fixed: numbered across the task,
|
||||
// the milestone plan is rev-2.
|
||||
run namedRevisionApprovesTheWrongGateTest =
|
||||
toArchSignoff
|
||||
.then(send("approve")).then(send("approveRev"))
|
||||
.then(runJob(true))
|
||||
.then(finishPlanning("submit", true))
|
||||
.then(runJob(true))
|
||||
.expect(s.gate.rev == 2 and not(s.gate.approved) and approval_only_of_what_was_seen)
|
||||
|
||||
// 3. Approval on both channels: the operator approves in Matrix and on
|
||||
// the Gitea issue. The Gitea approval is delivered and queued behind
|
||||
// the Matrix one, which approves the architecture and posts the
|
||||
// milestone plan. Re-attaching the plan watch does not recall a job
|
||||
// already queued, so the Gitea approval approved the milestone plan.
|
||||
// Fixed: it is about the plan posted before it, arch rev-1.
|
||||
run approvalOnBothChannelsApprovesTheNextPlanTest =
|
||||
toArchSignoff
|
||||
.then(send("approve")).then(commentPlan("approve")).then(pollPlan)
|
||||
.then(runJob(true))
|
||||
.then(finishPlanning("submit", true))
|
||||
.then(runJob(true))
|
||||
.expect(s.gate.g == "ms1" and not(s.gate.approved) and approval_only_of_what_was_seen)
|
||||
|
||||
// 4. An afterthought becomes a rejection: "approve", then "also, keep it
|
||||
// in one file", sent together. The note landed on the milestone plan
|
||||
// as rejection feedback and it was planned again. Fixed: recorded,
|
||||
// but it rejects nothing.
|
||||
run anAfterthoughtRejectsTheNextPlanTest =
|
||||
toArchSignoff
|
||||
.then(send("approve")).then(send("text"))
|
||||
.then(runJob(true))
|
||||
.then(finishPlanning("submit", true))
|
||||
.then(runJob(true))
|
||||
.expect(s.st == "AWAIT_MILESTONE_SIGNOFF" and feedback_only_on_what_was_seen)
|
||||
|
||||
// 5. A crash after the PR is opened but before PR_OPEN is recorded.
|
||||
// Boot found the intent's PR and marked it done, but the state still
|
||||
// said EXECUTING, so it asked the restart question; 'continue' and
|
||||
// 'start' then published again, which Gitea refused, with no path back
|
||||
// to PR_OPEN. Fixed: boot sees the open PR and adopts it.
|
||||
run crashAfterOpeningThePrPublishesAgainTest =
|
||||
toMilestoneApproved
|
||||
.then(send("start")).then(runJob(true))
|
||||
.then(finishExec("completed"))
|
||||
.then(publishStep("ok")) // begin_intent
|
||||
.then(publishStep("ok")) // push, open the PR
|
||||
.then(crash(true)) // adopted on boot
|
||||
.expect(s.st == "PR_OPEN" and s.prOn and one_pr_per_milestone)
|
||||
|
||||
// 5b. Gitea opens the PR but the response is lost; the operator starts
|
||||
// the milestone again. Publishing adopts the open PR.
|
||||
run lostResponseThenRetryAdoptsThePrTest =
|
||||
toMilestoneApproved
|
||||
.then(send("start")).then(runJob(true))
|
||||
.then(finishExec("completed"))
|
||||
.then(publishStep("ok")).then(publishStep("lost"))
|
||||
.then(send("continue")).then(runJob(true)) // back to the approved plan
|
||||
.then(send("start")).then(runJob(true))
|
||||
.then(finishExec("completed"))
|
||||
.then(publishStep("ok")).then(publishStep("ok"))
|
||||
.then(publishStep("ok")).then(publishStep("ok"))
|
||||
.expect(s.st == "PR_OPEN" and one_pr_per_milestone)
|
||||
|
||||
// 6. A crash while the executor answers a review comment. The comment's
|
||||
// cursor was saved before the work started (at most once), and a
|
||||
// restart in PR_OPEN resumed quietly, so it was never answered. Fixed:
|
||||
// the comment is marked while answered, and delivered again.
|
||||
run crashDuringAReviewLosesTheCommentTest =
|
||||
toPrOpen
|
||||
.then(commentPr).then(pollPr).then(runJob(true)) // the executor starts on it
|
||||
.then(crash(true))
|
||||
.expect(s.st == "PR_OPEN" and review_comments_answered)
|
||||
.then(pollPr).then(runJob(true)).then(finishReview("completed"))
|
||||
.expect(s.answered.size() == 1 and s.reviewing == 0)
|
||||
|
||||
// 7. 'project complete' left the plan issue open. Fixed: it closes it.
|
||||
run projectCompleteLeavesThePlanIssueOpenTest =
|
||||
toPrOpen
|
||||
.then(send("complete")).then(runJob(true))
|
||||
.expect(s.st == "IDLE" and no_open_issue_without_a_task)
|
||||
}
|
||||
Reference in new issue
Block a user