NuSmv安装与使用

来源自我的博客

http://www.yingzinanfei.com/2017/02/01/nusmvanzhuangyushiyong/

下载源代码

http://nusmv.fbk.eu/distrib/NuSMV-2.6.0.tar.gz

最新的2.6.0版本可以自动下载MiniSat和ZChaff

安装依赖

sudo yum install gcc flex bison cmake tar gzip libxml2 readline doxygen tex readline-devel

构建项目，记nusmv解压后的目录为

<TOPDIR>

创建空目录，以生成项目文件

进入子目录
# cd NuSMV
# pwd
<TOPDIR>/NuSMV
# mkdir build
# cd build
# pwd
<TOPDIR>/NuSMV/build

使用

cmake

来构建项目

# cmake ..
[...]
-- Build files have been written to: <TOPDIR>/NuSMV/build

如果构建项目成功，开始编译NuSMV

# pwd
<TOPDIR>/NuSMV/build
# make
make成功后可执行文件存放于<TOPDIR>/NuSMV/build/bin

将NuSMV依赖的文件

master.nusmvrc

所在目录导入环境变量

# export NUSMV_LIBRARY_PATH=<TOPDIR>/NuSMV/share/nusmv

现在可以使用NuSMV来测试安装包里的例子

# pwd
<TOPDIR>/NuSMV/build
# bin/NuSMV ../examples/smv-dist/counter.smv

样例中的smv文件表示的是由系统状态图转换成的SMV模型，其生成语法可参考官方文档

NuSMV语法

http://nusmv.fbk.eu/NuSMV/userman/v26/nusmv.pdf

NuSMV2.6手册

http://nusmv.fbk.eu/NuSMV/tutorial/v26/tutorial.pdf