タスク指示書: 対話モードに `/issue` スラッシュコマンドを追加する

[nrslib]

タスク指示書: 対話モードに /issue スラッシュコマンドを追加する

背景と目的

TAKT の対話モードは、takt #123 のように Issue 番号を付けて起動すると、GitHub Issue の本文を Source Context として取り込み、以降の対話と /go の指示書作成に使う。しかし対話を始めた後に別の Issue を取り込む手段がなく、話題を変えたいときは takt を起動し直すしかない。

対話モードに /issue スラッシュコマンドを追加し、対話の途中でも takt #xxx で起動したときと同じ形で Issue を取り込めるようにする。ユーザーの意図は「話題の切り替え」であり、既存の Source Context は新しい Issue の内容で置き換える。ただし会話履歴と AI セッションはそのまま継続する。

合意した要件

優先度: 高

• 対話モードに /issue スラッシュコマンドを追加する
• 引数は takt の直接起動と同じ形式を受け付ける。/issue 123、/issue #123、複数指定 /issue 12 34 を扱う。複数指定時の本文連結や、Issue 番号のトレース記録が「登録済み Issue が合計1件のときだけ」になる点も takt #12 #34 の既存挙動と同じにする
• 取り込んだ Issue 本文は Source Context として登録する。既に Source Context がある場合（takt #xxx 起動によるもの、前回の /issue によるもの）は追記ではなく置き換える
• 会話履歴と AI セッションはリセットしない。/issue の前後で会話はそのまま続く
• takt #xxx の起動時と同じく、取り込み時に AI へ自動送信しない。取得結果の通知（Issue fetched: #N title 相当）を表示し、ユーザーの次の発言を待つ
• /issue の後に /go で実行した run は、takt #N で起動した場合と同じく新しい Issue 番号にひもづく。run のメタデータ、PR 本文の Issue 参照、タスク表示ラベルが対象
• gh CLI が使えない、Issue が存在しない、引数なし、といった失敗時は Source Context を変更せずに通知し、会話を継続する

優先度: 中

• TUI と readline フォールバックの両方で /issue を使えるようにする。対象は通常の対話モードで、exec モードなど独自にコマンド一覧を絞っているモードには追加しない
• 追加・変更した挙動に対する単体テストを追加し、リポジトリの慣例に従って tsconfig.tests.json に登録する
• ユーザー向けドキュメント（README.md や docs/ の対話モードのコマンド一覧）に /issue を追記する

やらないこと

• /issue による会話履歴や AI セッションのリセット
• 複数回の /issue による Issue 本文の追記（連結）蓄積
• exec モードなど、独自にコマンド一覧を定義しているモードへの追加

現状の調査結果（参考情報）

対話中にワークスペースを確認して得た事実を記す。これらは変更対象や方式を固定するものではなく、実行ワークフローが改めて現状を調査して変更対象と方式を決める。

• takt #123 の起動処理は、Issue を gh 経由で取得し、formatIssueAsTask で整形した本文を Source Context として対話に登録している。Source Context は以降の各メッセージと /go の指示書作成プロンプトの先頭に付く（src/app/cli/routing.ts の sourceContext）
• 同じ起動処理は traceTaskContext = { source: 'issue', issueNumber } を実行オプションに載せ、run のメタデータ、PR 本文の Issue 参照、タスク表示ラベル（#123）に使っている。複数指定時は本文を --- で連結し、Issue 番号は1件のときだけ記録している
• 対話モードの Source Context は現状セッション開始時に一度だけ渡される固定値で、途中で差し替える経路はない
• スラッシュコマンドは SlashCommand 定数と slashCommandRegistry.ts に定義があり、TUI 側（tuiConversation.ts）と readline 側（conversationLoop.ts）の両方に処理の分岐がある
• takt #123 の起動時は Issue 本文を Source Context に登録するだけで AI には自動送信せず、ユーザーの最初の発言を待つ。conversationLoop.ts のログにもその旨が明記されている

受け入れ条件

