PEPA — Performance Evaluation Process Algebra

IPC: The International PEPA Compiler

Background

The International PEPA compiler (ipc) is a continuation of work on an earlier compiler for PEPA, the Imperial PEPA compiler, which compiles PEPA models into the input language of Will Knottenbelt's DNAmaca tool. Work on the Imperial PEPA Compiler was undertaken at Imperial College, London and is available from there. See the Imperial PEPA compiler web site for further details.

Modelling Features

IPC supports the full PEPA language plus some non-standard extensions. The extensions are:

• immediate actions with optional immediate rates;
• functional rates; and
• process arrays with or without cooperation.

Thorough static analysis of the input PEPA model is performed. The current list of static analysis checks detects:

• an undefined rate parameter which is used;
• a defined rate parameter which is not then used;
• an undefined process name which is used
• a defined process name which is not used;
• self-loops on states (which have no meaning at the Markov chain level);
• deadlocked states;
• cooperations in which one or both sides do not perform all of the actions in the cooperation set; and
• unnecessary hiding of actions which are not performed by the component.

Measurement Features

The International PEPA Compiler supports the full measurement specification language XSP (eXtended Stochastic Probes). This allows us to specify the set(s) of states in which we are interested in measuring. IPC natively supports the computation of probability density and cumulative distribution functions for passage-time queries. If one specifies that compilation should use the DNAmaca tool to perform the actual numerical analysis then one can also perform transient and steady-state analysis of the model.

Visualisation Features

The model may (with or without the addition of measurement probes) may be output as a .dot file which is in turn converted to a scalable vector graphics file (SVG) depicting the state space of the input model. The .dot file may also be transformed into a PDF file or other output formats see the graphviz website for more details.

Experimental Features

The following translations from the input model are experimental and in various stages of completion.

• translation into PRISM model format - This works well for transformation to an explicit state space but not as well for PRISM's native model description format.
• Translation into FSP - The implementation of this is quite advanced but requires further testing.
• Translation into Dizzy format - We have only an immature implementation so far.

Implementation Details

The International PEPA Compiler is written in the lazy functional programming language Haskell.

Downloading and installing IPC

We provide binary distributions of the smc/ipclib/hydra tool chain for Windows and Linux. Windows users must have cygwin installed. It is available for download at http://www.cygwin.com. Ensure that you include gcc and g++ in your distribution.

• To download the Windows binary distribution, click here
• To download the Linux binary distribution, click here. It has been successfully tested on Linux Fedora Core 6.

Building ipc/ipclib and smc from source