testcase-generator

name	testcase-generator
description	仕様からテストケースを体系的に生成するスキル。状態機械・自然言語・Mermaid・シーケンス図など多様な入力形式に対応し、CSP安定失敗モデルに基づいて受理テストケース（トレース集合内）と拒否テストケース（トレース集合外）を網羅的に導出する。活性・到達可能性・安全性の3性質を検証するテストスイートを生成する。要求定義・仕様記述・設計成果物からのテストケース生成、テスト設計レビュー、テストカバレッジ分析に使用する。
disable-model-invocation	true

テストケース生成スキル

仕様をCSP安定失敗モデルの枠組みで解析し、受理テストケースと拒否テストケースを体系的に生成する。

参照ファイル:

• 理論的フレームワーク → references/theory.md（基礎概念・形式定義が必要な場合）
• サンプリング戦略の詳細 → references/sampling-strategies.md（複雑な仕様や大規模テスト設計時）
• 具体的なウォークスルー例 → references/examples.md（自販機・ログイン・ECカートの例）

---

ワークフロー

Step 1: 入力の理解と正規化

入力形式を判定し、内部モデルに変換する:

入力形式	対応方法
自然言語	状態・遷移・ガード・事後条件を抽出して状態機械へ変換
状態機械（テキスト記法）	そのまま解析
Mermaid stateDiagram	状態・遷移を読み取り
シーケンス図	トレース1本として扱い、仕様が不完全であることをユーザーに通知

状態機械モデルの要素を確認する:

• 状態集合 S（初期状態を明示）
• イベント集合 Σ（内部イベント τ を識別）
• 遷移関係（イベント・ガード・事後条件）
• 状態変数とその型・初期値

情報が不足している場合はユーザーに確認する。

Step 2: トレース集合の導出

初期状態からの到達可能なトレースを列挙する:

1. BFS/DFSで遷移を展開 — 初期状態から遷移可能なイベント列を生成
2. τ除去 — 内部イベントτをトレースから取り除く
3. 安定状態の特定 — τ遷移できない状態を識別
4. 失敗集合の導出 — 各安定状態で拒否されるイベント集合を記録

無限ループへの対処: 同じ状態を2回以上訪問するケースはサイクルとして記録し、有界展開（デフォルト: 状態数×2 ステップ）で打ち切る。

導出結果を以下の形式でまとめる:

トレース集合（代表例）:
  ε（空トレース）
  ⟨e1⟩
  ⟨e1, e2⟩
  ⟨e1, e2, e3⟩
  ...

失敗集合（代表例）:
  (⟨⟩, {拒否イベント集合})
  (⟨e1⟩, {拒否イベント集合})
  ...

Step 3: 機能要求の確認

仕様が満たすべき性質を整理する:

性質	具体的な要求	検証対象トレース
活性	「Xが起こるといつかYが起こる」	Y到達トレース
到達可能性	「状態Sに到達できる」	S到達トレース
安全性	「Xが起きた後Yは起こらない」	Y出現トレース

ユーザーが機能要求を明示していない場合は、状態機械の構造から推定して確認を求める。

Step 4: 受理テストケースの生成

トレース集合内からリスクベースでサンプリングする。

詳細なサンプリング戦略は references/sampling-strategies.md を参照。

基本的な6つの優先度基準（高→低）:

1. ビジネスクリティカルフロー — 主要ユースケースの正常系トレース
2. 活性・到達可能性の証明 — 機能要求で指定された到達トレース
3. ガード条件の各分岐 — ガードが真/偽それぞれの遷移を含むトレース
4. 状態変数の境界値 — ガード条件の境界での動作
5. ループ・繰り返しの代表例 — 0回・1回・複数回のサイクル
6. 並行合成の同期点 — 複数コンポーネントの同期イベントを含むトレース

Step 5: 拒否テストケースの生成

トレース集合外のトレースを以下の5つの構成方法で生成する:

1. イベント順序逸脱 — 有効なトレースのイベント順序を入れ替える
2. ガード条件違反 — ガードが偽のときにイベントを発行する
3. 無効なイベント注入 — その状態で定義されていないイベントを挿入
4. 安全性違反トレース — 安全性要求が禁じているシーケンス
5. 失敗集合の活用 — 失敗集合に含まれるイベントをその状態で発行

Step 6: テストケースセットの出力

以下のフォーマットで出力する:

---

テストケース一覧

受理テストケース（トレース集合内）

ID	トレース	検証する性質	サンプリング理由
A-01	⟨e1, e2, e3⟩	活性: e3到達可能性	ビジネスクリティカルフロー
A-02	⟨e1, e2⟩	到達可能性: 状態S2	ガード真分岐

拒否テストケース（トレース集合外）

ID	トレース	検証する性質	拒否される理由
R-01	⟨e2, e1⟩	安全性: 順序制約	イベント順序逸脱
R-02	⟨e1, e4⟩	安全性: 無効遷移	ガード条件違反

カバレッジサマリ

指標	値
状態カバレッジ	N/M 状態（X%）
遷移カバレッジ	N/M 遷移（X%）
活性要求カバレッジ	N/M 要求（X%）
安全性要求カバレッジ	N/M 要求（X%）

---

入力仕様が不完全な場合

• シーケンス図のみ → トレース1本に相当。他のトレースの受理/拒否が不明なためカバレッジが限定的であることをユーザーに通知
• 機能要求なし → 状態機械の構造から推定し確認を求める
• 状態変数の初期値不明 → テストケース生成前に確認する