Chapter 2 実習

こんな簡単な例でも、読んだだけでは「ふーん、そう」という感じで、いまいちわかってない。問題は、この本をずっと読み進めていっても、いつまでたっても実際の使い方にたどり着かないことだ。（PlusCALのマニュアルはその点、少しだけ親切。それをもとにPlusCALを試してみよう - みょらみょらPython日記は書かれた。）

そこで、Chapter 3に進む前に、実際にToolboxを動かしてみることにする。

インストール

Index of /tlatoolbox/productsから、Mac版をダウンロードして、インストールの際に「古いJavaが必要です」とか言われるので言われるがままにインストールして、解凍したフォルダを適当なところにおき、toolboxを起動する。下にプログレスバーみたいなのが出てきて、起動中かとおもいきや、ただのメモリメーターみたいなので気にしなくていい。

Specの作成

File -> Open Spec -> Add new spec で、新たなプロジェクトを作成する。ファイル名を聞かれるので、<適当なディレクトリ>/<モジュール名>.tla と入力すると、モジュール名でテンプレートが作られ、エディタが開かれる。

よくわからなくてtla_trialっていれたら、それがモジュール名になってしまった。

----------------------------- MODULE tla_trial -----------------------------
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
=============================================================================

で、保存。

実行

TLC Model Checker -> Run Model って押しても、反応がない。ただの屍のようだ。
実行するにはモデルを作成する必要がある。

TLC Model Checker -> New Model で作成。

Model Overviewのタブを見る。作った瞬間からエラーが表示されている。が、なんのエラーかは表示されない。MSRさん厳しい。。結論から言うと、What is the behavior spec? は、「Temporal formula」を選び、箱に HC と入力する。これによって、「俺はHCのチェックをしたいんだよ」となる。

ようやくRun Modelで実行することができる。ふむ。24の状態があって、重複を除くと12種類あるよ、と。どうやら成功のようだ。

ここからが大変

では、エラーチェックをどうやって見つけるのかを見てみたいとする。ためしに、HCiniを以下のように変えてみた。

HCini == hr \in (1 .. 13)

で、実行！

あれ？止まらない。hr' = hr + 1で、ずーっとhrを増やし続けている模様。
期待値としては、hrが14担った時点でTHEOREMの行と矛盾するので、エラーで止まって欲しいんだけれど、そんなに親切ではないらしい。

それより、THEOREMがどう動いているのかがわからない。ためしにHCiniは戻して、THEOREMの行を消してもチェックは完了する。

What to check?

Model Overviewで、What to check?でデフォルトではDeadlockにチェックが入っているのみ。なにもチェックしてない？
Invariantsに hr # 20 とかいれておくと、止まるようになる。(初期値が１３の時に20になるよ、と教えてくれる。）でも、それってただの手動assertではなかろうか。

その他、いろいろ試行錯誤をしてみたが、だいたいエラーになる。まだまだ謎が多い。もう少し読み進めばわかるようになるのか？