// 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)

  // M4.3: a build VM the driver finds broken blocks its project; nothing is
  // taken up on it until the operator says `vm ready`, then work goes on.
  run aBrokenVmBlocksUntilReadyTest =
    init
      .then(assignIssue(1)).then(intake(1, "A", false))
      .then(activate(1)).then(requestReimage)
      .expect(s.vmBlocked.contains("A") and s.active == 0)
      .then(vmReady("A"))
      .then(activate(1))
      .expect(blocked_vm_runs_nothing and s.active == 1)

  // #137: an out-of-reach VM found at the check blocks its project; a probe
  // can't unblock it while it's down, and does once it's back.
  run anUnreachableVmBlocksUntilItAnswersTest =
    init
      .then(assignIssue(1)).then(intake(1, "A", false))
      .then(goDown("A"))
      .then(activate(1))
      .expect(s.vmUnreachable.contains("A") and s.active == 0)
      .then(comeBack("A")).then(probe("A"))
      .then(activate(1))
      .expect(all_properties and s.active == 1)
}