www.prismmodelchecker.org

PRISM-games: Installation

Binary releases

For binary releases of PRISM-games, the situation is similar to PRISM. The pre-requisites are:

  • Java (version 8 or above)

Installation instructions are the same as for PRISM. In short: Download PRISM-games. Then: for Windows, just run the installer executable; for other binaries, untar and run ./install.sh from inside the directory:

tar xfz prism-games-2.1-linux64.tar.gz
cd prism-games-2.1-linux64
./install.sh

And to run PRISM-games: for Windows, double-click the short-cut; on other OSs, run bin/xprism for the GUI or bin/prism for the command-line version.

Unfortunately, the Windows binary releases currently do not support multi-objective verification for stochastic games. This is because we do not currently have a way to compile the Parma Polyhedra Library (PPL), which is a dependency.


Source releases

To compile source code releases, the pre-requisites are:

  • A Java compiler (as above, for Java version 8 or above)
  • GNU make and a C/C++ compiler (e.g. gcc/g++)
  • Parma Polyhedra Library (PPL), version 1.1 or above, with Java interface (if you want multi-objective support)

Only the last item is different from a regular build of PRISM, which is required for multi-objective verification for stochastic games. If you don't need that, you can omit step 1 below.

For convenience, the repo contains a complete script for setting up PRISM-games on a fresh install of Ubuntu.


1. Install PPL and Java interface

If you are lucky, you may find that your package manager has a copy of PPL with its Java interface (try e.g. yum install ppl-java), but most do not (the ppl package alone is not enough).

So, you will likely need to download PPL and build it from source. This also requires that you have libgmp installed (PPL version 1.2 needs PPL version 4.1.3 or above) and GNU M4. Here is an example of the process on a Linux (Ubuntu) machine:

sudo apt -y install libppl-dev m4
wget http://www.bugseng.com/products/ppl/download/ftp/releases/1.2/ppl-1.2.tar.gz
tar xfz ppl-1.2.tar.gz
cd ppl-1.2
./configure --enable-interfaces=java --with-java=/usr/lib/jvm/java-8-openjdk-amd64
make
sudo make install

On Mac OS, version 1.2 of PPL does not seem to build so you need a newer version, which you can obtain from the PPL Git repo. You'll also need Autoconf, to build the configure script. Here's an example of the process:

brew install gmp autoconf
git clone git://git.cs.unipr.it/ppl/ppl.git
cd ppl
autoreconf -i
./configure --enable-interfaces=java --with-java=/Library/Java/JavaVirtualMachines/jdk1.8.0_171.jdk/Contents/Home
make
sudo make install

To see if the PPL install worked, check that all the libraries are present: whichever directory it was installed to (e.g. /usr/local/lib) should contain libppl.so (or libppl.dylib, or similar, on Mac OS) and a subdirectory ppl containing ppl_java.jar and libppl_java.so (or libppl_java.jnilib, or similar, on Mac OS). If the Java parts are missing, check the config.log to see if there were errors.

The above examples assume that you specify manually where Java is (you need a directory that contains include/jni.h). You might be able to omit the --with-java part.

If you don't want to install as root, you can do a local installation, by adding e.g. --prefix=/home/myname/usr to the call to the configure scripts, and then omitting sudo when running make install.

If libgmp is installed somewhere non-standard, you may need to specify to configure where it is. For example, on a Mac, if you installed libgmp with MacPorts, you might use --with-gmp=/opt/local.


2. Install PRISM-games

Now install PRISM-games. This is basically the usual procedure for PRISM (in short: cd prism and run make), but the Makefile needs to know where PPL is located, which is specified using the variable PPL_DIR.

If ppl-config is in your path, then the Makefile should be able to automatically deduce PPL_DIR (by running ppl-config -l). Then, you will see a line like PPL_DIR: /usr/local/lib displayed near the start when make runs.

cd prism
make

Otherwise, you will need to specify it manually. PPL_DIR should be the directory containing the PPL libraries. More precisely, it should contain libppl.so (or libppl.dylib, or similar, on Mac OS) and a subdirectory ppl containing ppl_java.jar and libppl_java.so (or libppl_java.jnilib, or similar, on Mac OS). This could be /usr/local/lib, if you installed PPL into a standard location, or the lib subdirectory of whatever you set --prefix to in the ./configure step above if you built from source.

cd prism
make PPL_DIR=/usr/local/lib

To check if everything worked, you can try the following (the second one will only work if PPL was successfully installed):

make test
make testppl

As for binary releases, to run PRISM-games: run bin/xprism for the GUI or bin/prism for the command-line version.

Check the PRISM instructions for more details about compiling PRISM from source in general.

PRISM-games