Feature: 対話モードの /issue コマンド

  Scenario: 既存の Source Context を置き換える
    Given takt #123 で起動した対話セッションで数回やり取りしている
    When ユーザーが /issue 456 を入力する
    Then Source Context は Issue #456 の本文だけになる
    And Issue #123 の本文は Source Context に残らない
    And 会話履歴と AI セッションは維持される
    And AI への自動送信は行われない
    And Issue #456 を取得した旨の通知が表示される

  Scenario: /issue 後の /go は新しい Issue にひもづく
    Given takt #123 で起動し /issue 456 で置き換えた対話セッション
    When ユーザーが /go で指示書を作成し実行を選ぶ
    Then 指示書作成プロンプトの Source Context は Issue #456 の本文である
    And 実行された run の Issue 番号は 456 である

  Scenario: 取り込みに失敗しても会話は壊れない
    Given Source Context に Issue #123 が登録された対話セッション
    When ユーザーが存在しない番号で /issue 999999 を入力する
    Then エラー通知が表示される
    And Source Context は Issue #123 のまま変わらない
    And 会話を続けられる

確認方法

• 上記 Gherkin の各 Scenario を、TUI と readline フォールバックの両方で手動確認する。takt #N で起動した後に /issue を打ち、/go まで進めて run のメタデータと PR 本文の Issue 参照を確認する
• /issue を引数なし、# 付き、複数番号、存在しない番号、gh を使えない状態でそれぞれ実行し、Source Context の変化有無と通知を確認する
• npm run lint、npm test、必要に応じて npm run test:it を通す

形式仕様: Quint

// 対話モードの /issue コマンドに関する要件のモデル。
// 対話セッションが持つ Source Context（Issue 番号の集合）、会話履歴、AI セッション、
// 最後に実行した操作、直近の通知、直近の run の記録を状態として持ち、
// ユーザー発言・/issue・/go・セッション終了の各操作でどう変化するかを定める。
module IssueSlashCommand {
  // Issue 番号のドメイン。
  // 1 と 2 はリポジトリに存在する Issue で、取得に成功しうる番号。
  // 3 は存在しない Issue 番号で、取得は必ず失敗する。
  // /issue コマンドは AllIssueNumbers の任意の部分集合（空集合 = 引数なしも含む）を要求できる。
  val ExistingIssues = Set(1, 2)
  val AllIssueNumbers = Set(1, 2, 3)

  // ユーザーに表示される通知の種類。
  // NoNotification: /issue 以外の操作の直後で、Issue 取り込みに関する通知が出ていない状態。
  // IssueFetched: /issue が成功し「Issue fetched: #N title」相当の通知が表示された状態。
  // IssueFailed: /issue が失敗し（gh CLI が使えない、Issue が存在しない、引数なし）、
  //              エラー通知が表示された状態。
  type Notification = NoNotification | IssueFetched | IssueFailed

  // 直前に実行された操作の種類。
  // Idle: セッション開始直後で、まだ何も操作していない。
  // UserTurn: ユーザーが通常の発言をし、会話履歴が伸びた。
  // IssueReplaced: /issue が成功し、Source Context が要求した Issue の本文だけに置き換わった。
  // IssueRejected: /issue が失敗し、Source Context は変更されなかった。
  // GoExecuted: /go により現在の Source Context を使って run が実行された。
  // SessionEnded: ユーザーが対話を終了した。
  type LastAction = Idle | UserTurn | IssueReplaced | IssueRejected | GoExecuted | SessionEnded

  // 状態変数。
  // sourceContext: 現在 Source Context として登録されている Issue 番号の集合。
  //   空集合は Source Context 未登録（Issue 番号なしで takt を起動した状態）。
  // historyLen: 会話履歴の長さ（0..2 に有界化）。/issue で変化しないことを検証するために持つ。
  // aiSessionId: 現在の AI セッションの識別子。リセットされないことを検証するために持つ。
  // conversationOpen: 対話を続けられる状態なら true。SessionEnded で false になる。
  // prevSourceContext / prevHistoryLen / prevAiSessionId: 直前の操作の前の値。
  //   「/issue が何を保ったか」を不変条件で述べるための履歴変数。
  // lastRequested: 直前の /issue でユーザーが要求した Issue 番号の集合。
  // lastAction: 直前に実行された操作。
  // notification: 直前の操作で表示された通知。
  // aiInvokedWithoutUserInput: 直前の操作がユーザーの発言なしに AI へ自動送信したなら true。
  // lastRunIssues: 直近の /go が使った Source Context の Issue 番号の集合。
  // lastRunTraced: 直近の /go の run に記録された Issue 番号。0 は記録なし。
  var sourceContext: Set[int]
  var historyLen: int
  var aiSessionId: int
  var conversationOpen: bool
  var prevSourceContext: Set[int]
  var prevHistoryLen: int
  var prevAiSessionId: int
  var lastRequested: Set[int]
  var lastAction: LastAction
  var notification: Notification
  var aiInvokedWithoutUserInput: bool
  var lastRunIssues: Set[int]
  var lastRunTraced: int

