You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
548 lines
45 KiB
548 lines
45 KiB
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
|
|
"http://www.w3.org/TR/html4/loose.dtd">
|
|
|
|
<html>
|
|
<head>
|
|
|
|
<title>
|
|
PRISM Manual | ConfiguringPRISM / AllOnOnePage
|
|
</title>
|
|
|
|
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
|
|
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">
|
|
|
|
<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
|
|
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
|
|
|
|
<!--HTMLHeader--><style type='text/css'><!--
|
|
ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
|
|
code.escaped { white-space: nowrap; }
|
|
.vspace { margin-top:1.33em; }
|
|
.indent { margin-left:40px; }
|
|
.outdent { margin-left:40px; text-indent:-40px; }
|
|
a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
|
|
a.createlink { text-decoration:none; position:relative; top:-0.5em;
|
|
font-weight:bold; font-size:smaller; border-bottom:none; }
|
|
img { border:0px; }
|
|
.editconflict { color:green;
|
|
font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }
|
|
|
|
table.markup { border:2px dotted #ccf; width:90%; }
|
|
td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
|
|
table.vert td.markup1 { border-bottom:1px solid #ccf; }
|
|
table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
|
|
table.markup caption { text-align:left; }
|
|
div.faq p, div.faq pre { margin-left:2em; }
|
|
div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
|
|
div.faqtoc div.faq * { display:none; }
|
|
div.faqtoc div.faq p.question
|
|
{ display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
|
|
div.faqtoc div.faq p.question * { display:inline; }
|
|
|
|
.frame
|
|
{ border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
|
|
.lfloat { float:left; margin-right:0.5em; }
|
|
.rfloat { float:right; margin-left:0.5em; }
|
|
a.varlink { text-decoration:none; }
|
|
|
|
.sourceblocklink {
|
|
text-align: right;
|
|
font-size: smaller;
|
|
}
|
|
.sourceblocktext {
|
|
padding: 0.5em;
|
|
border: 1px solid #808080;
|
|
color: #000000;
|
|
background-color: #f1f0ed;
|
|
}
|
|
.sourceblocktext div {
|
|
font-family: monospace;
|
|
font-size: small;
|
|
line-height: 1;
|
|
height: 1%;
|
|
}
|
|
.sourceblocktext div.head,
|
|
.sourceblocktext div.foot {
|
|
font: italic medium serif;
|
|
padding: 0.5em;
|
|
}
|
|
/**
|
|
* GeSHi Dynamically Generated Stylesheet
|
|
* --------------------------------------
|
|
* Dynamically generated stylesheet for bash
|
|
* CSS class: , CSS id:
|
|
* GeSHi (C) 2004 - 2007 Nigel McNie, 2007 - 2014 Benny Baumann
|
|
* (http://qbnz.com/highlighter/ and http://geshi.org/)
|
|
* --------------------------------------
|
|
*/
|
|
.bash .de1, .bash .de2 {font-family: monospace; font-weight: normal;}
|
|
.bash {font-family:monospace;}
|
|
.bash .imp {font-weight: bold; color: red;}
|
|
.bash li, .bash .li1 {font-family: monospace; color: black; font-weight: normal;}
|
|
.bash .ln {width:1px;text-align:right;margin:0;padding:0 2px;vertical-align:top;}
|
|
.bash .li2 {font-weight: bold;}
|
|
.bash .kw1 {color: #000000; font-weight: bold;}
|
|
.bash .kw2 {color: #c20cb9; font-weight: bold;}
|
|
.bash .kw3 {color: #7a0874; font-weight: bold;}
|
|
.bash .co0 {color: #666666; font-style: italic;}
|
|
.bash .co1 {color: #800000;}
|
|
.bash .co2 {color: #cc0000; font-style: italic;}
|
|
.bash .co3 {color: #000000; font-weight: bold;}
|
|
.bash .co4 {color: #666666;}
|
|
.bash .es1 {color: #000099; font-weight: bold;}
|
|
.bash .es2 {color: #007800;}
|
|
.bash .es3 {color: #007800;}
|
|
.bash .es4 {color: #007800;}
|
|
.bash .es5 {color: #780078;}
|
|
.bash .es_h {color: #000099; font-weight: bold;}
|
|
.bash .br0 {color: #7a0874; font-weight: bold;}
|
|
.bash .sy0 {color: #000000; font-weight: bold;}
|
|
.bash .st0 {color: #ff0000;}
|
|
.bash .st_h {color: #ff0000;}
|
|
.bash .nu0 {color: #000000;}
|
|
.bash .re0 {color: #007800;}
|
|
.bash .re1 {color: #007800;}
|
|
.bash .re2 {color: #007800;}
|
|
.bash .re4 {color: #007800;}
|
|
.bash .re5 {color: #660033;}
|
|
.bash .ln-xtra, .bash li.ln-xtra, .bash div.ln-xtra {background-color: #ffc;}
|
|
.bash span.xtra { display:block; }
|
|
|
|
--></style> <meta name='robots' content='index,follow' />
|
|
|
|
|
|
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
|
|
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
|
|
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">
|
|
|
|
</head>
|
|
|
|
<body text="#000000" bgcolor="#ffffff">
|
|
|
|
<div id="layout-maincontainer">
|
|
<div id="layout-main">
|
|
|
|
<div id="prism-mainbox">
|
|
|
|
<!-- ============================================================================= -->
|
|
|
|
<!--PageHeaderFmt-->
|
|
<!--/PageHeaderFmt-->
|
|
|
|
<!--PageTitleFmt--><!--PageText-->
|
|
<div id='wikitext'>
|
|
<div class='vspace'></div><h1><span class='big'>Configuring PRISM</span></h1>
|
|
<hr />
|
|
<h1>Introduction</h1>
|
|
<p>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).
|
|
</p>
|
|
<p class='vspace'>User options and settings for the GUI are saved in a file locally and reused. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the settings file is in a simple textual format and can also 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 settings file re-launch the GUI. The location of the settings file depends on the operating system. As of PRISM 4.5, it is stored in:
|
|
</p>
|
|
<div class='vspace'></div><ul><li><code>$XDG_CONFIG_HOME/prism.settings</code> (on Linux, if that environment variable is set)
|
|
</li><li><code>$HOME/.config/prism.settings</code> (on Linux, if <code>$XDG_CONFIG_HOME</code> is not set)
|
|
</li><li><code>$HOME/Library/Preferences/prism.settings</code> (on Mac OS)
|
|
</li><li><code>.prism</code> in the user's home directory, e.g. <code>C:\Documents and Settings\username</code> (on Windows)
|
|
</li><li><code>$HOME/.prism</code> (if the settings file was already created by an older version of PRISM)
|
|
</li></ul><p class='vspace'>From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock1'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism -help</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=1' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>For some switches, whose format is not straightforward, there is additional help available on the command-line, using <code>-help switch</code>. For example:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock2'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism -help const</span><br/>
|
|
<span style="font-weight:bold;">prism -help simpath</span><br/>
|
|
<span style="font-weight:bold;">prism -help exportresults</span><br/>
|
|
<span style="font-weight:bold;">prism -help exportmodel</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=2' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>The settings file is <em>ignored</em> by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file <em>is</em> read, using the <code>-settings</code> switch, e.g.:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock3'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism -settings ~/.prism</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=3' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>In the following sections, we give a brief description of the most important configuration options available.
|
|
</p>
|
|
<div class='vspace'></div><hr />
|
|
<h1>Computation Engines</h1>
|
|
<h3>Computation engines</h3>
|
|
<p>PRISM contains four main <em>engines</em>,
|
|
which implement the majority of its model checking functionality:
|
|
</p>
|
|
<div class='vspace'></div><ul><li>"MTBDD"
|
|
</li><li>"sparse"
|
|
</li><li>"hybrid"
|
|
</li><li>"explicit"
|
|
</li></ul><p class='vspace'>The first three of these engines are either wholly or partly <em>symbolic</em>,
|
|
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 [<a class='wikilink' href='../Main/References.html#KNP04b'>KNP04b</a>].
|
|
For detailed information about all three engines, see [<a class='wikilink' href='../Main/References.html#Par02'>Par02</a>].
|
|
</p>
|
|
<p class='vspace'>The fourth engine, "explicit", performs all aspects of model construction
|
|
and model checking using <em>explicit-state</em> 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).
|
|
</p>
|
|
<p class='vspace'>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.
|
|
</p>
|
|
<div class='vspace'></div><ul><li>The <strong>hybrid</strong> engine is enabled by default in PRISM. It uses a combination of <em>symbolic</em> and <em>explicit-state</em> data structures (as used in the MTBDD and sparse engines, respectively). In general it provides the best compromise between time and memory usage: it (almost) always uses less memory than the sparse engine, but is typically slightly slower. The size of model which can be handled with this engine is quite predictable. The limiting factor in terms of memory usage comes from the storage of 2-4 (depending on the computation being performed) arrays of 8-byte values, one for each state in the model. So, a typical PC can handle models with between 10<sup>7</sup> and 10<sup>8</sup> states (one vector for 10<sup>7</sup> states uses approximately 75 MB).
|
|
<div class='vspace'></div></li><li>The <strong>sparse</strong> engine can be a good option for smaller models where model checking takes a long time. For larger models, however, memory usage quickly becomes prohibitive. As a rule of thumb, the upper limit for this engine, in terms of model sizes which can be handled, is about a factor of 10 less than the hybrid engine.
|
|
<div class='vspace'></div></li><li>The <strong>MTBDD</strong> engine is much more unpredictable in terms of performance but, when a model exhibits a lot of structure and regularity, can be very effective. This engine has been successfully applied to extremely large structured (but non-trivial) models, in cases where the other two engines cannot be applied. The MTBDD engine often performs poorly when the model (or solutions computed from it) contain lots of distinct probabilities/rates; it performs best when there are few such values. For this reason the engine is often successfully applied to MDP models, but much less frequently to CTMCs. When using the MTBDD engine, the <em>variable ordering</em> of your model is especially important. This topic is covered in the <a class='wikilink' href='../FrequentlyAskedQuestions/PRISMModelling.html#ordering'>FAQ</a> section.
|
|
<div class='vspace'></div></li><li>The <strong>explicit</strong> engine is similar to the sparse engine, in that it can be a good option for relatively small models, but will not scale up to some of the models that can be handled by the hybrid or MTBDD engines. However, unlike the sparse engine, the explicit engine does not use symbolic data structures for model construction, which can be beneficial in some cases. One example is models with a potentially very large state space, only a fraction of which is actually reachable.
|
|
</li></ul><p class='vspace'>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 <code>-mtbdd</code>, <code>-sparse</code>, <code>-hybrid</code> and <code>-explicit</code> (or <code>-m</code>, <code>-s</code>, <code>-h</code> and <code>-ex</code>, respectively) switches, e.g.:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock4'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm -tr 1000 -m</span><br/>
|
|
<span style="font-weight:bold;">prism poll2.sm -tr 1000 -s</span><br/>
|
|
<span style="font-weight:bold;">prism poll2.sm -tr 1000 -h</span><br/>
|
|
<span style="font-weight:bold;">prism poll2.sm -tr 1000 -ex</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=4' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>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.
|
|
</p>
|
|
<p class='vspace'>PRISM also has some basic support for automatically selecting the engine (and other settings) heuristically,
|
|
based on the size and type of the model, and the property being checked.
|
|
Use, for example, <code>-heuristic speed</code> from the command-line to choose options
|
|
which target computation speed rather than saving memory.
|
|
This is also available from the "Heuristic" option under the "PRISM" tab of the "Options" dialog in the GUI.
|
|
</p>
|
|
<div class='vspace'></div><h3>Approximate/statistical model checking</h3>
|
|
<p>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 <code>-sim</code> switch.
|
|
See the "<a class='wikilink' href='../RunningPRISM/ApproximateModelChecking.html'>Statistical Model Checking</a>"
|
|
section for more details.
|
|
</p>
|
|
<p class='vspace'><a name='exact' id='exact'></a>
|
|
</p><h3>Exact model checking</h3>
|
|
<p>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 <a class='wikilink' href='../RunningPRISM/ParametricModelChecking.html'>parametric model checking</a>, 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 <code>-exact</code> from the command line.
|
|
</p>
|
|
<p class='vspace'><a name='pta' id='pta'></a>
|
|
</p><h3>PTA engines</h3>
|
|
<p>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:
|
|
</p>
|
|
<div class='vspace'></div><ul><li>The <strong>stochastic games</strong> engine uses abstraction-refinement techniques based on stochastic two-player games [<a class='wikilink' href='../Main/References.html#KNP09c'>KNP09c</a>].
|
|
<div class='vspace'></div></li><li>The <strong>digital clocks</strong> engine performs a discretisation, in the form of a language-level model translation, that reduces the problem to one of model checking over a finite-state MDP [<a class='wikilink' href='../Main/References.html#KNPS06'>KNPS06</a>].
|
|
<div class='vspace'></div></li><li>The <strong>backwards reachability</strong> engine is a zone-based method based on a backwards traversal of the state space and solution of the resulting finite-state MDP [<a class='wikilink' href='../Main/References.html#KNSW07'>KNSW07</a>].
|
|
</li></ul><p class='vspace'>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 <code>-ptamethod <name></code> should be used where <code><name></code> is either <code>games</code>, <code>digital</code> or <code>backwards</code>.
|
|
</p>
|
|
<p class='vspace'>The choice of engine for PTA model checking affects restrictions that imposed on both
|
|
the <a class='wikilink' href='../ThePRISMLanguage/Real-timeModels.html'>modelling language</a>
|
|
and the types of <a class='wikilink' href='../PropertySpecification/Real-timeModels.html'>properties</a> that can be checked.
|
|
</p><hr />
|
|
<h1>Solution Methods and Options</h1>
|
|
<p>Separately from the choice of <a class='wikilink' href='ComputationEngines.html'>engines</a>,
|
|
PRISM often offers several different solution methods
|
|
that can be used for the computation of probabilities and expected costs/rewards during model checking.
|
|
Many, but not all, of these are iterative numerical methods.
|
|
The choice of method (and their settings) depends on the type of analysis that is being done (i.e., what type of model and property).
|
|
</p>
|
|
<div class='vspace'></div><h3>Linear Equation Systems</h3>
|
|
<p>For many properties of Markov chains
|
|
(e.g. "reachability"/"until" properties for DTMCs and CTMCs, steady-state properties for CTMCs and "reachability reward" properties for DTMCs),
|
|
PRISM solves a set of linear equation systems, for which several numerical methods are available.
|
|
Below is a list of the alternatives and the switches used to select them from the command-line.
|
|
The corresponding GUI option is "Linear equations method".
|
|
</p>
|
|
<div class='vspace'></div><ul><li>Power method: <code>-power</code> (or <code>-pow</code>, <code>-pwr</code>)
|
|
</li><li>Jacobi method: <code>-jacobi</code> (or <code>-jac</code>)
|
|
</li><li>Gauss-Seidel method: <code>-gaussseidel</code> (or <code>-gs</code>)
|
|
</li><li>Backwards Gauss-Seidel method: <code>-bgaussseidel</code> (or <code>-bgs</code>)
|
|
</li><li>JOR method (Jacobi with over-relaxation): <code>-jor</code>
|
|
</li><li>SOR method: <code>-sor</code>
|
|
</li><li>Backwards SOR method: <code>-bsor</code>
|
|
</li></ul><p class='vspace'>When using the MTBDD engine, Gauss-Seidel/SOR based methods are not available.
|
|
When using the hybrid engine, <em>pseudo</em> variants of Gauss-Seidel/SOR based method can also be used [<a class='wikilink' href='../Main/References.html#Par02'>Par02</a>]
|
|
(type <code>prism -help</code> 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 <code>-omega <val></code>).
|
|
</p>
|
|
<p class='vspace'>For options relating to convergence (of this and other iterative methods),
|
|
see the <a class='wikilink' href='SolutionMethodsAndOptions.html#convergence'>Convergence</a> section below.
|
|
</p>
|
|
<p class='vspace'><a name='mdp' id='mdp'></a>
|
|
</p><h3>MDP Solution Methods</h3>
|
|
<p>When analysing MDPs, there are multiple solution methods on offer.
|
|
For most of these, you can select them 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 <a class='wikilink' href='ComputationEngines.html'>explicit engine</a>.
|
|
For more details of the methods, see e.g. [<a class='wikilink' href='../Main/References.html#FKNP11'>FKNP11</a>] (about probabilistic verification of MDPs)
|
|
or classic MDP texts such as [<a class='wikilink' href='../Main/References.html#Put94'>Put94</a>]).
|
|
</p>
|
|
<div class='vspace'></div><ul><li><strong>Value iteration</strong> (switch <code>-valiter</code>) [this is the default]
|
|
</li><li><strong>Gauss Seidel</strong> (switch <code>-gs</code>)
|
|
</li><li><strong>Policy iteration</strong> (switch <code>-politer</code>)
|
|
</li><li><strong>Modified policy iteration</strong> (switch <code>-modpoliter</code>)
|
|
</li></ul><p class='vspace'>Where the methods above use iterative numerical solution,
|
|
you can also use the settings under described in the <a class='wikilink' href='SolutionMethodsAndOptions.html#convergence'>Convergence</a> section below.
|
|
</p>
|
|
<p class='vspace'><a name='iiter' id='iiter'></a>
|
|
</p><h3>Interval Iteration</h3>
|
|
<p>Interval iteration [<a class='wikilink' href='../Main/References.html#HM14'>HM14</a>],[<a class='wikilink' href='../Main/References.html#BKLPW17'>BKLPW17</a>] is an alternative solution method for either MDPs or DTMCs
|
|
which performs two separate instances of numerical iterative solution,
|
|
one from below and one from above. This is designed to provide clearer information
|
|
about the accuracy of the computed values and avoid possible problems with premature convergence.
|
|
This can be enabled using the switch <code>-intervaliter</code> (or <code>-ii</code>)
|
|
or via the "Use interval iteration" GUI option.
|
|
A variety of options can be configured, either using
|
|
<code>-intervaliter:option1,option2,...</code> or by
|
|
setting the string "<code>option1,option2,...</code>" under "Interval iteration options" in the GUI.
|
|
Type <code>prism -help intervaliter</code> from the command-line for a list of the options
|
|
and see [<a class='wikilink' href='../Main/References.html#BKLPW17'>BKLPW17</a>] for the details.
|
|
</p>
|
|
<p class='vspace'><a name='topo' id='topo'></a>
|
|
</p><h3>Topological Value Iteration</h3>
|
|
<p>Topological value iteration is a variant of value iteration which improves efficiency
|
|
by analysing the graph structure of the model and using this to update the values for
|
|
states in an alternative order which increases the speed of convergence.
|
|
Use switch <code>-topological</code> or GUI option "Use topological value iteration" to enable this.
|
|
In addition to standard value iteration for MDPs, the topological variant can be used to optimise
|
|
both interval iteration (see above) and the numerical solution of DTMCs.
|
|
</p>
|
|
<p class='vspace'><a name='transient' id='transient'></a>
|
|
</p><h3>CTMC Transient Analysis</h3>
|
|
<p>When computing transient probabilities of a CTMC
|
|
(either <a class='wikilink' href='../RunningPRISM/ComputingSteady-stateAndTransientProbabilities.html'>directly</a> or when verifying <a class='wikilink' href='../PropertySpecification/ThePOperator.html#bounded'>time-bounded operators</a> of CSL), there are two options:
|
|
<em>uniformisation</em> and <em>fast adaptive uniformisation</em> (FAU). These can be selected using the GUI option "Transient probability computation method", or using the command-line switch <code>-transientmethod <name></code>, where <code><name></code> is either <code>unif</code> or <code>fau</code>.
|
|
</p>
|
|
<p class='vspace'><strong>Uniformisation</strong> 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 <code>-nossdetect</code>).
|
|
</p>
|
|
<p class='vspace'><a name='fau' id='fau'></a>
|
|
<strong>Fast adaptive uniformisation</strong> (FAU) [<a class='wikilink' href='../Main/References.html#MWDH10'>MWDH10</a>] 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 [<a class='wikilink' href='../Main/References.html#DHK13'>DHK13</a>], 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.
|
|
</p>
|
|
<p class='vspace'>The following options can be used to configure FAU:
|
|
</p>
|
|
<div class='vspace'></div><ul><li>"FAU epsilon" (switch <code>-fauepsilon <x></code>): 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.
|
|
<div class='vspace'></div></li><li>"FAU cut off delta" (switch <code>-faudelta <x></code>): States that have a lower probability than this value are discarded. The default is 1e-12.
|
|
<div class='vspace'></div></li><li>"FAU array threshold" (switch <code>-fauarraythreshold <x></code>): 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.
|
|
<div class='vspace'></div></li><li>"FAU time intervals" (switch <code>-fauintervals <x></code>): 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.
|
|
<div class='vspace'></div></li><li>"FAU initial time interval" (switch <code>-fauinitival <x></code>): 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.
|
|
</li></ul><p class='vspace'><a name='convergence' id='convergence'></a>
|
|
</p><h3>Convergence</h3>
|
|
<p>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 (or, in the case of interval iteration, if the difference of the elements in the iterations from above and below are below the threshold).
|
|
The default value for this threshold is 10<sup>-6</sup> but it can be altered with the "Termination epsilon" option (switch <code>-epsilon <val></code>). 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 <code>-relative</code> and <code>-absolute</code>, or <code>-rel</code> and <code>-abs</code> for short).
|
|
</p>
|
|
<p class='vspace'>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 <code>-maxiters <val></code>). Computations that reach this upper limit will trigger an error during model checking to alert the user to this fact.
|
|
</p><hr />
|
|
<h1>Automata Generation</h1>
|
|
<p>When PRISM performs verification of <a class='wikilink' href='../PropertySpecification/ThePOperator.html#ltl'>LTL formulas</a>, it does so by converting the formula into a deterministic omega automaton (such as a Rabin automaton) and then analysing a larger product model, constructed from the model being verified and the omega automaton. For this reason, the size of the omega automaton has an important effect on the efficiency of verification.
|
|
</p>
|
|
<p class='vspace'>By default PRISM uses a port of the <a class='urllink' href='http://www.ltl2dstar.de/'>ltl2dstar</a> library to construct these automata. But it also allows the use of external LTL-to-automata converters producing deterministic automata through support for the <a class='urllink' href='http://adl.github.io/hoaf/'>Hanoi Omega Automaton</a> (HOA) format. From the command line, an example of this is:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock5'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism model.pm -pf "P=? [ G F x=1 ]" -ltl2datool hoa-ltl2dstar-for-prism -ltl2dasyntax lbt</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=5' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>The <code>-ltl2datool</code> switch specifies the location of the program to be executed to perform the LTL-to-automaton conversion. This will be called by PRISM as "<code>exec</code> <code>in-file</code> <code>out-file</code>", where <code>exec</code> is the executable, <code>in-file</code> is the name of a file containing the LTL formula to be converted and <code>out-file</code> is the name of a file where the resulting automaton should be written, in HOA format. Typically, the executable will be a script. Here is a simple example (called as <code>hoa-ltl2dstar-for-prism</code> in the above example), which calls an external copy of <code>ltl2dstar</code> in the required fashion (assuming that the <code>ltl2dstar</code> and <a class='urllink' href='http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/'><code>ltl2ba</code></a> executables are located in the current directory or on the PATH).
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock6'>
|
|
<div class='sourceblocktext'><div class="bash"><span class="co0">#! /bin/bash</span><br />
|
|
ltl2dstar <span class="re5">--output</span>=automaton <span class="re5">--output-format</span>=hoa <span class="st0">"$1"</span> <span class="st0">"$2"</span></div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=6' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>PRISM is known to work with these HOA-enabled tools:
|
|
</p>
|
|
<div class='vspace'></div><ul><li><a class='urllink' href='http://ltl2dstar.de/'>ltl2dstar</a>
|
|
</li><li><a class='urllink' href='http://sourceforge.net/projects/ltl3dra/'>ltl3dra</a>
|
|
</li><li><a class='urllink' href='https://www7.in.tum.de/~kretinsk/rabinizer3.html'>Rabinizer 3</a>
|
|
</li></ul><p class='vspace'>and contains ready-made scripts for calling them in the <code>etc/scripts/hoa</code> directory of the distribution:
|
|
</p>
|
|
<div class='vspace'></div><ul><li><code>hoa-ltl2dstar-with-ltl2ba-for-prism</code> <br /> (<a class='urllink' href='http://ltl2dstar.de/'>ltl2dstar</a> using <a class='urllink' href='http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/'><code>ltl2ba</code></a> as the LTL-to-NBA tool)
|
|
</li><li><code>hoa-ltl2dstar-with-ltl2tgba-for-prism</code> <br /> (<a class='urllink' href='http://ltl2dstar.de/'>ltl2dstar</a> using <a class='urllink' href='http://spot.lip6.fr/wiki'>Spot</a>'s <a class='urllink' href='http://spot.lip6.fr/userdoc/ltl2tgba.html'><code>ltl2tgba</code></a> as the LTL-to-NBA tool
|
|
</li><li><code>hoa-ltl2dstar-with-ltl3ba-for-prism</code> <br /> (<a class='urllink' href='http://ltl2dstar.de/'>ltl2dstar</a> using <a class='urllink' href='http://sourceforge.net/projects/ltl3ba/'>LTL3BA</a> as the LTL-to-NBA tool
|
|
</li><li><code>hoa-ltl3dra-dra-for-prism</code> <br /> (<a class='urllink' href='http://sourceforge.net/projects/ltl3dra/'>ltl3dra</a>, generating Rabin automata)
|
|
</li><li><code>hoa-ltl3dra-tdgra-for-prism</code> <br /> (<a class='urllink' href='http://sourceforge.net/projects/ltl3dra/'>ltl3dra</a>, generating transition-based generalized Rabin automata)
|
|
</li><li><code>hoa-rabinizer3-dgra-for-prism</code> <br /> (<a class='urllink' href='https://www7.in.tum.de/~kretinsk/rabinizer3.html'>Rabinizer 3</a>, generating generalized Rabin automata)
|
|
</li><li><code>hoa-rabinizer3-dra-for-prism</code> <br /> (<a class='urllink' href='https://www7.in.tum.de/~kretinsk/rabinizer3.html'>Rabinizer 3</a>, generating Rabin automata)
|
|
</li><li><code>hoa-rabinizer3-tdgra-for-prism</code> <br /> (<a class='urllink' href='https://www7.in.tum.de/~kretinsk/rabinizer3.html'>Rabinizer 3</a>, generating transition-based generalized Rabin automata)
|
|
</li><li><code>hoa-rabinizer3-tdra-for-prism</code> <br /> (<a class='urllink' href='https://www7.in.tum.de/~kretinsk/rabinizer3.html'>Rabinizer 3</a>, generating transition-based Rabin automata)
|
|
</li></ul><p class='vspace'>There are also scripts for the upcoming <a class='urllink' href='https://www7.in.tum.de/~kretinsk/rabinizer3.html'>Rabinizer 3.1</a>.
|
|
</p>
|
|
<p class='vspace'>See the files themselves for details of any configuration required and for a reminder of the PRISM command-line arguments required.
|
|
</p>
|
|
<p class='vspace'>The <code>-ltl2dasyntax</code> switch is used to specify the textual format for passing the LTL formula to the external converter (i.e., in the file <code>out-file</code>). The options are:
|
|
</p>
|
|
<div class='vspace'></div><ul><li><code>lbt</code> - LBT format
|
|
</li><li><code>spin</code> - SPIN format
|
|
</li><li><code>spot</code> - Spot format
|
|
</li><li><code>rabinizer</code> - Rabinizer format
|
|
</li></ul><p class='vspace'>From the GUI, configuring the external LTL converter is done with the two options
|
|
"Use external LTL->DA tool" and "LTL syntax for external LTL->DA tool".
|
|
</p>
|
|
<p class='vspace'>Another related option is "All path formulas via automata" (command-line switch <code>-pathviaautomata</code>), which forces construction of an automata
|
|
when computing the probability of a path formula, even if it is not needed. This is primarily intended for debugging/testing, not regular use.
|
|
</p>
|
|
<p class='vspace'>As mentioned above, PRISM's external LTL-to-automaton interfacing works using the
|
|
<a class='urllink' href='http://adl.github.io/hoaf/'>HOA</a> format
|
|
(and, in particular, using the <a class='urllink' href='http://automata.tools/hoa/jhoafparser/'><code>jhoafparser</code></a> HOA parser.
|
|
Currently, PRISM can handle automata in HOA format that are
|
|
deterministic and complete, with state-based acceptance.
|
|
Automata with transition-based acceptance are converted to state-based acceptance by PRISM.
|
|
For DTMC and CTMC model checking, generic acceptance conditions are supported, i.e.,
|
|
anything that can be specified as an <code>Acceptance:</code> header in HOA format.
|
|
For MDP model checking, currently Rabin and generalized Rabin acceptance
|
|
specified via the <code>acc-name:</code> header are supported. See the <a class='urllink' href='http://adl.github.io/hoaf/'>HOA format specification</a> for details.
|
|
</p>
|
|
<div class='vspace'></div><hr />
|
|
<h1>Other Options</h1>
|
|
<h3>Output options</h3>
|
|
<p>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 <code>-verbose</code> or <code>-v</code>). To display additional statistics about MTBDDs after model construction, use the "Extra MTBDD information" option (switch <code>-extraddinfo</code>) and, to view MTBDD sizes during the process of reachability, use option "Extra reachability information" (switch <code>-extrareachinfo</code>).
|
|
</p>
|
|
<div class='vspace'></div><h3>Fairness</h3>
|
|
<p>Sometimes, model checking of properties for MDPs requires fairness constraints to be taken into account.
|
|
See e.g. [<a class='wikilink' href='../Main/References.html#BK98'>BK98</a>],[<a class='wikilink' href='../Main/References.html#Bai98'>Bai98</a>] for more information.
|
|
To enable the use of fairness constraints (for <code><strong>P</strong></code> operator properties), use the <code>-fair</code> switch.
|
|
</p>
|
|
<div class='vspace'></div><h3>Probability/rate checks</h3>
|
|
<p>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 <code>-noprobchecks</code>.
|
|
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 <code>-sumroundoff</code>.
|
|
</p>
|
|
<div class='vspace'></div><h3>CUDD memory</h3>
|
|
<p>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 <code>-cuddmaxmem</code> switch. For example:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock7'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism -cuddmaxmem 2g big_model.pm</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=7' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>Above, <code>g</code> denotes GB. You can also use <code>m</code> 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.
|
|
</p>
|
|
<p class='vspace'><a name='javamaxmem' id='javamaxmem'></a>
|
|
</p><h3>Java memory</h3>
|
|
<p>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 <code>java.lang.OutOfMemory</code>. To resolve this problem, you can increase this memory limit. On Unix, Linux or Mac OS X platforms, this can done by using the <code>-javamaxmem</code> switch, passed either to the command-line script <code>prism</code> or the GUI launcher <code>xprism</code>. For example:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock8'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism -javamaxmem 4g big_model.pm</span><br/>
|
|
<span style="font-weight:bold;">xprism -javamaxmem 4g big_model.pm</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=8' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>each set the limit to 4GB. Alternatively, you set the environment variable PRISM_JAVAMAXMEM before running PRISM. For example, under a <code>bash</code> shell:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock9'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">PRISM_JAVAMAXMEM=4g</span><br/>
|
|
<span style="font-weight:bold;">export PRISM_JAVAMAXMEM</span><br/>
|
|
<span style="font-weight:bold;">prism big_model.pm</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=9' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>If you get an error of the form <code>java.lang.StackOverflowError</code>, then you can try increasing the stack size of the JVM.
|
|
On Unix, Linux or Mac OS X platforms, this can done by using the <code>-javastack</code> switch or the <code>PRISM_JAVASTACKSIZE</code> environment variable.
|
|
Examples are:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock10'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism -javastack 1g big_model.pm</span><br/>
|
|
<span style="font-weight:bold;">xprism -javastack 1g big_model.pm</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=10' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>or:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock11'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">PRISM_JAVASTACKSIZE=1g</span><br/>
|
|
<span style="font-weight:bold;">export PRISM_JAVASTACKSIZE</span><br/>
|
|
<span style="font-weight:bold;">prism big_model.pm</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/ConfiguringPRISM/AllOnOnePage?action=sourceblock&num=11' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>If you are running PRISM on Windows you will have to do make adjustments to Java memory manually, by modifying the <code>prism.bat</code> or <code>xprism.bat</code> scripts.
|
|
To set the memory to 4GB, for example, add <code> -Xmx4g</code> to the list of arguments in the call to <code>java</code> or <code>javaw</code> at the end of the file.
|
|
To change the stack size to 1GB, add <code>-Xss1g</code>.
|
|
</p>
|
|
<div class='vspace'></div><h3>Precomputation</h3>
|
|
<p>By default, PRISM's probabilistic model checking algorithms use an initial <em>precomputation</em> 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 <code>-nopre</code> switch. You can also disable the individual algorithms for probability 0/1 using switches <code>-noprob0</code> and <code>-noprob1</code>.
|
|
</p>
|
|
<div class='vspace'></div><h3>Time-outs</h3>
|
|
<p>The command-line version of PRISM has a time-out option, specified using the switch <code>-timeout <n></code>.
|
|
This causes the program to exit after <code><n></code> seconds if it has not already terminated by that point.
|
|
This is particularly useful for benchmarking scenarios where you wish to ignore runs of PRISM that exceed a certain length of time.
|
|
</p>
|
|
</div>
|
|
|
|
|
|
<!--PageFooterFmt-->
|
|
<div id='prism-man-footer'>
|
|
</div>
|
|
<!--/PageFooterFmt-->
|
|
|
|
|
|
<!-- ============================================================================= -->
|
|
|
|
</div> <!-- id="prism-mainbox" -->
|
|
|
|
</div> <!-- id="layout-main" -->
|
|
</div> <!-- id="layout-maincontainer" -->
|
|
|
|
<div id="layout-leftcol">
|
|
<div id="prism-navbar2">
|
|
|
|
<h3><a class='wikilink' href='../Main/Main.html'>PRISM Manual</a></h3>
|
|
<p><strong><a class='wikilink' href='Main.html'>Configuring PRISM</a></strong>
|
|
</p><ul><li><a class='wikilink' href='Main.html'>Introduction</a>
|
|
</li><li><a class='wikilink' href='ComputationEngines.html'>Computation Engines</a>
|
|
</li><li><a class='wikilink' href='SolutionMethodsAndOptions.html'>Solution Methods And Options</a>
|
|
</li><li><a class='wikilink' href='AutomataGeneration.html'>Automata Generation</a>
|
|
</li><li><a class='wikilink' href='OtherOptions.html'>Other Options</a>
|
|
</li></ul><p>[ <a class='selflink' href='AllOnOnePage.html'>View all</a> ]
|
|
</p>
|
|
|
|
|
|
</div> <!-- id="prism-navbar2" -->
|
|
</div> <!-- id="layout-leftcol" -->
|
|
|
|
</body>
|
|
</html>
|