docs/Architecture-Build-Spec.md

@@ -322,13 +322,24 @@ Requirements:
   against a per-channel operator allowlist (Matrix MXID, Gitea username, Vikunja
   username).
 - **Approvals bind to a plan revision, never to "the current gate."** Every submitted
-  plan revision carries a monotonically-increasing tag (`rev-N`). An approval naming
-  a stale revision is rejected with a notice, never applied to a newer one — this is
-  what makes multi-channel approval race-free.
+  plan revision carries a monotonically-increasing tag (`rev-N`), numbered across
+  the whole work item rather than per gate, so a tag names exactly one plan. An
+  approval naming a stale revision is rejected with a notice, never applied to a
+  newer one — this is what makes multi-channel approval race-free.
+- **A reply that names no revision is about the one up when it arrived.** A bare
+  `approve`, or any feedback, is stamped on arrival with the revision last put up
+  for sign-off: in Matrix, the one whose approval request had been sent; in Gitea,
+  the latest plan comment older than the reply. If that is not the current
+  revision the reply is ambiguous: an approval is not applied, feedback is recorded
+  in the transcript but rejects nothing, and the agent says which revision is up.
+  So a repeated `approve`, an approval given on both channels, or an afterthought
+  sent while one plan was up can never land on the next. (Found by the Quint model,
+  `specs/orchestrator.qnt`.)
 - **One consistent approval UI across all channels.** Approval is always the typed
   word `approve`, attached to a specific revision: in Matrix, a reply to the plan
   message (the reply relation carries the binding; a bare `approve` in the room binds
-  to the latest revision only when unambiguous, otherwise the agent asks); in Gitea
+  to the latest revision only when unambiguous, in the sense above, otherwise the
+  agent asks; reply relations are not implemented yet); in Gitea
   and Vikunja, a comment `approve rev-N`, with the tag printed in the plan comment
   for copy-paste. Any other reply/comment is `reject <feedback>`. Reactions/emoji are
   never an approval path. Approvals are consumed at first sight; later edits to an

nisse-dev/src/nisse_dev/control.py

@@ -172,6 +172,16 @@ class StubAgent:
         return SubmitPlan(f"[stub] {gate} plan for {project}{notes}")
 
 
+def _rev_before(board_state: dict[str, Any] | None, comment_id: int) -> int | None:
+    """The revision a Gitea comment was about: the latest plan posted before
+    it. None for a record kept before plan posts were."""
+    posts = (board_state or {}).get("posts")
+    if posts is None:
+        return None
+    earlier = [int(rev) for cid, rev in posts if int(cid) < comment_id]
+    return max(earlier) if earlier else 0
+
+
 def _project_name(text: str) -> str:
     """The name in 'use <name>', as written: only the command word is
     case-insensitive."""
@@ -180,7 +190,13 @@ def _project_name(text: str) -> str:
 
 def _fresh_data() -> dict[str, Any]:
     return {
+        # Latest revision per gate; revision numbers themselves run across
+        # the whole work item (last_rev), so rev-N names one plan (A4).
         "revs": {},
+        "last_rev": 0,
+        # The revision last put up for sign-off: a reply that names none
+        # binds to the one up when it arrived.
+        "shown_rev": 0,
         "gate": None,
         # What an operator reply in AWAIT_INPUT should resume. Every path into
         # AWAIT_INPUT must set this, or the reply has nowhere to go.
@@ -248,6 +264,8 @@ class Orchestrator:
         # long work is running, and the state name for a "busy" reply.
         self._working = False
         self._state_name = IDLE
+        # The revision up for sign-off, stamped on each message as it arrives.
+        self._shown_rev = 0
         # Set by whichever path halted because of a stop, so the stop's own
         # job knows whether it stopped anything.
         self._halted_by_stop = False
@@ -279,6 +297,13 @@ class Orchestrator:
         self._project = state.project
         self._store.oplog.task_id = self._data.get("task_id")
         gate = self._data.get("gate")
+        # An open gate is announced again below, so its plan counts as up.
+        self._shown_rev = max(
+            int(self._data.get("shown_rev") or 0),
+            int(gate["rev"])
+            if gate and state.state in (AWAIT_ARCH_SIGNOFF, AWAIT_MILESTONE_SIGNOFF)
+            else 0,
+        )
         if report.action == "await_input":
             self._await_input(
                 cause="boot: unresolved intents",
@@ -359,8 +384,11 @@ class Orchestrator:
             )
             self._worker.submit(lambda: self._record(msg))
             return
+        # Stamped here, on arrival: by the time the worker reaches it, the
+        # plan it was about may have been replaced.
+        about = self._shown_rev
         self._worker.submit(
-            lambda: self._settled("your message", lambda: self._handle_now(msg))
+            lambda: self._settled("your message", lambda: self._handle_now(msg, about))
         )
 
     def _settled(self, what: str, job: Callable[[], None]) -> None:
@@ -434,7 +462,7 @@ class Orchestrator:
             pending=pending,
         )
 
