<!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>