TLA+に再挑戦(2021.09)

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

今回

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

冒頭から 45 ページ(第2章の途中)まで読んで試した。

  • TLA+ Toolbox の準備
  • サンプルコードの入力と実行

https://scrapbox.io/yujiorama/%E5%AE%9F%E8%B7%B5TLA+_%E5%85%A5%E9%96%80

次回

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

45 ページ(第2章の途中)から 97 ページ(第4章)まで読んで試す。

感想

  • TLA+ Toolbox(Eclipse ベースの IDE)
    • PlusCal から TLA+ への変換を忘れやすい
      • 本にも書いてありますが、[Translate PlusCal automatically]オプションを有効にすると楽です。保存のたびに自動でコンパイル(?)されます。
    • (Error Traceの見方、慣れが必要そう…)
      • TLA+ のエラー位置へジャンプするから、PlusCal のどこに対応するかは自力でたどり着かないといけない
    • 同時に1つのモジュールしか開けないのは不便だ
  • Eclipse に抵抗のある人は Visual Studio Code拡張機能 TLA+ を使用するとよさそう

参考リンク