statechart

Statechart

チャートは、これを読む人の言葉で、システムが状態間をどのように遷移するかを示します。読む人は、その動作が正しいかどうかを判断します。

実行

リポジトリの外にスクラッチフォルダーを作業用に用意します。TLA+ 仕様とその設定ファイルを作成します。次に、以下を実行します。

<skill dir>/scripts/statechart SPEC.tla [--config FILE] [--view FILE] [--out DIR]

scripts/statechart.ts は TypeScript なので、TypeScript を実行できるランタイムで実行してください。

初回の実行では mise を使って TLC と Java をインストールするため、ネットワーク接続が必要です。

仕様を書く

• 読む人が同意する各ルールを INVARIANT として記述します。ルールは画面、結果、保存された値、メッセージに関するものでもかまいません。モデルにルールに対応する変数がない場合は、その変数を追加します。ルールが成り立つように、決して弱めてはいけません。
• Next は、YouPressPlay \/ YouPressStop のように、アクションの選言として記述します。そうしないと、TLC はすべてのステップを Next と命名します。
• 次のステップがない状態は、正しい終了状態であっても NoDeadlock に違反します。INVARIANT または PROPERTY にすでにその名前がある場合、ルール名は CHECK_DEADLOCK になります。Next に、終了状態でのみ真となり、何も変更しないアクションを追加します。たとえば Done == phase \in {"paid", "failed"} /\ UNCHANGED vars のように記述し、step() でラベルを付けます。

チャートを選ぶ

判断が必要な作業を行います。各状態と矢印に表示する文言、フェーズと色、タイトル、読者向けのレポートを決めます。作業内容をビューのモジュールに記述し、--view で指定します。

読者向けの文言を表示するには、ビューから state(vars) をエクスポートします。state() の戻り値によって、チャートの形式が決まります。

• 文字列を返すと、フラットなチャートになります。export const state = (v) => (v.paid ? "Paid" : "Paying");
• 配列を返すと、親状態が表示されます。export const state = (v) => v.main.split(".");
• オブジェクトを返すと、キーごとに並列領域が表示されます。export const state = (v) => ({ Playback: v.playback, Volume: v.volume });

各状態には、「支払い中」や「リース取得済み、書き込み保留中」など、読者が目にすることや気にかけることを示すラベルを付けます。ラベルに変数名を含めないでください。vars では、TLA+ のシーケンスは 1 から始まるキーを持つオブジェクトなので、v.pc[1] は pc[1] です。集合は配列です。

ビューから step(action, from, to) をエクスポートすることもできます。これは TLC のアクション名と、ステップの前後の値を受け取り、矢印のラベルを返します。「再生ボタンを押す」や「接続に失敗する」のように、ステップが起きたときにユーザーが目にする表現でラベルを書きます。コード名や TLA+ のアクション名は書かないでください。チャート上で同じ状態に行き着く 2 つのアクションには同じラベルを付け、1 つの矢印にまとめます。

ステップが特定の条件下でのみ発生する場合は、「ファイルの読み込み中」のように、読者に伝わる言葉で条件を角括弧に入れてラベルの末尾に付けます。例：you press play [while the file loads]。領域チャートでは、コマンドが矢印に他の領域の条件をラベルの文言で表示します。例：[when Offline]。角括弧を付けると、その表示が置き換わり、同じ状態から出る 2 つの矢印が同じに見える場合があります。そのため、領域チャートでは、別の領域に関する条件を角括弧で書かないでください。どのラベルにも表示されない値によってステップの遷移先が決まる場合は、「名簿の読み込みに失敗する」のように、結果をラベルに含めます。

ビューから次の要素もエクスポートできます。

• group(vars) はフェーズ名を返します。各チャート状態は、そのグループの色になります。1 つのチャート状態の背後にあるモデル状態が異なるグループに属する場合、その状態には色が付きません。
• colors は各グループ名に色クラスを割り当てます。
• title は、チャートの上部に表示する文字列です。

コマンドはモデル状態ごとに state() と group() を最大 1 回、ステップごとに step() を最大 1 回呼び出します。チャートとレポートはどちらもその戻り値を使います。そのため、各関数は引数のみに依存するようにしてください。

同じラベルの状態にとどまるステップはチャートに描画されません。そのようなステップを読者に見せる必要がある場合は、ラベルを分けてください。

矢印は 20 本以下を目安にしてください。矢印が多すぎるとチャートが読みづらくなります。まず state() がより粗いラベルを返すようにします。同じように動作する値には同じラベルを付け、読み込み中の呼び出しのうち、戻り値が何も変えないものなど、読者が必要としない詳細は省きます。バグ経路の各状態と、各マークは残してください。マージによって breaks 状態が mayBreak に変わると、どこでルール違反が起きるかが見えなくなります。異なるルールに違反する 2 つの状態はマージしないでください。そうすると、読者がどのルールにどこで違反するのか分からなくなります。チャートがまだ煩雑な場合は、すべての状態にあるリセットや、他の矢印が示す内容を繰り返す矢印など、読者に必要のないステップについて step() が null を返すようにします。ステップを省く場合は、次のルールに従ってください。

