TLA+に再挑戦（2021.10） - yujioramaの日記

英語のドキュメントを読んだけどあまり理解できてなかったので日本語で再挑戦する会。

今回

第2章の途中から第3章の途中まで読んで試した。

"1.3 時相特性" では、共通する口座に、2つの電信依頼が独立して行われる場合に発生するエラーの可能性を検証してる。 時相特性 という性質を検証してるのが特徴。

PlusCal/TLA+ で記述する評価や代入といった操作からなる "プロセス" は、シングルスレッドで実行する処理だと考えればよい。つまり "マルチプロセス" はマルチスレッド処理になる。

操作や処理はアルゴリズムなので、実装によっては無限にタイムアウトする可能性がある。つまり、マルチスレッド処理しているとして、隣のスレッドがハングアップしてしまうような状況を想定する感じになる。

"図1-7：スタッタリングエラー" は次のような内容になっている。

Name	Value
`<<initial predicate>>`	Step (num = 1)
acc	[alice \|-> 5, bob \|-> 5]
amount	<<1, 1>>
pc	<<"CheckAndWithdraw", "Checkandwithdraw">>
people	{"alice", "bob"}
receiver	<<"bob", "bob">>
sender	<<"alice", "alice">>
`<<CheckAndWithdraw line 51, col 27>>`	Step (num = 2)
acc	[alice \|-> 4, bob \|-> 5]
amount	<<1, 1>>
pc	<<"Deposit", "Checkandwithdraw">>
people	{"alice", "bob"}
receiver	<<"bob", "bob">>
sender	<<"alice", "alice">>
`<<CheckAndWithdraw line 51, col 27>>`	Step (num = 3)
acc	[alice \|-> 3, bob \|-> 5]
amount	<<1, 1>>
pc	<<"Deposit", "Deposit">>
people	{"alice", "bob"}
receiver	<<"bob", "bob">>
sender	<<"alice", "alice">>
`<<Deposit line 59, col 18>>`	Step (num = 4)
acc	[alice \|-> 3, bob \|-> 6]
amount	<<1, 1>>
pc	<<"Deposit", "Done">>
people	{"alice", "bob"}
receiver	<<"bob", "bob">>
sender	<<"alice", "alice">>
`<<Stuttering>>`	Step (num = 5)

本文を読んでもよく分からないのだけど、次のように解釈するといいようだ。

同じ口座を共有する独立した2つの電信依頼が実行されている
- p1, p2 とする
どちらの依頼も送金額は "1" になっている
- amount | <<1, 1>>
- プロセスごとの amount の並びがシーケンスとして印字されている
Step (num = 2) では、p1 の依頼について Checkandwithdraw が行われた
- acc | [alice |-> 4, bob |-> 5]
- 送信者("alice")の口座から送金額 "1" が減っている
Step (num = 3) では、p2 の依頼について Checkandwithdraw が行われた
- acc | [alice |-> 3, bob |-> 5]
- 送信者("alice")の口座から送金額 "1" が減っている
Step (num = 4) では、p2 の依頼について Deposit が行われた
- acc | [alice |-> 3, bob |-> 6]
- 受信者("bob")の口座に送金額 "1" が増えている