TLA+に再挑戦（2021.12）

development tlaplus

英語のドキュメント を読んだけどあまり理解できてなかったので 日本語 で再挑戦する会。

今回

2021.12 実践TLA+もくもく会 - connpass

  • 72ページ「3.4 例」のナップサック問題の定式化
  • 「4章 定数、モデル、インポート」を読んで試した
  • 次回は「5章 並行処理」を読んで試す

感想

  • REPLが無いと試しにくいから読み飛ばしたくなる
    • これどうにかならないのかな

REPL したい

github.com/will62794/tlaplus_repl にこんな記述がある。

June 2020 Update: The newest versions of TLC include a built in REPL that provides most of the same functionality provided in this Python tool with considerably lower evaluation latency. You can use it by running java -cp tla2tools.jar tlc2.REPL from the command line.

tla2tools.jar の tlc2.REPL というクラスを実行すると REPL が使えるらしい。

TLA+ Toolbox 1.8.0 では、toolbox/tla2tools.jar というファイルが該当する。 ただし、GitHub のリリースページを見るとアセットに並んでいた。 （古いバージョンのアセットにも並んでいるけど、TLA+ Toolbox 1.8.0 から利用できるようになったみたい。）

 Assets 8

p2repository.zip 345 MB
tla2tools.jar 3.22 MB
TLAToolbox-1.8.0-linux.gtk.x86_64.zip 187 MB
TLAToolbox-1.8.0-macosx.cocoa.x86_64.zip 181 MB
TLAToolbox-1.8.0-win32.win32.x86_64.zip 184 MB
TLAToolbox-1.8.0.deb 181 MB
Source code (zip)
Source code (tar.gz)

実装クラスはこの辺。

tlc2.REPL

REPL する

次のように REPL できる。

  • ユーティリティ演算子が使える
  • モジュールの EXTENDS や INSTANCE はできない
    • 実装を読んだら、入力行ごとに spec file を生成して評価していた
    • 毎回新しいコンテキストで評価しているということ
  • 終了したいときは Ctrl+C を入力
$ java -cp toolbox/tla2tools.jar tlc2.REPL
12月 18, 2021 3:23:46 午後 org.jline.utils.Log logr
警告: Unable to create a system terminal, creating a dumb terminal (enable debug logging for more information)
Welcome to the TLA+ REPL!
TLC2 Version 2.16 of Day Month 20??
Enter a constant-level TLA+ expression.
(tla+) Print(<<"2 + 3 =", 5>>, <<1>>) \o <<2>>
Print(<<"2 + 3 =", 5>>, <<1>>)<<"2 + 3 =", 5>>  <<1>>
<<1, 2>>
(tla+) Assert(3 < 5, "3 is more than 5")
Assert(3 < 5, "3 is more than 5")TRUE
(tla+) Assert(3 > 5, "3 is more than 5")
Assert(3 > 5, "3 is more than 5")Error evaluating expression: 'Assert(3 > 5, "3 is more than 5")'
tlc2.tool.EvalException: The first argument of Assert evaluated to FALSE; the second argument was:
"3 is more than 5"
(tla+) LET x == 3 y == 5 IN Assert(x > y, ToString(x) \o " is more than " \o ToString(y))
LET x == 3 y == 5 IN Assert(x > y, ToString(x) \o " is more than " \o ToString(y))Error evaluating expression: 'LET x == 3 y == 5 IN Assert(x > y, ToString(x) \o " is more than " \o ToString(y))'
tlc2.tool.EvalException: The first argument of Assert evaluated to FALSE; the second argument was:
"3 is more than 5"

次回

2022.1 実践TLA+もくもく会 - connpass

参考リンク