-    def _handle_now(self, msg: InboundMessage) -> None:
+    def _handle_now(self, msg: InboundMessage, about: int | None = None) -> None:
         # Every operator message enters the canonical transcript, so planning
         # turns see feedback and answers as conversation rather than as
         # out-of-band parameters (A10).
@@ -479,7 +507,7 @@ class Orchestrator:
                     },
                 )
                 return
-            self._handle_gate_reply(msg, text)
+            self._handle_gate_reply(msg, text, about)
         elif current == PR_OPEN:
             self._handle_pr_open(text)
         elif current == AWAIT_INPUT:
@@ -563,7 +591,8 @@ class Orchestrator:
                 pending={"kind": "question", "gate": gate_name},
             )
             return
-        rev = self._data["revs"].get(gate_name, 0) + 1
+        rev = int(self._data.get("last_rev") or 0) + 1
+        self._data["last_rev"] = rev
         self._data["revs"][gate_name] = rev
         self._data["gate"] = {
             "name": gate_name,
@@ -583,9 +612,12 @@ class Orchestrator:
         )
         self._transition(await_state, cause=f"plan submitted ({gate_name} rev-{rev})")
         self._transport.send_approval_request(
-            f"{action.content}\n\nreply 'approve' to approve rev-{rev}; "
+            f"{action.content}\n\nreply 'approve' to approve {gate_name} rev-{rev}; "
             "any other reply is rejection feedback"
         )
+        # Up only once sent: a reply that arrived before was about another.
+        self._data["shown_rev"] = rev
+        self._shown_rev = rev
         self._post_plan_to_board(gate_name, rev, action.content)
         self._store.oplog.emit(
             "gate.open",
@@ -595,10 +627,16 @@ class Orchestrator:
             channel="transport",
         )
 
-    def _handle_gate_reply(self, msg: InboundMessage, text: str) -> None:
-        self._apply_gate_reply(sender=msg.sender, text=text, channel="transport")
+    def _handle_gate_reply(
+        self, msg: InboundMessage, text: str, about: int | None
+    ) -> None:
+        self._apply_gate_reply(
+            sender=msg.sender, text=text, channel="transport", about=about
+        )
 
-    def _apply_gate_reply(self, *, sender: str, text: str, channel: str) -> None:
+    def _apply_gate_reply(
+        self, *, sender: str, text: str, channel: str, about: int | None = None
+    ) -> None:
         """Shared by every approval source (A4). The allowlist is per channel:
         a Matrix MXID and a Gitea login are different names, and holding one
         says nothing about holding the other."""
@@ -618,7 +656,9 @@ class Orchestrator:
             return
         revision = PlanRevision(gate=name, rev=rev, content=gate_data["plan"])
         allowlist = self._operators if channel == "transport" else self._gitea_operators
-        result = Gate(revision, allowlist).evaluate(sender, text, channel=channel)
+        result = Gate(revision, allowlist).evaluate(
+            sender, text, channel=channel, about=about
+        )
         if isinstance(result, Ignored):
             if result.notice:
                 self._transport.send_message(result.notice)
@@ -720,6 +760,9 @@ class Orchestrator:
             # durability of the record, not the ability to approve.
             return
         board_state["comment_id"] = post.comment_id
+        # Which comment put which revision up: a Gitea reply binds to the
+        # latest plan posted before it, since comment IDs only grow.
+        board_state.setdefault("posts", []).append([post.comment_id, rev])
         # Approvals can arrive on the issue as well as over transport (A4),
         # so watch it for as long as the gate stands. A new revision skips
         # what came before it: an early "approve" must not approve it.
