diff --git a/specs/README.md b/specs/README.md index 9d53979..28bd402 100644 --- a/specs/README.md +++ b/specs/README.md @@ -36,3 +36,35 @@ Exhaustive bounded checking (`quint verify`) uses Apalache and needs Java 17. 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. diff --git a/specs/loop.qnt b/specs/loop.qnt new file mode 100644 index 0000000..4370a52 --- /dev/null +++ b/specs/loop.qnt @@ -0,0 +1,489 @@ +// A model of the agent loop as docs/Architecture.md describes it (PR #90): +// work items from assigned issues and conversations, restatements and +// go-aheads, park-and-switch, blocked dependencies, harness-owned milestones, +// waiting for merges, review follow-ups, and crashes at any point. +// +// Unlike orchestrator.qnt, this models a design, not code: the new loop +// doesn't exist yet, so a counterexample here is a gap in the architecture. +// +// Everything lives in one record, `s`. Durable state (the state store, +// Gitea, the build VM's disk) survives a crash; volatile state (work in +// flight) does not. Ghost fields record what the properties need to know +// and the agent never reads. +// +// Run: quint run specs/loop.qnt --invariant=all_properties +module loop { + + // ---- bounds -------------------------------------------------------------- + + pure val MAX_ITEMS = 3 // work items per run + pure val MAX_REV = 3 // restatement revisions per item + pure val MAX_MS = 2 // milestones per item + pure val MAX_INBOX = 3 // operator messages not yet handled + pure val PROJECTS = Set("A", "B") + pure val ISSUES = Set(1, 2) // issues the operator can file and assign + pure val DEP_ISSUES = Set(101, 102) // other issues an item can be blocked by + + // ---- state --------------------------------------------------------------- + + type Item = { + status: str, // ready / waiting / blocked / closed (active is s.active) + src: str, // issue / conv + issue: int, // its record issue, 0 if none yet + project: str, + bug: bool, + waitFor: str, // goahead / grace / answer / agree / merge, when waiting + question: bool, // a question to the operator is pending (L2) + rev: int, // latest restatement put up (L3) + needRestate: bool, // an answer changed the understanding: restate again + started: bool, // scope agreed: a go-ahead, or a bug's grace period over (D1) + ms: int, // current milestone, 0 before the first + attempt: int, // a redo of a milestone whose PR was closed gets a new branch + stage: str, // none / working / pr + review: bool, // a review comment is waiting to be answered (D5) + unpushed: bool, // work on the build VM not yet pushed + deps: Set[int], // recorded dependencies (L1) + } + + type Issue = { open: bool, assigned: bool, linked: int } + type Msg = { item: int, kind: str, saw: int } + + type Sys = { + // -- durable: the state store -- + items: int -> Item, + nextItem: int, + active: int, // 0: none (L1) + intents: Set[int], // pending publish intents, by PR key (L8) + // -- durable: Gitea -- + issues: int -> Issue, + depOpen: int -> bool, + prs: int -> str, // PR key -> open / merged / closed + opened: int -> int, // PR key -> PRs ever opened for it + // -- durable: Matrix holds messages until the agent handles them -- + inbox: List[Msg], + // -- volatile -- + work: str, // none / publish + pubStage: int, + pending: int, // a record issue created but not yet linked + // -- ghosts -- + badGo: bool, // work started on a revision the operator never saw + earlyMs: bool, // a milestone started before the previous merged + lostFix: bool, // a review fix pushed to a PR no longer open + lostWork: bool, // a parked item's unpushed work was set aside or wiped + } + + var s: Sys + + pure def prKey(i: int, ms: int, a: int): int = i * 100 + ms * 10 + a + pure def keyOf(t: Sys, i: int): int = prKey(i, t.items.get(i).ms, t.items.get(i).attempt) + pure def prOf(t: Sys, i: int): str = { + val k = keyOf(t, i) + if (t.prs.keys().contains(k)) t.prs.get(k) else "" + } + pure def upd(t: Sys, i: int, it: Item): Sys = { ...t, items: t.items.set(i, it) } + pure def itm(t: Sys, i: int): Item = t.items.get(i) + pure def live(t: Sys): Set[int] = t.items.keys().filter(i => t.items.get(i).status != "closed") + + pure def newItem(src: str, issue: int, project: str, bug: bool): Item = { + status: "ready", src: src, issue: issue, project: project, bug: bug, + waitFor: "", question: false, rev: 0, needRestate: false, started: false, + ms: 0, attempt: 0, stage: "none", review: false, unpushed: false, deps: Set(), + } + + pure def wait(it: Item, why: str, q: bool): Item = + { ...it, status: "waiting", waitFor: why, question: q } + pure def ready(it: Item): Item = { ...it, status: "ready", waitFor: "", question: false } + + action init = s' = { + items: Map(), nextItem: 1, active: 0, intents: Set(), + issues: ISSUES.mapBy(_ => { open: false, assigned: false, linked: 0 }), + depOpen: DEP_ISSUES.mapBy(_ => true), + prs: Map(), opened: Map(), inbox: List(), + work: "none", pubStage: 0, pending: 0, + badGo: false, earlyMs: false, lostFix: false, lostWork: false, + } + + // ---- the operator ---------------------------------------------------------- + + // Files an issue and assigns it to the agent (D1). + // (Its project and `bug` label are chosen at intake.) + action assignIssue(n: int): bool = all { + not(s.issues.get(n).open), s.issues.get(n).linked == 0, + s' = { ...s, issues: s.issues.set(n, { open: true, assigned: true, linked: 0 }) }, + } + + // Starts a conversation: a work item from its first message (L5). + action converse(p: str): bool = all { + s.nextItem <= MAX_ITEMS, + s' = { ...s, items: s.items.put(s.nextItem, newItem("conv", 0, p, false)), + nextItem: s.nextItem + 1 }, + } + + // Replies in an item's thread. `saw` is the revision on screen when sent. + action say(i: int, kind: str): bool = all { + live(s).contains(i), s.inbox.length() < MAX_INBOX, + s' = { ...s, inbox: s.inbox.append({ item: i, kind: kind, saw: itm(s, i).rev }) }, + } + + // Merges, closes or comments on an item's open PR (D4, D5). + action prAct(i: int, what: str): bool = { + val k = keyOf(s, i) + all { + s.items.keys().contains(i), prOf(s, i) == "open", + s' = if (what == "comment") upd(s, i, { ...itm(s, i), review: true }) + else { ...s, prs: s.prs.set(k, what) }, + } + } + + // Closes an issue another item depends on. + action closeDep(d: int): bool = all { + s.depOpen.get(d), s' = { ...s, depOpen: s.depOpen.set(d, false) }, + } + + // ---- intake and the duty --------------------------------------------------- + + // The duty picks up an assigned, open issue that no item is linked to (D1). + action intake(n: int, p: str, bug: bool): bool = { + val known = s.issues.keys().contains(n) + val is = s.issues.get(n) + all { + known, is.open, is.assigned, is.linked == 0, s.nextItem <= MAX_ITEMS, + s' = { ...s, items: s.items.put(s.nextItem, newItem("issue", n, p, bug)), + issues: s.issues.set(n, { ...is, linked: s.nextItem }), + nextItem: s.nextItem + 1 }, + } + } + + // The duty notices external truth: a merged or closed PR, a dependency + // closed. (L1 blocked, D4 wait for the merge.) + action observe(i: int): bool = { + val it = itm(s, i) + all { + live(s).contains(i), + any { + all { it.status == "blocked", it.deps.forall(d => not(s.depOpen.get(d))), + s' = upd(s, i, ready({ ...it, deps: Set() })) }, + all { it.stage == "pr", prOf(s, i) == "merged", not(it.review), + s' = upd(s, i, ready({ ...it, stage: "none" })) }, + // D4: ready with that fact; the agent asks what next. + // FIX 4 (D4): a redo is the same milestone on a new branch and PR. + all { it.stage == "pr", prOf(s, i) == "closed", + s' = upd(s, i, wait({ ...it, stage: "none", ms: it.ms - 1, + attempt: it.attempt + 1 }, "answer", true)) }, + all { it.stage == "pr", it.review, it.status == "waiting", + s' = upd(s, i, ready(it)) }, + }, + } + } + + // ---- handling messages (conversation is not work, L1) ---------------------- + + pure def handle(t: Sys, m: Msg): Sys = { + val it = itm(t, m.item) + if (it.status == "closed") t + else if (m.kind == "go") + // L3: bound to the revision up when the reply arrived. + if (it.status == "waiting" and it.waitFor == "goahead" and m.saw == it.rev) + { ...upd(t, m.item, ready({ ...it, started: true })), badGo: t.badGo or m.saw != it.rev } + else t + else if (m.kind == "answer") + if (it.question and (it.waitFor == "answer")) + upd(t, m.item, ready({ ...it, needRestate: not(it.started) })) + else t + else if (m.kind == "agree") + // D1/L1: the operator agrees a blocker should be recorded. + if (it.waitFor == "agree") upd(t, m.item, { ...it, status: "blocked", waitFor: "", + question: false, deps: Set(101) }) + else t + else if (m.kind == "decline") + if (it.waitFor == "agree") upd(t, m.item, ready(it)) else t + else if (m.kind == "abandon") + // L2: from any waiting point; closes the record, aborts its intents. + if (t.active == m.item and t.work != "none") t + else { + val closed = upd(t, m.item, { ...it, status: "closed", question: false }) + val withIssue = if (it.issue != 0) + { ...closed, issues: closed.issues.set(it.issue, + { ...closed.issues.get(it.issue), open: false }) } + else closed + val noIntents = { ...withIssue, intents: withIssue.intents.filter(k => k / 100 != m.item) } + // FIX 1 (L2): abandoning closes the item's open PR with a note. + { ...noIntents, prs: noIntents.prs.keys().mapBy(k => + if (k / 100 == m.item and noIntents.prs.get(k) == "open") "closed" + else noIntents.prs.get(k)) } + } + else t + } + + action handleMsg: bool = all { + s.inbox.length() > 0, s.work == "none", + s' = { ...handle(s, s.inbox.head()), inbox: s.inbox.tail() }, + } + + // ---- the agent --------------------------------------------------------------- + + // Switching: the active item is at a safe point; parking pushes its branch (D4). + action park: bool = { + val it = itm(s, s.active) + all { + s.active != 0, s.work == "none", s.intents.size() == 0, + Set("waiting", "blocked", "closed").contains(it.status), + s' = { ...upd(s, s.active, { ...it, unpushed: false }), active: 0 }, + } + } + + // Taking up a ready item: a fresh workspace on its project's build VM (D3) + // sets aside whatever is left there. + action activate(i: int): bool = all { + s.active == 0, s.work == "none", live(s).contains(i), itm(s, i).status == "ready", + s' = { + val leftovers = s.items.keys().exists(j => j != i and itm(s, j).project == itm(s, i).project + and itm(s, j).unpushed) + { ...s, active: i, lostWork: s.lostWork or leftovers } + }, + } + + // Restating (D1): bug → grace period; otherwise wait for a go-ahead; or ask. + action restate(ask: bool): bool = { + val i = s.active + val it = itm(s, i) + all { + i != 0, s.work == "none", it.status == "ready", not(it.started), + it.rev < MAX_REV, + s' = upd(s, i, + if (ask) wait({ ...it, rev: it.rev + 1, needRestate: false }, "answer", true) + else if (it.bug) wait({ ...it, rev: it.rev + 1, needRestate: false }, "grace", false) + else wait({ ...it, rev: it.rev + 1, needRestate: false }, "goahead", false)), + } + } + + // A bug's grace period runs out: the item is ready to work (D1). + action graceOver(i: int): bool = all { + live(s).contains(i), itm(s, i).waitFor == "grace", + s' = upd(s, i, ready({ ...itm(s, i), started: true })), + } + + // Work on a repository needs a record issue (D1). Opening one is an + // external effect, then the link is written: two steps. + action createRecord: bool = { + val it = itm(s, s.active) + val n = 100 - s.active // the record's issue number + all { + s.active != 0, s.work == "none", it.status == "ready", it.started, it.issue == 0, + s.pending == 0, + // FIX 5 (D1): the issue carries its work item's ID from creation, so + // intake never takes it for new work, even before the link is stored. + s' = { ...s, pending: s.active, + issues: s.issues.put(n, { open: true, assigned: true, linked: s.active }) }, + } + } + + action linkRecord: bool = { + val n = 100 - s.pending + all { + s.pending != 0, + s' = { ...upd(s, s.pending, { ...itm(s, s.pending), issue: n }), + issues: s.issues.set(n, { ...s.issues.get(n), linked: s.pending }), + pending: 0 }, + } + } + + // start_milestone (D4): only after the previous milestone's PR merged. + action startMilestone: bool = { + val i = s.active + val it = itm(s, i) + all { + i != 0, s.work == "none", it.status == "ready", it.started, it.issue != 0, + it.stage == "none", it.ms < MAX_MS, + s' = { + val early = it.ms > 0 and prOf(s, i) != "merged" + { ...upd(s, i, { ...it, ms: it.ms + 1, stage: "working", unpushed: true }), + earlyMs: s.earlyMs or early } + }, + } + } + + // A turn of work: progress, a blocker to propose, or a question. + action turn(outcome: str): bool = { + val i = s.active + val it = itm(s, i) + all { + i != 0, s.work == "none", it.status == "ready", it.stage == "working", + s' = upd(s, i, + if (outcome == "progress") { ...it, unpushed: true } + else if (outcome == "blocker") wait(it, "agree", true) + else wait(it, "answer", true)), + } + } + + // finish_milestone (D4): commit, push, open the PR, under an intent (L8). + action finishMilestone: bool = { + val it = itm(s, s.active) + all { + s.active != 0, s.work == "none", it.status == "ready", it.stage == "working", + s' = { ...s, work: "publish", pubStage: 0 }, + } + } + + action publishStep(lost: bool): bool = { + val i = s.active + val it = itm(s, i) + val k = keyOf(s, i) + all { + s.work == "publish", + s' = + if (s.pubStage == 0) { ...s, intents: s.intents.union(Set(k)), pubStage: 1 } + else if (s.pubStage == 1) { + val pushed = upd(s, i, { ...it, unpushed: false }) + if (s.prs.keys().contains(k) and s.prs.get(k) == "open") { ...pushed, pubStage: 2 } + // FIX 2 (D4, L8): the branch's PR was closed: report it, never open another. + else if (s.prs.keys().contains(k) and s.prs.get(k) != "open") + { ...upd(pushed, i, wait({ ...itm(pushed, i), stage: "pr" }, "answer", true)), + intents: pushed.intents.exclude(Set(k)), work: "none", pubStage: 0 } + else { + val n = if (s.opened.keys().contains(k)) s.opened.get(k) else 0 + val withPr = { ...pushed, prs: pushed.prs.put(k, "open"), + opened: pushed.opened.put(k, n + 1) } + // A lost response: Gitea opened it, the agent never heard. + if (lost) { ...withPr, work: "none", pubStage: 0 } else { ...withPr, pubStage: 2 } + } + } + else { ...upd(s, i, wait({ ...it, stage: "pr", unpushed: false }, "merge", false)), + intents: s.intents.exclude(Set(k)), work: "none", pubStage: 0 }, + } + } + + // Answering a review comment: commits pushed to the PR's branch (D5). + action answerReview: bool = { + val i = s.active + val it = itm(s, i) + all { + i != 0, s.work == "none", it.status == "ready", it.stage == "pr", it.review, + s' = + if (prOf(s, i) == "open") + upd(s, i, wait({ ...it, review: false, unpushed: false }, "merge", false)) + // FIX 3 (D5): the PR merged first: the fix goes out as a new PR. + else if (prOf(s, i) == "merged") + upd(s, i, { ...it, review: false, stage: "working", attempt: it.attempt + 1, + unpushed: true }) + // ...or it was closed: say so and ask. + else upd(s, i, wait({ ...it, review: false, stage: "none" }, "answer", true)), + } + } + + // Finishing: the last PR merged, the agent closes the item (D1). + action finish: bool = { + val i = s.active + val it = itm(s, i) + all { + i != 0, s.work == "none", it.status == "ready", it.ms > 0, it.stage == "none", + prOf(s, i) == "merged", + s' = upd(s, i, { ...it, status: "closed" }), + } + } + + // The build VM is wiped (D3): unpushed work on it is lost, accepted for + // the active item, never for a parked one. + action wipe(p: str): bool = all { + s' = { ...s, + items: s.items.keys().mapBy(j => + if (itm(s, j).project == p) { ...itm(s, j), unpushed: false } else itm(s, j)), + lostWork: s.lostWork or s.items.keys().exists(j => + j != s.active and itm(s, j).project == p and itm(s, j).unpushed) }, + } + + // ---- crash and boot (L8) -------------------------------------------------- + + // Volatile state is lost; boot reconciles each pending intent against + // Gitea: an open PR is adopted, otherwise the intent is aborted and the + // operator is told (L8 step 5). + pure def reconcile(t: Sys, k: int): Sys = { + val i = k / 100 + val it = itm(t, i) + val t2 = { ...t, intents: t.intents.exclude(Set(k)) } + if (t.prs.keys().contains(k) and t.prs.get(k) == "open") + upd(t2, i, wait({ ...it, stage: "pr", unpushed: false }, "merge", false)) + else upd(t2, i, wait(it, "answer", true)) + } + + action crash: bool = + s' = s.intents.fold({ ...s, work: "none", pubStage: 0, pending: 0 }, + (t, k) => reconcile(t, k)) + + // ---- step --------------------------------------------------------------------- + + action step = { + nondet n = ISSUES.oneOf() + nondet anyIssue = s.issues.keys().oneOf() + nondet i = 1.to(MAX_ITEMS).oneOf() + nondet p = PROJECTS.oneOf() + nondet b = Set(true, false).oneOf() + nondet kind = Set("go", "answer", "agree", "decline", "abandon").oneOf() + nondet what = Set("merged", "closed", "comment").oneOf() + nondet outcome = Set("progress", "blocker", "question").oneOf() + nondet d = DEP_ISSUES.oneOf() + any { + assignIssue(n), converse(p), say(i, kind), prAct(i, what), closeDep(d), + intake(anyIssue, p, b), observe(i), handleMsg, + park, activate(i), restate(b), graceOver(i), createRecord, linkRecord, + startMilestone, turn(outcome), finishMilestone, publishStep(b), answerReview, + finish, wipe(p), crash, + } + } + + // ---- properties --------------------------------------------------------------- + + // An issue is the record of at most one work item (D1 intake). + val one_item_per_issue = s.items.keys().forall(a => s.items.keys().forall(b => + (a != b and itm(s, a).issue != 0) implies itm(s, a).issue != itm(s, b).issue)) + + // Every wait is for something the operator can see or a dependency (L2). + val waits_are_explainable = live(s).forall(i => { + val it = itm(s, i) + and { + it.status == "waiting" implies or { + it.waitFor == "goahead" and it.rev > 0, + it.waitFor == "grace", + Set("answer", "agree").contains(it.waitFor) and it.question, + it.waitFor == "merge" and prOf(s, i) != "", + }, + it.status == "blocked" implies it.deps.size() > 0, + } + }) + + // Work starts only on a go-ahead for the revision the operator saw (L3). + val go_binds = not(s.badGo) + + // The next milestone starts only after the previous PR merged (D4). + val milestone_after_merge = not(s.earlyMs) + + // A parked item's work is never set aside or wiped (D4 parking). + val parked_work_safe = not(s.lostWork) + + // Never more than one PR opened for a milestone (L8). + val one_pr_per_milestone = s.opened.keys().forall(k => s.opened.get(k) <= 1) + + // A review fix always lands on an open PR (D5). + val review_fixes_land = not(s.lostFix) + + // A closed item leaves no open PR and no pending intent behind (L2). + val closed_items_leave_nothing = s.items.keys().forall(i => + itm(s, i).status == "closed" implies and { + s.prs.keys().forall(k => k / 100 == i implies s.prs.get(k) != "open"), + s.intents.forall(k => k / 100 != i), + }) + + val all_properties = and { + one_item_per_issue, waits_are_explainable, go_binds, milestone_after_merge, + parked_work_safe, one_pr_per_milestone, review_fixes_land, closed_items_leave_nothing, + } + + // ---- reachability witnesses (each should be violated) -------------------------- + val w_pr_opened = s.opened.keys().size() == 0 + val w_merged = not(s.prs.keys().exists(k => s.prs.get(k) == "merged")) + val w_second_ms = not(s.items.keys().exists(i => itm(s, i).ms == 2)) + val w_blocked = not(s.items.keys().exists(i => itm(s, i).status == "blocked")) + val w_review = not(s.items.keys().exists(i => itm(s, i).review)) + val w_record = not(s.items.keys().exists(i => itm(s, i).src == "conv" and itm(s, i).issue != 0)) + val w_finished = not(s.items.keys().exists(i => itm(s, i).status == "closed" and itm(s, i).ms > 0)) +} diff --git a/specs/loop_scenarios.qnt b/specs/loop_scenarios.qnt new file mode 100644 index 0000000..1d793d7 --- /dev/null +++ b/specs/loop_scenarios.qnt @@ -0,0 +1,77 @@ +// Counterexamples found in loop.qnt, written out as short traces. Each was a +// gap in docs/Architecture.md; the model now has the proposed fix (marked +// FIX n in loop.qnt), and each trace checks the fixed behaviour. +// +// Run: quint test specs/loop_scenarios.qnt (runs every *Test) +module loop_scenarios { + import loop.* from "./loop" + + // An assigned issue, restated, a go-ahead, milestone 1 under way. + action toWorking = init + .then(assignIssue(1)).then(intake(1, "A", false)) + .then(activate(1)).then(restate(false)) + .then(say(1, "go")).then(handleMsg) + .then(startMilestone) + + // ...and published: its PR is open and the item waits for the merge. + action toPrOpen = toWorking + .then(finishMilestone) + .then(publishStep(false)).then(publishStep(false)).then(publishStep(false)) + + // 1. Abandoning an item left its open PR open: L2 closed the record and + // aborted intents, but said nothing about PRs. Fixed: abandon closes + // the item's open PRs with a note. + run abandonClosesTheOpenPrTest = + toPrOpen + .then(park) + .then(say(1, "abandon")).then(handleMsg) + .expect(closed_items_leave_nothing and s.prs.get(prKey(1, 1, 0)) == "closed") + + // 2. Gitea opened the PR but the response was lost, so the agent never + // knew. The operator closed that PR; the agent's retry only adopted + // *open* PRs, so it opened a second one over the operator's close. + // Fixed: a closed PR on the branch is an answer: report it and ask. + run retryNeverReopensAClosedPrTest = + toWorking + .then(finishMilestone) + .then(publishStep(false)) + .then(publishStep(true)) // opened, response lost + .then(prAct(1, "closed")) // the operator closes it + .then(finishMilestone) // the agent retries + .then(publishStep(false)).then(publishStep(false)) + .expect(one_pr_per_milestone and itm(s, 1).waitFor == "answer") + + // 3. A review comment made the item ready; the operator merged the PR + // before the fix was pushed, so the fix went to a merged branch and + // never reached main. Fixed: a fix for a PR that merged meanwhile goes + // out as a new PR (and one for a closed PR is reported). + run reviewFixAfterMergeGetsANewPrTest = + toPrOpen + .then(prAct(1, "comment")).then(observe(1)) + .then(prAct(1, "merged")) + .then(answerReview) + .expect(review_fixes_land and itm(s, 1).stage == "working" and itm(s, 1).attempt == 1) + + // 4. After a PR closed unmerged and the operator answered, the next + // milestone could start with the closed one never merged. Fixed: a + // redo is the same milestone on a new branch and PR. + run closedPrRedoesTheSameMilestoneTest = + toPrOpen + .then(prAct(1, "closed")).then(observe(1)) + .then(say(1, "answer")).then(handleMsg) + .then(startMilestone) + .expect(milestone_after_merge and itm(s, 1).ms == 1 and itm(s, 1).attempt == 1) + + // 5. Work begun in conversation gets a record issue, assigned to the + // agent. Opening it and storing the link were two steps, and intake + // could take the assigned, unlinked issue for new work in between. + // Fixed: the issue carries its work item's ID from creation. + run recordIssueIsNeverTakenForNewWorkTest = + init + .then(converse("A")).then(activate(1)).then(restate(false)) + .then(say(1, "go")).then(handleMsg) + .then(createRecord) + .expect(s.issues.get(99).linked == 1) + .then(linkRecord) + .expect(one_item_per_issue and itm(s, 1).issue == 99) +}