-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathINSTALL
79 lines (52 loc) · 3.38 KB
/
INSTALL
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
This document contains the instruction to install F3.
The repository contains a Dockerfile, if this option is viable for you please consider following the instructions reported in README.md.
The following instructions should work on any linux-based operating system and have been tested on Ubuntu20.04.
## Install the dependencies
Please use your system packet manager to install (swig version >= 4, python version >= 3.5):
`python3`, `python3-pip`, `flex`, `bison`,
`libpcre3`, `libgmp`, `git`, `autoconf` and `swig` on your system.
F3 has been tested using python3.8 and should run using python3.5 or above.
The following commands install the required packages on Ubuntu20.04 (might require sudo):
$> apt -y update
$> apt -y install python3 python3-pip git libgmp-dev swig
## Download Pysmt
Let PYSMT_HOME be the directory in which to download Pysmt.
For example run:
$> export PYSMT_HOME=$HOME/pysmt
Then, download the Pysmt source code from GitHub:
$> git clone https://github.com/EnricoMagnago/pysmt.git $PYSMT_HOME
## Download F3
Let F3_HOME be the directory in which to download F3.
For example run:
$> export F3_HOME=$HOME/F3
Then, download the F3 source code from GitHub:
$> git clone https://github.com/EnricoMagnago/F3.git $F3_HOME
## Install Pysmt.
Change Pysmt branch to the nonlinear branch.
$> cd $PYSMT_HOME; git checkout nonlinear
Install Pysmt, might require sudo.
$> cd $PYSMT_HOME; python3 ./setup.py install;
Install the SMT-solvers mathsat and z3, this command will ask to accept their licences.
$> pysmt-install --z3 --msat
## Install F3
By default pysmt downloads the SMT-solvers in $HOME/.smt_solvers.
F3 requires the header and library of mathsat to be in the system paths.
Copy the header and library file in the system paths by running the following two commands as sudo:
$> cp $HOME/.smt_solvers/msat/mathsat-5.6.6-linux-x86_64/include/mathsat.h /usr/include/mathsat.h
$> cp $HOME/.smt_solvers/msat/mathsat-5.6.6-linux-x86_64/lib/libmathsat.a /usr/lib/libmathsat.a
The module used by F3 to perform the LTL tableau construction requires to include the mathsat header.
$> patch $F3_HOME/src/ltl/ltl.i $F3_HOME/ltl_i.patch
If you copied "mathsat.h" in some path different from "/usr/include/mathsat.h", please manually edit ltl.i and type the correct path of "mathsat.h".
## Build LTL module of F3
$F3_HOME/src/ltl, contains 2 scripts that build the LTL module and swig interface.
These scripts require the "libmathsat.a" to be available in the system paths and the include path of "mathsat.h" in "ltl.i" should be correct.
Build the LTL module in release mode by running the following command:
$> cd $F3_HOME/src/ltl; ./swig_release_build.sh
or in debug mode with:
$> cd $F3_HOME/src/ltl; ./swig_debug_build.sh
## Run F3
For a set of command line options $OPTS for F3 and benchmark file $BENCHMARK, the following command allows to run F3 with the given options on such benchmark.
$> python3 -O $F3_HOME/src/run_f3.py $OPTS $BENCHMARK
For example to run F3 with verbosity 1 on benchmark "NonTerminationSimple2_false-termination":
$> python3 -O $F3_HOME/src/run_f3.py -v 1 $F3_HOME/benchmarks/software_nontermination/f3/C/Ultimate/NonTerminationSimple2_false-termination.py
We use the -O option for the python interpreter because the source code of F3 contains many assertions that perform additional checks, meant for debugging, that significatly slow down its performance.