さすがに4日では厳しい感ある
そんなわけで、NuSMVだけですがこの本を使ってモデル検査の入門をしました。
Spinはちょっと環境を整えるところが面倒くさいな…ということで一旦放置中。NuSMVとちょっと動きが違うようなので、その差異は理解しておきたい。
4日目の演習だけ放置してしまってますが、来週後半で2日目あたりから再読するのでそこでやっていきます。時相論理の記法のいくつかは定番の記法として意味とともに暗記してしまった方が良いかもしれない。来週の目標としよう。上級編も購入して届いたわけですが、こちらは4日で～ではないようだ。CTLについて結構なページ数を使っているみたい。LTLとCTLの使い分けができると良さそうだけど、検索した範囲だとLTLで大体事足りそうな気がするが…まだよくわからないね。
発行から10年たってるので当時は難しかった計算量とかは現実に解けるレベルに下りてきているだろうし、ツールのバージョンも上がっているのでもっと効率的に出来ることなどもあると思うのですが、この本で書かれていた内容自体はそのまま使えそう＆そんなに難しくないので気になる人は読んでみると良さそう。1冊目にやるのにちょうど良いですね。ただ、後半は独学だと詰まった時に困る。が、それはどの本でも同じか…。
4日目でコードからモデルを作成するみたいなところがありましたが、NuSMVはステップを表現しないといけないのが面倒くさそう。verilogにはSVAあるし、それで検証すればよいというのもありそうなので、コード検査用にはSpinを見ておいた方が良いのかもしれない（いずれにしてもどこかのタイミングで触った方が良いかな）
あとは出力結果から状態遷移図や表で可視化するツールがあればなぁ…。ログから全部読み解くのはやっぱり厳しい印象。これも要調査ですね。
ちょっととりとめのない文章ですが、ひとまず記録として。最近は週に15時間勉強することにしていますが、なかなか難しいですね…。本を読むだけじゃなくて何かアウトプットしていかないとすぐ忘れてしまうので…
