niszetの日記

アナログCMOS系雑用エンジニアが頑張る備忘録系日記

NuSMVを使ってみたのでメモ

モデル検査に入門しているのです。

色々あって、モデル検査[初級編]を読んでます。出版社さんのサイトはこちら。今はAmazonの在庫があるのかな?なければyodobashiとか色々選択肢はあるはず。まだ在庫はあると思うので。

www.kindaikagaku.co.jp

ちょっと古い本(2009年)ですが、これが一番わかりやすそうだったので、モデル検査周りは一度この本からやってみようと思って始めました。今日は2日目。あと2日で終わるのか…(?)

この本ではモデル検査にSpinとNuSMVというツールを使っていますが、書籍中ではSpinはXSpinというGUIを持ったツールを使っていますが、これが既にディスコンぽく、ビルドするのも面倒なのでバイナリが配布されているNuSMVを使用することとしました(Windows上で使用しているため。WSLで使えばよいのではとかありますが、ちょっとお試ししたいだけなのに環境の立ち上げで躓くの嫌なので)

NuSMVの入手

こちらから入手します。2.6.0が最新らしい。登録しなくてもダウンロードできますが、CAPCHAを入れないと先に進めないので注意。あとは自分の環境にあったソースファイルでもバイナリでも入手すればOK。商用利用ではないけどwithoutの方をDLしましたが、お試しで使う分には問題ないかな…。

nusmv.fbk.eu

バイナリ版はインストーラがあるわけではないので、解凍して適当な場所に置いてパスを通すか、bin/下にあるexeファイルのある場所にコードを置いて、cmdたちあげてファイルを与えて実行、という形で、まぁ、ヨシ!って使っています。長期にわたって使うことになったら改めて考えよう。

NuSMVについて知る

NuSMVについてはQiitaに記事があったのでこれもあわせて読むと良いと思います。この本の内容を実行する上では本を読むだけで一応閉じると思いますが…。

qiita.com

最終的には公式のマニュアルを頼ることになるでしょう。

VSCodeの拡張

Simple nuXmv Language Supportって拡張があるので、VSCode上で書くならこれが良さそうです。シンタックスハイライトされて視認性が良くなります。

github.com

f:id:niszet:20200423115404p:plain

動かないコード

マニュアルにも書いてないぽいんですが、case文の左辺(条件式)に1 : a1 みたいな1を書く書き方が弾かれます。logicalを置け、integerを置くなと言われてしまう。なので、上のコードのようにTRUEを置いています。一応これで動いたのでいいのではないかなと。

結果が異なる

4.6のMini Life Gameは解答と実行結果が異なりました。これはご近所の1の数が1のときに{0,1}になってるので、どちらが選ばれるかはツールのバージョン依存があるのでは?と思ってます。コードは見た感じであってるぽいので…。

反例を表示しているので、反例が複数ある場合はどれが表示されるかは一意には決まらないのかな~。このあたりはマニュアルとにらめっこする日が必要かも。とりあえずあり得る遷移であればヨシ、ということで。

出力結果をエクセルに書き写したものはこんな感じになった。またあとでチェックしよう。

f:id:niszet:20200423115950p:plain

感想

省略する記法があるのかもしれないのだけど、同じようなルールをひたすら書いていくのは面倒くさいものがありますね。しかしあらかじめ考えた結果と一致していることが確認できるのは便利だな、と。これ以外のツールもあるだろうし、最終的に何を使うかは考えるとして、ひとまずこの本でモデル検査の概要は掴めそうかな…という感じです。上級編まであるのでひとまずそこまでやろう。