statechart

ステートチャート

このチャートは、読む人の言葉で、システムが状態間をどのように移行するかを示します。スクリプトでは、その人を reader と呼び、readerActions や reader ステップで使っています。振る舞いが正しいかどうかを判断するのは reader です。reader は、製品フローを読む PM、プロトコルやサービスを読むエンジニア、設計を読むレビュアーなどです。各状態には、アプリの「支払い中」やロックサービスの「リース取得済み、書き込み待ち」のように、reader が観察できることや関心を持つことを付けます。各ステップには、アプリの「支払いをタップする」、サービスの「リクエストが件数を読み取る」、ロックサービスの「リースが期限切れになる」など、システムを動かすイベントを付けます。ラベルには変数名やアクション名を使わないでください。

node <skill dir>/scripts/statechart.mjs --help を実行すると、コマンドとチャートの読み方を確認できます。リポジトリの外にスクラッチフォルダーを用意して作業してください。コマンドは入力ファイルと同じ場所にファイルを書き込みます。初回の実行では mise を使って TLC と Java がインストールされます。この処理では約 305 MB がダウンロードされるため、ネットワーク接続が必要です。TLC と Java をすでに用意している場合の使い方は、ヘルプの TLC の項を確認してください。

方向を選ぶ

TLA+ モデルが存在する場合、またはコードや設計がモデル化できるほど具体的な場合は、from-spec を使います。モデルがなく、実装や変更に着手する前に振る舞いの所有者間で合意しておく必要がある場合は、from-chart を使います。

コードにすでに TLA+ 仕様がある場合は、その仕様のコピーを出発点にします。ラベルとルールに必要な変数を追加し、既存の不変条件はそのまま残します。その仕様に照らしてコードを監査するには、コードの動作をモデル化したコピーを作成し、変更していない仕様を --against として渡します。仕様の作成者が合格するとしている設定でチェックし、その設定のファイル名が仕様のファイル名と異なる場合は、--against-config として渡します。1 つのマッピングで両方のモデルにラベルを付けるため、両方に存在する変数から状態とステップにラベルを付けます。コピーにしかない変数を参照するラベルでは、まず "name" in v をテストし、仕様の状態には別の方法でラベルを付けてください。モデルでコードを表す場合は、各変数とアクションを、レビュアーが確認できるコードに対応付け、その名前にはコード内の名前を使います。各アクションは、コード上の分割できない 1 つのステップにします。アクションの各条件を確認するコードのファイル名と行番号を、その条件のコメントに記載してください。例：\* pay.ts:120。

仕様からチャートを作成する

