TLA+のインストール手順

TLA+ Toolboxをインストールする

基本的には公式にあるとおり
https://lamport.azurewebsites.net/tla/toolbox.html

Windowsの場合

https://github.com/tlaplus/tlaplus/releases/tag/v1.5.7
から TLAToolbox-1.5.7-win32.win32.x86_64.zip をダウンロードして、展開します。環境変数PATHに展開したパスを追加します。

Mac OS Xの場合

https://github.com/tlaplus/tlaplus/releases/tag/v1.5.7
から TLAToolbox-1.5.7-macosx.cocoa.x86_64.zip をダウンロードして、展開して、Applicationフォルダにコピーするだけです。最初に起動するときにセキュリティの問題があるとかで起動できない場合は、右クリックで「開く」を選択すると、確認ダイアログがでるのでそこで確認すれば、以降はクリックだけで起動できるようになります。

Javaランタイムをインストールする

TLA+を起動したときにJavaランタイムがインストールされていないとエラーが出る場合はJavaランタイムをインストールしてください。こちらからダウンロードできます。

OpenJDKを使う場合は、OpenJDK11.0.2だとToolbox-1.5.7が動作しなかったので、他のバージョンを選択してください。OpenJDK10で動作することを確認してます。古いバージョンのOpenJDKは https://jdk.java.net/archive/ からダウンロードできます。