// 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.
//
// 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 approves the milestone plan,
  //    which the operator has not seen.
  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))

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

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

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

  // 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
  //    says EXECUTING, so it asks the restart question. 'continue' returns
  //    to the approved plan, and starting it publishes again: Gitea refuses
  //    a second PR for the branch, and there is no path back to PR_OPEN.
  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))         // intent verified and committed; state EXECUTING
      .then(send("continue")).then(runJob(true))
      .then(send("start")).then(runJob(true))
      .then(finishExec("completed"))
      .then(publishStep("ok")).then(publishStep("ok"))
      .expect(s.st == "AWAIT_INPUT" and not(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 resumes quietly, so the comment is never answered
  //    and nobody is told.
  run crashDuringAReviewLosesTheCommentTest =
    toPrOpen
      .then(commentPr).then(pollPr).then(runJob(true))  // the executor starts on it
      .then(crash(true))
      .expect(s.st == "PR_OPEN" and not(review_comments_answered))

  // 7. A completed task leaves its plan issue open: 'project complete'
  //    closes nothing, unlike 'abandon'.
  run projectCompleteLeavesThePlanIssueOpenTest =
    toPrOpen
      .then(send("complete")).then(runJob(true))
      .expect(s.st == "IDLE" and not(no_open_issue_without_a_task))
}