使用cygwin在win32平台下模拟Unix，假设安装在F:\cygwin，这里安装cygwin时，可以简单地选择全部安装，避免编译过程中缺少某些文件。 1.从NuSMV homepage下载压缩包NuSMV-2.5.，解压至F:\NuSMV-2.5.4
2.参照F:\NuSMV-2.5.4\nusmv\README，下载所需Unix组件，如果cygwin选择全部安装，这一步可以略去
3.下载minisat软件包至F:\NuSMV-2.5.4\MiniSat，以minisat2-070721.zip为例，并解压至当前文件夹，可得到文件夹minisat，复制minisat-default.in并重命名为minisat-default. 4.下载zchaff软件包至F:\NuSMV-2.5.4\zchaff，以zchaff.64bit.2007.3.12.zip为例，并解压至当前文件夹，可得到文件夹zchaff64，复制zchaff-default.in并重命名为zchaff-default.
5.在cygwin的bash中依次键入：
cd F:/NuSMV-2.5.4/cudd-2.4.1.1 (回车)
make (回车)
cd F:/NuSMV-2.5.4/MiniSat (回车)
sh build.sh (回车)
cd F:/NuSMV-2.5.4/nusmv (回车)
./configure (回车)华北油田
make (回车)
至此编译完成，NuSMV 执行命令./configure时默认连接的sat-solver是minisat，所以此时运行，可以看到提示说minisat已连接。
6. 如果希望NuSMV可以使用sat-solver zchaff，需要在cygwin中依次输入：
fla格式
cd F:/NuSMV-2.5.4/zchaff (回车)
sh build.sh (回车)
cd F:/NuSMV-2.5.4/nusmv (回车)
./configure --enable-zchaff
--with-zchaff-incdir=F:/NuSMV-2.5.4/zchaff/zchaff64
--with-zchaff-libdir=F:/NuSMV-2.5.4/zchaff/zchaff64 (回车)
make (回车)香桃木
(这里incdir是SAT_C.h所在文件夹的全路径名，libdir是libsat.a所在文件夹的全路径名)
编译完成后运行，可以看到zchaff也连接上
*****************************************
在F:\cygwin\bin中复制cygexpat-1.dll和cygwin1.dll至F:\NuSMV\NuSMV-2.4.3\nusmv，在其他文件中看到的，需要吗？（不清楚，没有dll文件也可正常运行的）
***************************************
rbd-573
若果不需要sat-solver zchaff，第4步和第6步略去即可，一般情况下有默认连接的minisat就可以了。
这里考虑了使用NuSMV进行限界模型检测的情况，故将sat-solver加载进去了，如果不需要这项功能，略去相应的命令即可。 感谢夏扬同学在NuSMV的编译过程中的帮助！！！
我的特岗生活
NuSMV的使用：
1.首先完成上述编译过程，得到NuSMV的可执行文件。
2.在cygwin中依次输入：
cd F:/NuSMV-2.5.4/nusmv (回车)
./NuSMV -int (回车)
接着屏幕会输出NuSMV的相关信息及NuSMV提示符：
NuSMV>
迷途的女人这里./NuSMV -int 是进入NuSMV的交互运行模式，出现NuSMV提示符，由用户输入相关命令进行验证
若果输入的是./NuSMV filename.smv，则进入批处理模式，系统会对文件描述的模型和性质进行自动验证，这里filename.smv与在同一目录下。
o
k，NuSMV的编译及使用方法介绍就到这里
豫公网安备41160202000603
站长QQ:729038198
关于我们
投诉建议