デザインリースの検証は何をしますか？

crates/server/tla/DesignLeases.tla は、1つのストアを共有する2台のFiniteサーバーと、それらの間を移動する1つのデザインのTLA+モデルです。TLA+モデルチェッカーであるTLCは、小さな境界内で全てのステップ順序を試行し、2つのルールをチェックします:

StoredEditsStay (フェンシング): ストアが編集を受け入れた後、他のサーバー上の古いコピーがそれを上書きすることは決してありません。これが破られると、停止していたサーバーが復帰し、新しい所有者が保存した編集を消去します。
AckedEditsStay: MCPツールが完了したと報告した編集は、その編集が保存される前にサーバーがクラッシュしたりリースが期限切れになっていない限り、ストア内、またはそれを保存できるコピー内に存在します。これが破られると、エージェントは編集が成功したと通知され、その後編集は消失します。閲覧者はそれが消えるのを見ますが、エージェントには何も通知されません。

現在のコードは最初のルールをパスし、4つの既知の方法で2番目のルールを破ります。それらは下記の「既知の問題」にリストされています。

あなたの変更はこれに触れますか？

はい、以下の表のいずれかの関数を変更する場合。各モデルステップはそれが表すコードに名前を付けており、レビュアーは両方を並べて開くことができます。

モデルステップ	コード
`CallStarts`, `CallFindsHandle`, `CallLoads`, `CallEdits`, `CallReads`	`mcp/mod.rs` `design`, `edit_checked`; `api.rs` `open`; `hub/mod.rs` `Hub::open`, `handle_for`; `hub/design.rs` `DesignHandle::load`, `edit`
`SaveTakes`, `SaveWrites`, `SaveFenced`, `SaveFails`, `SaveReleases`, `SaveDrops`	`hub/mod.rs` `persist`; `hub/design.rs` `take_save`, `save_failed`
`Unload`	`hub/mod.rs` `Hub::sweep`; `hub/design.rs` `unload_if_idle`, `is_idle`
`TickRenews` … `TickDiscovers`	`hub/mod.rs` `Hub::tick`, `let_go`, `remove`, `drop_copy`, `discover`, `summaries`; `hub/design.rs` `retire`, `end`, `lease`
`Owns`, `LeaseLapses`, `HeartbeatExpires`	`cluster.rs` `Members::now`, `lapsed`, `renewed`, `Cluster::owns`, `owner`
`CanClaim`, `Claimed`, store writes	`postgres/mod.rs` `claim`, `save`, `append`, `release`, `held`; `store.rs` `trait Store` (インメモリ共有ストアは一致する必要があります)
`Start`, `Crash`	`hub/mod.rs` `Hub::shared`

パスは crates/server/src/ 以下です。

同期コミット: 6606714。 これはモデルがこのコードに対してチェックされた最後のコミットです。それ以降にカバーされたコードで何が変更されたかを確認するには、次を実行します:

git diff 6606714 -- crates/server/src/hub crates/server/src/mcp/mod.rs crates/server/src/api.rs crates/server/src/cluster.rs crates/server/src/postgres/mod.rs crates/server/src/store.rs

差分が表内の関数に触れている場合、パスを信頼する前に、その隣にあるモデルステップを再読してください。新しいコミットで変更された各ステップがまだコードと一致することを確認した後にのみ、このファイル内の同期コミットを進めてください。

実行方法

crates/server/tla/check.sh          # 日常チェック、約2分
crates/server/tla/check.sh --full   # Finding4.cfg と AllFixes.cfg を追加、さらに約3分

スクリプトは最初の実行時にTLC（tla2tools.jar v1.7.4、SHA-256チェック済み）を ~/.cache/finite にダウンロードします。Java 11以降が必要です。各設定は、これまでのコードに対して記録された結果を出力するときに ok を表示し、そうでない場合は FAIL を表示します。ルールが破られた場合、TLCの出力（違反への最短パスを含む）は crates/server/tla/<設定名>.out として保存されます。Gitはこれらのファイルを無視します。

