Blame view
prism-4.3-linux64/doc/manual/ThePRISMLanguage/ModulesAndVariables.html
12.2 KB
8146dcf82
first commit
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>
PRISM Manual | ThePRISMLanguage / ModulesAndVariables
</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'>The PRISM Language</a> /
</p><h1>Modules And Variables</h1>
</div>
<!--PageText-->
<div id='wikitext'>
<p>The <a class='wikilink' href='Example1.html'>previous example</a> uses two modules, <code>M1</code> and <code>M2</code>, one representing each process.
A module is specified as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">module</span> <span class="prismident">name</span> ... <span class="prismkeyword">endmodule</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/ModulesAndVariables?action=sourceblock&num=1' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>The definition of a module contains two parts: its <em>variables</em> and its <em>commands</em>.
The variables describe the possible states that the module can be in;
the <a class='wikilink' href='Commands.html'>commands</a> describe its behaviour, i.e. the way in which the state changes over time.
Currently, PRISM supports just a few simple types of variables:
they can either be (finite ranges of) integers or Booleans
(we ignore <a class='wikilink' href='PTAs.html'>clocks</a> for now).
</p>
<p class='vspace'>In the example above, each module has one integer variable with range <code>[0..2]</code>.
A variable declaration looks like:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
<div class='sourceblocktext'><div class="prism"><span class="prismident">x</span> : [<span class="prismnum">0</span>..<span class="prismnum">2</span>] <span class="prismkeyword">init</span> <span class="prismnum">0</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/ModulesAndVariables?action=sourceblock&num=2' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Notice that the initial value of the variable is also specified.
A Boolean variable is declared as follows:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
<div class='sourceblocktext'><div class="prism"><span class="prismident">b</span> : <span class="prismkeyword">bool</span> <span class="prismkeyword">init</span> <span class="prismkeyword">false</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/ModulesAndVariables?action=sourceblock&num=3' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>It is also possible to omit the initial value of a variable,
in which case it is assumed to be the lowest value in the range (or <code>false</code> for a Boolean).
Thus, the variable declarations shown below are equivalent to the ones above.
As will be described later, it is also possible to specify
<a class='wikilink' href='MultipleInitialStates.html'>multiple initial states</a> for a model.
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
<div class='sourceblocktext'><div class="prism"><span class="prismident">x</span> : [<span class="prismnum">0</span>..<span class="prismnum">2</span>] <span class="prismkeyword">init</span> <span class="prismnum">0</span>;<br/>
<span class="prismident">b</span> : <span class="prismkeyword">bool</span> <span class="prismkeyword">init</span> <span class="prismkeyword">false</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/ModulesAndVariables?action=sourceblock&num=4' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>We also mention that, for a few kinds of model analysis (typically those based on simulation, such as <a class='wikilink' href='../RunningPRISM/ApproximateModelChecking.html'>approximate model checking</a> or <a class='wikilink' href='../ConfiguringPRISM/SolutionMethodsAndOptions.html#fau'>fast adaptive simulation</a>, it is also permissable to use integer variables with unbounded ranges, denoted as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
<div class='sourceblocktext'><div class="prism"><span class="prismident">x</span> : <span class="prismkeyword">int</span>;<br/>
<span class="prismident">y</span> : <span class="prismkeyword">int</span> <span class="prismkeyword">init</span> <span class="prismnum">3</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/ModulesAndVariables?action=sourceblock&num=5' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Where the state space of the model remains finite, despite the presence of such unbounded variables, you can use the <a class='wikilink' href='../ConfiguringPRISM/ComputationEngines.html'>explicit engine</a> to build and analyse the model.
</p>
<div class='vspace'></div><h3>Identifiers</h3>
<p>The names given to modules and variables are referred to as <em>identifiers</em>.
Identifiers can be made up of letters, digits and the underscore character, but cannot begin with a digit,
i.e. they must satisfy the regular expression [A-Za-z_][A-Za-z0-9_]*, and are case-sensitive.
Furthermore, identifiers cannot be any of the following, which are all reserved keywords in PRISM:
<code><strong>A</strong></code>, <code><strong>bool</strong></code>, <code><strong>clock</strong></code>, <code><strong>const</strong></code>, <code><strong>ctmc</strong></code>, <code><strong>C</strong></code>, <code><strong>double</strong></code>, <code><strong>dtmc</strong></code>, <code><strong>E</strong></code>, <code><strong>endinit</strong></code>, <code><strong>endinvariant</strong></code>, <code><strong>endmodule</strong></code>, <code><strong>endrewards</strong></code>, <code><strong>endsystem</strong></code>, <code><strong>false</strong></code>, <code><strong>formula</strong></code>, <code><strong>filter</strong></code>, <code><strong>func</strong></code>, <code><strong>F</strong></code>, <code><strong>global</strong></code>, <code><strong>G</strong></code>, <code><strong>init</strong></code>, <code><strong>invariant</strong></code>, <code><strong>I</strong></code>, <code><strong>int</strong></code>, <code><strong>label</strong></code>, <code><strong>max</strong></code>, <code><strong>mdp</strong></code>, <code><strong>min</strong></code>, <code><strong>module</strong></code>, <code><strong>X</strong></code>, <code><strong>nondeterministic</strong></code>, <code><strong>Pmax</strong></code>, <code><strong>Pmin</strong></code>, <code><strong>P</strong></code>, <code><strong>probabilistic</strong></code>, <code><strong>prob</strong></code>, <code><strong>pta</strong></code>, <code><strong>rate</strong></code>, <code><strong>rewards</strong></code>, <code><strong>Rmax</strong></code>, <code><strong>Rmin</strong></code>, <code><strong>R</strong></code>, <code><strong>S</strong></code>, <code><strong>stochastic</strong></code>, <code><strong>system</strong></code>, <code><strong>true</strong></code>, <code><strong>U</strong></code>, <code><strong>W</strong></code>.
</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'>The PRISM Language</a></strong>
</p><ul><li><a class='wikilink' href='Main.html'>Introduction</a>
</li><li><a class='wikilink' href='Example1.html'>Example 1</a>
</li><li><a class='wikilink' href='ModelType.html'>Model Type</a>
</li><li><a class='selflink' href='ModulesAndVariables.html'>Modules And Variables</a>
</li><li><a class='wikilink' href='Commands.html'>Commands</a>
</li><li><a class='wikilink' href='ParallelComposition.html'>Parallel Composition</a>
</li><li><a class='wikilink' href='LocalNondeterminism.html'>Local Nondeterminism</a>
</li><li><a class='wikilink' href='CTMCs.html'>CTMCs</a>
</li><li><a class='wikilink' href='Example2.html'>Example 2</a>
</li><li><a class='wikilink' href='Constants.html'>Constants</a>
</li><li><a class='wikilink' href='Expressions.html'>Expressions</a>
</li><li><a class='wikilink' href='Synchronisation.html'>Synchronisation</a>
</li><li><a class='wikilink' href='ModuleRenaming.html'>Module Renaming</a>
</li><li><a class='wikilink' href='MultipleInitialStates.html'>Multiple Initial States</a>
</li><li><a class='wikilink' href='GlobalVariables.html'>Global Variables</a>
</li><li><a class='wikilink' href='FormulasAndLabels.html'>Formulas And Labels</a>
</li><li><a class='wikilink' href='PTAs.html'>PTAs</a>
</li><li><a class='wikilink' href='CostsAndRewards.html'>Costs And Rewards</a>
</li><li><a class='wikilink' href='ProcessAlgebraOperators.html'>Process Algebra Operators</a>
</li><li><a class='wikilink' href='PRISMModelFiles.html'>PRISM Model Files</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>
</div> <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->
</body>
</html>
|