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.
To compile source code releases, the pre-requisites are:
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.