設定名	修正対象	境界	現在の結果
`Fencing.cfg`	なし	1編集, 1読み取り, 2ハンドル, 最大18ステップのすべての動作	パス、約280万状態、2分
`DesignLeases.cfg`	なし	1編集, 2ハンドル	問題1、数秒
`Finding2.cfg`	FixRetire	1編集, 2ハンドル	問題2
`Finding3.cfg`	FixRetire, FixOrphan	2編集, 2ハンドル	問題3
`Finding4.cfg`	+ FixStaleDrop	2編集, 2ハンドル	問題4、約1分
`AllFixes.cfg`	全て	2編集, 2ハンドル	パス、約1600万状態、2分

すべての設定はストアのエポックを3に制限しており、クラッシュや書き込み失敗は含みません。読み取りとは、MCP読み取りツールやビューワーのソケットのように、編集せずにデザインをロードする呼び出しです。フェンシングには読み取りが必要です。なぜなら、古いコピーが存在できるのは2つの呼び出しがデザインをロードした場合のみだからです。読み取りを含む完全な状態空間は30分以内に終了しなかったため、check.sh はTLCの反復深化（-dfid 18）で実行します: 最大18ステップのすべての動作。最も短い古い上書きは17ステップかかります。問題の設定は、その境界内のすべてを探索します。TLCは最初に破られたルールで停止するため、各問題設定はその前の問題に対する提案された修正を有効にします。Fix* 定数はwhat-ifスイッチです。それらすべてが FALSE の場合、モデルは現在のコードそのものです。

結果の読み方

各結果は /statechart スキルを使用して読みます。これにより、破られたルールへのTLCの最短パスが平易な言葉で番号付きのステップリストに変換され、設定がパスする場合は、デザインがサーバー間をどのように移動するかのチャートが描画されます。

設定が FAIL を出力した場合、バグがコードにあるのかモデルにあるのかを判断します:

実際のバグ は、コードで再現可能なパスを生成します。各ステップをウォークスルーし、表から関数を開き、コードがその順序でそのステップを許可することを確認します。次に、下記の問題と同様に、コードの言葉でパスを報告します。チェックがパスするまでルールや境界を弱めず、依頼されない限りプロダクトコードを変更しないでください。
モデリングエラー は、コードが取ることのできないステップを生成します。例: コードが1つのロック（状態ミューテックス、永続化ミューテックス）の下で実行する2つのステップがモデルで分割されている、コードが持つガードがないモデルステップ、または更新直後にハートビートが期限切れになる場合などです。モデルをコードに合わせて修正し、修正した内容を説明します。
Fencing.cfg の違反は深さ制限実行から発生し、そのパスはステップに名前を付けません。名前付きの最短パスを取得するには、同じ設定を幅優先で実行します: cd crates/server/tla && java -cp ~/.cache/finite/tla2tools-1.7.4.jar tlc2.TLC -workers auto -config Fencing.cfg DesignLeases.tla。最初の違反で停止します（「カバーされたコードを意図的に変更する場合」の違反では約6秒かかりました）。
error はTLCが完了しなかったことを意味します: パースエラー、またはアクションが未割り当ての変数を残す場合です。.out ファイルを読んでください。

コードが以前はルールを破っていたが現在はパスする場合の FAIL は良いニュースです。「既知の問題」の下にある問題テーブルは、それを記録する方法を示しています。

カバーされたコードを意図的に変更する場合

コードと同じコミットでモデルステップを変更し、関数に名前を付けるコメントを維持します。
変更が問題を修正する場合、修正をスイッチとしてではなくコードとしてモデルに配置します: Fix* 定数を削除し、ステップが新しいコードと同様に動作するようにし、すべての設定からスイッチを削除します。次の問題の設定がデフォルト設定になり、check.sh は新しい期待される結果を取得します。
パスを信頼する前に、スクラッチコピーでコードを意図的に壊し、モデルにもその破損を反映させ、設定がそれをキャッチすることを確認します。例えば、PgStore::save から AND epoch = $3 を削除し、SaveWrites から x.ptok = store.epoch を削除すると、Fencing.cfg が StoredEditsStay を破ります。一度も失敗を見たことがないチェックは何も証明しません。
check.sh --full を実行し、同期コミットを進めます。

既知の問題

それぞれは 6606714 のコードに対する競合状態です。それぞれにおいて、エージェントのツール呼び出しは成功を返しますが、編集は消失します。

