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.
For binary releases of PRISM-games, the situation is similar to PRISM. The pre-requisites are:
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 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:
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 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.
Site hosted at the Department of Computer Science, University of Oxford