`PARAM` Tool Homepage

PARAM is a tool with the purpose of handling parametric variants of models specified in a variant of the PRISM language. PARAM is capable of computing the unbounded reachability probability for parametric discrete-time Markov chains. Apart from this, it can also handle special classes of Markov decision processes, as well as reachability rewards for Markov reward models. To speed up computations, it can compute the (strong and weak) bisimulation quotient of parametric models. The PARAM source code is available under the GNU GENERAL PUBLIC LICENSE (GPL) Version 3.

PARAM has two sisters, PASS and INFAMY, that accept virtually the same language, but have different strengths.

Download and Installation

The latest binaries of PARAM 2 with the improvements of our recent NFM paper [HahnHZ11] can be obtained below. Notice that the version is not tested very well so far. This version includes support for nested PCTL properties and parametric Markov decision processes.

Downloads

The latest binaries of PARAM 1 [HahnHWZ10] can be obtained here:

Compared to the version described in the STTT journal paper [HahnHZ10], within others the following technical improvements have been done. They should lead to a better performance in the most common use cases, and make the tool easier to be build.

more memory-efficient data structures
usage of LuaJIT instead of calling C++ compiler
usage of GiNaC instead of CoCoALib to cancel rational functions
improved parser
no support for nondeterminism. The technique from papers before the NFM paper [HahnHZ11] did not work anyway. A preliminary version including support for nondeterminism can be found above.

Note: for earlier versions of GiNaC, there is a problem with the cancellation routine. If you get an error message which mentions "mpz_set_str", please use the version of GiNaC from its Git repository. In case problems remain, the latest version still based on CoCoALib is still available.

The PARAM source code is also available (download form).

To build PARAM on Mac OS X, please do the following (thanks to Steffen Märcker):

Use MacPorts GCC >= 4.4 for PARAM and dependencies
(Attention! Dependencies will be incompatible with other ports!)

sudo port install gcc47
sudo port install boost configure.compiler=macports-gcc-4.7
sudo port install ginac configure.compiler=macports-gcc-4.7
sudo port install liblua configure.compiler=macports-gcc-4.7

sudo port select gcc mp-gcc47
make
sudo port select gcc none


--- Makefile modifications ---
LIB    = -lginac -lcln -lgmpxx -lgmp -lboost_program_options-mt \
-lluajit-5.1 -ldl

INCLUDE_DIRS = -I. -I/opt/local/include
LINK_DIRS = -L/opt/local/lib

FLAGS        = -Wall -O3 -w -DNDEBUG -pipe $(INCLUDE_DIRS) $(LINK_DIRS)

Changes in PARAM 2.3 Alpha

expected accumulated rewards for CTMCs (take care, did not apply many tests there yet)

Changes in PARAM 2.2 Alpha

probabilities and rewards may depend on model variables (for probabilities already in 2.1)
dependency to CVC3 removed

Compilation

Once you have unzipped the source package, change to the param-vXXXX directory. Delete the existing file "param" there. Type make to compile PARAM. In order to compile PARAM, Boost 1.39.0 or higher must be installed on your system (ideally, the latest version should be installed). Once compilation finishes, the binary may be executed in place. You may have to adopt the Makefile accordingly

Installation

There in no installation routine; once you have unzipped the binaries package or compiled PARAM from source, you can run the tool in place. If you wish, you can copy the executables to your bin directory (~/bin as normal user or /usr/bin as root to make PARAM available system-wide).

In case of problems with running the binary or compiling the sources, please contact Ernst Moritz Hahn.

Authors

PARAM was developed by Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang and Björn Wachter.

Contact/Support

For questions, comments and support requests regarding PARAM, please contact "emh [at] cs [dot] uni [minus] saarland [dot] de".

PARAM Tool Homepage