保存中の最後のスナップショットを持つコピーに編集が着地する。 サーバーAがデザインをロードしており、MCP呼び出しが Hub::open を通過しました。サーバーBが参加し、デザインを獲得します（Aのリース期限切れでも発生します）。Aのtickが let_go を呼び出し、retire がコピーを Retiring とマークします。保存タスクの take_save が最後のスナップショットを取得します。その後、呼び出しの DesignHandle::edit がロックを取得し、edit が life を決して確認しないため、退避中のコピーにコミットします。保存タスクは編集なしでスナップショットを保存し、リースを解放し、drop_copy が pending をクリアします。Bは編集なしでデザインをロードします。実際のアプリでこれをトリガーするには、tickが実行される時点で既に編集がデザインのロックで待機している必要があります（例えば、複数のエージェントが大きな write_html 呼び出しを実行している場合）。元に戻す、やり直し、インポート、コメントの更新も同じパスを取ります。
ハブが既にリストから削除したハンドルに編集が着地する。 呼び出しの handle_for がロードされていないハンドルを返します。Bが参加し、Aの let_go は何もロードされていないと見なして remove を呼び出します。呼び出しの load がリースを主張し、そのハンドルにコピーをロードします。次のtickの loaded リストはハブのリストから取得されますが、このハンドルはもう含まれていません。そのため、tickはリースを解放し、コピーの次の保存は Fenced で失敗します。これには停止は必要なく、サーバーが参加するだけです。
tickがコピーを読み取った後で再ロードされたコピーをtickがドロップする。 1台のサーバー、メンバーシップ変更なし。tickが lease()（トークン1）を読み取ります。その後、デザインがアンロードされ、呼び出しが再ロードし（トークン2）、編集をコミットします。tickが held()（トークン2）を読み取り、2 ≠ 1 であることを確認し、drop_copy を呼び出します。drop_copy は新しいコピーを終了させ、保留中の編集もすべて破棄します。ウィンドウは2回の読み取りの間にあるため狭いですが、すべてのtickで実行されます。
リースを更新したばかりのサーバーが古いコピーを提供する。 Bがリース期限を過ぎて停止し、Aがデザインを引き継いで編集を保存します。Bが復帰します。そのtickがハートビートを更新し、その瞬間から Members::now はBを生きているとみなし、再び所有者とします。しかし、let_go ループはまだ実行されていません。B上の呼び出しがまだ Live の古いコピーをロードし、編集をコミットしますが、後で Fenced で失敗します。これには最初に停止が必要です。

AllFixes.cfg は各問題に対して1つの提案された修正をチェックします: edit は Live でないコピー（1）またはリストにないハンドル（2）を拒否します。tickは、そのトークンが読み取ったトークンである場合にのみコピーをドロップします（3）。停止後に更新したサーバーは、let_goするまで自身を除外します（4）。これら4つすべてで、AckedEditsStay はこれらの境界で成立します。

これがカバーしないもの

1つのデザイン、2台のサーバー、MCP編集。元に戻す、やり直し、インポート、コメント、名前変更は同じロックとコミットのパスを取りますが、個別にはモデル化されていません。Hub::delete も同様です。
ファイルストアと FINITE_NODES のハンドオフ（hand_off_one、adopt）、およびルーター。
シャットダウン時の Hub::flush、ジャーナル圧縮しきい値（COMPACT_AFTER、COMPACT_BYTES）、およびビューワー再開の背後にあるバッファ Recent。
タイミング。TLCはすべてのステップ順序を試行するため、モデルは競合が存在することを示しますが、その発生頻度は示しません。サーバー自身のリースタイマー（Members::lapsed）は、データベースがハートビートを期限切れと見なす時点より遅くならないと仮定しています。これは2つのクロックが同じ速度で動作する場合に成り立ちます。
より大きな境界。より多くの編集、読み取り、ハンドル、またはエポック、クラッシュや書き込み失敗は日常の設定には含まれていません。AllFixes.cfg は1編集、1クラッシュ、1書き込み失敗（340万状態）でもパスしました。18ステップを超えるフェンシングはまだ完了していません: 1編集と1読み取りで5000万の異なる状態をパスし、まだ進行中でした。読み取りなしの古いフェンシングパスは信頼しないでください: 1つの編集だけで1つのコピーのみがロードされるため、古くなるものは何もありません。

デザインリースの検証