TLA+ 仕様書レビュー

パース、シンボル抽出、スモークテスト、ベストプラクティスチェックリストを含む、TLA+ 仕様書の包括的なレビューを実行します。

重要: 上記の MCP ツールを常に使用してください。Bash 経由で Java または TLC コマンドを実行することは避けてください。

使用方法

/tla-review test-specs/Counter.tla
/tla-review test-specs/Counter.tla test-specs/Counter.cfg
/tla-review test-specs/Counter.tla --no-smoke

注記: 最初の引数として @path.tla と入力した場合、このスキルは先頭の @ を削除し、ファイルが存在することを検証します。

このスキルの動作

1. 引数から仕様ファイルパスを検証および正規化します
2. SANY パーサーを実行して構文と意味論をチェックします
3. シンボルを抽出して仕様構造を分析します
4. スモークテストを実行します(--no-smoke フラグがない場合)
5. 推奨事項付きの包括的レビューレポートを生成します

実装

ステップ 1: 仕様パスの正規化

このスキルの引数として指定された仕

...