• 各チャート状態に、開始状態から矢印をたどって到達できるようにします。
• モデル内で外向きのステップがある各チャート状態に、少なくとも 1 本の矢印を残します。
• 1 本の矢印に含まれるステップは、すべて隠すか、まったく隠さないようにします。一部だけ隠すと、その条件がより限定されます。
• 引き継ぎ時に、チャートで隠したステップを明記します。

レポートを読む

• チャートでは、ルールに違反する状態に breaks クラスが付きます。その状態の背後にあるモデル状態の一部だけがルールに違反する場合は、mayBreak クラスが付きます。凡例には各マークのルールが示されます。2つのルールに違反する場合、1つのマークに両方のルールが示されるため、引き継ぎでは、どの状態がどのルールに違反するかを伝えてください。領域チャートでは、その状態を含む領域状態の各組み合わせがルールに違反する可能性がある場合、その状態にマークが付きます。ある組み合わせがルールに違反する可能性があり、その組み合わせのどの状態にもマークが付いていない場合、その組み合わせの各状態にマークが付きます。
• TLC はルールに違反する状態を通り越すため、チャートにはバグの後の状態も表示されます。
• TLC はバグを通り越すため、状態数に上限のないモデルは終わりなく実行される可能性があります。定数を小さくするか、CONSTRAINT を追加してください。
• VIEW または SYMMETRY がある場合、TLC は同一とみなす状態を1つの状態として数え、チャートにもその1つの状態を描画します。矢印は、ステップで到達する状態ではなく、その状態に向かうことがあり、レポートにもその旨が示されます。
• TLC は CONSTRAINT または ACTION_CONSTRAINT を通り越した各状態でルールをチェックしますが、その状態を探索せず、デッドロックもチェックしません。ルールに対する TLC の最短パスがそのような状態で終わる場合、チャートにはその状態が描画され、レポートにはそのパスが示されます。上限を超えたその他の状態はチャートに描画されません。そのような状態のデッドロックは表示されません。また、TLC は ACTION_CONSTRAINT によって除外される各ステップの後でもルールをチェックします。別の経路で次の状態に到達した場合も同様です。ルールに対する TLC の最短パスがそのようなステップで終わる場合、チャートにはそのステップが描画されます。
• このコマンドは、記述されたとおりの設定で、1つのワーカーを使って TLC にルールをチェックさせます。ルールに違反した場合、コマンドはそのルールを削除して TLC を再実行し、違反するルールがなくなるまで繰り返します。最初の違反の後は、各実行で異なる状態を100,000個検出した時点で停止するため、大きなモデルが終わりなく実行されることはありません。実行がこの上限に達した場合、またはエラーで停止した場合、レポートの「Rules not checked」にはチェックされなかったルールが列挙され、チャートにはそれらのマークが付きません。チェックされなかったルールは、成立する場合も違反する場合もあります。チェックするには、設定から違反するルールを削除するか、モデルを小さくしてください。この上限は TLC の変数の順序を変更するモジュールを追加するため、あるプロパティについて、TLC が上限なしの実行とは異なる反例を見つけることがあります。
• tlc.out には、記述されたとおりの設定で TLC が出力した内容が記録されます。チャートに違反するルールのバグパスが表示されない場合、tlc-RULE.out には、そのバグを見つけた実行で TLC が出力した内容が記録されます。TLC が最初の警告を繰り返すと、通常の TLC はその警告を2回出力しますが、tlc.out には1回だけ表示されます。これは、このコマンドが読み取る出力から、TLC が2回目の出力を除外するためです。これは Java が -XX:+UseParallelGC で実行される場合に限って起こります。それ以外の場合、TLC の最初の警告はそのフラグを渡すよう促す内容であり、TLC はそれを1回だけ出力するためです。

チャートを表示する

chart.mmd を mermaid コードブロックとしてユーザーに表示してください。チャートの上限は、記述されたとおりの設定で TLC が数えた状態数500個です。それを超えると、チャートには違反するルールへのパスだけが描画され、違反するルールがない場合、コマンドは chart.mmd を出力しません。各ルールのチェックは引き続き行われ、レポートには状態数と各バグパスが記載されます。グラフ全体を見るには、モデルを小さくしてください。

チャートのレンダリングには Pele を使ってください。ユーザーが画像を求めた場合、またはチャートが大きすぎてテキストでは読みにくい場合は、references/render.md に従ってください。ユーザーが求めない限り、別のレンダラーは使わないでください。

引き継ぐ

各チャートとその Mermaid テキストを、判断を行う担当者に渡してください。各バグについて1行ずつ、ルール、そのルールを読んだ人が説明する文、レポートに記載されたパスを記してください。モデルが対象に含めていないものも伝えてください。新しい --out フォルダーを指定して、ファイルを再生成するコマンドも伝えてください。

モデルがコードを記述している場合は、各バグパスを実際のコードに対して再現し、各アクションにつき1ステップずつ、テストまたはライブ再現として実施してください。バグが発生しない場合は、そうではないと示すまではモデルが間違っていると考えてください。