  // 初期状態。takt を Issue 番号なしで起動した場合（空集合）と、
  // takt #N または takt #N #M のように存在する Issue を指定して起動した場合を
  // すべて初期状態として許す。会話履歴は空、AI セッションは 1、対話は開いている。
  action init = {
    nondet startContext = ExistingIssues.powerset().oneOf()
    all {
      sourceContext' = startContext,
      historyLen' = 0,
      aiSessionId' = 1,
      conversationOpen' = true,
      prevSourceContext' = startContext,
      prevHistoryLen' = 0,
      prevAiSessionId' = 1,
      lastRequested' = Set(),
      lastAction' = Idle,
      notification' = NoNotification,
      aiInvokedWithoutUserInput' = false,
      lastRunIssues' = Set(),
      lastRunTraced' = 0
    }
  }

  // ユーザーの通常の発言。対話が開いていれば常に実行でき、会話履歴が伸びる（上限 2 で有界化）。
  // Source Context、AI セッション、直近の run の記録は変わらない。
  // ユーザー自身の発言による AI 呼び出しなので「自動送信」には当たらない。
  action userTurn = all {
    conversationOpen,
    sourceContext' = sourceContext,
    historyLen' = if (historyLen < 2) historyLen + 1 else historyLen,
    aiSessionId' = aiSessionId,
    conversationOpen' = true,
    prevSourceContext' = sourceContext,
    prevHistoryLen' = historyLen,
    prevAiSessionId' = aiSessionId,
    lastRequested' = lastRequested,
    lastAction' = UserTurn,
    notification' = NoNotification,
    aiInvokedWithoutUserInput' = false,
    lastRunIssues' = lastRunIssues,
    lastRunTraced' = lastRunTraced
  }

  // /issue コマンド。ユーザーは AllIssueNumbers の任意の部分集合を要求し、
  // gh CLI が使えるかどうかは非決定に決まる。
  // 成功条件: gh CLI が使え、要求が空でなく、要求したすべての Issue が存在する。
  //   成功時は Source Context を要求した Issue の集合だけに置き換え（以前の内容は残さない）、
  //   IssueFetched を通知し、lastAction を IssueReplaced にする。
  // 失敗条件: gh CLI が使えない、引数なし（要求が空）、存在しない Issue を含む、のいずれか。
  //   失敗時は Source Context を変更せず、IssueFailed を通知し、lastAction を IssueRejected にする。
  // 成功・失敗のどちらでも、会話履歴と AI セッションは変えず、AI へ自動送信せず、対話は開いたまま。
  action issueCommand = {
    nondet requested = AllIssueNumbers.powerset().oneOf()
    nondet ghAvailable = Set(true, false).oneOf()
    val accepted = ghAvailable and requested != Set() and requested.subseteq(ExistingIssues)
    all {
      conversationOpen,
      sourceContext' = if (accepted) requested else sourceContext,
      historyLen' = historyLen,
      aiSessionId' = aiSessionId,
      conversationOpen' = true,
      prevSourceContext' = sourceContext,
      prevHistoryLen' = historyLen,
      prevAiSessionId' = aiSessionId,
      lastRequested' = requested,
      lastAction' = if (accepted) IssueReplaced else IssueRejected,
      notification' = if (accepted) IssueFetched else IssueFailed,
      aiInvokedWithoutUserInput' = false,
      lastRunIssues' = lastRunIssues,
      lastRunTraced' = lastRunTraced
    }
  }

