www.prismmodelchecker.org

PRISM-games: Installation

Pre-requisites

  • Java, version 7 or above
  • Parma Polyhedra Library (PPL), version 1.1 or above, with Java interface (if you want multi-objective support)
  • gcc, g++, make, etc. (if you want to build from source)

Currently, PRISM-games version 2.0 (with multi-objective support, amongst other things), is available as source code or Linux/Max binaries but we do not yet have a Windows binary.


Basic Installation

If you do not need support for multi-objective properties, installation of PRISM-games is exactly the same as for PRISM (see these instructions).

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; for source code distributions, untar and run make from inside the directory

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


Full Installation (with multi-objective support)

To use the multi-objective functionality in PRISM-games, you need to make sure that you have the Parma Polyhedra Library (PPL) installed. To be more precise, you need version 1.1 or higher of PPL, and you need it's Java interface.


1. Install PPL

If your software package manager has a new enough version, you can do something like:

yum install ppl-java

If not, you may need to build PPL from source. This also requires that you have libgmp installed.

Download PPL from http://bugseng.com/products/ppl/download. Then, for example:

./configure --enable-interfaces=java
make
sudo make install

If you don't want to install as root, you might prefer to do a local installation:

./configure --enable-interfaces=java --prefix=/home/myname/usr
make
make install

For the first step, if libgmp is installed somewhere non-standard, you may need to specify where it is. For example, on a Mac, if you installed libgmp with MacPorts, you might use:

./configure --with-gmp=/opt/local --enable-interfaces=java --prefix=/home/myname/usr

And you may also need to specify where Java is (you need a directory that contains include/jni.h). For example, on a Mac, this might look like:

./configure --with-gmp=/opt/local --enable-interfaces=java --with-java=/Library/Java/JavaVirtualMachines/jdk1.7.0_17.jdk/Contents/Home --prefix=/home/myname/usr

2. Install PRISM-games

Now install PRISM-games. This is basically the usual procedure for PRISM, but the Makefile needs to know where PPL is located, which is specified 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).

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.jnilib, or similar) and a subdirectory ppl containing ppl_java.jar and libppl_java.so (or libppl_java.jnilib, or similar). 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.

If building PRISM-games from source, it should suffice to run make. For example:

make PPL_DIR=/usr/local/lib

Check the PRISM instructions for more details.

For a (non-Windows) binary distribution, untar the file and then run the install script:

PPL_DIR=/usr/local/lib ./install.sh

To run PRISM-games: run bin/xprism for the GUI or bin/prism for the command-line version.

PRISM-games