■

ゼミ。新人（B4）研修のためにモデル検査の説明をしました。ほぼ半年前と同じ内容で申し訳ない限りです。新人研修だから簡単にインストールさせたい→SPINはアウト、UPPAALにしよう。課題は簡単にしたい→2ドア問題はUPPAALでは難しいうえにdemoフォルダに解答が入っているからアウト、川を渡る問題はそんなに難しくはないけどなんだかUPPAALに向いていない気がするからアウト、結局信号機問題が一番という結論に。

もうちょっと世の中の役に立ちそうな課題が良いのだろうけど…。どうにもモデル検査の初心者向け課題は世の中の役に立ちそうになくて面白くありません。産総研の本もそこが駄目。どうせ役に立たないのならパズルっぽいやつが良いです。でもパズルならSAT Solverだよなあ。その方がスマート。

いつの間にか蚊がうろうろする季節になっていたようです。