  // /go コマンド。現在の Source Context を使って run を実行する。
  // run には Source Context に登録された Issue の集合がそのまま使われ、
  // 登録済み Issue がちょうど 1 件のときだけその番号が run に記録され、
  // 0 件または 2 件以上のときは Issue 番号を記録しない（0 で表す）。
  // Source Context、会話履歴、AI セッションは変わらない。
  action goCommand = all {
    conversationOpen,
    sourceContext' = sourceContext,
    historyLen' = historyLen,
    aiSessionId' = aiSessionId,
    conversationOpen' = true,
    prevSourceContext' = sourceContext,
    prevHistoryLen' = historyLen,
    prevAiSessionId' = aiSessionId,
    lastRequested' = lastRequested,
    lastAction' = GoExecuted,
    notification' = NoNotification,
    aiInvokedWithoutUserInput' = false,
    lastRunIssues' = sourceContext,
    lastRunTraced' = if (sourceContext.size() == 1) sourceContext.fold(0, (acc, n) => n) else 0
  }

  // ユーザーによる対話の終了。対話を閉じ、それ以外の状態は変えない。
  // /issue コマンドが対話を閉じることはなく、対話を閉じるのはこの操作だけである。
  action endSession = all {
    conversationOpen,
    sourceContext' = sourceContext,
    historyLen' = historyLen,
    aiSessionId' = aiSessionId,
    conversationOpen' = false,
    prevSourceContext' = sourceContext,
    prevHistoryLen' = historyLen,
    prevAiSessionId' = aiSessionId,
    lastRequested' = lastRequested,
    lastAction' = SessionEnded,
    notification' = NoNotification,
    aiInvokedWithoutUserInput' = false,
    lastRunIssues' = lastRunIssues,
    lastRunTraced' = lastRunTraced
  }

  // 各ステップでは、ユーザー発言・/issue・/go・対話終了のいずれか 1 つが起きる。
  action step = any {
    userTurn,
    issueCommand,
    goCommand,
    endSession
  }

  // 不変条件: /issue は成功・失敗にかかわらず会話を壊さない。
  // 直前の操作が IssueReplaced または IssueRejected なら、会話履歴の長さと
  // AI セッションの識別子は /issue の前と同じで、AI への自動送信は行われず、対話は開いたままである。
  val invIssueCommandKeepsConversation =
    (lastAction == IssueReplaced or lastAction == IssueRejected) implies all {
      historyLen == prevHistoryLen,
      aiSessionId == prevAiSessionId,
      not(aiInvokedWithoutUserInput),
      conversationOpen
    }

  // 不変条件: /issue の成功は Source Context を「要求した Issue だけ」に置き換える。
  // 直前の操作が IssueReplaced なら、Source Context は要求した Issue の集合と一致し、
  // 通知は IssueFetched で、以前の Source Context にあって今回要求していない Issue は残っていない。
  val invReplacedContextIsOnlyRequestedIssues =
    (lastAction == IssueReplaced) implies all {
      sourceContext == lastRequested,
      notification == IssueFetched,
      prevSourceContext.forall(n => lastRequested.contains(n) or not(sourceContext.contains(n)))
    }

  // 不変条件: /issue の失敗は Source Context を変えない。
  // 直前の操作が IssueRejected なら、Source Context は /issue の前と同じで、通知は IssueFailed である。
  val invRejectedKeepsContext =
    (lastAction == IssueRejected) implies all {
      sourceContext == prevSourceContext,
      notification == IssueFailed
    }

  // 不変条件: /go の run は現在の Source Context にひもづく。
  // 直前の操作が GoExecuted なら、run が使った Issue の集合は現在の Source Context と一致し、
  // Source Context の Issue がちょうど 1 件ならその番号が run に記録され、
  // それ以外（0 件または複数件）なら Issue 番号は記録されない（0）。
  val invRunTracesSingleIssue =
    (lastAction == GoExecuted) implies all {
      lastRunIssues == sourceContext,
      if (sourceContext.size() == 1) sourceContext.contains(lastRunTraced) else lastRunTraced == 0
    }