@@ -758,7 +801,10 @@ class Orchestrator:
             UserMessage(text=comment.body, source=f"gitea:comment:{comment.id}")
         )
         self._apply_gate_reply(
-            sender=comment.author, text=comment.body.strip(), channel="gitea"
+            sender=comment.author,
+            text=comment.body.strip(),
+            channel="gitea",
+            about=_rev_before(board_state, comment.id),
         )
 
     def handle_review_comment(self, comment: Any) -> None:
@@ -1131,3 +1177,4 @@ class Orchestrator:
             new_state, cause=cause, project=self._project, data=self._data
         )
         self._state_name = new_state
+        self._shown_rev = int(self._data.get("shown_rev") or 0)

nisse-dev/src/nisse_dev/gates.py

@@ -7,6 +7,13 @@ approval wins. Approval is always the typed word ``approve`` (optionally
 ``approve rev-N``); any other reply is a rejection with feedback. The approver
 is authenticated against a per-channel operator allowlist.
 
+Revisions are numbered across a whole work item, not per gate, so ``rev-N``
+names one plan. A reply that does not name a revision binds to the one that
+was up when it arrived (its ``about``): if that is not the current revision,
+it is ambiguous and not applied, neither as an approval nor as feedback. That
+is how a second "approve", or an afterthought, sent while one plan was up can
+never land on the next.
+
 The channel seam: any approval source (Matrix transport, Gitea comment poller,
 Vikunja comments) feeds operator replies to ``Gate.evaluate`` with its channel
 name.
@@ -64,15 +71,34 @@ class Gate:
         self._operators = operators
 
     def evaluate(
-        self, sender: str, text: str, channel: str
+        self, sender: str, text: str, channel: str, about: int | None = None
     ) -> Approved | Rejected | Ignored:
+        """`about` is the revision that was up when the reply arrived; None
+        only for records kept before replies were stamped."""
         if sender not in self._operators:
             return Ignored(notice=None)
         text = text.strip()
         match = _APPROVE_RE.match(command_form(text))
+        named = match.group(1) if match else None
+        current = self._revision
+        if named is None and about is not None and about != current.rev:
+            was = f"rev-{about}" if about else "no plan"
+            if match is None:
+                return Ignored(
+                    notice=(
+                        f"noted, but it arrived while {was} was up, so it is not "
+                        f"taken as feedback on {current.gate} {current.tag}"
+                    )
+                )
+            return Ignored(
+                notice=(
+                    f"that approval arrived while {was} was up; the current plan is "
+                    f"{current.gate} {current.tag}, not applied. Reply again to "
+                    "approve it"
+                )
+            )
         if match is None:
             return Rejected(feedback=text, approver=sender, channel=channel)
