The following contains instructions to get a working PathFinder build. PathFinder only runs on Linux.
Downloading PathFinder
You can get the sources over at Github, or use this direct link to the ZIP archive.
Requirements
bam
PathFinder uses the bam build system. Get it from Github or install the Debian package:
apt-get install bam
OTAWA
Get it at http://otawa.fr/. You will need OTAWA v2. If you run into trouble with dependencies on Debian, I suggest using
apt-get install flex bison bzr g++ ocaml libxml2-dev libxslt-dev mercurial
An SMT solver
PathFinder supports two SMT solvers, CVC4 and z3. You can use either with very comparable performances and almost identical outputs.
CVC4
If you have admin rights on your machine, you can get CVC4 with an automated script:
./get_cvc4.sh
You may also want to try a local install (which can be trickier) with
./get_cvc4_local/all.sh
Z3
Z3 tends to be significantly less tricky to install. You can follow the instructions at https://github.com/Z3Prover/z3.
Installing PathFinder
To install, type bam
and follow the instructions. bam config
will run a default config, which you can reset by removing the config.lua file. In order to select either solver, use bam config solver=cvc4
or bam config solver=z3
.
Alternatively, you can use ./make_cvc4
or ./make_z3
.
Note: In order to run PathFinder with maximum performance (for benchmarking), you must run bam config O=3 debug=false warnings=false v1=false
.
Note: If your terminal does not support UTF-8, use bam config utf8=false