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.
213 lines
9.9 KiB
213 lines
9.9 KiB
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
|
|
"http://www.w3.org/TR/html4/loose.dtd">
|
|
|
|
<html>
|
|
<head>
|
|
|
|
<title>
|
|
PRISM Manual | RunningPRISM / ModelChecking
|
|
</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'>Running PRISM</a> /
|
|
</p><h1>Model Checking</h1>
|
|
|
|
</div>
|
|
<!--PageText-->
|
|
<div id='wikitext'>
|
|
<p>Typically, once a model has been constructed, it is analysed through model checking.
|
|
Properties are specified as described in the "<a class='wikilink' href='../PropertySpecification/Main.html'>Property Specification</a>" section,
|
|
and are usually kept in files with extensions <code>.props</code>, <code>.pctl</code> or <code>.csl</code>.
|
|
There are properties files accompanying most of the sample PRISM models in the <code>examples</code> directory.
|
|
</p>
|
|
<p class='vspace'><a name='gui' id='gui'></a>
|
|
</p><h3>GUI</h3>
|
|
<p>To load a file containing properties into the GUI, select menu option "Properties | Open properties list".
|
|
The file can only be loaded if there are no errors, otherwise an error is displayed.
|
|
Note that it may be necessary to have loaded the corresponding model first,
|
|
since the properties will probably make reference to variables (and perhaps constants) declared in the model file.
|
|
Once loaded, the properties contained in the file are displayed in a list in the "Properties" tab of the GUI.
|
|
Constants and labels are displayed in separate lists below.
|
|
You can modify or create new properties, constants and labels from the GUI,
|
|
by right-clicking on the appropriate list and selecting from the pop-up menu which appears. Properties with errors are shaded red and marked with a warning sign.
|
|
Positioning the mouse pointer over the property displays the corresponding error message.
|
|
</p>
|
|
<p class='vspace'>The pop-up menu for the properties list also contains a "Verify" option,
|
|
which allows you instruct PRISM to model check the currently selected properties
|
|
(hold down Ctrl/Cmd to select more than one property simultaneously).
|
|
All properties can be model checked at once by selecting "Verify all".
|
|
PRISM verifies each property individually.
|
|
Upon completion, the icon next to the property changes according to the result of model checking. For Boolean-valued properties, a result of true or false is indicated by a green tick or red cross, respectively. For properties which have a numerical result (e.g. <code>P=? [ ...]</code>), position the mouse pointer over the property to view the result.
|
|
In addition, this and further information about model checking is displayed in the log in the "Log" tab.
|
|
</p>
|
|
<p class='vspace'><a name='cl' id='cl'></a>
|
|
</p><h3>Command-line</h3>
|
|
<p>From the command-line, model checking is achieved by passing both a model file and a properties file as arguments, e.g.:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock1'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm poll.csl</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/RunningPRISM/ModelChecking?action=sourceblock&num=1' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>The results of model checking are sent to the display and are as described above for the GUI version.
|
|
By default, all properties in the file are checked.
|
|
To model check only a single property, use the <code>-prop</code> switch.
|
|
For example, to check only the fourth property in the file:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock2'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm poll.csl -prop 4</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/RunningPRISM/ModelChecking?action=sourceblock&num=2' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>or to check only the property with <a class='wikilink' href='../PropertySpecification/PropertiesFiles.html#names'>name</a> "safe" in the file:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock3'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm poll.csl -prop safe</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/RunningPRISM/ModelChecking?action=sourceblock&num=3' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>Alternatively, the contents of a properties file can be specified directly from the command-line, using the <code>-pf</code> switch:
|
|
</p>
|
|
<div class='vspace'></div>
|
|
<div class='sourceblock ' id='sourceblock4'>
|
|
<div class='sourceblocktext'><div class="shell"><span style="font-weight:bold;">prism poll2.sm -pf 'P>=0.5 [ true U<=5 (s=1 & a=0) ]'</span><br/>
|
|
</div></div>
|
|
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/RunningPRISM/ModelChecking?action=sourceblock&num=4' type='text/plain'>[$[Get Code]]</a></div>
|
|
</div>
|
|
|
|
<p class='vspace'>The switches <code>-pctl</code> and <code>-csl</code> are aliases for <code>-pf</code>.
|
|
</p>
|
|
<p class='vspace'>Note the use of single quotes (<code>'...'</code>) to avoid characters such as
|
|
<code>(</code> and <code>></code> being interpreted by the command-line shell.
|
|
Single quotes are preferable to double quotes since PRISM properties often include double quotes, e.g. for references to labels or properties.
|
|
</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'>Running PRISM</a></strong>
|
|
</p><ul><li><a class='wikilink' href='Main.html'>Starting PRISM</a>
|
|
</li><li><a class='wikilink' href='LoadingAndBuildingAModel.html'>Loading And Building a Model</a>
|
|
</li><li><a class='wikilink' href='DebuggingModelsWithTheSimulator.html'>Debugging Models With The Simulator</a>
|
|
</li><li><a class='wikilink' href='ExportingTheModel.html'>Exporting The Model</a>
|
|
</li><li><a class='selflink' href='ModelChecking.html'>Model Checking</a>
|
|
</li><li><a class='wikilink' href='ApproximateModelChecking.html'>Statistical Model Checking</a>
|
|
</li><li><a class='wikilink' href='ComputingSteady-stateAndTransientProbabilities.html'>Computing Steady-state And Transient Probabilities</a>
|
|
</li><li><a class='wikilink' href='Experiments.html'>Experiments</a>
|
|
</li><li><a class='wikilink' href='Adversaries.html'>Adversaries</a>
|
|
</li><li><a class='wikilink' href='SupportForPEPAModels.html'>Support For PEPA Models</a>
|
|
</li><li><a class='wikilink' href='SupportForSBML.html'>Support For SBML</a>
|
|
</li><li><a class='wikilink' href='ExplicitModelImport.html'>Explicit Model Import</a>
|
|
</li><li><a class='wikilink' href='ParametricModelChecking.html'>Parametric Model Checking</a>
|
|
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
|
|
</p>
|
|
|
|
|
|
</div> <!-- id="prism-navbar2" -->
|
|
</div> <!-- id="layout-leftcol" -->
|
|
|
|
</body>
|
|
</html>
|