1. チャートの状態を選びます。ラベルでは隠れてしまう情報を読者が重視する場合は、「二重に請求されたまま支払い中」のように、その情報をラベルに含めます。最初は状態を少なくします。分割によって別々のバグを区別できる場合や、件数を読み取るリクエストのように、ラベルが変わらないステップを読者が確認する必要がある場合は、状態を分割します。チャートにはそのようなステップが描かれないためです。
2. 読者が合意した各ルールを、読者の文をコメントとして添えた不変条件にします。ルールは、モデル内のどの状態についても記述できます。画面に表示される内容、リクエストの戻り値、保存された値、または各部分間のメッセージが対象になります。モデルがコードを記述する場合、ルールにはその状態を変更できるコードも示します。ルールの対象となる変数がモデルにない場合は、その変数を追加します。ルールを削除してはいけません。すべてが落ち着いた後に適用されるルールには、Settled == ~ENABLED System を定義します。ここで System は、読者が関与せずに発生するアクションの選言です。リクエストの完了後など、より限定された時点で適用されるルールには、その時点を表す述語を記述し、それが真となる箇所でルールを成立させます。システムが到達できなければならない目標については、その目標が決して発生しないとするルールを記述し、そのルールを --expect-broken とともに実行します。そのルールに違反する経路が、目標への到達方法になります。チャートには、ルールに違反する状態として目標が描かれ、stories.md ではバグとして説明されるため、引き継ぎ資料で各目標ルールに名前を付けてください。それ以外のルール違反はすべてバグとして報告します。チャートを通すためにルールを弱めてはいけません。
3. from-spec を実行し、出力されたマッピングファイルに内容を記入します。ラベルは state と step に記述します。チャートで読者の操作と読者の周囲で起きることを区別する必要がある場合は、アクション名で読者の操作を readerActions に列挙します。すべてのアクションを同じように扱う場合は、リストを空のままにします。概要が大きすぎて読めない場合は、--cover を追加します。この場合、概要には落ち着いた各状態への最短経路と、すべてのバグ経路だけが残され、コマンドは省略した内容を一覧表示します。異なる理由で2つのバグが同じ状態で終わる場合は、cause を追加し、それぞれの理由を表す名前を付けます。「注文を出荷済み」のように読者が重視する内容で状態を色分けするには、そのグループを group から返します。凡例にはグループ名が表示され、PNG ではルールに違反する状態がグループ色の代わりに赤で表示されます。
4. 修正案がある場合は、それをモデル化し、そのモデルを --fixed として渡します。
5. 各チャートを --png でレンダリングし、すべての PNG を確認します。番号付きの各経路を順番に読めることを確認します。ラベルがコードのように見える場合は、state または step を修正して、コマンドを再実行します。
6. モデルがコードを記述する場合は、各バグのストーリーを、テストまたは実環境での再現によって実際のコードに照らして検証します。モデルのアクションごとに1ステップずつ検証します。ユーザー、クライアント、またはシステムの別の部分が到達できるエントリーポイントのみを操作し、それらが観測できる内容だけをアサートします。自分で設定したフラグをアサートするテストや、ソーステキストを検索するテストには意味がありません。実行によってストーリーの一部が裏付けられ、コードを読むことで残りが裏付けられる場合は、それぞれがどの部分を裏付けるかを記述します。インポートできないコードをテストがコピーしている場合は、そのコピーのコミットと行範囲を示し、コピーで省略されている内容を列挙します。バグが再現されない場合は、そうでないことを示すまではモデルが誤っていると考えます。ルールではなくモデルを修正します。まだコードのない設計では、TLC のトレースが証拠となるため、引き継ぎ資料にその旨を記載します。

チャートから仕様へ

1. 読者が合意したチャートを描きます。デバイスの接続や、そのデバイスが実行するジョブなど、独立して変化する部分ごとに領域を1つ使います。各ルールにつき1行の %% never を追加し、読者の文を記載します。「アプリが閉じる」「プロセスが再起動する」など、ある部分を停止または再起動させるイベントは、次の状態へのエッジとして描きます。render CHART.mmd を実行し、読者にチャートの PNG を渡します。
2. from-chart を実行します。ルールに違反する場合、合意したチャートに設計上のバグがあります。チャートに合意した人たちにバグを伝えます。
3. from-chart が書き出した仕様に、実際のコードのガードと変数を追加し、再度 from-chart を実行します。出力された差分ごとに、コードが間違っているのか、チャートを修正する必要があるのかを読者に確認します。

引き継ぎ

各チャートの PNG と Mermaid ソースを、判断が必要な人に渡します。バグごとに、違反するルール、チャートで番号付けされた手順、再現したかどうか、提案した修正で解消するかどうかを1行で記載します。PROPERTY の反例にはチャート上の経路がないため、stories.md が示す TLC の反例を提示します。--against を使う場合は、その不具合がすでに仕様に記載されているかどうかも伝えます。記載場所は、stories.md が示す設定ファイル、モデルが対象外とする事項についての仕様の注記、または未記載のいずれかです。モデルがコードを記述している場合、コマンドがファイル名と行番号のない条件を列挙しているのに、ルールが成立すると報告してはいけません。引用するすべての件数は summary.json から取得します。stories.md と、すべてを再生成するコマンドを添付します。モデルが対象外とする事項も伝えます。