<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>
PRISM Manual | ThePRISMLanguage / Expressions
</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>Expressions</h1>
</div>
<!--PageText-->
<div id='wikitext'>
<p>The definition of the <code>area</code> constant, in the example above, uses an <em>expression</em>.
We now define more precisely what types of expression are supported by PRISM.
Expressions can contain literal values (12, 3.141592, <code><strong>true</strong></code>, <code><strong>false</strong></code>, etc.),
identifiers (corresponding to variables, constants, etc.) and operators from the following list:
</p>
<div class='vspace'></div><ul><li><code>-</code> (unary minus)
</li><li><code>*</code>, <code>/</code> (multiplication, division)
</li><li><code>+</code>, <code>-</code> (addition, subtraction)
</li><li><code><</code>, <code><=</code>, <code>>=</code>, <code>></code> (relational operators)
</li><li><code>=</code>, <code>!=</code> (equality operators)
</li><li><code>!</code> (negation)
</li><li><code>&</code> (conjunction)
</li><li><code>|</code> (disjunction)
</li><li><code><=></code> (if-and-only-if)
</li><li><code>=></code> (implication)
</li><li><code>?</code> (condition evaluation: <code>condition ? a : b</code> means "if <code>condition</code> is true then <code>a</code> else <code>b</code>")
</li></ul><p class='vspace'>All of these operators except <code>?</code> are left associative
(i.e. they are evaluated from left to right).
The precedence of the operators is as found in the list above,
most strongly binding operators first.
Operators on the same line (e.g. <code>+</code> and <code>-</code>) are of equal precedence.
</p>
<p class='vspace'>Much of the notation for expressions is hence essentially equivalent to that of C/C++ or Java.
One notable exception to this is that the division operator <code>/</code> always performs floating point, not integer, division,
i.e. the result of <code>22/7</code> is 3.142857... not 3.
All expressions must evaluate correctly in terms of type (integer, double or Boolean).
</p>
<p class='vspace'><strong>Built-in Functions</strong>
</p>
<p class='vspace'>Expressions can make use of several built-in functions:
</p>
<div class='vspace'></div><ul><li><code>min(...)</code> and <code>max(...)</code>, which select the minimum and maximum value, respectively, of two or more numbers;
</li><li><code>floor(x)</code> and <code>ceil(x)</code>, which round <code>x</code> down and up, respectively, to the nearest integer;
</li><li><code>pow(x,y)</code> which computes <code>x</code> to the power of <code>y</code>;
</li><li><code>mod(i,n)</code> for integer modulo operations;
</li><li><code>log(x,b)</code>, which computes the logarithm of <code>x</code> to base <code>b</code>.
</li></ul><p class='vspace'>Examples of their usage are:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">min</span>(<span class="prismident">x</span>+<span class="prismnum">1</span>, <span class="prismident">x_max</span>)<br/>
<span class="prismkeyword">max</span>(<span class="prismident">a</span>,<span class="prismident">b</span>,<span class="prismident">c</span>)<br/>
<span class="prismident">floor</span>(<span class="prismnum">13.5</span>)<br/>
<span class="prismident">ceil</span>(<span class="prismnum">13.5</span>)<br/>
<span class="prismident">pow</span>(<span class="prismnum">2</span>, <span class="prismnum">8</span>)<br/>
<span class="prismident">pow</span>(<span class="prismnum">9.0</span>, <span class="prismnum">0.5</span>)<br/>
<span class="prismident">mod</span>(<span class="prismnum">1977</span>, <span class="prismnum">100</span>)<br/>
<span class="prismident">log</span>(<span class="prismnum">123</span>, <span class="prismnum">2.71828183</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/Expressions?action=sourceblock&num=1' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>For compatibility with older versions of PRISM, all functions can also be expressed via the <code><strong>func</strong></code> keyword, e.g. <code>func(floor, 13.5)</code>.
</p>
<p class='vspace'><strong>Use of Expressions</strong>
</p>
<p class='vspace'>Expressions can be used in a wide range of places in a PRISM language description, e.g.:
</p>
<div class='vspace'></div><ul><li>constant definitions
</li><li>lower/upper bounds and initial values for variables
</li><li>guards
</li><li>probabilities/rates
</li><li>updates
</li></ul><p class='vspace'>This allows, for example, the probability in a command to be dependent on the current state:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
<div class='sourceblocktext'><div class="prism">[] (<span class="prismident">x</span>>=<span class="prismnum">1</span> & <span class="prismident">x</span><=<span class="prismnum">10</span>) -> <span class="prismident">x</span>/<span class="prismnum">10</span> : (<span class="prismident">x</span>'=<span class="prismkeyword">max</span>(<span class="prismnum">1</span>,<span class="prismident">x</span>-<span class="prismnum">1</span>)) + <span class="prismnum">1</span>-<span class="prismident">x</span>/<span class="prismnum">10</span> : (<span class="prismident">x</span>'=<span class="prismkeyword">min</span>(<span class="prismnum">10</span>,<span class="prismident">x</span>+<span class="prismnum">1</span>))<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/Expressions?action=sourceblock&num=2' type='text/plain'>[$[Get Code]]</a></div>
</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'>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='wikilink' 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='selflink' 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>