The operation of PRISM can be configured in a number of ways. From the GUI, select "Options" from the main menu to bring up the "Options" dialog. The settings are grouped under several tabs. Those which affect the basic model checking functionality of the tool are under the heading "PRISM". Separate settings are available for the simulator and various aspects of the GUI (the model editor, the property editor and the log).
User options and settings for the GUI are saved locally and reused. They are stored in the file .prism
, which can be found in your home directory (~
) under Unix, Linux or Mac OS X and in e.g. C:\Documents and Settings\username
under Windows. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the .prism
file is in a simple textual format and can be edited by hand. To restore the default options for PRISM, click "Load Defaults" and then "Save Options" from the "Options" dialog in the GUI. Alternatively, delete the .prism
file and then re-launch the GUI.
From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
For some switches, whose format is not straightforward, there is additional help available on the command-line, using -help switch
. For example:
The .prism
settings file is ignored by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file is read, using the -settings
switch, e.g.:
In the following sections, we give a brief description of the most important configuration options available.
Separately from the choice of engines, PRISM often offers several different solution methods that can be used when performing model checking. The choice of method (and their settings) depends on the type of analysis that is being done.
When analysing MDPs, there are several options. You can select these under the "MDP solution method" setting from the GUI, or use the command-line switches listed below. Currently, all except value iteration are only supported by the explicit engine. For more details of the methods, see e.g. [FKNP11] (about probabilistic verification of MDPs) or classic MDP texts such as [Put94]).
-valiter
) [this is the default]
-gs
)
-politer
)
-modpoliter
)
Where the methods above use iterative numerical solution, you can also use the settings under "Convergence" described in the Iterative Numerical Methods section.
When computing transient probabilities of a CTMC
(either directly or when verifying time-bounded operators of CSL), there are two options:
uniformisation and fast adaptive uniformisation (FAU). These can be selected using the GUI option "Transient probability computation method", or using the command-line switch -transientmethod <name>
, where <name>
is either unif
or fau
.
Uniformisation is a standard iterative numerical method for computing transient probabilities on a CTMC, which works by reducing the problem to an analysis of a "uniformised" DTMC.
As an optimisation, when it is detected that the transient probabilities have converged, no further iterations are performed. If necessary (e.g. in case of round-off problems), this optimisation can be disabled with the "Use steady-state detection" option (command-line switch -nossdetect
).
Fast adaptive uniformisation (FAU) [MWDH10] is a method to efficiently approximate transient properties of large CTMCs. The basic idea is that only the parts of the model that are relevant for the current time period are kept in memory. In more detail, starting with the initial states, in each step FAU explores further states in a DTMC which is a discrete-time version of the original CTMC. By combining the probabilities there with those of a certain continuous-time stochastic process (a birth process), transient properties in the original CTMC can be computed. If it turns out that the probability of being in some state in the DTMC is below a given threshold, this state is removed from the model explored so far. After a given number of steps, which corresponds to the number of steps which are likely to happen within the time bound, the exploration can be stopped. In the implementation in PRISM [DHK13], FAU can be used to compute transient probability distributions and to model check the following types of non-nested CSL formulas: time-bounded until, instantaneous reward, cumulative reward.
The following options can be used to configure FAU:
-fauepsilon <x>
): FAU analyses the DTMC for a number of iterations such that the probability of more steps being relevant is below this value. The default is 1e-6.
-faudelta <x>
): States that have a lower probability than this value are discarded. The default is 1e-12.
-fauarraythreshold <x>
): After this number of steps without any new states being explored or discarded, FAU will switch to a faster, fixed-size data structure until further states have to be explored or discarded. The default is 100.
-fauintervals <x>
): In some cases, it is advantageous to divide the time interval the analysis is done for into several smaller intervals. This option dictates the number of (equal length) intervals used for this split. The default is 1, meaning that only one time interval is used.
-fauinitival <x>
): It is also possible to specify an additional initial time interval which is handled separately from the rest of the time. This is often advantageous, because in this interval certain parameters of the model can be explored, which can subsequently be used to speed up the computation of the remaining time interval. The default for this option is 1.0.
PRISM contains four main engines, which implement the majority of its model checking functionality:
The first three of these engines are either wholly or partly symbolic, meaning that they use data structures such as binary decision diagrams (BDDs) and multi-terminal BDDs (MTBDDs). For these three engines, the process of constructing a probabilistic model (DTMC, MDP or CTMC) is performed in a symbolic fashion, representing the model as an MTBDD. Subsequent numerical computation performed during model checking, however, is carried out differently for the three engines. The "MTBDD" engine is implemented purely using MTBDDs and BDDs; the "sparse" engine uses sparse matrices; and the "hybrid" engine uses a combination of the other two. The "hybrid" engine is described in [KNP04b]. For detailed information about all three engines, see [Par02].
The fourth engine, "explicit", performs all aspects of model construction and model checking using explicit-state data structures. Models are typically stored as sparse matrices or variants of. This engine is implemented purely in Java, unlike the other engines which make use of code/libraries implemented in C/C++. One goal of the "explicit" engine is to provide an easily extensible model checking engine without the complication of symbolic data structures, although it also has other benefits (see below).
The choice of engine ("MTBDD", "sparse", "hybrid" or "engine") should not affect the results of model checking - all engines perform essentially the same calculations. In some cases, though, certain functionality is not available with all engines and PRISM will either automatically switch to an appropriate engine, or prompt you to do so. Performance (time and space), however, may vary significantly and if you are using too much time/memory with one engine, it may be worth experimenting. Below, we briefly summarise the key characteristics of each engine.
When using the PRISM GUI, the engine to be used for model checking can be selected from the "Engine" option under the "PRISM" tab of the "Options" dialog. From the command-line, engines are activated using the -mtbdd
, -sparse
, -hybrid
and -explicit
(or -m
, -s
, -h
and -ex
, respectively) switches, e.g.:
Note also that precise details regarding the memory usage of the current engine are displayed during model checking (from the GUI, check the "Log" tab). This can provide valuable feedback when experimenting with different engines.
Although it is not treated as a separate "engine", like those above,
PRISM also provides approximate/statistical model checking,
which is based on the use of discrete-event simulation.
From the GUI, this is enabled by choosing "Simulate" menu items or tick boxes;
from the command-line, add the -sim
switch.
See the "Statistical Model Checking"
section for more details.
Most of PRISM's model checking functionality uses numerical solution based on floating point arithmetic and, often, this uses iterative numerical methods, which are run until some user-specified precision is reached. PRISM currently has some support for "exact" model checking, i.e., using arbitrary precision arithmetic to provide exact numerical values. Currently, this is implemented as a special case of parametric model checking, which limits is application to relatively small models. It can be used for analysing DTMCs/CTMCs (unbounded until, steady-state probabilities, reachability reward and steady-state reward) or MDPs (unbounded until and reachability rewards). You can enable this functionality using the "Do exact model checking" option in the GUI or using switch -exact
from the command line.
The techniques used to model check PTAs are different to the ones used for DTMCs, MDPs and CTMCs. For PTAs, PRISM currently has three distinct engines that can be used:
The default engine for PTAs is "stochastic games". The engine to be used can be specified using the "PTA model checking method" setting in the "PRISM" options panel in the GUI. From the command-line, switch -ptamethod <name>
should be used where <name>
is either games
, digital
or backwards
.
The choice of engine for PTA model checking affects restrictions that imposed on both the modelling language and the types of properties that can be checked.
When performing the computation of probabilities and expected costs/rewards during verification, PRISM often uses iterative numerical methods. The methods used vary depending on the type of verification being performed. In some cases, PRISM solves systems of linear equation systems (e.g. "until" properties for DTMCs and CTMCs, steady-state properties for CTMCs and "reachability reward" properties for DTMCs). For this, a range of methods are available (see below). For "until" and "reachability reward" properties of MDPs, PRISM uses a method called "value iteration". For computations involving transient probabilities of CTMCs (e.g. "bounded until" and "cumulative reward" properties), it uses a method called "uniformisation".
Common to all of these methods is the way that PRISM checks convergence, i.e. decides when to terminate the iterative methods because the answers have converged sufficiently. This is done by checking when the maximum difference between elements in the solution vectors from successive iterations drops below a given threshold. The default value for this threshold is 10-6 but it can be altered with the "Termination epsilon" option (switch -epsilon <val>
). The way that the maximum difference is computed can also be varied:
either "relative" or "absolute" (the default is "relative"). This can be changed using the "Termination criteria" option (command-line switches -relative
and -absolute
, or -rel
and -abs
for short).
Also, the maximum number of iterations performed is given an upper limit
in order to trap the cases when computation will not converge.
The default limit is 10,000 but can be changed with the "Termination max. iterations" option (switch -maxiters <val>
). Computations that reach this upper limit will trigger an error during model checking to alert the user to this fact.
For instances where PRISM has to solve a linear equation system (see above), the numerical method used can be selected by the user. Below is a list of the alternatives available and the switches used to select them from the command-line. The corresponding GUI option is "Linear equations method".
-power
(or -pow
, -pwr
)
-jacobi
(or -jac
)
-gaussseidel
(or -gs
)
-bgaussseidel
(or -bgs
)
-jor
-sor
-bsor
When using the MTBDD engine, Gauss-Seidel/SOR based methods are not available. When using the hybrid engine, pseudo variants of Gauss-Seidel/SOR based method can also be used [Par02] (type prism -help
at the command-line for details of the corresponding switches). For methods which use over-relaxation (JOR/SOR), the over-relaxation parameter (between 0.0 and 2.0) can also be specified with option "Over-relaxation parameter" (switch -omega <val>
).
For more information about all the issues discussed in this section, see e.g. [Ste94].
To increase the amount of information displayed by PRISM (in particular, to display lists of states and probability vectors), you can use the "Verbose output" option (activated with comand-line switch -verbose
or -v
). To display additional statistics about MTBDDs after model construction, use the "Extra MTBDD information" option (switch -extraddinfo
) and, to view MTBDD sizes during the process of reachability, use option "Extra reachability information" (switch -extrareachinfo
).
Sometimes, model checking of properties for MDPs requires fairness constraints to be taken into account.
See e.g. [BK98],[Bai98] for more information.
To enable the use of fairness constraints (for P
operator properties), use the -fair
switch.
By default, when constructing a model, PRISM checks that all probabilities and rates are within acceptable ranges (i.e. are between 0 and 1, or are non-negative, respectively). For DTMCs and MDPs, it also checks that the probabilities sum up to one for each command. These checks are often very useful for highlighting user modelling errors and it is strongly recommended that you keep them enabled, however if you need to disable them you can do so via option "do prob checks?" in the GUI or command-line switch -noprobchecks
.
You can also change the level of precision used to check that probabilities sum to 1 using the option "Probability sum threshold" (or command-line switch -sumroundoff
.
CUDD, the underlying BDD and MTBDD library used in PRISM has an upper memory limit. By default, this limit is 1 GB. If you are working on a machine with significantly more memory this and PRISM runs out of memory when model checking, it may help to change this. To set the limit, from the command-line, use the -cuddmaxmem
switch. For example:
Above, g
denotes GB. You can also use m
for MB.
You can also the CUDD maximum memory setting from the options panel in the GUI, but you will need to close and restart the GUI (saving the settings as you do) for this to take effect.
The Java virtual machine (JVM) used to execute PRISM also has upper memory limits. Sometimes this limit will be exceeded and you will see an error of the form java.lang.OutOfMemory
. To resolve this problem, you can increase this memory limit. On Unix, Linux or Mac OS X platforms, this can done by using the -javamaxmem
switch, passed either to the command-line script prism
or the GUI launcher xprism
. For example:
each set the limit to 4GB. Alternatively, you set the environment variable PRISM_JAVAMAXMEM before running PRISM. For example, under a bash
shell:
If you are running PRISM on Windows you will have to do this manually by modifying the prism.bat
or xprism.bat
scripts. To set the memory to 4GB, for example, add -Xmx4g
to the list of arguments in the call to java
or javaw
at the end of the file.
If you get an error of the form java.lang.StackOverflowError
, then you can try increasing the stack size.
On Unix, Linux or Mac OS X platforms, you can change the value of PRISM_JAVASTACKSIZE
in the prism
script
(but note that, if you are compiling PRISM from source, this file gets regenerated from a template in src/bin
when you recompile).
On Windows, you can edit the call to java
or javaw
directly, adding e.g. -Xss32M
.
By default, PRISM's probabilistic model checking algorithms use an initial precomputation step which uses graph-based techniques to efficient detect trivial cases where probabilities are 0 or 1. This can often result in improved performance and also reduce round-off errors. Occasionally, though, you may want to disable this step for efficiency (e.g. if you know that there are no/few such states and the precomputation process is slow). This can be done with the -nopre
switch. You can also disable the individual algorithms for probability 0/1 using switches -noprob0
and -noprob1
.