ParaVerifier安装配置

发表于 更新于 分类于 阅读次数：

本文详细介绍ParaVerifier的安装配置过程

  • ParaVerifier：形式化验证工具，自动化证明协议的框架

  • 下载地址

    ​

安装环境

  • Mac OX (不限，本机是mac)
  • 需要gcc，cmake等。如果有其他提示，依然是brew install。如果没有homebrew，就安装一下

所需安装

###NuSMV

介绍

符号化的模式识别器，开源，适用于各大平台

安装

安装依赖库
1
2
brew install cmake
brew install gcc
开始安装
1
2
3
4
5
6
7
8
9
10
11
12
13
14
# 切换到某路径下
cd some-where-you-want-save-NuSMV

# 下载压缩包
wget http://nusmv.fbk.eu/distrib/NuSMV-2.6.0.tar.gz

# 解压
tar xzf NuSMV-2.6.0.tar.gz 

# 切换到刚刚解压的NuSMV目录下
cd NuSMV-2.6.0/NuSMV

# 新建一个build文件夹
mkdir build

接着继续，刚刚已经在NuSMV中新建了一个build文件夹，之后就是进入，安装即可：

1
2
3
4
# 进入新建的build文件夹中
cd build

cmake ..

这时候就完成了configure的过程，现在要make一下，进行编译（仍然在build文件夹的路径里）：

1
make
检验是否编译成功

compile成功的标志是build 文件夹里新增了一个bin文件夹，里面有可执行文件NuSMV

配置

接下去就是设置环境变量。

NuSMV 在使用的时候，会在共享环境变量中找文件”master.nusmvrc” ，所以要设置一下路径，链接到NuSMV／share／nusmv的路径：

1
export NUSMV_LIBRARY_PATH=../NuSMV-2.6.0/NuSMV/share/nusmv

Z3

介绍

Z3是一个定理证明器，可以在github上直接下载

安装

从git上clone
1
git clone https://github.com/Z3Prover/z3.git
解压

接下来两种方法，cmake 和 gcc可以安装（各种平台的安装方式，详见z3 github页面）

用gcc进行安装
1
2
3
4
5
6
# 进入解压的路径
python scripts/mk_make.py
mkdir build # 新建文件夹
cd build
make # 这个过程很漫长！
sudo make install #这就成功安装啦！

配置环境变量

安装成功之后，需要配置环境。在github的文档中没有写，但是如果不设置，就无法在python中引入z3。

注意！！因为这个无法用pip安装！！但是python运行的时候会提示找不到z3

（通过pip install z3是可以安装的，但是经过测试发现，那样安装上的z3 仍然不够，会出现其他的错误。）

1
2
Bella$ export DYLD_LIBRARY_PATH=../z3-master/build 
Bella$ export PYTHONPATH=/z3-master/build/python

CMurphi

介绍

模型检测工具

具体安装方法见Murphi入门

Isabelle

点击链接，直接下载

Python

python2.7.13 是python2中比较稳定的一个版本，所以安装的是这个版本。

当然，目前出到python3.相较于2还是有很多优势的。但是这个脚本是用python2写的，所以就先用python2运行。

安装库

python的包管理是pip，所以也需要安装pip

1
2
3
4
5
# 以下两条命令选一条执行

easy_install pip
# 或者
brew install pip

如果执行失败，则加sudo

安装pexpect

这个pexpect是用于python运行服务器的时候用的

1
pip install pexpect

编译Murphi到Ocaml

牛刀小试，试试看可以用安装好的python直接运行murphi2ocaml文件夹下的脚本进行murphi到Ocaml语言的翻译（.m到.ml）

1
2
3
cd ../murphi2ocaml

python gen.py -m murphi/mutualEx.m > ../examples/mutualEx.ml

在examples目录下就可以看到新生成的mutualEx.ml了

Ocaml

安装

1
2
3
4
5
6
7
brew install ocaml

# opam 用来管理ocaml及其包
brew install opam  

#opam 还需要初始化
opam init

这时，ocaml-4.04.0和opam-1.2.2_2就安装好了～

其他系统的安装方式见链接

注意

如果在opam安装的时候路径没有配置好，就需要：

1
2
eval `opam config env`
. ~/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

安装依赖库

Ocaml的安装包统一由opam进行管理。就像python的pip一样。

直接用opam进行安装

1
opam install ocaml-nox ocaml-native-compilers ocaml-doc ocaml-findlib oasis libpcre-ocaml-dev

注意

Mac和Ubuntu上，Ocaml的依赖包名称是不一样的，对应关系如下：

  • 安装了oasis，也就相当于安装了ocaml-nox，因为oasis依赖ocaml-nox. 还需要再安装 oasis2opam 
  • ocaml-doc = opam-file-format
  • ocaml-findlib = ocamlfind
  • libpcre-ocaml-dev = sexplib

继续安装依赖库

1
opam install utop core async yojson core_extended core_bench cohttp async_graphics cryptokit menhir re2

注意

最后一定要记得检查一下，是否安装好了core 和utop这两个重要的包。因为有可能它们在第一次安装时不成功。

一般安装不成功，是由于其他的依赖包没有安装成功or环境变量没配置好or前面的哪个步骤没有做，所以如果安装失败，则重新检查以上步骤，直到安装成功为止。

1
2
3
4
5
opam install core utop

# show
∗  installed core_kernel.113.33.02+4.03
∗  installed core.113.33.02+4.03

安装配置

配置ocaml初始化文件，通过在命令行输入：vim ~/.ocamlinit 进入，摁i键进行INSERT，把这些复制在已有的文字下面：

1
2
3
4
5
6
#use "topfind";;
#thread;;
#camlp4o;;
#require "core.top";;
#require "core.syntax";;
#require “async”;;

然后esc, ：wq即可退出。

编译.ml文件

安装Ocaml成功之后，试试看能否将Ocaml语言编译成可执行文件：

1
2
cd ../examples
corebuild mutualEx.byte -pkg re2 -I src

C/S框架

整个ParaVerifier是一个基于服务端／客户端的框架，所以要开两个命令窗口，一个运行server，一个运行客户端的程序。

服务器端

路径设置

在sever／settings.py里设置SMV_PATH, MU_PATH, MU_INCLUDE的路径。

写上相应路径即可

1
2
3
4
5
6
7
SMV_PATH = '../NuSMV-2.6.0/NuSMV/build/bin/NuSMV'

MU_PATH = '../cmurphi5.4.9.1/src/mu'

MU_INCLUDE = '../cmurphi5.4.9.1/include'

GXX_PATH = （用命令行： gcc -v 查看）

运行服务器

1
2
cd server
python server.py -v

客户端

新开一个terminal

切换到/example路径下，运行之前的步骤在examples下生成的mutualEx.byte

1
./muturalEx.byte

这时候在客户端可以看到两个初始化状态：

1
2
initial invs:
((n[1] = c) & (n[2] = c))

在服务端可以看到数据在疯狂地跑：（遍历所有的情况）

1
2
3
4
.........
2,2371,n_mutualEx:  None
2,2372,n_mutualEx:  None
........

至此，ParaVerifier安装、配置、运行成功！

​