statechart

Statechart

このチャートは、アプリのユーザーに何が表示されるかを示します。PM は、表示される挙動が適切かどうかを判断するために読みます。各状態には「支払い中」のように画面に表示される内容を、各ステップには「支払うをタップする」や「請求が通る」のようにユーザーが行うこと、または起きるのを見ることを示すラベルを付けます。ラベルに変数名やアクション名を含めないでください。スクリプトでは、このユーザーを reader と呼びます。たとえば、readerActions や reader steps で使われます。

コマンドとチャートの読み方については、node <skill dir>/scripts/statechart.mjs --help を実行してください。リポジトリの外にあるスクラッチフォルダーで作業してください。コマンドは入力ファイルと同じ場所にファイルを書き出します。

方向を選ぶ

TLA+ モデルがある場合、またはコードが具体的でモデル化できる場合は、from-spec を使います。モデルがなく、コードを書く、または変更する前に PM が挙動に合意する必要がある場合は、from-chart を使います。

コードに TLA+ 仕様がすでにある場合は、その仕様のコピーから始めます。ユーザーに見える変数を追加し、仕様に既存の不変条件をそのまま残します。仕様に照らしてコードを監査するには、コードが実際に行うことをコピーにモデル化し、変更していない仕様を --against として渡します。新しい仕様では、すべての変数とアクションをレビュー担当者が確認できるコードに対応付け、その名前はコードから取ります。各アクションは、コード内の分割できない 1 ステップにします。

仕様からチャートへ

1. チャートの状態を選びます。PM が画面に表示されない内容を重視する場合（たとえば画面には「支払い中」と表示されたまま、2 回目の請求が発生する場合）は、状態を「支払い中、二重請求」と名付けます。状態は少数から始め、状態の分割によって 2 つのバグを区別できる場合にのみ分割します。
2. PM が合意する各ルールを 1 つの不変条件として記述し、PM の文をそのコメントにします。すべてが落ち着いた後に適用されるルールには、Settled == ~ENABLED System を定義します。ここで System は、ユーザーが行わないアクションの選言です。破られたルールはそれぞれバグとして報告します。チャートを通すためにルールを弱めてはいけません。
3. from-spec を実行し、書き出されたマッピングファイルを完成させます。ラベルは state と step に記述し、ユーザーのアクションはアクション名で readerActions に列挙します。異なるコードパスを経て 2 つのバグが同じ画面で終わる場合は、cause を追加し、コードパスを示す名前を付けます。PM が重視する項目（「トーストが表示される」など）で状態に色を付けるには、そのグループを group から返します。凡例にグループ名が表示され、ルールを破る状態には引き続き赤い枠線が付きます。
4. 修正が未適用の場合は、コードに基づいてモデル化し、そのモデルを --fixed として渡します。
5. 各チャートを --png でレンダリングし、すべての PNG を確認します。番号付きの各経路が順番どおりに読めることを確認します。ラベルがコードのように見える場合は、state または step を修正してコマンドを再実行します。
6. 各バグのストーリーを、モデルの各アクションにつき 1 ステップずつ、テストまたは実際の再現手順として実コードで再現します。バグが再現しない場合は、そうでないことを示せるまではモデルが誤っていると考えます。ルールではなくモデルを修正します。

チャートから仕様へ

1. PM が合意するチャートを描きます。接続や同期バッジなど、独立して変化するものごとに領域を 1 つ使います。各ルールにつき、PM の文を添えた %% never の行を 1 つ追加します。「アプリが閉じる」は、ユーザーが次に見る状態へのエッジとして描きます。
2. from-chart を実行します。ルールが破られる場合は、合意したチャートに設計上のバグがあります。そのバグを PM に伝えます。
3. 実コードのガードと変数を、from-chart が書き出した仕様に追加し、もう一度 from-chart を実行します。出力される差異ごとに、コードが誤っているのか、チャートを修正する必要があるのかを PM に確認します。

引き継ぎ

各チャートの PNG と Mermaid ソースを PM に渡します。各バグについて、破られるルール、チャート上の番号に沿ったステップ、再現したかどうか、未適用の修正で解決するかどうかを 1 行で記載します。引用する件数はすべて summary.json から取得します。stories.md と、すべてを再生成するコマンドを添付します。モデルが扱っていない内容も伝えます。