cloverrose's blog

Python, Machine learning, Emacs, CI/CD, Webアプリなど

NuSMV 2.5.1でBooleanとIntegerが明確に区別されるようになってた

久しぶりにNuSMVを触っていて、参考書Amazon.co.jp: 4日で学ぶモデル検査 (初級編) (CVS教程 (1)): 産業技術総合研究所システム検証研究センター: 本の通りに書いてたら文法エラーでたので調べてみたら、

The new version 2.5.1 makes a strong distinction between integers and boolean types. This breaks backward compatibility,

http://nusmv.fbk.eu/announce-NuSMV-2.5.1.txt

caseでdefault節を表すために1って書いてたけど、これからはTRUEって書こう。