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に設定されるが、それは単なる便利機能であって、本質ではない。）
次にユークリッド法での実装に進む。とりあえずここまでを読んだ。