  // 不変条件: Source Context には存在する Issue しか登録されない。
  // 存在しない Issue を要求した /issue は失敗するため、Source Context に存在しない番号が
  // 入ることはない。あわせて会話履歴の長さと記録された Issue 番号が有界の範囲に収まることを述べる。
  val invContextHoldsOnlyExistingIssues = all {
    sourceContext.subseteq(ExistingIssues),
    historyLen >= 0,
    historyLen <= 2,
    AllIssueNumbers.union(Set(0)).contains(lastRunTraced)
  }
}

形式仕様: Alloy

// 対話モードの /issue コマンドに関する要件のモデル。
// 対話セッションが持つ Source Context（Issue の集合）、会話履歴、AI セッション、
// 直前の操作、直近の通知、直近の run の記録を可変フィールドとして持ち、
// ユーザー発言・/issue・/go・対話終了の各遷移でどう変化するかを定める。
module issue_slash_command

// Issue のドメイン。
// ExistingIssue: リポジトリに存在し、取得に成功しうる Issue。
// MissingIssue: 存在しない番号を指す Issue で、取得は必ず失敗する。
abstract sig Issue {}
sig ExistingIssue extends Issue {}
sig MissingIssue extends Issue {}

// gh CLI の利用可否。各ステップで自由に変わる（環境要因であり、対話側から制御しない）。
// Available: gh CLI で Issue を取得できる。
// Unavailable: gh CLI が使えず、取得は必ず失敗する。
abstract sig Availability {}
one sig Available, Unavailable extends Availability {}
one sig Gh { var availability: one Availability }

// ユーザーに表示される通知の種類。
// NoNotification: /issue 以外の操作の直後で、Issue 取り込みに関する通知が出ていない。
// IssueFetched: /issue が成功し「Issue fetched: #N title」相当の通知が表示された。
// IssueFailed: /issue が失敗し（gh CLI が使えない、Issue が存在しない、引数なし）、
//              エラー通知が表示された。
abstract sig Notification {}
one sig NoNotification, IssueFetched, IssueFailed extends Notification {}

// 直前に実行された操作の種類。
// Idle: セッション開始直後で、まだ何も操作していない。
// UserTurn: ユーザーが通常の発言をし、会話履歴が伸びた。
// IssueReplaced: /issue が成功し、Source Context が要求した Issue の本文だけに置き換わった。
// IssueRejected: /issue が失敗し、Source Context は変更されなかった。
// GoExecuted: /go により現在の Source Context を使って run が実行された。
// SessionEnded: ユーザーが対話を終了した。
abstract sig ActionKind {}
one sig Idle, UserTurn, IssueReplaced, IssueRejected, GoExecuted, SessionEnded extends ActionKind {}

// 対話の状態。
// Open: ユーザーが発言やコマンド入力を続けられる。
// Closed: ユーザーが対話を終了し、以後の操作はできない。
abstract sig Status {}
one sig Open, Closed extends Status {}

// Message: 会話履歴を構成するユーザー発言。会話履歴は Message の集合として伸びていく。
// AiSession: AI セッションの識別子。リセットされれば別の AiSession に切り替わる。
sig Message {}
sig AiSession {}

// 対話セッション（常に 1 つ）。
// sourceContext: 現在 Source Context に登録されている Issue の集合。空なら未登録。
// history: 会話履歴として蓄積されたユーザー発言の集合。
// aiSession: 現在の AI セッション。
// status: 対話が Open か Closed か。
// lastRequested: 直前の /issue でユーザーが要求した Issue の集合。空は引数なし。
// lastAction: 直前に実行された操作。
// notification: 直前の操作で表示された通知。
// lastRunIssues: 直近の /go が使った Source Context の Issue の集合。
// lastRunTraced: 直近の /go の run に記録された Issue。空なら Issue 番号は記録されていない。
one sig Conversation {
  var sourceContext: set Issue,
  var history: set Message,
  var aiSession: one AiSession,
  var status: one Status,
  var lastRequested: set Issue,
  var lastAction: one ActionKind,
  var notification: one Notification,
  var lastRunIssues: set Issue,
  var lastRunTraced: lone Issue
}

// 直前の操作がユーザーの発言なしに AI へ自動送信したなら Conversation がこの集合に含まれる。
// /issue を含むどの操作も自動送信を行わないため、この集合は常に空でなければならない。
var sig AiAutoInvoked in Conversation {}

