読者です 読者をやめる 読者になる 読者になる

cloverrose's blog

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

NuSMV 2.5.3をMacでビルド

2013/04/26現在NuSMVの最新バージョンは2.5.4です。そちらではデバッグも必要なくビルドできます。こちらは自分のメモです。
バージョン2.5.4のビルドに関してはNuSMV 2.5.4をMacでビルド - cloverrose's blogを。

Linux,Windows用のバイナリーは提供されていたのでMacはLinux用でOK?と思ってやってみたがうまくいかない。
そこで、ソースコードからビルドすることにしました。

準備

macportでwgetをインストールする

sudo port install wget

その他にもNuSMVのREADMEに記載されてる必要条件を満たすようにアプリをインストール(この要件は最初から満たしていた)

手順

cd NuSMV-2.5.3
cd MiniSat
bash build.sh
cd ../cudd-2.4.1.1
make -f  Makefile_os_x_64bit
cd ../nusmv
./configure
make  # ここでエラーが発生!!

デバッグ

本来ならこの一連の作業でOKのはずだが、ver2.5.3のNuSMVにはバグがあって、makeを実行するとエラーが出ました。
バグはtypedefしたbooleanを使わずboolを使っていたことが原因。

以下に出現するboolをbooleanに置換

  • BddEncBddPrintWff.c Line682
  • compileWrit.c Line940,Line 4625
  • compileWriteUdg.c Line718
  • nodeWffPrint.c Line119

これで再度makeしたらうまく行った。

make

確認

nusmvディレクトリにNuSMVのバイナリが生成されます。

./NuSMV -help

おまけ(デバッグ過程メモ)

makeするとでたエラーはboolをbooleanにして直せたのですが、その他に試みたけどバグが治らなかった方法が1つあって一応メモしておきます。
エラー出力をみると、stdbool.hを#includeしていないせいかと思い、BddEncBddPrintWff.cに#includeを追加して再度makeした。でもそうしたら、また違うエラーが出て、それを読むと、src/util/defs.hで#includeしてて、更にtypedef bool booleanとしていた。この修正は間違っていたことに気づき、自分で追加した#includeを削除。