| name | spec |
| description | CSPの安定失敗モデルに基づく状態機械ベースの形式仕様書を作成するスキル。 機能要求（活性・到達可能性・安全性）を入力として、 状態変数・遷移（イベント[ガード]/事後条件）・失敗集合を定義する トップレベル仕様およびコンポーネント仕様を生成する。 画面表示を持つシステムでは画面表示関数も定義する。
|
| disable-model-invocation | true |
Spec Writer
スコープ
含まれるもの
- 機能要求（活性・到達可能性・安全性）からのトップレベル仕様の作成
- 状態変数・イベント・遷移・失敗集合の定義
- 画面表示を持つシステムでは画面表示関数の定義
- 失敗集合の分析（デッドロック検出を含む）
- コンポーネント仕様への分解とAPI設計書の作成（Phase 4）
含まれないもの
- 機能要求の作成（上流スキル
rdd が担当）
- 機能要求のレビュー（上流スキル
requirements-reviewer が担当）
- 実装コードの生成
- 非機能要求の定義・検証
上流スキルとの連携: rdd（EARS記法要件定義）→ requirements-reviewer（要求レビュー）→ spec（仕様作成）→ 実装
コア概念（クイックリファレンス）
| 概念 | 定義 |
|---|
| イベント | 状態遷移の引き金（UIイベント、通信、τ（内部イベント）） |
| トレース | 初期状態から連続して遷移可能なイベントの列（τを除く） |
| トレース集合 | その状態機械が出せるすべてのトレースの集合 |
| 安定状態 | τで遷移できない状態 |
| 失敗 | 「安定状態に至るトレース」と「その状態で拒否されるイベント集合」の組 |
| 失敗集合 | すべての失敗の集合 |
| 詳細化条件 | 下位仕様のトレース集合・失敗集合が上位仕様のそれぞれの部分集合になること |
詳細な理論的背景は references/notation-guide.md を参照。
仕様記法（インライン）
遷移の基本記法:
イベント名(引数) [ガード条件] / 事後条件
- ガード: 遷移できる事前条件。常に true なら省略可
- 事後条件: 遷移後の変数を
変数名'（プライム）で表現
- フレーム条件: 事後条件に言及されていない変数は変化しない（暗黙）
例:
insert_coin(amount: Nat) [amount > 0 ∧ dispensing = false] /
balance' = balance + amount
press_button(id: ProductId)
[balance >= price(id) ∧ products[id] > 0] /
purchasable' = Some(id)
dispensing' = true
詳細な記法ルール（状態変数規約・遷移表・API記法・並行合成）は references/notation-guide.md を参照。
実行フロー
Phase 1: 機能要求の分析
目標: 入力された要求を3性質に分類し、仕様構築の基盤を作る。
-
要求の分類
受け取った機能要求を以下に分類する:
| 性質 | 定義 | 判別の目安 |
|---|
| 活性 | いつかいいことが起こる | 「～するといつか～が起こる」 |
| 到達可能性 | 特定の状態・動作が可能 | 「～できる」「～に到達できる」 |
| 安全性 | 悪いことが決して起こらない | 「～は発生しない」「～後に～は起きない」 |
-
イベント一覧の抽出
要求から登場するイベントを列挙する。ユーザーに確認:
- 「以下のイベントを想定しています。不足・修正はありますか？」
- 内部イベント（τ）の候補も提示する（例: 自動タイムアウト、バックグラウンド処理）
-
暗黙の前提の確認
要求に明記されていない前提（在庫の存在、残高の上限など）をユーザーに確認する。
Phase 2: 状態機械の構築
目標: 状態変数→イベント→遷移の順で定義し、各ステップでユーザーに確認する。画面表示を持つシステムでは追加で画面表示関数を定義する。
Step 2-1: 状態変数の定義
- Phase 1 で抽出したイベント・性質から必要な状態変数を特定する
- 各変数の型・初期値・値域をユーザーに確認する
変数名 : 型 = 初期値 -- 値域コメント
Step 2-2: イベントの詳細化
- 各イベントの引数の型を決定する
- 内部イベント（τ）を特定する
Step 2-3: 遷移の定義
各イベントについて以下を定義し、ユーザーに確認する:
- ガード条件: どの状態でそのイベントが受理されるか
- 事後条件: 遷移後に何が変わるか（プライム記法で記述）
フレーム条件の徹底: 変化しない変数は事後条件に書かない。
Step 2-4: 画面表示関数の定義（画面表示を持つシステムのみ）
画面表示のないソフトウェア（バックエンドサービス、バッチ処理、ライブラリ等）はこのステップをスキップする。
screen(state) =
case 条件1 => 画面A(...)
case 条件2 => 画面B(...)
default => デフォルト画面
すべての状態で画面が定義されていることを確認する。
Phase 3: 完全性チェック
目標: 仕様が機能要求を満たすことと、デッドロックがないことを確認する。
3-1: トレース分析（3性質の充足確認）
| 性質 | 確認方法 |
|---|
| 活性 | 活性要求で要求されるイベント列が遷移定義から導けるか |
| 到達可能性 | 対応するトレースが実際に初期状態から到達可能か |
| 安全性 | 禁止された振る舞いを引き起こす遷移がないか（ガード条件で排除されているか） |
3-2: 失敗分析（デッドロック検出）
各安定状態について:
- その状態で受理されるイベントと拒否されるイベントを列挙する
- すべての安定状態で少なくとも1つのイベントが受理されることを確認する
- 拒否イベントが失敗集合として正しく定義されているか確認する
デッドロック: 安定状態ですべてのイベントが拒否される状態。仕様バグ。
Phase 4: コンポーネント分解（オプション）
適用条件: 仕様が大きく、人間が理解しやすい小さなコンポーネントに分解したい場合。
4-1: 分解方針の決定
ユーザーに確認:
- 「どのような観点でコンポーネントを分けますか？（例: UI/ロジック/DB、ユーザー側/システム側）」
4-2: コンポーネント仕様の定義
各コンポーネントについて:
- 担当する状態変数
- 担当するイベント（同期/非同期の区別）
- 遷移定義
4-3: 同期イベント集合の宣言
合成後の仕様 = ComponentA [| SyncEvents |] ComponentB
SyncEvents = { イベント名1, イベント名2 }
4-4: 詳細化条件の確認
並行合成後のトレース集合 ⊆ トップレベル仕様のトレース集合
並行合成後の失敗集合 ⊆ トップレベル仕様の失敗集合
4-5: API設計書の作成
同期イベントを Design by Contract 形式で記述する:
operation_name(params) -> ReturnType
requires: 事前条件（満たされない場合は何をしてもよい）
ensures: 事後条件（リクエストとレスポンスの関係）
出力仕様
ファイル名
<システム名>-specification.md
例: vending-machine-specification.md
出力構成（10セクション）
# <システム名> 仕様書
## 1. 概要
- 対象システム、スコープ
## 2. 機能要求（入力）
- 要求一覧（活性/到達可能性/安全性の分類付き）
## 3. 状態変数定義
- 変数名・型・初期値・値域
## 4. イベント定義
- イベント一覧（引数・種別・説明）
## 5. 遷移定義
- 各イベントの [ガード] / 事後条件
## 6. 画面表示定義（画面表示を持つシステムのみ）
- screen(state) 関数
## 7. 失敗分析
- 各安定状態で拒否されるイベント一覧
- デッドロックなしの確認
## 8. 機能要求との対応確認
- 各要求が仕様で充足されていることの確認
## 9. コンポーネント仕様（Phase 4 実施時のみ）
- コンポーネント定義・同期イベント・API設計書
リファレンス
| ファイル | 内容 |
|---|
references/notation-guide.md | 記法の詳細ガイド（状態変数規約・遷移表・API記法・並行合成記法） |
references/vending-machine-example.md | 自販機の完成例（入力→出力の全ステップ） |
