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.
252 lines
14 KiB
252 lines
14 KiB
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
|
|
"http://www.w3.org/TR/html4/loose.dtd">
|
|
|
|
<html>
|
|
<head>
|
|
|
|
<title>
|
|
PRISM Manual | FrequentlyAskedQuestions / PRISMProperties
|
|
</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;
|
|
}
|
|
|
|
--></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-->
|
|
<div id="prism-man-title">
|
|
<p><a class='wikilink' href='Main.html'>Frequently Asked Questions</a> /
|
|
</p><h1>PRISM Properties</h1>
|
|
|
|
</div>
|
|
<!--PageText-->
|
|
<div id='wikitext'>
|
|
<p><a name='inf_rewards' id='inf_rewards'></a>
|
|
</p><h3>Why is my expected reward infinite?</h3>
|
|
<div class='answer' >
|
|
<p>This mostly commonly occurs when you are computing the expected reward that is accumulated up until some target set of states is reached ("reachability reward" properties). For example:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock1'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">end</span>" ]<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=1' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>As mentioned <a class='wikilink' href='../PropertySpecification/Reward-basedProperties.html'>earlier</a>, this kind of property returns infinity if <code>"end"</code> is not eventually reached with probability 1. This is a choice that we made when designing the property specification language. Often, it is reasonable to assume that, if a path continues indefinitely without reaching a goal state, then reward will continue to be accumulated infinitely often (this would usually be true when modelling time as a reward structure, for instance). If there is a non-zero probability of <em>not</em> reaching the target (i.e. the probability of reaching it is less than 1), we would then expect the overall expected reward to be infinite.
|
|
</p>
|
|
<p class='vspace'>You can check whether the probability of reaching the target <em>is</em> 1 with a property like:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock2'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">end</span>" ]<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=2' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>A similar situation arises with models that contain nondeterminism, such as MDPs. The <em>maximum</em> expected reward to reach a target is finite if and only if the <em>minimum</em> probability of reaching the target is 1. Conversely, the <em>minimum</em> expected reward is finite if and only if the <em>maximum</em> probability is 1.
|
|
</p>
|
|
<div class='vspace'></div></div>
|
|
<p class='vspace'><a name='mult_states' id='mult_states'></a>
|
|
</p><h3>How do I check if a property is true in multiple (or all) states?</h3>
|
|
<div class='answer' >
|
|
<p>Consider a typical boolean-valued PRISM property, such as:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock3'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span><<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=3' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>i.e. "the probability of reaching a state labelled with <code>"error"</code> is less than 0.01. By default, when model checking this query, PRISM will report the result of this property <em>for the initial state</em> of the model, i.e. whether, <em>starting from the initial state</em>, the probability of reaching <code>"error"</code> is below 0.01.
|
|
(This is in contrast to older versions of PRISM, which used to report whether the property was true <em>for all</em> states.)
|
|
</p>
|
|
<p class='vspace'>To check whether the above property is true for, say, all (reachable) states satisfying the label <code>"safe"</code>, you should use <a class='wikilink' href='../PropertySpecification/Filters.html'>filters</a>, as
|
|
illustrated below:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock4'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span><<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismident">safe</span>")<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=4' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>If you want to check whether the property is true for <em>all</em> reachable states, you can use either of the following two (equivalent) properties:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock5'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span><<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], <span class="prismkeyword">true</span>)<br/>
|
|
<span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span><<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ])<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=5' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>In older versions of PRISM, checking that a property was true in a particular set of states was done using implication (<code>=></code>). If you wish, you can still use a similar form of property to achieve this, as shown by the following example:
|
|
</p>
|
|
<div class='sourceblock ' id='sourceblock6'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, "<span class="prismident">safe</span>" => <span class="prismkeyword">P</span><<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ])<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=6' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
</div>
|
|
<p class='vspace'><a name='action' id='action'></a>
|
|
</p><h3>How do I compute the probability of an action occurring?</h3>
|
|
<div class='answer' >
|
|
<p>PRISM's property specification language is primarily state-based, e.g. you can compute the probability of reaching a <em>state</em> that satisfies the label <code>"error"</code>:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock7'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=7' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>So how do you compute the probability of a some action <code>b</code> occurring? You need to make a small change to your model. The cleanest way to do this is to add a small module that changes state when the action occurs, e.g.:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock8'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">module</span> <span class="prismident">checker</span><br/>
|
|
<br/>
|
|
<span class="prismident">q</span> : [<span class="prismnum">0</span>..<span class="prismnum">1</span>] <span class="prismkeyword">init</span> <span class="prismnum">0</span>;<br/>
|
|
<br/>
|
|
[<span class="prismident">b</span>] <span class="prismident">q</span>=<span class="prismnum">0</span> -> (<span class="prismident">q</span>'=<span class="prismnum">1</span>);<br/>
|
|
[<span class="prismident">b</span>] <span class="prismident">q</span>=<span class="prismnum">1</span> -> (<span class="prismident">q</span>'=<span class="prismnum">1</span>);<br/>
|
|
<br/>
|
|
<span class="prismkeyword">endmodule</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=8' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>You can determine the probability of action <code>b</code> occurring in the model with the property:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock9'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">q</span>=<span class="prismnum">1</span> ]<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=9' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>By design, the module above will not affect the behaviour (timing, probability, etc.) of your model at all, so all other properties will remain unchanged. This is true for any of the model types that PRISM supports. It may, though, lead to a (hopefully small) increase in total model size.
|
|
</p>
|
|
<p class='vspace'>You can also modify the property above to compute, for example, the probability of <code>b</code> occurring within <code>T</code> time-units or the expected time until <code>b</code> occurs:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock10'>
|
|
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span><=<span class="prismident">T</span> <span class="prismident">q</span>=<span class="prismnum">1</span> ]<br/>
|
|
<span class="prismkeyword">R</span>{"<span class="prismident">time</span>"}=? [ <span class="prismkeyword">F</span> <span class="prismident">q</span>=<span class="prismnum">1</span> ]<br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/FrequentlyAskedQuestions/PRISMProperties?action=sourceblock&num=10' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>(where a constant <code>T</code> or reward structure <code>time</code> have been added to the model, as appropriate).
|
|
</p></div>
|
|
</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'>Frequently Asked Questions</a></strong>
|
|
</p><ul><li><a class='wikilink' href='MemoryProblems.html'>Memory Problems</a>
|
|
</li><li><a class='wikilink' href='PRISMModelling.html'>PRISM Modelling</a>
|
|
</li><li><a class='selflink' href='PRISMProperties.html'>PRISM Properties</a>
|
|
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
|
|
</p>
|
|
|
|
|
|
</div> <!-- id="prism-navbar2" -->
|
|
</div> <!-- id="layout-leftcol" -->
|
|
|
|
</body>
|
|
</html>
|