// 初期状態。takt を Issue 番号なしで起動した場合（Source Context が空）と、
// takt #N または takt #N #M のように存在する Issue を指定して起動した場合をすべて許す。
// 会話履歴は空、対話は Open、通知なし、run の記録なし、自動送信なし。
pred init {
  Conversation.sourceContext in ExistingIssue
  no Conversation.history
  Conversation.status = Open
  no Conversation.lastRequested
  Conversation.lastAction = Idle
  Conversation.notification = NoNotification
  no Conversation.lastRunIssues
  no Conversation.lastRunTraced
  no AiAutoInvoked
}

// 直近の run の記録を変えない補助述語。
pred keepRuns {
  Conversation.lastRunIssues' = Conversation.lastRunIssues
  Conversation.lastRunTraced' = Conversation.lastRunTraced
}

// ユーザーの通常の発言。対話が Open なら実行でき、会話履歴に新しい発言が 1 つ加わる。
// Source Context、AI セッション、直前の要求、run の記録は変わらず、対話は Open のまま。
// ユーザー自身の発言による AI 呼び出しなので自動送信には当たらない。
pred userTurn {
  Conversation.status = Open
  some m: Message - Conversation.history | Conversation.history' = Conversation.history + m
  Conversation.sourceContext' = Conversation.sourceContext
  Conversation.aiSession' = Conversation.aiSession
  Conversation.status' = Open
  Conversation.lastRequested' = Conversation.lastRequested
  Conversation.lastAction' = UserTurn
  Conversation.notification' = NoNotification
  no AiAutoInvoked'
  keepRuns
}

// /issue コマンドの成功。gh CLI が Available で、要求した Issue（lastRequested'）が
// 空でなくすべて ExistingIssue のときに起きる。
// Source Context は要求した Issue の集合だけに置き換わり、以前の内容は残らない。
// IssueFetched を通知し、会話履歴と AI セッションは変えず、AI へ自動送信せず、対話は Open のまま。
pred issueReplaced {
  Conversation.status = Open
  Gh.availability = Available
  some Conversation.lastRequested'
  Conversation.lastRequested' in ExistingIssue
  Conversation.sourceContext' = Conversation.lastRequested'
  Conversation.history' = Conversation.history
  Conversation.aiSession' = Conversation.aiSession
  Conversation.status' = Open
  Conversation.lastAction' = IssueReplaced
  Conversation.notification' = IssueFetched
  no AiAutoInvoked'
  keepRuns
}

