Blame view
prism-4.3-linux64/doc/manual/ThePRISMLanguage/AllOnOnePage.html
77.1 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 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>
PRISM Manual | ThePRISMLanguage / PTAs
</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--><!--PageText-->
<div id='wikitext'>
<div class='vspace'></div><h1><span class='big'>The PRISM Language</span></h1>
<hr />
<h1>Introduction</h1>
<p>In order to construct and analyse a model with PRISM,
it must be specified in the PRISM language,
a simple, state-based language,
based on the Reactive Modules formalism of Alur and Henzinger [<a class='wikilink' href='../Main/References.html#AH99'>AH99</a>].
This is used for all of the types of model that PRISM supports:
discrete-time Markov chains (DTMCs),
continuous-time Markov chains (CTMCs),
Markov decision processes (MDPs)
and probabilistic timed automata (PTAs).
For background material on these models, look at the pointers to
<a class='urllink' href='http://www.prismmodelchecker.org/about.php'>resources</a>
on the PRISM web site.
</p>
<p class='vspace'>In this section, we describe the PRISM language and present a number of small illustrative examples.
A precise definition of the semantics of the language is available from the "<a class='urllink' href='http://www.prismmodelchecker.org/doc/'>Documentation</a>" section of the PRISM web site. One of the best ways to learn what can be done with the PRISM language is to look at some existing examples.
A number of these are included with the tool distribution in the <code>examples</code> directory.
Many additional examples can be found on the "<a class='urllink' href='http://www.prismmodelchecker.org/casestudies/'>Case Studies</a>" section of the <a class='urllink' href='http://www.prismmodelchecker.org/'>PRISM website</a>.
</p>
<p class='vspace'>The fundamental components of the PRISM language are <em>modules</em> and <em>variables</em>.
A model is composed of a number of <em>modules</em> which can interact with each other.
A module contains a number of local <em>variables</em>.
The values of these variables at any given time constitute the state of the module.
The <em>global state</em> of the whole model is determined by the <em>local state</em> of all modules.
The behaviour of each module is described by a set of <em>commands</em>.
A command takes the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">guard</span> -> <span class="prismident">prob_1</span> : <span class="prismident">update_1</span> + ... + <span class="prismident">prob_n</span> : <span class="prismident">update_n</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=1' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>The <em>guard</em> is a predicate over all the variables in the model (including those belonging to other modules). Each <em>update</em> describes a transition which the module can make if the guard is true. A transition is specified by giving the new values of the variables in the module, possibly as a function of other variables. Each update is also assigned a probability (or in some cases a rate) which will be assigned to the corresponding transition.
</p><hr />
<h1>Example 1</h1>
<p>We will use the following simple example to illustrate the basic concepts of the PRISM language.
Consider a system comprising two identical processes which must operate under mutual exclusion.
Each process can be in one of 3 states: {0,1,2}.
From state 0, a process will move to state 1 with probability 0.2
and remain in the same state with probability 0.8.
From state 1, it tries to move to the critical section: state 2.
This can only occur if the other process is not in its critical section.
Finally, from state 2, a process will either remain there or move back to state 0
with equal probability.
The PRISM code to describe an MDP model of this system can be seen below.
In the next sections, we explain each aspect of the code in turn.
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
<div class='sourceblocktext'><div class="prism"><span class="prismcomment">// Example 1</span><br/>
<span class="prismcomment">// Two process mutual exclusion</span><br/>
<br/>
<span class="prismkeyword">mdp</span><br/>
<br/>
<span class="prismkeyword">module</span> <span class="prismident">M1</span><br/>
<br/>
<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/>
<br/>
[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> <span class="prismnum">0.8</span>:(<span class="prismident">x</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">x</span>'=<span class="prismnum">1</span>);<br/>
[] <span class="prismident">x</span>=<span class="prismnum">1</span> & <span class="prismident">y</span>!=<span class="prismnum">2</span> -> (<span class="prismident">x</span>'=<span class="prismnum">2</span>);<br/>
[] <span class="prismident">x</span>=<span class="prismnum">2</span> -> <span class="prismnum">0.5</span>:(<span class="prismident">x</span>'=<span class="prismnum">2</span>) + <span class="prismnum">0.5</span>:(<span class="prismident">x</span>'=<span class="prismnum">0</span>);<br/>
<br/>
<span class="prismkeyword">endmodule</span><br/>
<br/>
<span class="prismkeyword">module</span> <span class="prismident">M2</span><br/>
<br/>
<span class="prismident">y</span> : [<span class="prismnum">0</span>..<span class="prismnum">2</span>] <span class="prismkeyword">init</span> <span class="prismnum">0</span>;<br/>
<br/>
[] <span class="prismident">y</span>=<span class="prismnum">0</span> -> <span class="prismnum">0.8</span>:(<span class="prismident">y</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">y</span>'=<span class="prismnum">1</span>);<br/>
[] <span class="prismident">y</span>=<span class="prismnum">1</span> & <span class="prismident">x</span>!=<span class="prismnum">2</span> -> (<span class="prismident">y</span>'=<span class="prismnum">2</span>);<br/>
[] <span class="prismident">y</span>=<span class="prismnum">2</span> -> <span class="prismnum">0.5</span>:(<span class="prismident">y</span>'=<span class="prismnum">2</span>) + <span class="prismnum">0.5</span>:(<span class="prismident">y</span>'=<span class="prismnum">0</span>);<br/>
<br/>
<span class="prismkeyword">endmodule</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=2' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace' style='text-align: center;'><strong>The PRISM Language: Example 1</strong>
</p><hr />
<h1>Model Type</h1>
<p>As mentioned above, the PRISM language can be used to describe several types of probabilistic models:
DTMCs, CTMCs, MDPs and PTAs.
To indicate which type is being described, a PRISM model should include one of the keywords
<code><strong>dtmc</strong></code>, <code><strong>ctmc</strong></code>, <code><strong>mdp</strong></code> or <code><strong>pta</strong></code>.
This is typically at the very start of the file,
but can actually occur anywhere in the file (except inside modules and other declarations).
If no such model type declaration is included, the model is by default assumed to be an MDP.
</p>
<p class='vspace'><strong>Note:</strong> As mentioned earlier, PRISM also supports probabilistic automata (PAs) [<a class='wikilink' href='../Main/References.html#Seg95'>Seg95</a>], but (mis)uses the terminology Markov decision process (MDP) for this model.
</p>
<p class='vspace'><strong>Note:</strong> For compatibility with old versions of PRISM,
the keywords <code><strong>probabilistic</strong></code>, <code><strong>stochastic</strong></code> and <code><strong>nondeterministic</strong></code>
can be used as alternatives for <code><strong>dtmc</strong></code>, <code><strong>ctmc</strong></code> and <code><strong>mdp</strong></code>, respectively.
</p>
<div class='vspace'></div><hr />
<h1>Modules And Variables</h1>
<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='sourceblock3'>
<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/AllOnOnePage?action=sourceblock&num=3' 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='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/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=4' 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='sourceblock5'>
<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/AllOnOnePage?action=sourceblock&num=5' 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='sourceblock6'>
<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/AllOnOnePage?action=sourceblock&num=6' 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='sourceblock7'>
<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/AllOnOnePage?action=sourceblock&num=7' 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><hr />
<h1>Commands</h1>
<p>The behaviour of each module is described by <em>commands</em>,
comprising a <em>guard</em> and one or more <em>updates</em>.
The first command of module <code>M1</code> in our <a class='wikilink' href='Example1.html'>example</a> is:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock8'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> <span class="prismnum">0.8</span>:(<span class="prismident">x</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">x</span>'=<span class="prismnum">1</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=8' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>The guard <code>x=0</code> indicates that this describes the behaviour of the module when the variable <code>x</code> has value 0.
The updates <code>(x'=0)</code> and <code>(x'=1)</code> and their associated probabilities state that the value of <code>x</code> will
remain at 0 with probability 0.8 and change to 1 with probability 0.2.
Note that the inclusion of updates in parentheses, e.g. <code>(x'=1)</code>, is essential.
While older versions of PRISM did not report the absence of parentheses as an error, newer versions do.
Note also that PRISM will complain if the probabilities on the right hand side of a command do not sum to one.
</p>
<p class='vspace'>The second command:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock9'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">1</span> & <span class="prismident">y</span>!=<span class="prismnum">2</span> -> (<span class="prismident">x</span>'=<span class="prismnum">2</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=9' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>illustrates that guards can contain constraints on any variable, not just the ones in that module,
i.e. the behaviour of one module can depend on the state of another.
Updates, however, can only specify values for variables belonging to the module.
In general a module can <em>read</em> the variables of any other module, but only <em>write</em> to its own.
When a command comprises a single update with probability 1, the <code>1.0:</code> can be omitted,
as is done in the example above.
</p>
<p class='vspace'>If a module has more than one variable, updates describe the new value for each of them.
For example, if it had two variables <code>x1</code> and <code>x2</code>, a possible command would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock10'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x1</span>=<span class="prismnum">0</span> & <span class="prismident">x2</span>><span class="prismnum">0</span> & <span class="prismident">x2</span><<span class="prismnum">10</span> -> <span class="prismnum">0.5</span>:(<span class="prismident">x1</span>'=<span class="prismnum">1</span>)&(<span class="prismident">x2</span>'=<span class="prismident">x2</span>+<span class="prismnum">1</span>) + <span class="prismnum">0.5</span>:(<span class="prismident">x1</span>'=<span class="prismnum">2</span>)&(<span class="prismident">x2</span>'=<span class="prismident">x2</span>-<span class="prismnum">1</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=10' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Notice that elements of the updates are concatenated with <code>&</code> and that each element must be bracketed individually.
If an update does not give a new value for a local variable, it is assumed not to change.
As a special case, the keyword <code><strong>true</strong></code> can be used to denote an update where no variable's value changes, i.e. the following are all equivalent:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock11'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x1</span>><span class="prismnum">10</span> | <span class="prismident">x2</span>><span class="prismnum">10</span> -> (<span class="prismident">x1</span>'=<span class="prismident">x1</span>)&(<span class="prismident">x2</span>'=<span class="prismident">x2</span>);<br/>
[] <span class="prismident">x1</span>><span class="prismnum">10</span> | <span class="prismident">x2</span>><span class="prismnum">10</span> -> (<span class="prismident">x1</span>'=<span class="prismident">x1</span>);<br/>
[] <span class="prismident">x1</span>><span class="prismnum">10</span> | <span class="prismident">x2</span>><span class="prismnum">10</span> -> <span class="prismkeyword">true</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=11' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Finally, it is important to remember that the expressions on the right hand side of each update refer to the state of the model <em>before</em> the update occurs. So, for example, this command:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock12'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x1</span>=<span class="prismnum">0</span> & <span class="prismident">x2</span>=<span class="prismnum">1</span> -> (<span class="prismident">x1</span>'=<span class="prismnum">2</span>)&(<span class="prismident">x2</span>'=<span class="prismident">x1</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=12' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>updates variable <code>x2</code> to 0, not 2.
</p>
<div class='vspace'></div><hr />
<h1>Parallel Composition</h1>
<p>The probabilistic model corresponding to a PRISM language description is constructed as the <em>parallel composition</em> of its modules. In every state of the model, there is a set of commands (belonging to any of the modules) which are enabled, i.e. whose guards are satisfied in that state. The choice between which command is performed (i.e. the <em>scheduling</em>) depends on the model type.
</p>
<p class='vspace'>For an MDP, as in <a class='wikilink' href='Example1.html'>Example 1</a>, the choice is <em>nondeterministic</em>. By way of example, consider state <code>(0,0)</code> (i.e. <code>x=0</code> and <code>y=0</code>). There are two commands enabled, one from each module:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock13'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> <span class="prismnum">0.8</span>:(<span class="prismident">x</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">x</span>'=<span class="prismnum">1</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=13' type='text/plain'>[$[Get Code]]</a></div>
</div>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock14'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">y</span>=<span class="prismnum">0</span> -> <span class="prismnum">0.8</span>:(<span class="prismident">y</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">y</span>'=<span class="prismnum">1</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=14' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>In state <code>(0,0)</code> of the MDP, there would be a nondeterministic choice between these two probability distributions:
</p>
<div class='vspace'></div><ul><li><code>0.8:(0,0) + 0.2:(1,0)</code> (module <code>M1</code> moves)
</li><li><code>0.8:(0,0) + 0.2:(0,1)</code> (module <code>M2</code> moves)
</li></ul><p class='vspace'>For a DTMC, the choice is <em>probabilistic</em>: each enabled command is selected with equal probability.
If <a class='wikilink' href='Example1.html'>Example 1</a> was a DTMC, then in state <code>(0,0)</code> of the model
the following probability distribution would result:
</p>
<div class='vspace'></div><ul><li><code>0.8:(0,0) + 0.1:(1,0) + 0.1:(0,1)</code>
</li></ul><p class='vspace'>For a <a class='wikilink' href='CTMCs.html'>CTMC</a>, as will be discussed shortly,
the choice is modelled as a "race" between transitions.
</p>
<p class='vspace'>See the later sections on "<a class='wikilink' href='Synchronisation.html'>Synchronisation</a>" and "<a class='wikilink' href='ProcessAlgebraOperators.html'>Process Algebra Operators</a>" for other topics related to parallel composition.
</p><hr />
<h1>Local Nondeterminism</h1>
<p>PRISM models that support nondeterminism, such as are MDPs, can also exhibit <em>local nondeterminism</em>,
which allows the modules themselves to make nondeterministic choices.
In <a class='wikilink' href='Example1.html'>Example 1</a>, we can make the probabilistic choice in the first state of module <code>M1</code> nondeterministic by replacing the command:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock15'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> <span class="prismnum">0.8</span>:(<span class="prismident">x</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.2</span>:(<span class="prismident">x</span>'=<span class="prismnum">1</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=15' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>with the commands:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock16'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> (<span class="prismident">x</span>'=<span class="prismnum">0</span>);<br/>
[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> (<span class="prismident">x</span>'=<span class="prismnum">1</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=16' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Assuming we do the same for module <code>M2</code>, in state <code>(0,0)</code> of the MDP
there will be a nondeterministic choice between the three (trivial) probability distributions listed below. (There are three, not four, distributions because two possibilities result in identical behaviour: staying with probability 1 in the state state.)
</p>
<div class='vspace'></div><ul><li><code>1.0:(0,0)</code>
</li><li><code>1.0:(1,0)</code>
</li><li><code>1.0:(0,1)</code>
</li></ul><p class='vspace'>More generally, local nondeterminism can also arise when the guards of two commands overlap only partially, rather than completely as in the example above.
</p>
<p class='vspace'>PRISM also permits local nondeterminism in models which are DTMCs,
although the nondeterministic choice is randomised when the parallel composition of the modules occurs.
Since the appearance of nondeterminism in a DTMC is often the result of
a user error in the model specification, PRISM displays a warning when local nondeterminism is detected in a DTMC.
Overlapping guards in <a class='wikilink' href='CTMCs.html'>CTMCs</a> are not treated as nondeterministic choices.
</p>
<div class='vspace'></div><hr />
<h1>CTMCs</h1>
<p class='vspace'>Specifying the behaviour of a continuous-time Markov chain (CTMC)
is done in similar fashion to a DTMC or an MDP, as discussed so far.
The main difference is that updates in commands are
labelled with (positive-valued) <em>rates</em>, rather than probabilities.
The notation used in commands, however, to associate rates to transitions is identical to
the one used to assign probabilities:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock17'>
<div class='sourceblocktext'><div class="prism"><span class="prismident">rate_1</span>:<span class="prismident">update_1</span> + <span class="prismident">rate_2</span>:<span class="prismident">update_2</span> + ...<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=17' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>In a CTMC, when multiple possible transitions are available in a state, a <em>race condition</em> occurs
(see e.g. [<a class='wikilink' href='../Main/References.html#KNP07a'>KNP07a</a>] for more details).
In terms of PRISM commands, this can arise in several ways.
Firstly, within in a module, multiple transitions can be specified either as several different updates in a command, or as multiple commands with overlapping guards. The following, for example. are equivalent:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock18'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> <span class="prismnum">50</span>:(<span class="prismident">x</span>'=<span class="prismnum">1</span>) + <span class="prismnum">60</span>:(<span class="prismident">x</span>'=<span class="prismnum">2</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=18' type='text/plain'>[$[Get Code]]</a></div>
</div>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock19'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> <span class="prismnum">50</span>:(<span class="prismident">x</span>'=<span class="prismnum">1</span>);<br/>
[] <span class="prismident">x</span>=<span class="prismnum">0</span> -> <span class="prismnum">60</span>:(<span class="prismident">x</span>'=<span class="prismnum">2</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=19' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Furthermore, parallel composition between modules in a CTMC is modelled as a race condition,
rather as a nondeterministic choice, like for <a class='wikilink' href='ParallelComposition.html'>MDPs</a>.
</p><hr />
<h1>Example 2</h1>
<p>We now introduce a second example: a CTMC that models an <em>N</em>-place queue of jobs and
a server which removes jobs from the queue and processes them.
The PRISM code is as follows:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock20'>
<div class='sourceblocktext'><div class="prism"><span class="prismcomment">// Example 2</span><br/>
<span class="prismcomment">// N-place queue + server</span><br/>
<br/>
<span class="prismkeyword">ctmc</span><br/>
<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">int</span> <span class="prismident">N</span> = <span class="prismnum">10</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">mu</span> = <span class="prismnum">1</span>/<span class="prismnum">10</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">lambda</span> = <span class="prismnum">1</span>/<span class="prismnum">2</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">gamma</span> = <span class="prismnum">1</span>/<span class="prismnum">3</span>;<br/>
<br/>
<span class="prismkeyword">module</span> <span class="prismident">queue</span><br/>
<span class="prismident">q</span> : [<span class="prismnum">0</span>..<span class="prismident">N</span>];<br/>
<br/>
[] <span class="prismident">q</span><<span class="prismident">N</span> -> <span class="prismident">mu</span>:(<span class="prismident">q</span>'=<span class="prismident">q</span>+<span class="prismnum">1</span>);<br/>
[] <span class="prismident">q</span>=<span class="prismident">N</span> -> <span class="prismident">mu</span>:(<span class="prismident">q</span>'=<span class="prismident">q</span>);<br/>
[<span class="prismident">serve</span>] <span class="prismident">q</span>><span class="prismnum">0</span> -> <span class="prismident">lambda</span>:(<span class="prismident">q</span>'=<span class="prismident">q</span>-<span class="prismnum">1</span>);<br/>
<span class="prismkeyword">endmodule</span><br/>
<br/>
<span class="prismkeyword">module</span> <span class="prismident">server</span><br/>
<span class="prismident">s</span> : [<span class="prismnum">0</span>..<span class="prismnum">1</span>];<br/>
<br/>
[<span class="prismident">serve</span>] <span class="prismident">s</span>=<span class="prismnum">0</span> -> <span class="prismnum">1</span>:(<span class="prismident">s</span>'=<span class="prismnum">1</span>);<br/>
[] <span class="prismident">s</span>=<span class="prismnum">1</span> -> <span class="prismident">gamma</span>:(<span class="prismident">s</span>'=<span class="prismnum">0</span>);<br/>
<span class="prismkeyword">endmodule</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=20' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace' style='text-align: center;'><strong>The PRISM Language: Example 2</strong>
</p>
<p class='vspace'>This example also introduces a number of other PRISM language concepts,
including <a class='wikilink' href='Constants.html'>constants</a>, action labels and <a class='wikilink' href='Synchronisation.html'>synchronisation</a>.
These are described in the following sections.
</p><hr />
<h1>Constants</h1>
<p>PRISM supports the use of <em>constants</em>, as seen in <a class='wikilink' href='Example2.html'>Example 2</a>.
Constants can be integers, doubles or Booleans
and can be defined using literal values or as constant expressions (including in terms of each other) using the <code><strong>const</strong></code>
keyword. For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock21'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">const</span> <span class="prismkeyword">int</span> <span class="prismident">radius</span> = <span class="prismnum">12</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">pi</span> = <span class="prismnum">3.141592</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">area</span> = <span class="prismident">pi</span> * <span class="prismident">radius</span> * <span class="prismident">radius</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">bool</span> <span class="prismident">yes</span> = <span class="prismkeyword">true</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=21' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>The identifiers used for their names are subject to the same rules as <a class='wikilink' href='ModulesAndVariables.html'>variables</a>.
</p>
<p class='vspace'>Constants can be used anywhere that a constant value would be expected,
such as the lower or upper range of a variable (e.g. <code>N</code> in <a class='wikilink' href='Example2.html'>Example 2</a>),
the probability or rate associated with an update (<code>mu</code> in <a class='wikilink' href='Example2.html'>Example 2</a>),
or anywhere in a guard or update.
As will be described later constants can also be left undefined
and specified later, either to a single value or a range of values, using <a class='wikilink' href='../RunningPRISM/Experiments.html'>experiments</a>.
</p>
<p class='vspace'><strong>Note:</strong> For the sake of backward-compatibility, the notation used in earlier versions of PRISM
(<code><strong>const</strong></code> for <code><strong>const int</strong></code> and <code><strong>rate</strong></code> or <code><strong>prob</strong></code> for <code><strong>const double</strong></code>) is still supported.
</p><hr />
<h1>Expressions</h1>
<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='sourceblock22'>
<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/AllOnOnePage?action=sourceblock&num=22' 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='sourceblock23'>
<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/AllOnOnePage?action=sourceblock&num=23' type='text/plain'>[$[Get Code]]</a></div>
</div>
<hr />
<h1>Synchronisation</h1>
<p>Another feature of PRISM introduced in <a class='wikilink' href='Example2.html'>Example 2</a> is <em>synchronisation</em>.
In the style of many process algebras, we allow commands to be labelled with <em>actions</em>.
These are placed inside the square brackets which mark the start of the command,
for example <code>serve</code> in this command from <a class='wikilink' href='Example2.html'>Example 2</a>:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock24'>
<div class='sourceblocktext'><div class="prism">[<span class="prismident">serve</span>] <span class="prismident">q</span>><span class="prismnum">0</span> -> <span class="prismident">lambda</span>:(<span class="prismident">q</span>'=<span class="prismident">q</span>-<span class="prismnum">1</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=24' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>These actions can be used to force two or more modules to make transitions simultaneously
(i.e. to <em>synchronise</em>).
For example, in state <code>(3,0)</code> (i.e. <code>q=3</code> and <code>s=0</code>),
the composed model can move to state <code>(2,1)</code>,
synchronising over the <code>serve</code> action.
The rate of this transition is equal to the product of the two individual rates
(in this case, <code>lambda * 1 = lambda</code>).
The product of two rates does not always meaningfully represent the rate of a synchronised transition.
A common technique, as seen here, is to make one action <em>passive</em>, with rate 1 and one action <em>active</em>,
which actually defines the rate for the synchronised transition.
By default, all modules are combined using the standard CSP parallel composition
(i.e. modules synchronise over all their common actions).
</p><hr />
<h1>Module Renaming</h1>
<p>PRISM also supports <em>module renaming</em>, which allows duplication of modules.
In <a class='wikilink' href='Example1.html'>Example 1</a>, module <code>M2</code> is identical to module <code>M1</code> so we can in fact replace its entire definition with:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock25'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">module</span> <span class="prismident">M2</span> = <span class="prismident">M1</span> [ <span class="prismident">x</span>=<span class="prismident">y</span>, <span class="prismident">y</span>=<span class="prismident">x</span> ] <span class="prismkeyword">endmodule</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=25' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>All of the variables in the module being renamed (in this case, just <code>x</code>) <em>must</em> be renamed to new, unused names. Optionally, it is also possible to rename other aspects of the module definition. In fact, the renaming is done at a textual level, so any identifiers (including <a class='wikilink' href='Synchronisation.html'>action labels</a>, <a class='wikilink' href='Constants.html'>constants</a> and <a class='wikilink' href='Expressions.html'>functions</a>) used in the module definition can be changed in this way.
</p>
<p class='vspace'><strong>Note:</strong> Care should be taken when renaming modules that make use of <a class='wikilink' href='FormulasAndLabels.html'>formulas</a>.
</p><hr />
<h1>Multiple Initial States</h1>
<p>Typically, a <a class='wikilink' href='ModulesAndVariables.html'>variable</a> declaration
specifies the initial value for that variable.
The <em>initial state</em> for the model is then defined by the initial value for all variables.
It is possible, however, to specify that a model has <em>multiple</em> initial states.
This is done using the <code><strong>init</strong>...<strong>endinit</strong></code> construct,
which can be placed anywhere in the file except within a module definition,
and removing any initial values from variable declarations.
Between the <code><strong>init</strong></code> and <code><strong>endinit</strong></code> keywords, there should be a
predicate over all the variables of the model.
Any state which satisfies this predicate is an initial state.
</p>
<p class='vspace'>Consider again <a class='wikilink' href='Example1.html'>Example 1</a>.
As it stands, there is a single initial state <code>(0,0)</code> (i.e. <code>x=0</code> and <code>y=0</code>).
If we remove the <code><strong>init</strong> 0</code> part of both variable declarations
and add the following to the end of the file:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock26'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">init</span> <span class="prismident">x</span>=<span class="prismnum">0</span> <span class="prismkeyword">endinit</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=26' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>there will be three initial states: <code>(0,0)</code>, <code>(0,1)</code> and <code>(0,2)</code>.
Similarly, we could instead add:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock27'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">init</span> <span class="prismident">x</span>+<span class="prismident">y</span>=<span class="prismnum">1</span> <span class="prismkeyword">endinit</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=27' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>in which case there would be two initial states: <code>(0,1)</code> and <code>(1,0)</code>.
</p><hr />
<h1>Global Variables</h1>
<p>In addition to the local variables belonging to each module, a PRISM model can also include <em>global variables</em>,
which can be written to, as well as read, by all modules.
Like local variables, these can be integers or Booleans.
Global variables are declared in identical fashion to a module's local variables,
except that the declaration must not be inside the definition of any module.
Some example declarations are as follows:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock28'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">global</span> <span class="prismident">g</span> : [<span class="prismnum">1</span>..<span class="prismnum">10</span>];<br/>
<span class="prismkeyword">global</span> <span class="prismident">b</span> : <span class="prismkeyword">bool</span> <span class="prismkeyword">init</span> <span class="prismkeyword">true</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=28' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>A global variable can be modified by any module and provides another way for modules to interact.
An important restriction on the use of global variables is the fact that commands which synchronise with other modules
(i.e. those with an action label attached; see the section "<a class='wikilink' href='Synchronisation.html'>Synchronisation</a>") cannot modify global variables.
PRISM will detect this and report an error.
</p><hr />
<h1>Formulas And Labels</h1>
<p>PRISM models can include <em>formulas</em> which are used to avoid duplication of code.
A formula comprises a name (an identifier) and an <a class='wikilink' href='Expressions.html'>expression</a>.
The formula name can then be used as shorthand for the expression anywhere an expression might usually be accepted.
A formula is defined as follows:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock29'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">formula</span> <span class="prismident">num_tokens</span> = <span class="prismident">q1</span>+<span class="prismident">q2</span>+<span class="prismident">q3</span>+<span class="prismident">q</span>+<span class="prismident">q5</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=29' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>It can then be used anywhere within that file, as for example in this command:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock30'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">p1</span>=<span class="prismnum">2</span> & <span class="prismident">num_tokens</span>=<span class="prismnum">5</span> -> (<span class="prismident">p1</span>'=<span class="prismnum">4</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=30' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>The effect is exactly as if the following had been typed:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock31'>
<div class='sourceblocktext'><div class="prism">[] <span class="prismident">p1</span>=<span class="prismnum">2</span> & (<span class="prismident">q1</span>+<span class="prismident">q2</span>+<span class="prismident">q3</span>+<span class="prismident">q</span>+<span class="prismident">q5</span>)=<span class="prismnum">5</span> -> (<span class="prismident">p1</span>'=<span class="prismnum">4</span>);<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=31' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Formulas defined in a model can also be used when specifying its properties.
</p>
<div class='vspace'></div><h3>Formulas and renaming</h3>
<p>During parsing of the model, expansion of formulas is done before module renaming so, if a module which uses formulas is renamed to another module, it is the contents of the formula which will be renamed, not the formula itself.
</p>
<div class='vspace'></div><h3>Labels</h3>
<p>PRISM models can also contain <em>labels</em>. These are are a way of identifying sets of states that are of particular interest. Labels can only be used when specifying <a class='wikilink' href='../PropertySpecification/Main.html'>properties</a> but, for convenience, can be defined in model files as well as property files.
</p>
<p class='vspace'>Labels differ from formulas in two other ways: firstly, they must be of Boolean type;
secondly, they are written using quotation marks (<code>"..."</code>), as illustrated in the following example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock32'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">label</span> "<span class="prismident">safe</span>" = <span class="prismident">temp</span><=<span class="prismnum">100</span> | <span class="prismident">alarm</span>=<span class="prismkeyword">true</span>;<br/>
<span class="prismkeyword">label</span> "<span class="prismident">fail</span>" = <span class="prismident">temp</span>><span class="prismnum">100</span> & <span class="prismident">alarm</span>=<span class="prismkeyword">false</span>;<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=32' type='text/plain'>[$[Get Code]]</a></div>
</div>
<hr />
<h1>PTAs</h1>
<p class='vspace'>So far in this section, we have mainly focused on three types of models: DTMCs, MDPs and CTMCs.
PRISM also supports a fourth: <em>probabilistic timed automata</em> (PTAs), which extend MDPs with the ability to model real-time behaviour. This is done in the style of <em>timed automata</em> [<a class='wikilink' href='../Main/References.html#AD94'>AD94</a>], by adding real-valued <em>clocks</em> which increase with time and can be reset. For background material on PTAs, see for example [<a class='wikilink' href='../Main/References.html#NPS13'>NPS13</a>].
You can also find several example PTA models included in the PRISM distribution. Look in the <code>examples/pta</code> directory.
</p>
<p class='vspace'>Before describing how PTA features are incorporated into the PRISM modelling language, we give a simple example. Here is a small PTA:
</p>
<div class='vspace'></div><div><img src='../uploads/pta.png' alt='' title='' /></div>
<p class='vspace'>and here is a corresponding PRISM model:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock33'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">pta</span><br/>
<br/>
<span class="prismkeyword">module</span> <span class="prismident">M</span><br/>
<br/>
<span class="prismident">s</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">x</span> : <span class="prismkeyword">clock</span>;<br/>
<br/>
<span class="prismkeyword">invariant</span><br/>
(<span class="prismident">s</span>=<span class="prismnum">0</span> => <span class="prismident">x</span><=<span class="prismnum">2</span>) &<br/>
(<span class="prismident">s</span>=<span class="prismnum">2</span> => <span class="prismident">x</span><=<span class="prismnum">3</span>)<br/>
<span class="prismkeyword">endinvariant</span><br/>
<br/>
[<span class="prismident">send</span>] <span class="prismident">s</span>=<span class="prismnum">0</span> & <span class="prismident">x</span>>=<span class="prismnum">1</span> -> <span class="prismnum">0.9</span>:(<span class="prismident">s</span>'=<span class="prismnum">1</span>)&(<span class="prismident">x</span>'=<span class="prismnum">0</span>) + <span class="prismnum">0.1</span>:(<span class="prismident">s</span>'=<span class="prismnum">2</span>)&(<span class="prismident">x</span>'=<span class="prismnum">0</span>);<br/>
[<span class="prismident">retry</span>] <span class="prismident">s</span>=<span class="prismnum">2</span> & <span class="prismident">x</span>>=<span class="prismnum">2</span> -> <span class="prismnum">0.95</span>:(<span class="prismident">s</span>'=<span class="prismnum">1</span>) + <span class="prismnum">0.05</span>:(<span class="prismident">s</span>'=<span class="prismnum">2</span>)&(<span class="prismident">x</span>'=<span class="prismnum">0</span>);<br/>
<br/>
<span class="prismkeyword">endmodule</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=33' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>For modelling PTAs in PRISM, there is a new datatype, <strong><code>clock</code></strong>, used for variables that are clocks. These must be local to a particular module, not global. Other types of PRISM variables can be defined in the usual way. In the example above, we use just a single integer variable <code>s</code> to represent the locations of the PTAs.
</p>
<p class='vspace'>In a PTA, transitions can include a <em>guard</em>, which constrains when it can occur based on the current value of clocks, and <em>resets</em>, which specify that a clock's values should be set to a new (integer) value. These are both specified in PRISM commands in the usual way: see, for example, the inclusion of <code>x>=1</code> in the guard for the <code>send</code>-labelled command and the updates of the form <code>(x'=0)</code> which reset the clock <code>x</code> to 0.
</p>
<p class='vspace'>The other new addition is an <code>invariant</code> construct, which is used to specify an expression describing the clock <em>invariants</em> for each PRISM module. These impose restrictions on the allowable values of clock variables, depending on the values of the other non-clock variables. The <code>invariant</code> construct should appear between the variable declarations and the commands of the module. Often, clock invariants are described separately for each PTA location; hence, the invariant will often take the form of a conjunction of implications, as in the example model above, but more general expressions are also permitted. In the example, the clock <code>x</code> must satisfy <code>x<=2</code> or <code>x<=3</code> when local variables <code>s</code> is 0 or 2, respectively. If <code>s</code> is 1, there is no restriction (since the invariant is effectively <code>true</code> in this case).
</p>
<p class='vspace'>Expressions that include reference to clocks, whether in guards or invariants, must satisfy certain conditions to facilitate model checking. In particular, references to clocks must appear as conjunctions of <em>simple clock constraints</em>, i.e. conjunctions of expressions of the form <code>x~c</code> or <code>x~y</code> where <code>x</code> and <code>y</code> are clocks, <code>c</code> is an integer-valued expression and <code>~</code> is one of <code><</code>, <code><=</code>, <code>>=</code>, <code>></code>, <code>=</code>).
</p>
<p class='vspace'>There are also some additional restrictions imposed on PTA models that are dependent on which of the PTA model checking <a class='wikilink' href='../ConfiguringPRISM/ComputationEngines.html#pta'>engines</a> is in use.
</p>
<p class='vspace'>For the <strong>stochastic games</strong> and <strong>backwards reachability</strong> engines:
</p>
<div class='vspace'></div><ul><li>Modules cannot read the local variables of other modules and global variables are not permitted.
<div class='vspace'></div></li><li>The model must also have a single initial state (i.e. the <code>init...endinit</code> construct is not permitted).
</li></ul><p class='vspace'>For the <strong>digital clocks</strong> engine:
</p>
<div class='vspace'></div><ul><li>Clock constraints cannot use strict comparison operators, e.g. <code>x<=5</code> is allowed, but <code>x<5</code> is not.
<div class='vspace'></div></li><li>Diagonal clock constraints are not allowed, i.e. those containing references to two clocks, such as <code>x<=y</code>.
</li></ul><p class='vspace'>Finally, PRISM makes several assumptions about PTAs, regardless of the engine used.
</p>
<div class='vspace'></div><ul><li>Firstly PTAs should not exhibit <em>timelocks</em>, i.e. the possibility of reaching a state where no transitions are possible and time cannot elapse beyond a certain point (due to invariant conditions). PRISM checks for timelocks and reports an error if one is found.
<div class='vspace'></div></li><li>Secondly, PTAs should be <em>well-formed</em> and <em>non-zeno</em> (see e.g. [<a class='wikilink' href='../Main/References.html#KNSW07'>KNSW07</a>] for details). Currently, PRISM does not check automatically that these assumptions are satisfied.
</li></ul><div class='vspace'></div><hr />
<h1>Costs And Rewards </h1>
<p>PRISM supports the specification and analysis of
properties based on <em>costs</em> and <em>rewards</em>.
This means that it can be used to reason,
not just about the probability that a model behaves in a certain fashion,
but about a wider range of quantitative measures relating to model behaviour.
For example, PRISM can be used to compute properties such as
"expected time", "expected number of lost messages" or "expected power consumption".
The implementation of cost- and reward-based techniques in the tool is only partially completed and is still ongoing.
If you have questions, comments or feature-requests relating to this functionality,
please feel free to contact the PRISM team about this.
</p>
<p class='vspace'>The basic idea is that probabilistic models (of all three types) developed in PRISM
can be augmented with costs or rewards: real values associated with certain states or transitions of the model.
In fact, since there is no practical distinction between costs and rewards
(except that costs are generally perceived to be "bad" and rewards to be "good"),
PRISM only supports rewards.
The user is, however, free to interpret the values however they choose.
</p>
<p class='vspace'>In this section, we describe how models described in the PRISM language
can be augmented with rewards.
Later, we will discuss how to express properties that relate to these rewards.
Rewards are associated with models using <code><strong>rewards</strong> ... <strong>endrewards</strong></code> constructs,
which can appear anywhere in a model file except within a module definition.
These constructs contains one or more <em>reward items</em>.
Consider the following simple example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock34'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">rewards</span><br/>
<span class="prismkeyword">true</span> : <span class="prismnum">1</span>;<br/>
<span class="prismkeyword">endrewards</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=34' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>This assigns a reward of 1 to every state of the model.
It comprises a single reward item, the left part of which (<code><strong>true</strong></code>) is a guard
and the right part of which (<code>1</code>) is a reward.
States of the model which satisfy the predicate in the guard are assigned the corresponding reward.
More generally, state rewards can be specified using multiple reward items,
each of the form <code>guard : reward;</code>,
where <code>guard</code>is a predicate (over all the variables of the model)
and <code>reward</code> is an expression (containing any variables, constants, etc. from the model).
For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock35'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">rewards</span><br/>
<span class="prismident">x</span>=<span class="prismnum">0</span> : <span class="prismnum">100</span>;<br/>
<span class="prismident">x</span>><span class="prismnum">0</span> & <span class="prismident">x</span><<span class="prismnum">10</span> : <span class="prismnum">2</span>*<span class="prismident">x</span>;<br/>
<span class="prismident">x</span>=<span class="prismnum">10</span> : <span class="prismnum">100</span>;<br/>
<span class="prismkeyword">endrewards</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=35' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>assigns a reward of 100 to states satisfying <code>x=0</code> or <code>x=10</code>
and a reward of <code>2*x</code> to states satisfying <code>x>0 & x<10</code>.
Note that a single reward item can assign different rewards to different states,
depending on the values of model variables in each one.
Any states which do not satisfy the guard of any reward item will have no reward assigned to them.
For states which satisfy multiple guards, the reward assigned to the state
is the sum of the rewards for all the corresponding reward items.
</p>
<p class='vspace'>Rewards can also be assigned to transitions of a model.
These are specified in a similar fashion to state rewards,
within the <code><strong>rewards</strong> ... <strong>endrewards</strong></code> construct.
Reward items describing transition rewards are of the form <code>[action] guard : reward;</code>,
the interpretation being that transitions from states which satisfy the guard <code>guard</code>
and are labelled with the action <code>action</code> acquire the reward <code>reward</code>.
For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock36'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">rewards</span><br/>
[] <span class="prismkeyword">true</span> : <span class="prismnum">1</span>;<br/>
[<span class="prismident">a</span>] <span class="prismkeyword">true</span> : <span class="prismident">x</span>;<br/>
[<span class="prismident">b</span>] <span class="prismkeyword">true</span> : <span class="prismnum">2</span>*<span class="prismident">x</span>;<br/>
<span class="prismkeyword">endrewards</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=36' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>assigns a reward of 1 to all transitions in the model with no action label,
and rewards of <code>x</code> and <code>2*x</code> to all transitions labelled with actions <code>a</code> and <code>b</code>, respectively.
</p>
<p class='vspace'>As is the case for states, multiple reward items can specify rewards for a single transition,
in which case the resulting reward is the sum of all the individual rewards.
A model description can specify rewards for both states and transitions.
These are all placed together in a single <code><strong>rewards</strong>...<strong>endrewards</strong></code> construct.
</p>
<p class='vspace'>A PRISM model can have multiple reward structures. Optionally, these can be given labels such as in the following example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock37'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">rewards</span> "<span class="prismident">total_time</span>"<br/>
<span class="prismkeyword">true</span> : <span class="prismnum">1</span>;<br/>
<span class="prismkeyword">endrewards</span><br/>
<br/>
<span class="prismkeyword">rewards</span> "<span class="prismident">num_failures</span>"<br/>
[<span class="prismident">fail</span>] <span class="prismkeyword">true</span> : <span class="prismnum">1</span>;<br/>
<span class="prismkeyword">endrewards</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/AllOnOnePage?action=sourceblock&num=37' type='text/plain'>[$[Get Code]]</a></div>
</div>
<div class='vspace'></div><hr />
<h1>Process Algebra Operators</h1>
<p>To make the concept of synchronisation described above more powerful,
PRISM allows you to define precisely the way in which the set of modules are composed in parallel.
This is specified using the <code><strong>system</strong> ... <strong>endsystem</strong></code> construct,
placed at the end of the model description, which should contain a process-algebraic expression.
This expression should feature each module exactly once, and can use the following (CSP-based) operators:
</p>
<div class='vspace'></div><ul><li><code>M1 || M2</code> : alphabetised parallel composition of modules <code>M1</code> and <code>M2</code> (synchronising on only actions appearing in both <code>M1</code> and <code>M2</code>)
<div class='vspace'></div></li><li><code>M1 ||| M2</code> : asynchronous parallel composition of <code>M1</code> and <code>M2</code> (fully interleaved, no synchronisation)
<div class='vspace'></div></li><li><code>M1 |[a,b,...]| M2</code> : restricted parallel composition of modules <code>M1</code> and <code>M2</code> (synchronising only on actions from the set {<code>a</code>, <code>b</code>,...})
<div class='vspace'></div></li><li><code>M / {a,b,...</code>} : hiding of actions {<code>a</code>, <code>b</code>, ...} in module <code>M</code>
<div class='vspace'></div></li><li><code>M {a<-b,c<-d,...</code>} : renaming of actions <code>a</code> to <code>b</code>, <code>c</code> to <code>d</code>, etc. in module <code>M</code>.
</li></ul><p class='vspace'>The first two types of parallel composition (<code>||</code> and <code>|||</code>) are associative and can be applied to more than two modules at once.
When evaluating the expression, the hiding and renaming operators bind more tightly than the three parallel composition operators.
No other rules of precedence are defined and parentheses should be used to specify the order in which modules are composed.
</p>
<p class='vspace'>Some examples of expressions which could be included in the <code><strong>system</strong> ... <strong>endsystem</strong></code> construct are as follows:
</p>
<div class='vspace'></div><ul><li><code>(station1 ||| station2 ||| station3) |[serve]| server</code>
</li><li><code>((P1 |[a]| P2) / {a}) || Q</code>
</li><li><code>((P1 |[a]| P2) {a<-b}) |[b]| Q</code>
</li></ul><p class='vspace'>When no parallel composition is specified by the user,
PRISM implicitly assumes an expression of the form <code>M1 || M2 || ...</code> containing all of the modules in the model.
For a more formal definition of the process algebra operators described above, check the semantics of the PRISM language, available from the "<a class='urllink' href='http://www.prismmodelchecker.org/doc/'>Documentation</a>" section of the PRISM web site.
</p>
<p class='vspace'>PRISM is also able to <a class='wikilink' href='../RunningPRISM/SupportForPEPAModels.html'>import</a> model descriptions written in (a subset of) the stochastic process algebra <a class='urllink' href='http://www.dcs.ed.ac.uk/pepa/'>PEPA</a> [<a class='wikilink' href='../Main/References.html#Hil96'>Hil96</a>].
</p><hr />
<h1>PRISM Model Files</h1>
<p>Files containing model descriptions written in the PRISM language
can contain any amount of white space (spaces, tabs, new lines, etc.),
all of which is ignored when the file is parsed by the tool.
Comments can also be used included in files in the style of the C programming language,
by preceding them with the characters <code>//</code>.
This is illustrated by the PRISM language examples from earlier in this section.
</p>
<p class='vspace'>By convention, the file extensions used for PRISM model files vary according to the model type:
</p>
<div class='vspace'></div><ul><li><code>.nm</code> (for MDPs or PTAs)
</li><li><code>.pm</code> (for DTMCs)
</li><li><code>.sm</code> (for CTMCs)
</li></ul><p class='vspace'>but, since new models are added over time, we now recommend that you use:
</p>
<div class='vspace'></div><ul><li><code>.prism</code> (for any model type)
</li></ul><div class='vspace'></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='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='selflink' href='AllOnOnePage.html'>View all</a> ]
</p>
</div> <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->
</body>
</html>
|