4.3-4.8 ユークリッド法続き
4.3 は、ユークリッド法での最大公約数の求め方。
以前PlusCALを試してみよう - みょらみょらPython日記で同じことを試したのが、少しは役立っている。
基本的にはテキストにそっていけばよいのだが、実行しても「エラーが起きない」だけで肝心の最大公約数は表示してくれないためややわかりにくい。while loopの後に、
print <<"have gcd", x>>;
をいれて実行することでだいぶ理解が早いと思う。
4.4はPlusCALからTLA+への変換、特に while loopがどう実現されるかについて。
translatorがpcという変数を用意してくれて、例えば、while (x < 10) { x++ }というループがあったとすると（これは別にPlusCALの構文じゃない。簡単のため。）、
Loop状態の定義：
pc = loopフラグ でなおかつ
IF x < 10
THEN x' = x + 1 /\ pc' = loopフラグ
ELSE pc' = 終了フラグのように変換する。普通のプログラムと違うのは、 x' = x + 1というのは別に状態遷移を行っているわけではない。x が 7から8になる、のではなく、x < 10かつ「xの次の値はx+1」かつpc=loopフラグで次のpcもloopフラグ、という式を満たす状態があるよ、というスペックを示している。ここはなんとも日本語で説明しにくいところだけれど、慣れるしか無い。
あとはtupleを
<< >>
で表示するとか、TLA+にはUNCHANGEDという文法があるよ、という話。
4.5は、どうやって結果をチェックするのか、という話。ここの章はなぜかハイパーリンクで例がなく、ちょっとつらい。assertを使ったり、Model Checkerでinvariant式をいれてチェックしたり色々出来るよ、といっているだけ。わざとエラーを出させたりするので、わりと進め方も意地悪。
4.6 Checking Liveness
Model Checkerでterminationをチェックするとエラーになる。それは、このスペックは必ずしも終了状態になることを保証してないから、という話。前の本(Chapter 2 Specifying a Simple Clock - みょらみょらPython日記)で、進まない時計の話があったけど、スペックの検査をする上で、状態が進まないで終わることも許している。具体的には
[][Next]_vars
の、_varsの部分は、vars(ここではx, y と、勝手に作られたpc)が変わらないのもありだよ、という意味。PlusCALの書き出しを
--fair algorithm
に変えてやると、Nextにweak fairnessが設定されて、かならず終わるようになる。なんでこんなものがあるかというと、たとえばクライアント・サーバのアルゴリズムをTLA+で書いたとすると、「あるプロセスがずっと待っている」という状態を書く必要があって、別にヨーイドンでゴールまで行くことがうれしいわけじゃない。TLA+のモデルチェッカーとしては、取りうる状態を全部検査できるのがゴールなので。
多分詳しい説明は以降で出てくるので、まあ、そんなもんか、くらいでよい。
4.7 なぜ以下は必要か。
Next == Lbl_1 \/ (pc = "Done" /\ UNCHANGED vars)
Lbl_1は立派なスペックに見えるけど、それでは足りない。なぜか。
大事なのは以下の文。
TLC considers a reachable state from which there is no next state satis- fying the next-state action to be a deadlock error.
行き場がなくなった状態（つまり、すべての変数varsが変化しない状態）はデッドロックとみなされてエラーとなる。終了状態というのは、デッドロックの一つに「これは良いデッドロックだよ」と印をつけたに過ぎない。ここでは、pcがDoneになった上で全ての変数が動かなくなった状態もNextだとありだよ、と言っている。
では、なぜUNCHANGEDは必要なのか。試しに以下のように変えて実行してみた。
Next == Lbl_1
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done")すると、xとyに最大公約数が入ってpcが"Done"になった後、xもyもpcもnullになってエラーとなる。これは、pcが"done"になった際のx', y', pc'の値が定義されていないので起こる。話が前後するけど、最初の文は、以下を簡潔に書いたにすぎない。
Next == Lbl_1 \/ (pc = "Done" /\ x' = x /\ y'=y /\ ... /\ pc' = pc)
4.8 Label
いよいよ粘っこい話題に入ってくる。前の本で読んだはずだけどすっかり忘れている。
ラベルは、PlusCALをTLA+に変換する際に、translatorに区切る単位を教えるためにある。たとえば、
a' = a + 1 b' = b - 1
という２行があったとして、これがかならず一度に実行されるのか、それとも別々に実行されて良いのか、それによって後々並列アルゴリズムを記述するときに大きく違ってくる。translatorは何も書かないと、一番ラベルが少なくなるように変換してくれる。当然そうすると、試す状態の数が減るので処理は速くなる、が、その分バグをみつけられないかもしれない。
ラベルは、以下の場合には必ず必要：
- アルゴリズムの最初の文
- Whileループ
上記のユークリッド法の例では、whileループが最初の文なので、勝手にLbl_1をつけてくれたわけだ。（んでもって、終了条件のためにpc = "Done"もつけてくれた。)
ラベルはある文の前であればいくらでもつけることができる。ラベルからラベルまでがひとかたまりとして扱われる。
以下のようにPlusCALの記述を変えたとすると、
--fair algorithm euclid {
variables x = N, y = M;
{ abc: while (x # y) { d: if (x < y) { e: y := y - x }
else { f: x := x - y }
};
print <<"have gcd", x>>;
assert (x = y) /\ (x = gcd(N, M));
}
}生成されるのは以下のようになる。
(前略)
Init == (* Global variables *)
/\ x = N
/\ y = M
/\ pc = "abc"
abc == /\ pc = "abc"
/\ IF x # y
THEN /\ pc' = "d"
ELSE /\ PrintT(<<"have gcd", x>>)
/\ Assert((x = y) /\ (x = gcd(N, M)),
"Failure of assertion at line 15, column 4.")
/\ pc' = "Done"
/\ UNCHANGED << x, y >>
d == /\ pc = "d"
/\ IF x < y
THEN /\ pc' = "e"
ELSE /\ pc' = "f"
/\ UNCHANGED << x, y >>
e == /\ pc = "e"
/\ y' = y - x
/\ pc' = "abc"
/\ x' = x
f == /\ pc = "f"
/\ x' = x - y
/\ pc' = "abc"
/\ y' = y
Next == abc \/ d \/ e \/ f
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done" /\ UNCHANGED vars)
(後略)dを見てみよう。dは分岐をしてるだけで、xもyもいじってない。なので、UNCHANGED <
eは、y' = y - x となるパターンで、xは変わらない。そして、次の状態がabcに戻る。
fは、x' = x - yで、yは変わらず、abcに、戻る。
abcはdにいくか、Doneに行く。x, yは変わらない。
