山火事問題
前回２フェーズコミットを試した後、他の例として出てくるPaxosと、もう一つの問題（本件）がありました。PaxosはPlusCALで書かれていて記述自体はシンプルなものの、アルゴリズム自体が難しい点、pdf上にざっくりと載っているだけで、動くスペックにするのが大変な予感がしたことから、ひとまずこっちを試してみようかと。
こちらの問題は、もとのWebページに「ネット上でこの文字列で検索したときにこのページのみ出てくるようにするため、決してこの文字列をお前のウェブページやその他ネット上に書き込んではならぬ」と、２０年前ならではの俺俺っぷりで「名前を言ってはいけないあの問題」的な状態を作り出していて、今ならGoogle先生に任せろよ、の一言ですが、ランポート先生を怒らせても何もいいことありません。幸い日本人には日本語が使えるため、ここでは山火事問題と呼ぶことにします。
Alphaプロセッサのキャッシュの同期アルゴリズムをTLA+で表したものにバグを入れてあるので、それを探しましょう、というお題です。どうやら１５年経った今も問題としては生きているようで、多分答えをみつけてチューリング賞受賞者にメールすると答え合わせをしてくれるというすごい状況（なはず）。
さて、今日はまだ問題をダウンロードしただけなので、本題にははいれませんが、ひとつ、「ほう」と思った記述を。
Data == [0..(DataLen - 1) -> {0,1}]DataLenが正の整数だとすると、これは長さがDataLenの任意のバイナリ列を表します。確かに。現実のシステムをTLA+に落とす参考になりますね。実際にこれをモデルチェックかけようとすると、たぶんDataLenをとても小さくしないと計算量が膨大すぎて無理だと思うけど。
PlusCALで2フェーズコミット
PlusCAL Manualは、実は読み終わったのですが、後半はわりとつまらないのでここには書きません。Hyperbook は時間があれば読み進める予定。iPadで読みにくいのが難点。
さて、実践編その１としまして、AWSの人が書いた２フェーズコミットのブログ記事があるので、それを見て行きたいと思います。
Exploring TLA+ with two-phase commit - Marc's Blog
ひと通りPlusCALの文法を抑えた今なら何をしてるのかわかりますね。でも、いざブログを頼りに動くスペックを書こうとすると、エラーの嵐。細かいところは覚えてないのである程度試行錯誤が必要なのですが。。
面倒なので、PlusCALと、変換後のTLA+を両方載せてしまいますね。
-------------------------------- MODULE 2pc --------------------------------
(***************************************************************************
--algorithm 2pc {
variables
managers = { "bob", "chuck", "dave" };
restaurant_stage = [ i \in managers |-> "start" ];
process (Restaurant \in managers) {
c: await restaurant_stage[self] = "propose";
either {
restaurant_stage[self] := "accept";
} or {
restaurant_stage[self] := "refuse";
};
c1: await (restaurant_stage[self] = "commit")
\/ (restaurant_stage[self] = "abort");
if (restaurant_stage[self] = "commit") {
restaurant_stage[self] := "committed";
} else {
restaurant_stage[self] := "aborted";
};
};
process (Controller = "alice")
variable k, aborted = FALSE;
{
n: k := managers;
n2: while (k # {}) {
with (p \in k) {
restaurant_stage[p] := "propose";
k := k \ {p};
};
};
k := managers;
n3: while (k # {}) {
with (p \in k) {
await (restaurant_stage[p] = "accept")
\/ (restaurant_stage[p] = "refuse");
if (restaurant_stage[p] = "refuse") {
aborted := TRUE;
};
k := k \ {p};
};
};
k := managers;
if (aborted = TRUE) {
n6: while (k # {}) {
with (p \in k) {
restaurant_stage[p] := "abort";
k := k \ {p};
};
};
} else {
n4: while (k # {}) {
with (p \in k) {
restaurant_stage[p] := "commit";
k := k \ {p};
};
};
};
};
}
***************************************************************************)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES managers, restaurant_stage, pc, k, aborted
vars == << managers, restaurant_stage, pc, k, aborted >>
ProcSet == (managers) \cup {"alice"}
Init == (* Global variables *)
/\ managers = { "bob", "chuck", "dave" }
/\ restaurant_stage = [ i \in managers |-> "start" ]
(* Process Controller *)
/\ k = defaultInitValue
/\ aborted = FALSE
/\ pc = [self \in ProcSet |-> CASE self \in managers -> "c"
[] self = "alice" -> "n"]
c(self) == /\ pc[self] = "c"
/\ restaurant_stage[self] = "propose"
/\ \/ /\ restaurant_stage' = [restaurant_stage EXCEPT ![self] = "accept"]
\/ /\ restaurant_stage' = [restaurant_stage EXCEPT ![self] = "refuse"]
/\ pc' = [pc EXCEPT ![self] = "c1"]
/\ UNCHANGED << managers, k, aborted >>
c1(self) == /\ pc[self] = "c1"
/\ (restaurant_stage[self] = "commit")
\/ (restaurant_stage[self] = "abort")
/\ IF restaurant_stage[self] = "commit"
THEN /\ restaurant_stage' = [restaurant_stage EXCEPT ![self] = "committed"]
ELSE /\ restaurant_stage' = [restaurant_stage EXCEPT ![self] = "aborted"]
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << managers, k, aborted >>
Restaurant(self) == c(self) \/ c1(self)
n == /\ pc["alice"] = "n"
/\ k' = managers
/\ pc' = [pc EXCEPT !["alice"] = "n2"]
/\ UNCHANGED << managers, restaurant_stage, aborted >>
n2 == /\ pc["alice"] = "n2"
/\ IF k # {}
THEN /\ \E p \in k:
/\ restaurant_stage' = [restaurant_stage EXCEPT ![p] = "propose"]
/\ k' = k \ {p}
/\ pc' = [pc EXCEPT !["alice"] = "n2"]
ELSE /\ k' = managers
/\ pc' = [pc EXCEPT !["alice"] = "n3"]
/\ UNCHANGED restaurant_stage
/\ UNCHANGED << managers, aborted >>
n3 == /\ pc["alice"] = "n3"
/\ IF k # {}
THEN /\ \E p \in k:
/\ (restaurant_stage[p] = "accept")
\/ (restaurant_stage[p] = "refuse")
/\ IF restaurant_stage[p] = "refuse"
THEN /\ aborted' = TRUE
ELSE /\ TRUE
/\ UNCHANGED aborted
/\ k' = k \ {p}
/\ pc' = [pc EXCEPT !["alice"] = "n3"]
ELSE /\ k' = managers
/\ IF aborted = TRUE
THEN /\ pc' = [pc EXCEPT !["alice"] = "n6"]
ELSE /\ pc' = [pc EXCEPT !["alice"] = "n4"]
/\ UNCHANGED aborted
/\ UNCHANGED << managers, restaurant_stage >>
n6 == /\ pc["alice"] = "n6"
/\ IF k # {}
THEN /\ \E p \in k:
/\ restaurant_stage' = [restaurant_stage EXCEPT ![p] = "abort"]
/\ k' = k \ {p}
/\ pc' = [pc EXCEPT !["alice"] = "n6"]
ELSE /\ pc' = [pc EXCEPT !["alice"] = "Done"]
/\ UNCHANGED << restaurant_stage, k >>
/\ UNCHANGED << managers, aborted >>
n4 == /\ pc["alice"] = "n4"
/\ IF k # {}
THEN /\ \E p \in k:
/\ restaurant_stage' = [restaurant_stage EXCEPT ![p] = "commit"]
/\ k' = k \ {p}
/\ pc' = [pc EXCEPT !["alice"] = "n4"]
ELSE /\ pc' = [pc EXCEPT !["alice"] = "Done"]
/\ UNCHANGED << restaurant_stage, k >>
/\ UNCHANGED << managers, aborted >>
Controller == n \/ n2 \/ n3 \/ n6 \/ n4
Next == Controller
\/ (\E self \in managers: Restaurant(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================ブログ中、まずTLA+のところにvariablesを定義するぜ、とかいってるけどどう見てもそれでは動かない。なので、少し変えてあります。
一番困ったのがmacroの書き方。どこに書けばいいのかわからない。それと、C Manualをみると、macroにはwhileは使えないと書いてある。（なぜなら、macroの中にラベルを持てないから）それにもかかわらず、便利なmacroをつかうぜ！とかいってるのでわけわかめ。しょうがないので手で展開して書きました。
あとは、ハマリポイントとしては、 }のあとに；がいるのかいらないのかいちいち判別がつかん。面倒なので orで繋がる場合などをのぞき、すべて;をつけておきました。
できあがったものをとりあえず何もinvariant check無しでモデルチェックにかけると、無事ブログと同じ、718 states, 296 distinct states、となりました。checkの追加は後ほど。
一番謎なのは、これだと Aliceが各マネージャのステージをpropose, commit, abortにするところはatomicになってるんですが、それでいいの？という疑問。じつはこれ、2PCを昔見た時からずっと疑問なので、僕でもわかるように誰か教えて下さい。
C Manual (PlusCAL) つづき。３章。
Cマニュアル、意外によみやすいのでこのまま続けて読むことにした。
3は言語仕様。
3.2.1 Assignment
:= はわかる。けど、-> と |-> の違いがいまいちわかってない。S->Tは写像（集合と集合のマッピング）と理解できそうだけど、それだけだとしっくりこない使い方もされている。
| はPlusCALの特殊表記。同じ変数への複数の代入をアトミックに行うときに使う。主に arrayなどに使うことになりそう。 |
3.2.2 If
If (test) hogehoge else boroboro
TLA+の場合は IF THEN ELSEだったと思うので、ちょっと違う。
3.2.3 Either
etiher A or B or C
と使う。TLC(TLAのモデルチェッカー）にどれか選ばせる（というか全通り組み合わせを調べさせる）ための分岐。
なので、switch文とは違う。
3.2.4 While
label_1: while (test) body
まあ、普通だ。なんでわざわざlabel_1: とラベルがついてるかというと、while文にはかならずラベルがつくという鉄の掟があるから。もちろん、translatorが必要に応じてつけてくれるんだけど、鉄の掟を忘れぬようにとのLamport先生がおっしゃっております。
3.2.5 Await (When)
条件がTrueになったときだけ実行される。主にマルチプロセッシングのblockingを表現するのに使う。同じラベルの中であれば、どこにあろうとその条件を満たさなければそのラベルは実行されない。
3.2.6 With
with (id \in S) body
Sが空じゃない時は、idはSからランダムに選ばれる。これまたTLCに分岐させるために使われるってことだな。
Sが空の時は待つ。つまりblock。
3.2.7 Skip
なにもしない。
3.2.8 Print
何かを表示。モデルチェック的には何の影響もないのでskipと同じ。
3.2.9 Assert
TLCモジュールが必要。 モデルチェック的にはなんの影響もないが、assertがFalseになればそこでエラーとなる。
3.2.11 Goto
どこかのラベルに飛ぶ
3.3 Process
process (ProcName \in IdSet) と複数プロセスを定義するか、process (ProcName = Id) と一つのプロセスを定義するか。
宣言の次に local variableを持つことができて、その後に bodyがくる。
3.4~3.6 Procedure, Macro, Definition
Procedureはさっき飛ばした3.10のcall, returnを使う。正直、この後の Macro, Definitionと合わせて理解が充分でない。今後復習したい。
3.7 Label
何度も出ているラベル。いつものラベルを置けるところ、置かないといけないところのルール。
C Manual (PlusCAL)に浮気
Hyperbookの4.9に入ったら、Lamport先生我慢できなくなったのか、「でもやっぱり数学的証明も必要だよね」みたいなかんじで証明モードに入ったため、ややゲッソリして PlusCALのC Manualをつまみ食い。（PlusCALには、Cっぽい文法とPascalっぽい文法の２通りある。）
以前の記事では2.5のユークリッド法まで試してあったので、2.6へ。複数プロセス間の排他制御のアルゴリズム。いままで学んだことを踏まえると、なんとか理解できる。
process (Proc \in 1..N)
がN個のプロセスで動くことを宣言する。それぞれのプロセスは、process行の後に宣言された変数をローカル変数として持ち、selfを自分のプロセス番号を示す変数として持つ。（番号、というとintっぽいけど、それは Proc \in 1..N で宣言してるからであって、文字列にすることも可能。）
LTA+に変換されると、pcがアレイになり、pc[index]で各プロセスの現在のラベルを表す模様。（まだ実際に試してみてないので、予想）
2.7 ラベルはどこにつくのか。色々とルールが有る。それほど気にする必要はなさそうだ。while文にはラベルがつく必要がある。つまり、
process (Proc \in 1..4)
{ while (True) {
action1;
action2;
action3;
}}という一番簡単なスペックがあったとすると、自動ではwhileループにのみラベルがつく。１番目のプロセス（１から４のどれか）がaction1,2,3を一回実行し、次のプロセスがaction1,2,3を実行し、... となる。
それを以下のようにラベルを付けたとしよう。
process (Proc \in 1..4)
{ a: while (True) {
b: action1;
c: action2;
d: action3;
}}すると、Process1がaを実行して、次に(Process1がbを実行するか）他のプロセスがaを実行して、と並列動作が行われる。Process1がa,b,c,dと実行してからProcess3がa,b,c,dと実行するかもしれないし、Process2がa,b,cといったところでProcess4がaを実行し、Process1がa,b,c,dと実行するかもしれない。その組み合わせをLTA+は検証してくれる。
では、実際に試してみよう。
EXTENDS Integers, TLC
(***************************************************************************
--algorithm Counter {
variables x = 0; i = 0;
process (Proc \in 1..2)
variable j;
{a: while (i < 5) {
j := x;
x := j + 1;
i := i + 1;
};
\*print <<"counter is ", x>>;
};
}
***************************************************************************)(print文は邪魔なのでコメントアウトしてある。assert使ってないのでTLCはいらない)
プロセス２つで、カウンターXを５回インクリメントしたい。ループに使っているiはアトミックに i := i + 1で増やしているので必ず５回になるはず。さて、xの値は一度 jに入れて、それに１を足している。この状態でTLA+に変換し、Modelのinvariantsに以下を入れて動かしてみよう。
(\A self \in ProcSet: pc[self] = "Done")=> x = 5
つまり、終了条件になっていれば、xは5であるはず。
動かしてみると、成功する。LTA+に変換後のスペックを見るとわかるけれど、xの値はatomicに変更されている。
これを、以下のように変える。（process部分のみ載せている）
process (Proc \in 1..2)
variable j;
{a: while (i < 5) {
b: j := x;
c: x := j + 1;
i := i + 1;
};
};
***************************************************************************)で、変換してモデルチェック。すると、今回は失敗してくれる。xが４になるパターンで停止して、どういう順序で実行されたらxが4で終わるかを教えてくれる。
思ったよりも期待通りの動きをしてくれた。なかなか楽しい。
さて、2.7が終わり、C Manualの３章は言語スペックに入るようなので、またHyperbookに戻ろうかと思う。
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は変わらない。
TLA+ : Hyperbookを使って仕切り直し
せっかく Chapter 1と Chapter 2を終わって動かしてみたものの、なんだかずいぶん進めにくいなー、と思って、ふとHyperbook (前回 TLA+の本、と紹介した横にあったもの。最初HTML形式のオンライン物だと思ってて、避けてた）を読んでみたら、なにこれわかりやすい。らんぱーとさんのメモ書き状態ではなく、ちゃんと人間向けに書いてある。いままでの苦労は。。
と、いうことで、Hyperbookに乗り換えて仕切りなおすことにしました。
Chapter 1は紹介、Chapter 2は 1 bit clock (0 -> 1 -> 0 -> 1 -> ... )と、前回のHour Clockより更に単純。特に面白いところもないのでさらっと流した。
Chapter 2の「ダイ・ハード」はなかなか面白い。3L入るバケツと、5L入るバケツで4Lを作る、という話。考えられる操作は以下の４通り
- 3Lのバケツを空にする
- 5Lのバケツを空にする
- 3Lのバケツを満たす
- 5Lのバケツを満たす
- 3Lのバケツから5Lのバケツに水を移す
- 5Lのバケツから3Lのバケツに水を移す
で、初期状態（どちらも空）をいれてやると、TLA+のモデルチェッカーは取りえるすべての状態遷移をチェックする。それだけだとチェックするだけで終わるので、バケツ大 # 4 (not equal) を条件に与えると、それが失敗する。その失敗した遷移が実際には知りたい「4Lにする手順」となる、という寸法。
へー、そんなことができるんだ。Prologみたい、と思ったあなた。確かにそんなこともできるんだけど、実際に裏で何が起きているかというと、起こりえる状態を虱潰しに探している。TLA+はあくまでも、「複雑なシステムを単純な数学式で表して、それの正しさを証明する」というためにあるので、なにかの答えを得るためにつかうものではない。
いまのところ、TLA+とPlusCALを平行して扱っている。「TLA+で解けたけど、ダイ・ハードのヒーローは数学の素養があるようには見えないから、PlusCALのほうがいいでしょう」などと冗談を挟んだりする。
Chapter 3 は以前PlusCALの記事で試した ユークリッド法による最小公約数の取得。
が、いきなりユークリッド法に入っても何がうれしいのかわからないことにらんぱーどさんも学んだらしく、最初は以下の様な一番単純な解き方をTLA+で表す。
まず、pはnの約数であるとは、
Divides(p, n) == \E q \in Int : n = q * p
と書ける。ここで、Intは EXTENDS Integer でimportするんだけど、そのままだと無限個ある。そのため、ModelのAdvanced OptionのDefinition Overrideで、Intは 0..100とかしてあげる必要がある。
次に、約数の集合は
DivisorsOf(n) == {p \in Int : Divides(p, n)}と書ける。
集合の最大値を取るSetMaxを定義して
SetMax(S) == CHOOSE i \in S : \A j \in S : i >= j
nの約数とmの約数の積が公約数。最大値を取ると最大公約数。となる。
gcd(n, m) == SetMax(DivisorsOf(n) \cap DivisorsOf(m))
ここで、CHOOSE は条件を満たす要素を一つ選ぶ。複数あったらどれかを選ぶ。ここでは、定義から最大値を選んでいるので、仮に最大値が集合の中に２つあってもどちらをとっても問題ない。
ところで、このgcdはfunctionとして定義している。specの定義と特に違うところはない。（specの場合は、InitとNextという名前で式を書くと自動的にそれがモデルチェッカーのInitとNextに設定されるが、それは単なる便利機能であって、本質ではない。）
次にユークリッド法での実装に進む。とりあえずここまでを読んだ。
Chapter 2 Specifying a Simple Clock
2.1 Behaviors
「コンピュータシステムにおいて、状態の変化は非連続のステップで起こると仮定できるので、システムの実行をstatesのシーケンスと表すことができる。ここで、stateとはvalueをvariableにアサインすること。システムをpossible behaviorsの集合として定義する。」
まったく日本語になってないが、まあ、簡単にいえば、起こりえる状態変化を全部集めれば、それがシステムを表したことになるよ、ということだ。そしてそれが、これからTLA+をつかって挑むことだ。
2.2 An Hour Clock
デジタル時計の例がスタート。この時計は1 から 12までの時間を表示するだけだとする。hr が時間を表す変数ね。
[hr=11] -> [hr=12] -> [hr=1] -> [hr=2] -> ...
こんなふうに動いていく。2.1で述べたように、起こり得るすべてのbehaviorを書き出す必要がある。まずは初期値の定義。初期値は1から12まで、HCini と呼んで、以下のように定義する。ここで、== は、defined to equal。等しい、ではないので注意。（==は=の上に△.これはTexとも違うらしい。気まぐれだな。。）
HCini == hr \in {1, ..., 12}まだ右の部分がTLA+記法になってない。次に、ある値と次の値の関係を表現する、HCnxtを定義しよう。hr'はhrの次の値、という意味とする。
HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1
(# はnot equalに使う記号）
こういう式をActionと呼ぶ。HCnxtを満たすstepをHCnxt stepと呼ぶ。このstepが起こった時、stepが実行された、と言いがちだけど、formulaはformulaであって実行されるわけじゃないので厳密には正しい言い回しではない。
さて、 HCiniとHCnxtの２つじゃなくて、ひとつの式で表したい。それには、[] (□, boxと読む)という記号を使う。[]FはFが常に正しいことをassertする。(assertってどう訳すのがいいのだろうか。）[]HCnxtは、HCnxtがすべてのstepにおいてTrueであることを示す。HCini /\ []HCnxt は、初期値がHCini で、すべてのstepがHCnxtを満たす、となって、この時計のSpecとしては良さそうだ。
もしも、その時計に温度計もついていて、まだ１時なのに温度が変わって表示が変わることがあるかもしれない。e.g. [1時22度] -> [1時23度] -> [2時23度]。って、いきなりな仮定が来たけど、ようするに、時間が変わらない、というstepも表現したい。この、hr'=hr となるstepを、stuttering stepという。よって、stepが HCnxt \/ (hr' = hr) であればよい。前述の[]を使ってSpecを書いてみると、
HCini /\ [](HCnxt \/ (hr' = hr))
面倒なので、HCnxt \/ (hr' = hr)のことを、[HCnxt]_hr と書くことにする。HCnxtだけど、hrは変わらないかもよ、というのをむりやり短くしてみたのだ。_hrは、hrは添字（ちっちゃく右下につく）という意味。
HCini /\ [][HCnxt]_hr
この時計は、ある時間で止まって進まないかもしれない。つまり、時計は進まなくて、stepは進む（ややこしい）。時計は必ず進むという前提をつけることもできて、それはChapter 8で扱う。
とりあえず、時計は以下の式で表された。
HC == HCini /\ [][HCnxt]_hr
2.3 A closer look at the specification
HCはtemopral formulaだ。temporal formulaのいい訳語がわからん。HCを満たすすべてのbehaviorについて、[]HCiniがTrueであるので、つまりそれは、HC implies []HCiniといえる。
HC => []HCini
temopral formula satisfied by every behavior はtheoremと呼ばれる。ので、上の式はTheoremといえる。はいそうですか、という感じだけど、このへん、微妙。数学の素養がないのでちょっときつい。
2.4 The Specification in TLA+
さて、いままでPseudo Codeでやってきたが、これをTLA+で書く日がやってきた。
まず、モジュール名から始める。
---- MODULE HourClock ----
なんと、TLA+では数字の足し算演算子"+"はbuiltinではない。それは、自然数モジュールで定義されている。EXTENDS文でモジュールをimportする。（python用語だけど）
EXTENDS Naturals
変数の定義は
VARIABLE hr
---- MODULE HourClock ---- EXTENDS Naturals VARIABLE hr HCini == hr \in (1 .. 12) HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1 HC == HCini /\ [][HCnxt]_hr -------------------------- THEOREM HC => []HCini ==========================
---- や ====は、４文字以上ならいくつでもいい。..もoperatorで、Naturalsモジュールに定義されている。
THEOREMの前の区切り線は見た目を整えているだけ。で、問題のTHEOREMだが、これは、上の式によって表現された時計が、このTHEOREMを満たすことをチェックするために存在する。つまり、上の式が正しく定義されていれば、HCならばHCiniが常にTrueであるはずで、もしもそうでないならこのSpecには矛盾があります、と。上がSpecで、下がassert文みたいなもんね。すんげー大雑把な理解だけど、そのくらいじゃないと頭が簡単に爆発しそう。
上のSpecにおいて、時計を表すのがHCなのか、HCnxtなのか、HCiniなのかは、TLA+の知ったことではない。TLA+はあくまで数学上の表現であり、その解釈は利用者側に委ねられる。
