菜单
CSPの安定失敗モデルに基づく状態機械ベースの形式仕様書を作成するスキル。 機能要求（活性・到達可能性・安全性）を入力として、 状態変数・遷移（イベント[ガード]/事後条件）・失敗集合を定義する トップレベル仕様およびコンポーネント仕様を生成する。 画面表示を持つシステムでは画面表示関数も定義する。
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
| name | spec |
| description | CSPの安定失敗モデルに基づく状態機械ベースの形式仕様書を作成するスキル。 機能要求（活性・到達可能性・安全性）を入力として、 状態変数・遷移（イベント[ガード]/事後条件）・失敗集合を定義する トップレベル仕様およびコンポーネント仕様を生成する。 画面表示を持つシステムでは画面表示関数も定義する。 |
| disable-model-invocation | true |
rdd が担当）requirements-reviewer が担当）上流スキルとの連携: rdd（EARS記法要件定義）→ requirements-reviewer（要求レビュー）→ spec（仕様作成）→ 実装
| 概念 | 定義 |
|---|---|
| イベント | 状態遷移の引き金（UIイベント、通信、τ（内部イベント）） |
| トレース | 初期状態から連続して遷移可能なイベントの列（τを除く） |
| トレース集合 | その状態機械が出せるすべてのトレースの集合 |
| 安定状態 | τで遷移できない状態 |
| 失敗 | 「安定状態に至るトレース」と「その状態で拒否されるイベント集合」の組 |
| 失敗集合 | すべての失敗の集合 |
| 詳細化条件 | 下位仕様のトレース集合・失敗集合が上位仕様のそれぞれの部分集合になること |
詳細な理論的背景は
references/notation-guide.mdを参照。
遷移の基本記法:
イベント名(引数) [ガード条件] / 事後条件
変数名'（プライム）で表現例:
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を参照。
目標: 入力された要求を3性質に分類し、仕様構築の基盤を作る。
要求の分類
受け取った機能要求を以下に分類する:
| 性質 | 定義 | 判別の目安 |
|---|---|---|
| 活性 | いつかいいことが起こる | 「～するといつか～が起こる」 |
| 到達可能性 | 特定の状態・動作が可能 | 「～できる」「～に到達できる」 |
| 安全性 | 悪いことが決して起こらない | 「～は発生しない」「～後に～は起きない」 |
イベント一覧の抽出
要求から登場するイベントを列挙する。ユーザーに確認:
暗黙の前提の確認
要求に明記されていない前提（在庫の存在、残高の上限など）をユーザーに確認する。
目標: 状態変数→イベント→遷移の順で定義し、各ステップでユーザーに確認する。画面表示を持つシステムでは追加で画面表示関数を定義する。
変数名 : 型 = 初期値 -- 値域コメント
各イベントについて以下を定義し、ユーザーに確認する:
フレーム条件の徹底: 変化しない変数は事後条件に書かない。
画面表示のないソフトウェア（バックエンドサービス、バッチ処理、ライブラリ等）はこのステップをスキップする。
screen(state) =
case 条件1 => 画面A(...)
case 条件2 => 画面B(...)
default => デフォルト画面
すべての状態で画面が定義されていることを確認する。
目標: 仕様が機能要求を満たすことと、デッドロックがないことを確認する。
| 性質 | 確認方法 |
|---|---|
| 活性 | 活性要求で要求されるイベント列が遷移定義から導けるか |
| 到達可能性 | 対応するトレースが実際に初期状態から到達可能か |
| 安全性 | 禁止された振る舞いを引き起こす遷移がないか（ガード条件で排除されているか） |
各安定状態について:
デッドロック: 安定状態ですべてのイベントが拒否される状態。仕様バグ。
適用条件: 仕様が大きく、人間が理解しやすい小さなコンポーネントに分解したい場合。
ユーザーに確認:
各コンポーネントについて:
合成後の仕様 = ComponentA [| SyncEvents |] ComponentB
SyncEvents = { イベント名1, イベント名2 }
並行合成後のトレース集合 ⊆ トップレベル仕様のトレース集合
並行合成後の失敗集合 ⊆ トップレベル仕様の失敗集合
同期イベントを Design by Contract 形式で記述する:
operation_name(params) -> ReturnType
requires: 事前条件（満たされない場合は何をしてもよい）
ensures: 事後条件（リクエストとレスポンスの関係）
<システム名>-specification.md
例: vending-machine-specification.md
# <システム名> 仕様書
## 1. 概要
- 対象システム、スコープ
## 2. 機能要求（入力）
- 要求一覧（活性/到達可能性/安全性の分類付き）
## 3. 状態変数定義
- 変数名・型・初期値・値域
## 4. イベント定義
- イベント一覧（引数・種別・説明）
## 5. 遷移定義
- 各イベントの [ガード] / 事後条件
## 6. 画面表示定義（画面表示を持つシステムのみ）
- screen(state) 関数
## 7. 失敗分析
- 各安定状態で拒否されるイベント一覧
- デッドロックなしの確認
## 8. 機能要求との対応確認
- 各要求が仕様で充足されていることの確認
## 9. コンポーネント仕様（Phase 4 実施時のみ）
- コンポーネント定義・同期イベント・API設計書
| ファイル | 内容 |
|---|---|
references/notation-guide.md | 記法の詳細ガイド（状態変数規約・遷移表・API記法・並行合成記法） |
references/vending-machine-example.md | 自販機の完成例（入力→出力の全ステップ） |
TerraformプロジェクトのAWSインフラにおけるネットワーク接続性と権限設定を分析します。セキュリティグループ、IAMポリシー、NACLなどを解析し、リソース間の通信可否、不要な接続、権限の過不足を検出します。Terraformファイルやtfstateがあるプロジェクトで、インフラのセキュリティレビューやネットワーク接続の検証が必要な場合に使用します。
要求定義書のレビューを行うスキル。品質チェック・矛盾検出・抜け漏れ検出・曖昧性分析を実施し、 構造化レポートを出力する。以下の場合に使用: (1) 要求定義書・要件定義書をレビューしたい時、 (2) 要求の品質や完全性を確認したい時、 (3) 矛盾・抜け漏れ・曖昧な表現を検出したい時
言語非依存のプログラミングベストプラクティスとガイドライン。コードを書く・関数/クラス/モジュールを実装する・プログラムを新規作成するあらゆる場面でPROACTIVELYに使用すること。コーディング開始前に必ずこのスキルを読み込む。コードレビュー・設計レビューにも使用する。
言語非依存の単体テストベストプラクティスとガイドライン。テストコードを書く・テストケースを追加する・テストスイートを作成するあらゆる場面でPROACTIVELYに使用すること。テストコーディング開始前に必ずこのスキルを読み込む。既存テストのレビューにも使用する。
仕様からテストケースを体系的に生成するスキル。状態機械・自然言語・Mermaid・シーケンス図など多様な入力形式に対応し、CSP安定失敗モデルに基づいて受理テストケース（トレース集合内）と拒否テストケース（トレース集合外）を網羅的に導出する。活性・到達可能性・安全性の3性質を検証するテストスイートを生成する。要求定義・仕様記述・設計成果物からのテストケース生成、テスト設計レビュー、テストカバレッジ分析に使用する。
EARS記法を用いた要件定義書を作成するスキル。要件定義書の作成のみを行い、実装計画や実装は含まない。以下の場合に使用:(1)機能追加や改修の要件を明確化したい時、(2)受け入れ条件やエッジケースを整理したい時