Skip to content

Install

To get ProVeLines running on your computer, please follow the following steps. Note that ProVeLines is meant to run under Linux and Mac OS X only. We do not guarantee compatibility with other operating systems and do not provide support for them.

  1. Download ProVeLines.
  2. Unzip the archive and go to the ProVeLines/src directory.
  3. Open configure.h and uncomment the lines related to the features you want to include to ProVeLines.
  4. If you have enabled the real-time (CLOCK option) :
    1. Open build.sh, comment the line beginning by REALTIME="" and uncomment the next one.
    2. Go to the ProVeLines/src/lib/UPPAAL-dbm/modules directory.
    3. Follow the instructions written in the README file to compile DBM. You need boost for this. If the make command fails, open makefile and check that the seventh line is export AR := ar.
    4. Go back to the ProVeLines/src directory.
  5. If you have enabled the numeric features (ATTR option) :
    1. Go to the ProVeLines/src/lib/z3 directory.
    2. Follow the instructions written in the README file to compile Z3. You need wine and autoconf for this.
    3. Copy libz3.dylib (or libz3.so depending on your OS) into the ProVeLines/src/lib/z3 directory. By default it is found in your /usr/lib/ directory.
    4. Go back to the ProVeLines/src directory.
  6. Open build.sh and look for the lines beginning by “BOOL=“. Uncomment only the line related to the data structure you want ProVeLines to use. Note that if you enabled NUMERIC_FEATURES then you must uncomment the Z3-related line.
  7. Execute build.sh.

You’re done! You may now execute ProVeLines. If you enabled MULTI-FEATURES, you must first
execute the following: export DYLD_LIBRARY_PATH=./lib/z3:$DYLD_LIBRARY_PATH