// /issue コマンドの失敗。gh CLI が Unavailable、要求が空（引数なし）、
// 要求に MissingIssue が含まれる、のいずれかで起きる。
// Source Context は変更せず、IssueFailed を通知し、会話履歴と AI セッションは変えず、
// AI へ自動送信せず、対話は Open のまま（会話を続けられる）。
pred issueRejected {
  Conversation.status = Open
  (Gh.availability = Unavailable
    or no Conversation.lastRequested'
    or some (Conversation.lastRequested' - ExistingIssue))
  Conversation.sourceContext' = Conversation.sourceContext
  Conversation.history' = Conversation.history
  Conversation.aiSession' = Conversation.aiSession
  Conversation.status' = Open
  Conversation.lastAction' = IssueRejected
  Conversation.notification' = IssueFailed
  no AiAutoInvoked'
  keepRuns
}

// /go コマンド。現在の Source Context を使って run を実行する。
// run が使う Issue の集合は現在の Source Context と一致し、
// Source Context の Issue がちょうど 1 件ならその Issue が run に記録され、
// 0 件または複数件なら Issue は記録されない。
// Source Context、会話履歴、AI セッション、直前の要求は変わらず、対話は Open のまま。
pred goCommand {
  Conversation.status = Open
  Conversation.lastRunIssues' = Conversation.sourceContext
  (one Conversation.sourceContext)
    implies Conversation.lastRunTraced' = Conversation.sourceContext
    else no Conversation.lastRunTraced'
  Conversation.sourceContext' = Conversation.sourceContext
  Conversation.history' = Conversation.history
  Conversation.aiSession' = Conversation.aiSession
  Conversation.status' = Open
  Conversation.lastRequested' = Conversation.lastRequested
  Conversation.lastAction' = GoExecuted
  Conversation.notification' = NoNotification
  no AiAutoInvoked'
}

// ユーザーによる対話の終了。対話を Closed にし、それ以外は変えない。
// 対話を Closed にできるのはこの遷移だけであり、/issue が対話を閉じることはない。
pred endSession {
  Conversation.status = Open
  Conversation.status' = Closed
  Conversation.sourceContext' = Conversation.sourceContext
  Conversation.history' = Conversation.history
  Conversation.aiSession' = Conversation.aiSession
  Conversation.lastRequested' = Conversation.lastRequested
  Conversation.lastAction' = SessionEnded
  Conversation.notification' = NoNotification
  no AiAutoInvoked'
  keepRuns
}

// 何も起きないステップ。対話セッションの状態はすべて保たれる（gh CLI の利用可否だけは変わりうる）。
pred stutter {
  Conversation.sourceContext' = Conversation.sourceContext
  Conversation.history' = Conversation.history
  Conversation.aiSession' = Conversation.aiSession
  Conversation.status' = Conversation.status
  Conversation.lastRequested' = Conversation.lastRequested
  Conversation.lastAction' = Conversation.lastAction
  Conversation.notification' = Conversation.notification
  AiAutoInvoked' = AiAutoInvoked
  keepRuns
}

// トレース制約。初期状態から始まり、各ステップでは
// ユーザー発言・/issue 成功・/issue 失敗・/go・対話終了・無操作のいずれか 1 つが起きる。
fact traces {
  init
  always (userTurn or issueReplaced or issueRejected or goCommand or endSession or stutter)
}

// 検証: /issue は成功・失敗にかかわらず会話を壊さない。
// /issue が起きたステップの直後、会話履歴と AI セッションは直前と同じで、
// AI への自動送信は行われず、対話は Open のまま（会話を続けられる）。
assert IssueCommandKeepsConversation {
  always ((issueReplaced or issueRejected) implies (
    Conversation.history' = Conversation.history
    and Conversation.aiSession' = Conversation.aiSession
    and Conversation.status' = Open
    and no AiAutoInvoked'))
}

// 検証: /issue の成功は Source Context を「要求した Issue だけ」に置き換える。
// 成功直後の Source Context は要求した Issue の集合と一致し、通知は IssueFetched で、
// 以前の Source Context にあって今回要求していない Issue は新しい Source Context に残らない。
assert ReplacedContextIsOnlyRequestedIssues {
  always (issueReplaced implies (
    Conversation.sourceContext' = Conversation.lastRequested'
    and Conversation.notification' = IssueFetched
    and no ((Conversation.sourceContext - Conversation.lastRequested') & Conversation.sourceContext')))
}

// 検証: /issue の失敗は Source Context を変えず、エラー通知を表示する。
assert RejectedKeepsContext {
  always (issueRejected implies (
    Conversation.sourceContext' = Conversation.sourceContext
    and Conversation.notification' = IssueFailed))
}

// 検証: /go の run は現在の Source Context にひもづく。
// run が使う Issue の集合は /go 時点の Source Context と一致し、
// Source Context の Issue がちょうど 1 件ならその Issue が run に記録され、
// 0 件または複数件なら Issue は記録されない。
assert RunTracesSingleIssue {
  always (goCommand implies (
    Conversation.lastRunIssues' = Conversation.sourceContext
    and ((one Conversation.sourceContext)
      implies Conversation.lastRunTraced' = Conversation.sourceContext
      else no Conversation.lastRunTraced')))
}

// 検証: Source Context には存在する Issue しか登録されない。
// 存在しない Issue を含む要求は失敗するため、MissingIssue が Source Context に入ることはない。
assert ContextHoldsOnlyExistingIssues {
  always Conversation.sourceContext in ExistingIssue
}

check IssueCommandKeepsConversation for 4 but 8 steps
check ReplacedContextIsOnlyRequestedIssues for 4 but 8 steps
check RejectedKeepsContext for 4 but 8 steps
check RunTracesSingleIssue for 4 but 8 steps
check ContextHoldsOnlyExistingIssues for 4 but 8 steps