TLC Model CheckerをCUI（コマンドライン）で使う
TLC Model Checkerとは形式仕様記述言語であるTLA+のモデル検査ツールです。TLA+で書かれた仕様の不変式のviolationやLivenessやSafety 特性のviolationの検出などをしてくれます。
そんで、このTLC Model Checkerというのは、CUIで使えたほうが便利だと思うんですよね。実はTLA+にはTLA ToolboxというIDEがあって、GUIからマウスポチポチで呼び出して検証することもできるのですが、仕様検証という作業は（仕様規模によりますが）すごいCPUパワーとストレージを食います。
そのため、実務的な観点で言えば、DCとかにおいてある高性能なコンピュータにSSHで入って操作することになると思うのですが、この場合GUIは邪魔になります。
この間公開したスライドでもTLC Model CheckerをCUIで使っています。でもCUIのTLC Model Checkerをどうやってインストールするのかを解説してませんでしたのでここで書いておきます。
このtla-binというツールを使えば簡単にオフィシャルのTLA+環境一式をCUI化してインストールできます。
マニュアルにも書いてありますが、こんな感じでやればインストールできます。インストール先はデフォルトだと /usr/local になりますが、第一引数に与えればインストール先は変えられます。
$ git clone https://github.com/pmer/tla-bin.git $ ./download_or_update_tla.sh $ sudo ./install.sh
やってることは、オフィシャルページのTLA+ Toolboxをダウンロードしてjarを解凍してjavaのclassファイルを取り出し、適切なオプションを付けてJVMで実行しているみたいです。
なお、TLA+のツール一式はJavaで書かれていますのでJavaのインストールも必要です。OpenJDKでは動きません。Oracle JVMじゃないとだめですね。
[xxx@host:~/xxx/tla+/raft]$ tlc -config SPEC.cfg ./first.tla
TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)
Running breadth-first search Model-Checking with fp 82 and seed 1539151492344761609 with 1 worker on 24 cores with 21424MB heap and 64MB offheap memory (Linux 3.10.0-862.9.1.el7.x86_64 amd64, Oracle Corporation 1.8.0_181 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/xxx/xxx/tla+/raft/first.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/TLC.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module first
Starting... (2020-02-13 11:51:47)
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NullPointerException
java.lang.NullPointerException
at tlc2.tool.impl.SpecProcessor.processSpec(SpecProcessor.java:346)
at tlc2.tool.impl.SpecProcessor.<init>(SpecProcessor.java:157)
at tlc2.tool.impl.Spec.<init>(Spec.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:126)
at tlc2.tool.impl.Tool.<init>(Tool.java:121)
at tlc2.tool.impl.Tool.<init>(Tool.java:116)
at tlc2.TLC.process(TLC.java:930)
at tlc2.TLC.main(TLC.java:247)
Finished in 00s at (2020-02-13 11:51:47)
