##chalmers-lava2000 の verify をうごかそうとしてるんだけど、外部の定理証明器を呼ぼうとするらしい。さてさてどうするべか。
#半加算器の出力が共にhighになることはないというpropertyをverifyしたいだけなんだけどなぁ。。。
#prover.wrapper が必要。Script/にはsatzoo.wrapperとsmv.wrapperがあるわけだから、どちらかをインストールすればいいのかな。
#satzoo と smv はバージョンがあわないのか、うまくいかん
#Visはwrapperスクリプトがないなぁ。。。ふむ
#自分で書くのかぁ
haskell-ja > Archives > 2009/06/11