Pre-preparation for paraVerifier (Eng. ver)

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

This article shows how to install paraVerifier

  • ParaVerifier：an automatic framework for parameterized verification

  • Download here

NuSMV

Follow the instructions here

Prepreparation

1
2
brew install cmake
brew install gcc

Install

1
2
3
4
5
6
7
8
9
10
11
12
13
cd some-where-you-want-save-NuSMV

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

# unzip
tar xzf NuSMV-2.6.0.tar.gz 

cd NuSMV-2.6.0/NuSMV
mkdir build
cd build
cmake ..
make
Check

If there is a folder bin in build, and there is an executive file NuSMV, then you are success.

Environment variable

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

Z3

Download

1
git clone https://github.com/angr/angr-z3.git

Install

1
2
cd angr-z3
python scripts/mk_make.py --prefix=/root-path-is-better --python --pypkgdir=/dir-to-python-site-packages

NOTE

  • --prefix sets the scale within which you would like to use z3

  • dir-to-python-site-packages: e.g., /home/bella/lib/python-2.7/site-packages

  • either python 2 or 3 works, but need to use the desired python version to compile scripts

1
2
3
cd build
make
make install

Run example

1
2
cd examples/python
python example.py

show:

1
2
sat
[y = 3/2, x = 4]

CMurphi

here

Isabelle

here

Ocaml

1
2
3
4
5
6
7
brew install ocaml

# opam:manage Ocaml packages
brew install opam  

#opam initialization
opam init

Version:

  • ocaml-4.04.0
  • opam-1.2.2_2

The above commands are for MacOS, for other systems, commands can be found here

Note

Environment path of opam can be configured as follow:

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

Package needed

Opam is used to manage Ocaml packages, so we use opam to install the following pacakges:

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

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

NOTE1

On Mac and Ubuntu上，some packages have different names，the correspondent are as follow：

  • oasis = ocaml-nox + oasis2opam 
  • ocaml-doc = opam-file-format
  • ocaml-findlib = ocamlfind
  • libpcre-ocaml-dev = sexplib

NOTE2

Make sure you have installed core 和utop successfully.

1
2
3
4
5
opam install core utop

# if success, these two lines will show
∗  installed core_kernel.113.33.02+4.03
∗  installed core.113.33.02+4.03

Configuration

vim ~/.ocamlinit and insert the following statements:

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

Compile

Try an example:

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

Run example

paraVerifier has a server and a client, so we need 2 terminal windows to run the example.

Server

Set path

SetSMV_PATH, MU_PATH, MU_INCLUDE in server／settings.py 

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 = （look up by typing： gcc -v ）

Run server

1
2
cd server
python server.py -v

Client

Open another terminal window

cd to /example, runmutualEx.byte

1
./muturalEx.byte

Then we can see from client window that there are two initial states:

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

while in server window we can see data flow like this:

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

Success and done!