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つのモジュールしか開けないのは不便だ
- PlusCal から TLA+ への変換を忘れやすい
- Eclipse に抵抗のある人は Visual Studio Code の拡張機能 TLA+ を使用するとよさそう
参考リンク
- Practical TLA+ - Planning Driven Development | Hillel Wayne | Apress
- 原著
- 実践TLA+ 電子書籍|翔泳社の本
- 翻訳
- The TLA+ Home Page
- TLA+ の総本山的なWebページ