TLA+に再挑戦（2021.11）

development tlaplus

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

今回

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

55ページ（第3章の冒頭）から復習しつつ、72ページからの「3.4 例」で行き詰まった。

デバッグトレースを取得するために、PlusCal アルゴリズムにしてみよう

[What is the behavior spec?] を [Temporal formula] に変更すると、検証すべき式が存在しないエラーになってしまう。 （私が）どこかに Spec を書き忘れているみたい。

感想

  • 3章、4章はリファレンス的な内容だった
    • REPLが無いと試しにくいから読み飛ばしたくなる
  • 5章や6章も部品の説明
  • 第2部、7章からは具体的なアルゴリズムを検証していく感じ
  • Discord サーバーに FredBoat を追加してBGM流してみた。わりと良い

次回

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

参考リンク