-        named = match.group(1)
         if named is not None and named != self._revision.tag:
             return Ignored(
                 notice=(

nisse-dev/tests/test_approval_binding.py

@@ -0,0 +1,147 @@
+"""Approvals and feedback bind to the plan revision they were about (A4)."""
+
+import io
+from pathlib import Path
+
+from nisse_dev.canonical import UserMessage
+from nisse_dev.control import (
+    AWAIT_MILESTONE_SIGNOFF,
+    Orchestrator,
+    StubAgent,
+)
+from nisse_dev.gitea import Comment
+from nisse_dev.oplog import OpLog
+from nisse_dev.state import StateStore
+from nisse_dev.transport import InMemoryTransport
+
+
+class Held:
+    """A worker that queues jobs until released, like one under load."""
+
+    def __init__(self) -> None:
+        self.jobs: list = []
+        self.busy = False
+
+    def submit(self, job) -> None:
+        self.jobs.append(job)
+
+    def call(self, job, timeout=None):
+        return job()
+
+    def run(self) -> None:
+        while self.jobs:
+            self.jobs.pop(0)()
+
+
+class Board:
+    def __init__(self) -> None:
+        self.next_id = 100
+
+    def open_project_issue(self, project: str, task_id: str) -> int:
+        return 10
+
+    def post_plan(self, issue: int, gate: str, rev: int, plan: str):
+        self.next_id += 1
+
+        class Posted:
+            comment_id = self.next_id
+
+        return Posted()
+
+    def echo(self, issue: int, text: str) -> None:
+        pass
+
+
+def build(tmp_path: Path, worker: Held | None = None, board: Board | None = None):
+    store = StateStore(tmp_path / "state.db", oplog=OpLog("nisse-dev", io.StringIO()))
+    transport = InMemoryTransport()
+    orch = Orchestrator(
+        store,
+        transport,
+        StubAgent(),
+        operators={"don"},
+        gitea_operators={"don"},
+        board=board,
+        **({"worker": worker} if worker else {}),
+    )
+    orch.start()
+    return store, transport, orch
+
+
+def gate(store: StateStore) -> dict:
+    return store.get_state().data.get("gate") or {}
+
+
+def test_revisions_run_across_the_task(tmp_path: Path) -> None:
+    store, transport, _ = build(tmp_path)
+    transport.receive("don", "use demo")
+    assert gate(store)["rev"] == 1
+    transport.receive("don", "approve")
+    assert gate(store) == {**gate(store), "name": "milestone-1", "rev": 2}
+    assert "milestone-1 rev-2" in transport.outbound[-1].text
+
+
+def test_a_stale_approval_is_answered_and_a_fresh_one_works(tmp_path: Path) -> None:
+    worker = Held()
+    store, transport, _ = build(tmp_path, worker)
+    transport.receive("don", "use demo")
+    worker.run()
+    transport.receive("don", "approve")
+    transport.receive("don", "approve")  # both while arch rev-1 was up
+    worker.run()
+    assert store.get_state().state == AWAIT_MILESTONE_SIGNOFF
+    assert not gate(store)["approved"]
+    assert "arrived while rev-1 was up" in transport.outbound[-1].text
+    transport.receive("don", "approve")  # now about milestone-1 rev-2
+    worker.run()
+    assert gate(store)["approved"]
+
+
+def test_stale_feedback_is_recorded_but_rejects_nothing(tmp_path: Path) -> None:
+    worker = Held()
+    store, transport, _ = build(tmp_path, worker)
+    transport.receive("don", "use demo")
+    worker.run()
+    transport.receive("don", "approve")
+    transport.receive("don", "also, keep it in one file")
+    worker.run()
+    assert store.get_state().state == AWAIT_MILESTONE_SIGNOFF
+    assert gate(store)["rev"] == 2
+    assert "not taken as feedback" in transport.outbound[-1].text
+    said = [
+        e.event.text for e in store.read_events() if isinstance(e.event, UserMessage)
+    ]
+    assert "also, keep it in one file" in said  # the planner still hears it
+
+
+def test_a_gitea_reply_binds_to_the_latest_plan_posted_before_it(
+    tmp_path: Path,
+) -> None:
+    board = Board()
+    store, transport, orch = build(tmp_path, board=board)
+    transport.receive("don", "use demo")  # arch rev-1 posted as comment 101
+    orch._handle_plan_comment_now(
+        Comment(id=102, author="don", body="approve", created_at="t")
+    )
+    # Approved arch rev-1; milestone-1 rev-2 is now posted as comment 103.
+    assert gate(store) == {**gate(store), "name": "milestone-1", "approved": False}
+    # A reply older than that post was about arch rev-1: not applied.
+    orch._handle_plan_comment_now(
+        Comment(id=102, author="don", body="approve", created_at="t")
+    )
+    assert not gate(store)["approved"]
+    # One after it is about milestone-1 rev-2.
+    orch._handle_plan_comment_now(
+        Comment(id=104, author="don", body="approve", created_at="t")
+    )
+    assert gate(store)["approved"]
+
+
+def test_the_plan_up_survives_a_restart(tmp_path: Path) -> None:
+    _, transport, _ = build(tmp_path)
+    transport.receive("don", "use demo")  # arch rev-1 up; no board, so unsaved
+    store, transport, _ = build(tmp_path)  # restart at the open gate
+    transport.receive("don", "approve")  # stamped with the restored rev-1
+    assert store.get_state().state == AWAIT_MILESTONE_SIGNOFF
+    assert gate(store)["name"] == "milestone-1"
+    assert gate(store)["rev"] == 2

nisse-dev/tests/test_control.py

@@ -128,7 +128,9 @@ def test_start_milestone_requires_approval_first(h: Harness) -> None:
     h.transport.receive("don", "approve")
     h.transport.receive("don", "start milestone 1")
     assert h.state == AWAIT_MILESTONE_SIGNOFF  # it was rejection feedback
-    h.transport.receive("don", "approve rev-2")
+    # Revisions run across the task: arch rev-1, milestone-1 rev-2, and
+    # after that rejection milestone-1 rev-3.
+    h.transport.receive("don", "approve rev-3")
     h.transport.receive("don", "start milestone 1")
     assert executed(h)
 

nisse-dev/tests/test_gates.py

@@ -67,3 +67,39 @@ def test_a_sentence_containing_approve_is_still_feedback() -> None:
     result = gate().evaluate("don", "I approve of most of it", channel="transport")
     assert isinstance(result, Rejected)
     assert result.feedback == "I approve of most of it"
+
+
+# --- binding by arrival (A4): a reply that names no revision is about the one
+# that was up when it arrived.
+
+
+def test_a_bare_approval_about_an_earlier_revision_is_not_applied() -> None:
+    result = gate().evaluate("don", "approve", channel="transport", about=1)
+    assert isinstance(result, Ignored)
+    assert "arrived while rev-1 was up" in result.notice
+    assert "arch rev-2" in result.notice
+
+
+def test_feedback_about_an_earlier_revision_is_not_a_rejection() -> None:
+    result = gate().evaluate("don", "also add docs", channel="transport", about=1)
+    assert isinstance(result, Ignored)
+    assert "not taken as feedback on arch rev-2" in result.notice
+
+
+def test_a_reply_before_any_plan_was_up_is_not_applied() -> None:
+    result = gate().evaluate("don", "approve", channel="transport", about=0)
+    assert isinstance(result, Ignored)
+    assert "no plan" in result.notice
+
+
+def test_replies_about_the_current_revision_apply() -> None:
+    assert isinstance(gate().evaluate("don", "approve", "transport", about=2), Approved)
+    result = gate().evaluate("don", "add docs", "transport", about=2)
+    assert isinstance(result, Rejected)
+
+
+def test_a_named_revision_binds_by_its_number() -> None:
+    # "approve rev-2" says which plan it means, whenever it arrived.
+    assert isinstance(
+        gate().evaluate("don", "approve rev-2", "gitea", about=1), Approved
+    )

nisse-dev/tests/test_quint_counterexamples.py

@@ -191,7 +191,6 @@ class Agent:
 XFAIL = pytest.mark.xfail(strict=True, reason="counterexample; fix pending")
 
 
-@XFAIL
 def test_double_approve_approves_an_unseen_plan(tmp_path: Path) -> None:
     """doubleApproveApprovesAnUnseenPlanTest"""
     worker = QueueingWorker()
@@ -205,7 +204,6 @@ def test_double_approve_approves_an_unseen_plan(tmp_path: Path) -> None:
     assert not agent.gate().get("approved")
 
 
-@XFAIL
 def test_named_revision_approves_the_wrong_gate(tmp_path: Path) -> None:
     """namedRevisionApprovesTheWrongGateTest"""
     worker = QueueingWorker()
@@ -218,7 +216,6 @@ def test_named_revision_approves_the_wrong_gate(tmp_path: Path) -> None:
     assert not agent.gate().get("approved")
 
 
-@XFAIL
 def test_approval_on_both_channels_approves_the_next_plan(tmp_path: Path) -> None:
     """approvalOnBothChannelsApprovesTheNextPlanTest"""
     gitea = FakeGitea()
@@ -237,7 +234,6 @@ def test_approval_on_both_channels_approves_the_next_plan(tmp_path: Path) -> Non
     assert not agent.gate().get("approved")
 
 
-@XFAIL
 def test_an_afterthought_rejects_the_next_plan(tmp_path: Path) -> None:
     """anAfterthoughtRejectsTheNextPlanTest"""
     worker = QueueingWorker()
@@ -250,7 +246,7 @@ def test_an_afterthought_rejects_the_next_plan(tmp_path: Path) -> None:
     # The note was about the architecture; the milestone plan was not
     # rejected by it.
     assert agent.state == AWAIT_MILESTONE_SIGNOFF
-    assert agent.gate().get("rev") == 1
+    assert agent.gate().get("rev") == 2  # arch was rev-1; not re-planned
 
 
 @XFAIL

nisse-dev/tests/test_stop.py

@@ -229,8 +229,12 @@ def test_stop_reaches_work_running_on_the_worker(tmp_path: Path, word: str) -> N
         cancel=cancel,
     )
     worker.call(orch.start)
-    for text in ("use demo", "approve", "approve", "start milestone 1"):
+    for text in ("use demo", "approve", "approve"):
         transport.receive("don", text)
+        # Reply only once the plan is up: a reply stamped with an earlier
+        # revision is not applied to a later one.
+        worker.call(lambda: None)
+    transport.receive("don", "start milestone 1")
     assert executor.running.wait(5)
 
     transport.receive("don", "status")  # delivered while the milestone runs

specs/orchestrator.qnt

@@ -55,7 +55,8 @@ module orchestrator {
     tid: int,                 // task counter; a task's branches are its own
     task: bool,               // a project is in use
     gate: Gate,
-    revs: str -> int,
+    revs: str -> int,         // latest revision per gate
+    lastRev: int,             // revisions run across the task (A4)
     ms: int,
     pending: Pending,
     prOn: bool, prKey: int, prLast: int,          // _data["pr"]
@@ -120,7 +121,7 @@ module orchestrator {
     val t = s.tid + 1
     startPlanning(
       { ...s, tid: t, task: true, gate: NO_GATE,
-        revs: Map("arch" -> 0, "ms1" -> 0, "ms2" -> 0), ms: 1, pending: NO_PENDING,
+        revs: Map("arch" -> 0, "ms1" -> 0, "ms2" -> 0), lastRev: 0, ms: 1, pending: NO_PENDING,
         prOn: false, prKey: 0, prLast: 0,
         boardOn: giteaUp, boardPosted: false, boardLast: 0,
         openIssues: if (giteaUp) s.openIssues.union(Set(t)) else s.openIssues,
@@ -132,10 +133,10 @@ module orchestrator {
   // skips what is already there).
   pure def planSubmitted(s: Sys, giteaUp: bool): Sys =
     val g = s.workGate
-    val rev = s.revs.get(g) + 1
+    val rev = s.lastRev + 1
     val posted = s.boardOn and giteaUp
     val t = endWork({ ...s,
-      revs: s.revs.set(g, rev),
+      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 } })
@@ -146,19 +147,24 @@ module orchestrator {
   // _execute_milestone: start
   pure def startExec(s: Sys): Sys = { ...s, st: "EXECUTING", work: "exec" }
 
-  // _apply_gate_reply, for Matrix and Gitea alike.
+  // _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 == "approve" or (j.kind == "approveRev" and j.saw.rev == s.gate.rev))
+    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 if (j.kind == "approveRev")
-      s  // names another revision: ignored with a notice
     else
       // Anything else is rejection feedback, and the gate is planned again.
       startPlanning({ ...s, staleFeedback: s.staleFeedback or j.saw != current, gate: NO_GATE },
@@ -267,7 +273,7 @@ module orchestrator {
 
   action init = s' = {
     st: "IDLE", tid: 0, task: false, gate: NO_GATE,
-    revs: Map("arch" -> 0, "ms1" -> 0, "ms2" -> 0), ms: 1, pending: NO_PENDING,
+    revs: Map("arch" -> 0, "ms1" -> 0, "ms2" -> 0), lastRev: 0, ms: 1, pending: NO_PENDING,
     prOn: false, prKey: 0, prLast: 0,
     boardOn: false, boardPosted: false, boardLast: 0,
     intents: Set(),

specs/orchestrator_scenarios.qnt

@@ -1,6 +1,7 @@
 // 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, flip the expectation and keep the trace as a regression.
+// is fixed, the expectation is flipped and the trace kept as a regression.
+// Fixed: 1-4 (replies bind to the revision up when they arrived).
 //
 // Run:  quint test specs/orchestrator_scenarios.qnt   (runs every *Test)
 module orchestrator_scenarios {
@@ -26,50 +27,54 @@ module orchestrator_scenarios {
   // 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 approves the milestone plan,
-  //    which the operator has not seen.
+  //    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 s.gate.approved and not(approval_only_of_what_was_seen))
+      .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 matches the milestone's rev-1, because a
-  //    revision tag carries no gate name.
+  //    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.approved and not(approval_only_of_what_was_seen))
+      .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 approves the milestone plan.
+  //    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 s.gate.approved and not(approval_only_of_what_was_seen))
+      .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 lands on the milestone plan
-  //    as rejection feedback and it is planned again.
+  //    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 == "MILESTONE_PLANNING" and not(feedback_only_on_what_was_seen))
+      .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 finds the intent's PR and marks it done, but the state still