www.prismmodelchecker.org

PRISM-games: Installation

PRISM-games is known to run on Linux, Windows and Mac OS X, both 64-bit and 32-bit versions.

We provide both binary and source releases. For more up-to-date source code, see the GitHub repo.


Installing binary releases

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

  • Java, version 9 or above: a Java Runtime Environment (JRE) suffices, e.g. from Oracle or AdoptOpenJDK

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-3.0-linux64.tar.gz
cd prism-games-3.0-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.


Compiling from source (without multi-objective support)

Compiling PRISM-games from source code is somewhat easier if you do not need support for multi-objective verification of stochastic games.

If this is the case, the situation is similar to PRISM. The pre-requisites are:

  • Java, version 9 or above: a Java Development Kit (JDK), e.g. from Oracle or AdoptOpenJDK
  • GNU make and a C/C++ compiler (e.g. gcc/g++)

Compilation instructions are the same as for PRISM.

On non-Windows platforms, untar and run make from inside the prism sub-directory:

tar xfz prism-games-3.0-src.tar.gz
cd prism-games-3.0-src/prism
make

Then, as for binaries, run bin/xprism for the GUI or bin/prism for the command-line version.

Compiling on Window needs Cygwin. See this page (about compiling PRISM) for details.


Compiling from source (with multi-objective support)

Compiling PRISM-games from source code with support for multi-objective verification of stochastic games also needs:

in addition to Java 9, GNU make and gcc/g++, as above.

Notes on the two main steps (installing PPL; building PRISM) are given below.

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


1. Install PPL and its Java interface

Most package managers do not provide PPL with its Java interface (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 libgmp version 4.1.3 or above) and GNU M4.

As a further complication, the PPL install seems to need Java 8 (because it looks for javah), which means that you need to compile PPL with Java 8 and then PRISM-games with Java 9 or above.

Here is an example of the process on a Linux (Ubuntu) machine:

sudo apt -y install openjdk-8-jdk libgmp-dev m4
export JAVA8_HOME=`find /usr/lib/jvm -name 'java-8*'`
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=$JAVA8_HOME
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.

At present we do not have a way of building PPL on Cywgin (and therefore on Windows). So, if you want to compile from source on Windows, then do so without muti-objective support.

PRISM-games


2,962 downloads of PRISM-games to date.