takaha.siの技術メモ

勉強したことをお伝えします。ちょっとでも誰かの役に立てればいいな…

2020-03-06から1日間の記事一覧

TLC Model CheckerをCUI(コマンドライン)で使う

TLC Model Checkerとは形式仕様記述言語であるTLA+のモデル検査ツールです。TLA+で書かれた仕様の不変式のviolationやLivenessやSafety 特性のviolationの検出などをしてくれます。 そんで、このTLC Model Checkerというのは、CUIで使えたほうが便利だと思う…