Blame view
prism-4.3-linux64/doc/manual/PropertySpecification/AllOnOnePage.html
97.7 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 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>
PRISM Manual | PropertySpecification / AllOnOnePage
</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'>Property Specification</span></h1>
<hr />
<h1>Introduction</h1>
<p>In order to analyse a probabilistic model which has been specified and constructed in PRISM,
it is necessary to identify one or more <em>properties</em> of the model
which can be evaluated by the tool.
PRISM's <em>property specification language</em> subsumes several well-known probabilistic temporal logics, including PCTL, CSL, probabilistic LTL and PCTL*.
PCTL is used for specifying properties of DTMCs, MDPs or PTAs;
CSL is an extension of PCTL for CTMCs;
LTL and PCTL* can be used to specify properties of
DTMCs and MDPs (or untimed properties of CTMCs).
PRISM also supports most of the (non-probabilistic) temporal logic CTL.
</p>
<p class='vspace'>In fact, PRISM also supports numerous additional customisations and extensions of these two logics.
Full details of the property specifications permitted in PRISM are provided in the following sections. The presentation given here is relatively informal. For the precise syntax and semantics of the various logics, see [<a class='wikilink' href='../Main/References.html#HJ94'>HJ94</a>],[<a class='wikilink' href='../Main/References.html#BdA95'>BdA95</a>] for PCTL, [<a class='wikilink' href='../Main/References.html#ASSB96'>ASSB96</a>],[<a class='wikilink' href='../Main/References.html#BKH99'>BKH99</a>] for CSL and, for example, [<a class='wikilink' href='../Main/References.html#Bai98'>Bai98</a>] for LTL and PCTL*. You can also find various pointers to useful papers in the <a class='urllink' href='http://www.prismmodelchecker.org/about.php'>About</a> and <a class='urllink' href='http://www.prismmodelchecker.org/doc/'>Documentation</a> sections of the PRISM website.
</p>
<p class='vspace'>Before discussing property specifications in more detail,
it is perhaps instructive to first illustrate some typical examples of properties which PRISM can handle.
The following are a selection of such properties.
In each case, we give both the PRISM syntax and a natural language translation:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">terminate</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=1' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p>"the algorithm eventually terminates successfully with probability 1"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
<div class='sourceblocktext'><div class="prism">"<span class="prismkeyword">P</span><<span class="prismnum">0.1</span> [ <span class="prismkeyword">F</span><=<span class="prismnum">100</span> <span class="prismident">num_errors</span> > <span class="prismnum">5</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=2' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p>"the probability that more than 5 errors occur within the first 100 time units is less than 0.1"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span><<span class="prismnum">0.01</span> [ <span class="prismident">num_sensors</span> < <span class="prismident">min_sensors</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=3' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p>"in the long-run, the probability that an inadequate number of sensors are operational is less than 0.01"
</p>
<p class='vspace'>Note that the above properties are all assertions,
i.e. ones to which we would expect a "yes" or "no" answer.
This is because all references to probabilities are associated with an upper or lower bound
which can be checked to be either true or false.
In PRISM, we can also directly specify properties which evaluate to a numerical value, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ !<span class="prismident">proc2_terminate</span> <span class="prismkeyword">U</span> <span class="prismident">proc1_terminate</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=4' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p>"the probability that process 1 terminates before process 2 does"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">Pmax</span>=? [ <span class="prismkeyword">F</span><=<span class="prismident">T</span> <span class="prismident">messages_lost</span> > <span class="prismnum">10</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=5' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p>"the maximum probability that more than 10 messages have been lost by time <code>T</code>" (for an MDP/PTA)
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock6'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span>=? [ <span class="prismident">queue_size</span> / <span class="prismident">max_size</span> > <span class="prismnum">0.75</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=6' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p>"the long-run probability that the queue is more than 75% full"
</p>
<p class='vspace'>Furthermore, PRISM makes it easy to combine such properties into more complex expressions,
compute their values for a range of parameters
and plot graphs of the results using <a class='wikilink' href='../RunningPRISM/Experiments.html'>experiments</a>.
This is often a very useful way of identifying interesting
patterns or trends in the behaviour of a system.
See 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> for many examples of this kind of analysis.
</p><hr />
<h1>Identifying A Set Of States</h1>
<p>One of the most fundamental tasks when specifying properties of a model
is to identify particular sets or classes of states of the model.
For example, to verify a property such as
"the algorithm eventually terminates successfully with probability 1",
it is first necessary to identify the states of the model
which correspond to situations where "the algorithm has terminated successfully".
In terms of the way temporal logics are usually presented,
these correspond to <em>atomic propositions</em>.
</p>
<p class='vspace'>In PRISM, this is achieved simply by writing an <a class='wikilink' href='../ThePRISMLanguage/Expressions.html'>expression</a> in the PRISM language which evaluates to a Boolean value. This expression will typically contain references to variables (and constants) from the model to which it relates. The set of states corresponding to this expression is those for which it evaluates to <code>true</code>. We say that the expression is "satisfied" in these states.
</p>
<p class='vspace'>For example, in the property given above:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock7'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span><<span class="prismnum">0.1</span> [ <span class="prismkeyword">F</span><=<span class="prismnum">100</span> <span class="prismident">num_errors</span> > <span class="prismnum">5</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=7' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>the expression <code>num_errors > 5</code> is used to identify states of the model where more than 5 errors have occurred.
</p>
<p class='vspace'>It is also common to use <a class='wikilink' href='../ThePRISMLanguage/FormulasAndLabels.html'>labels</a> to identify states in this way, like <code>"terminate"</code> in the example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock8'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">terminate</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=8' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Properties can refer to <a class='wikilink' href='../ThePRISMLanguage/FormulasAndLabels.html'>labels</a> either from the model to which the property relates, or included in the same <a class='wikilink' href='PropertiesFiles.html'>properties file</a>.
</p><hr />
<h1>The P Operator</h1>
<p>One of the most important operators in the PRISM property specification language is the <code><strong>P</strong></code> operator, which is used to reason about the probability of an event's occurrence. This operator was originally proposed in the logic PCTL but also features in the other logics supported by PRISM, such as CSL. The <code><strong>P</strong></code> operator is applicable to all types of models supported by PRISM.
</p>
<p class='vspace'>Informally, the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock9'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span> <span class="prismident">bound</span> [ <span class="prismident">pathprop</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=9' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>is true in a state <em>s</em> of a model if
"the probability that path property <code>pathprop</code> is satisfied by the paths from state <em>s</em>
meets the bound <code>bound</code>".
A typical example of a bound would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock10'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>><span class="prismnum">0.98</span> [ <span class="prismident">pathprop</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=10' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which means: "the probability that <code>pathprop</code> is satisfied by the paths from state <em>s</em> is greater than 0.98". More precisely, <code>bound</code> can be any of <code>>=p</code>, <code>>p</code>, <code><=p</code> or <code><p</code>,
where <code>p</code> is a PRISM language expression evaluating to a double in the range [0,1].
</p>
<p class='vspace'>The types of path property supported by PRISM and their semantics will be discussed shortly.
</p>
<div class='vspace'></div><h3>Nondeterminism</h3>
<p>For models that can exhibit nondeterministic behaviour (MDPs or PTAs), some additional clarifications are necessary. Whereas for fully probabilistic models such as DTMCs and CTMCs, probability measures over paths are well defined (see e.g. [<a class='wikilink' href='../Main/References.html#KSK76'>KSK76</a>] and [<a class='wikilink' href='../Main/References.html#BKH99'>BKH99</a>], respectively), for nondeterministic models a probability measure can only be feasibly defined once all nondeterminism has been removed.
</p>
<p class='vspace'>Hence, the actual meaning of the property <code>P bound [ pathprop ]</code> in these cases is:
"the probability that <code>pathprop</code> is satisfied by the paths from state <em>s</em>
meets the bound <code>bound</code> <em>for all possible resolutions of nondeterminism</em>".
This means that, properties using the <code><strong>P</strong></code> operator then effectively reason about the
<em>minimum</em> or <em>maximum</em> probability, over all possible resolutions of nondeterminism,
that a certain type of behaviour is observed.
This depends on the bound attached to the <code><strong>P</strong></code> operator:
a lower bound (<code>></code> or <code>>=</code>) relates to minimum probabilities
and an upper bound (<code><</code> or <code><=</code>) to maximum probabilities.
</p>
<div class='vspace'></div><h3>Quantitative properties</h3>
<p>It is also very often useful to take a <em>quantitative</em> approach to probabilistic model checking, computing the actual probability that some behaviour of a model is observed,
rather than just verifying whether or not the probability is above or below a given bound.
Hence, PRISM allows the <code><strong>P</strong></code> operator to take the following form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock11'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=11' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>These properties return a numerical rather than a Boolean value.
The <a class='wikilink' href='TheSOperator.html'>S</a> and <a class='wikilink' href='Reward-basedProperties.html'>R</a> operators, discussed later, can also be used in this way.
</p>
<p class='vspace'>As mentioned above, for nondeterministic models (MDPs or PTAs), either minimum or maximum probability values can be computed. Therefore, in this case, we have two possible types of property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock12'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">Pmin</span>=? [ <span class="prismident">pathprop</span> ]<br/>
<span class="prismkeyword">Pmax</span>=? [ <span class="prismident">pathprop</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=12' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which return the minimum and maximum probabilities, respectively.
</p>
<p class='vspace'>It is also possible to specify to which state the probability returned by a quantitative property refers. This is covered in the later section on <a class='wikilink' href='Filters.html'>filters</a>.
</p>
<div class='vspace'></div><h3>Path properties</h3>
<p>PRISM supports a wide range of path properties that can be used with the <code><strong>P</strong></code> operator.
A path property is a formula that evaluates to either true or false for a single path in a model.
Here, we review some of the simpler properties that feature a single <em>temporal operator</em>,
as used for example in the logics PCTL and CSL. Later, we briefly describe how PRISM also supports more complex LTL-style path properties.
</p>
<p class='vspace'>The basic different types of path property that can be used inside the <code><strong>P</strong></code> operator are:
</p>
<div class='vspace'></div><ul><li><code><strong>X</strong></code> : "ne<strong>x</strong>t"
</li><li><code><strong>U</strong></code> : "<strong>u</strong>ntil"
</li><li><code><strong>F</strong></code> : "eventually" (sometimes called "<strong>f</strong>uture")
</li><li><code><strong>G</strong></code> : "always" (sometimes called "<strong>g</strong>lobally")
</li><li><code><strong>W</strong></code> : "<strong>w</strong>eak until"
</li><li><code><strong>R</strong></code> : "<strong>r</strong>elease"
</li></ul><p class='vspace'>In the following sections, we describe each of these <em>temporal operators</em>. We then discuss the (optional) use of time bounds with these operators. Finally, we also discuss LTL-style path properties.
</p>
<div class='vspace'></div><h3>"Next" path properties</h3>
<p>The property <code><strong>X</strong> prop</code> is true for a path if <code>prop</code> is true in its second state,
An example of this type of property, used inside a <code><strong>P</strong></code> operator, is:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock13'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span><<span class="prismnum">0.01</span> [ <span class="prismkeyword">X</span> <span class="prismident">y</span>=<span class="prismnum">1</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=13' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which is true in a state if "the probability of the expression <code>y=1</code> being true in the next state is less than 0.01".
</p>
<div class='vspace'></div><h3>"Until" path properties</h3>
<p>The property <code>prop1 <strong>U</strong> prop2</code> is true for a path if
<code>prop2</code> is true in some state of the path and <code>prop1</code> is true in all preceding states.
A simple example of this would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock14'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>><span class="prismnum">0.5</span> [ <span class="prismident">z</span><<span class="prismnum">2</span> <span class="prismkeyword">U</span> <span class="prismident">z</span>=<span class="prismnum">2</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=14' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which is true in a state if "the probability that <code>z</code> is eventually equal to 2, and that <code>z</code> remains less than 2 up until that point, is greater than 0.5".
</p>
<div class='vspace'></div><h3>"Eventually" path properties</h3>
<p>The property <code><strong>F</strong> prop</code> is true for a path if <code>prop</code> eventually becomes true at some point along the path. The <code><strong>F</strong></code> operator is in fact a special case of the <code><strong>U</strong></code> operator (you will often see <code> <strong>F</strong> prop</code> written as <code><strong>true</strong> <strong>U</strong> prop</code>). A simple example is:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock15'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span><<span class="prismnum">0.1</span> [ <span class="prismkeyword">F</span> <span class="prismident">z</span>><span class="prismnum">2</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=15' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which is true in a state if "the probability that <code>z</code> is eventually greater than 2is less than 0.1".
</p>
<div class='vspace'></div><h3>"Globally" path properties</h3>
<p>Whereas the <code><strong>F</strong></code> operator is used for "reachability" properties, <code><strong>G</strong></code> represents "invariance". The property <code><strong>G</strong> prop</code> is true of a path if <code>prop</code> remains true at all states along the path. Thus, for example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock16'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">0.99</span> [ <span class="prismkeyword">G</span> <span class="prismident">z</span><<span class="prismnum">10</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=16' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>states that, with probability at least 0.99, <code>z</code> never exceeds 10.
</p>
<div class='vspace'></div><h3>"Weak until" and "release" path properties</h3>
<p>Like <code><strong>F</strong></code> and <code><strong>G</strong></code>, the operators <code><strong>W</strong></code> and <code><strong>R</strong></code> are derivable from other temporal operators.
</p>
<p class='vspace'>Weak until (<code>a <strong>W</strong> b</code>), which is equivalent to <code>(a <strong>U</strong> b) | <strong>G</strong> a</code>, requires that <code>a</code> remains true until <code>b</code> becomes true, but does not require that <code>b</code> ever does becomes true (i.e. <code>a</code> remains true forever). For example, a weak form of the until example used above is:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock17'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>><span class="prismnum">0.5</span> [ <span class="prismident">z</span><<span class="prismnum">2</span> <span class="prismkeyword">U</span> <span class="prismident">z</span>=<span class="prismnum">2</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=17' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which states that, with probability greater than 0.5, either <code>z</code> is always less than 2, or it is less than 2 until the point where <code>z</code> is 2.
</p>
<p class='vspace'>Release (<code>a <strong>R</strong> b</code>), which is equivalent to <code>!(!a U !b)</code>, informally means that <code>b</code> is true until <code>a</code> becomes true, or <code>b</code> is true forever.
</p>
<p class='vspace'><a name='bounded' id='bounded'></a>
</p><h3>"Bounded" variants of path properties</h3>
<p>All of the temporal operators given above, with the exception of <code><strong>X</strong></code>, have "bounded" variants, where an additional time bound is imposed on the property being satisfied.
The most common case is to use an upper time bound, i.e. of the form "<code><=t</code>" or "<code><t</code>", where <code>t</code> is a PRISM expression evaluating to a constant, non-negative value.
</p>
<p class='vspace'>For example, a bounded until property <code>prop1 <strong>U</strong><=t prop2</code>, is satisfied along a path if <code>prop2</code> becomes true within <code>t</code> steps and <code>prop1</code> is true in all states before that point.
A typical example of this would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock18'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">0.98</span> [ <span class="prismident">y</span><<span class="prismnum">4</span> <span class="prismkeyword">U</span><=<span class="prismnum">7</span> <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=18' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which is true in a state if "the probability of <code>y</code> first exceeding 3 within 7 time units is greater than or equal to 0.98". Similarly:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock19'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">0.98</span> [ <span class="prismkeyword">F</span><=<span class="prismnum">7</span> <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=19' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>is true in a state if "the probability of <code>y</code> being equal to 4 within 7 time units is greater than or equal to 0.98" and:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock20'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">0.98</span> [ <span class="prismkeyword">G</span><=<span class="prismnum">7</span> <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=20' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>is true if the probability of <code>y</code> staying equal to 4 for 7 time units is at least 0.98.
</p>
<p class='vspace'>The time bound can be an arbitrary (constant) expression,
but note that you may need to bracket it,
as in the following example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock21'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">0.98</span> [ <span class="prismkeyword">G</span><=(<span class="prismnum">2</span>*<span class="prismident">k</span>+<span class="prismnum">1</span>) <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=21' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>You can also use lower time-bounds (i.e. <code>>=t</code> or <code>>t</code>) and time intervals <code>[t1,t2]</code>, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock22'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">0.98</span> [ <span class="prismkeyword">F</span>>=<span class="prismnum">10</span> <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
<span class="prismkeyword">P</span>>=<span class="prismnum">0.98</span> [ <span class="prismkeyword">F</span>[<span class="prismnum">10</span>,<span class="prismnum">20</span>] <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=22' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which refer to the probability of <code>y</code> becoming equal to 4 after 10 or more time units, and after between 10 and 20 time-units respectively.
</p>
<p class='vspace'>For CTMCs, the time bounds can be any (non-negative) numerical values - they are not restricted to integers, as for DTMCs and MDPs.
For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock23'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">0.25</span> [ <span class="prismident">y</span><=<span class="prismnum">1</span> <span class="prismkeyword">U</span><=<span class="prismnum">6.5</span> <span class="prismident">y</span>><span class="prismnum">1</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=23' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>means that the probability of <code>y</code> being greater than 1 within 6.5 time-units (and remaining less than or equal to 1 at all preceding time-points) is at least 0.25.
</p>
<div class='vspace'></div><h3>Transient probabilities</h3>
<p>We can also use the bounded <code><strong>F</strong></code> operator to refer to a single time instant, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock24'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>[<span class="prismnum">10</span>,<span class="prismnum">10</span>] <span class="prismident">y</span>=<span class="prismnum">6</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=24' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>or, equivalently:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock25'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>=<span class="prismnum">10</span> <span class="prismident">y</span>=<span class="prismnum">6</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=25' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>both of which give the probability of <code>y</code> being 6 at time instant 10.
</p>
<p class='vspace'><a name='ltl' id='ltl'></a>
</p><h3>LTL-style path properties</h3>
<p>PRISM also supports probabilistic model checking of the temporal logic LTL (and, in fact, PCTL*). LTL provides a richer set of path properties for use with the <code><strong>P</strong></code> operator, by permitting temporal operators to be combined. Here are a few examples of properties expressible using this functionality:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock26'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>><span class="prismnum">0.99</span> [ <span class="prismkeyword">F</span> ( "<span class="prismident">request</span>" & (<span class="prismkeyword">X</span> "<span class="prismident">ack</span>") ) ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=26' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>"with probability greater than 0.99, a request is eventually received, followed immediately by an acknowledgement"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock27'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>>=<span class="prismnum">1</span> [ <span class="prismkeyword">G</span> <span class="prismkeyword">F</span> "<span class="prismident">send</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=27' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>"a message is sent infinitely often with probability 1"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock28'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismkeyword">G</span> ("<span class="prismident">error</span>" & !"<span class="prismident">repair</span>") ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=28' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>"the probability of an error occurring that is never repaired”
</p>
<p class='vspace'>Note that logical operators have precedence over temporal ones, so you will often need to include parentheses when using logical operators, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock29'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ (<span class="prismkeyword">F</span> "<span class="prismident">error1</span>") & (<span class="prismkeyword">F</span> "<span class="prismident">error2</span>") ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=29' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>For temporal operators, unary operators (such as <code><strong>F</strong></code>, <code><strong>G</strong></code> and <code><strong>X</strong></code>) have precedence over binary ones (such as <code><strong>U</strong></code>). Unary operators can be nested, without parentheses, but binary ones cannot.
</p>
<p class='vspace'>So, these are allowed:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock30'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismkeyword">X</span> <span class="prismkeyword">X</span> <span class="prismkeyword">X</span> "<span class="prismident">a</span>" ]<br/>
<span class="prismkeyword">P</span>=? [ "<span class="prismident">a</span>" <span class="prismkeyword">U</span> <span class="prismkeyword">X</span> <span class="prismkeyword">X</span> <span class="prismkeyword">X</span> "<span class="prismident">error</span>" ]<br/>
<span class="prismkeyword">P</span>=? [ ("<span class="prismident">a</span>" <span class="prismkeyword">U</span> "<span class="prismident">b</span>") <span class="prismkeyword">U</span> "<span class="prismident">c</span>" "<span class="prismident">error</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=30' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>but this is not:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock31'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ "<span class="prismident">a</span>" <span class="prismkeyword">U</span> "<span class="prismident">b</span>" <span class="prismkeyword">U</span> "<span class="prismident">c</span>" "<span class="prismident">error</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=31' type='text/plain'>[$[Get Code]]</a></div>
</div>
<hr />
<h1>The S Operator</h1>
<p>The <code><strong>S</strong></code> operator is used to reason about the <em>steady-state</em> behaviour of a model,
i.e. its behaviour in the <em>long-run</em> or <em>equilibrium</em>.
Although this could in principle relate to all three model types,
PRISM currently only provides support for DTMCs and CTMCs.
The definition of steady-state (long-run) probabilities for finite DTMCS and CTMCs is well defined (see e.g. [<a class='wikilink' href='../Main/References.html#Ste94'>Ste94</a>]).
Informally, the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock32'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span> <span class="prismident">bound</span> [ <span class="prismident">prop</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=32' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>is true in a state <em>s</em> of a DTMC or CTMC if
"starting from <em>s</em>, the steady-state (long-run) probability of being in a state which satisfies the (Boolean-valued) PRISM property <code>prop</code>, meets the bound <code>bound</code>".
A typical example of this type of property would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock33'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span><<span class="prismnum">0.05</span> [ <span class="prismident">queue_size</span> / <span class="prismident">max_size</span> > <span class="prismnum">0.75</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=33' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which means: "the long-run probability of the queue being more than 75% full is less than 0.05".
</p>
<p class='vspace'>Like the <code><strong>P</strong></code> <a class='wikilink' href='ThePOperator.html'>operator</a>, the <code><strong>S</strong></code> operator can be used in a <em>quantitative</em> form, which returns the actual probability value, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock34'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span>=? [ <span class="prismident">queue_size</span> / <span class="prismident">max_size</span> > <span class="prismnum">0.75</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=34' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>and can be further customised with the use of <a class='wikilink' href='Filters.html'>filters</a>.
</p><hr />
<h1>Reward-based Properties</h1>
<p>PRISM models can be augmented with information about <a class='wikilink' href='../ThePRISMLanguage/CostsAndRewards.html'>rewards</a> (or, equivalently, costs).
The tool can analyse properties which relate to the <em>expected values</em> of these rewards.
This is achieved using the <code><strong>R</strong></code> operator, which works in a similar fashion to the
<code><strong>P</strong></code> and <code><strong>S</strong></code> operators, and can be used either in a Boolean-valued query, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock35'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span> <span class="prismident">bound</span> [ <span class="prismident">rewardprop</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=35' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>where <code>bound</code> takes the form <code><r</code>, <code><=r</code>, <code>>r</code> or <code>>=r</code> for an expression <code>r</code> evaluating to a non-negative double,
or a real-valued query, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock36'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span> <span class="prismident">query</span> [ <span class="prismident">rewardprop</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=36' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>where <code>query</code> is <code>=?</code>, <code>min=?</code> or <code>max=?</code>.
In the latter case, <a class='wikilink' href='Filters.html'>filters</a> can be used, as for the <code><strong>P</strong></code> and <code><strong>S</strong></code> operators.
</p>
<p class='vspace'>Informally, "<code><strong>R</strong> bound [ rewardprop ]</code>" is true in a state of a model if
"the expected reward associated with <code>rewardprop</code> of the model when starting from that state''
meets the bound <code>bound</code> and "<code><strong>R</strong> query [ rewardprop ]</code>" returns the actual expected reward value.
</p>
<p class='vspace'>There are various different types of reward properties:
</p>
<div class='vspace'></div><ul><li>"reachability reward": <code><strong>F</strong> prop</code>
</li><li>"cumulative reward" : <code><strong>C</strong><=t</code>
</li><li>"total reward" : <code><strong>C</strong></code>
</li><li>"instantaneous reward" : <code><strong>I</strong>=t</code>
</li><li>"steady-state reward" : <code><strong>S</strong></code>.
</li></ul><p class='vspace'>Below, we consider each of these cases in turn.
The descriptions here are kept relatively informal.
Precise definitions for most of these can be found in, for example,
[<a class='wikilink' href='../Main/References.html#KNP07a'>KNP07a</a>] (for DTMCs and CTMCs) or [<a class='wikilink' href='../Main/References.html#FKNP11'>FKNP11</a>] (for MDPs).
</p>
<div class='vspace'></div><h3>"Reachability reward" properties</h3>
<p>"Reachability reward" properties associate a reward with each path of a model.
More specifically, they refer to the reward accumulated along a path until a certain point is reached.
The manner in which rewards are accumulated depends on the model type.
For DTMCs and MDPs, the total reward for a path is the sum of the state rewards for each state along the path
plus the sum of the transition rewards for each transition between these states.
The situation for CTMCs is similar, except that the state reward assigned to each state
of the model is interpreted as the <em>rate</em> at which rewards are accumulated in that state,
i.e. if <em>t</em> time units are spent in a state with state reward <em>r</em>,
the reward accumulated in that state is <em>r</em> x <em>t</em>.
Hence, the total reward for a path in a CTMC is the sum of these products for each state along the path
plus the sum of the transition rewards for each transition between these states.
</p>
<p class='vspace'>The reward property "<code>F prop</code>" corresponds to the reward cumulated along a path
until a state satisfying property <code>prop</code> is reached,
where rewards are cumulated as described above.
State rewards for the <code>prop</code>-satisfying state reached are not included in the cumulated value.
In the case where the probability of reaching a state satisfying <code>prop</code> is less than 1, the reward is equal to infinity.
</p>
<p class='vspace'>A common application of this type of property is the case when the rewards associated with the model correspond to time.
One can then state, for example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock37'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span><=<span class="prismnum">9.5</span> [ <span class="prismkeyword">F</span> <span class="prismident">z</span>=<span class="prismnum">2</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=37' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which is true in a state <em>s</em> if "the expected time taken to reach, from <em>s</em>, a state where <code>z</code> equals 2 is less than or equal to 9.5".
</p>
<div class='vspace'></div><h3>"Cumulative reward" properties</h3>
<p>"Cumulative reward" properties also associate a reward with each path of a model,
but only up to a given time bound.
The property <code>C<=t</code> corresponds to the reward cumulated along a path
until <code>t</code> time units have elapsed.
For DTMCs and MDPs, the bound <code>t</code> must evaluate to an integer;
for CTMCs, it can evaluate to double.
State and transition rewards along a path are cumulated exactly as described in the previous section.
</p>
<p class='vspace'>A typical application of this type of property is the following.
Consider a model of a disk-drive controller which includes a queue of incoming disk requests.
If we assign a reward of 1 to each transition of the model
corresponding to the situation where an incoming request is lost because the queue is full,
then the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock38'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>=? [ <span class="prismkeyword">C</span><=<span class="prismnum">15.5</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=38' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>would return, for a given state of the model,
"the expected number of lost requests within 15.5 time units of operation".
</p>
<p class='vspace'><a name='total' id='total'></a>
</p><h3>"Total reward" properties</h3>
<p>"Total reward" properties refer to the accumulation of state and transition rewards
in the same way as for "reachability reward" and "cumulative reward" properties,
but the rewards is accumulated indefinitely,
i.e. the total reward accumulated along the whole (infinite) path.
Note that this means that, unless a path ends up remaining forever in states with zero reward,
the total reward will be infinite.
</p>
<p class='vspace'>Re-using the reward structure in the previous example,
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock39'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>=? [ <span class="prismkeyword">C</span><=<span class="prismnum">15.5</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=39' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>returns "the expected total number of lost requests".
</p>
<div class='vspace'></div><h3>"Instantaneous reward" properties</h3>
<p>"Instantaneous reward" properties refer to the reward of a model at a particular instant in time.
The reward property <code>I=t</code> associates with a path the reward in the state
of that path when exactly <code>t</code> time units have elapsed.
For DTMCs and MDPs, the bound <code>t</code> must evaluate to an integer;
for CTMCs, it can evaluate to double.
</p>
<p class='vspace'>Returning to our example from the previous section of a model for a disk-request queue in a disk-drive controller,
consider the case where the rewards assigned to each state of the model give the current size of the queue in that state.
Then, the following property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock40'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span><<span class="prismnum">4.4</span> [ <span class="prismkeyword">I</span>=<span class="prismnum">100</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=40' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>would be true in a state <em>s</em> of the model if
"starting from <em>s</em>, the expected queue size exactly 100 time units later is less than 4.4".
Note that, for this type of reward property, state rewards for CTMCs do not have to refer to rates;
they can refer to any instantaneous measure of interest for a state.
</p>
<div class='vspace'></div><h3>"Steady-state reward" properties</h3>
<p>Unlike the previous three types of property,
"steady-state reward" properties relate not to paths, but rather to the reward in the long-run.
A typical application of this type of property would be, in the case where
the rewards associated with the model correspond to power consumption, the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock41'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span><=<span class="prismnum">0.7</span> [ <span class="prismkeyword">S</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=41' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which is true in a state <em>s</em> if "starting from <em>s</em>, the long-run average power consumption is less than 0.7".
</p>
<div class='vspace'></div><h3>Which reward structure?</h3>
<p>In the case where a PRISM model has multiple <a class='wikilink' href='../ThePRISMLanguage/CostsAndRewards.html'>reward structures</a> you may need to specify which reward structure your property refers to. This is done by placing the information in braces (<code>{}</code>) after the <code>R</code> operator. You can do so either using the name assigned to a reward structure (if any) or using the index (where <code>1</code> means the first rewards structure in the PRISM model file, <code>2</code> the second, etc.). Examples are:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock42'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>{"<span class="prismident">num_failures</span>"}=? [ <span class="prismkeyword">C</span><=<span class="prismnum">10.0</span> ]<br/>
<span class="prismkeyword">R</span>{"<span class="prismident">time</span>"}=? [ <span class="prismkeyword">F</span> <span class="prismident">step</span>=<span class="prismident">final</span> ]<br/>
<span class="prismkeyword">R</span>{<span class="prismnum">2</span>}=? [ <span class="prismkeyword">F</span> <span class="prismident">step</span>=<span class="prismident">final</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=42' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Note that when using an index to specify the reward structure, you can actually put any expression that evaluates to an integer. This allows you to, for example, write a property of the form <code>R{c}=?[...]</code> where <code>c</code> is an undefined integer constant. You can then vary the value of <code>c</code> in an experiment and compute values for several different reward structures at once.
</p>
<p class='vspace'>If you don't specify a reward structure to the <code>R</code> operator, by default, the first one in the model file is used.
</p>
<div class='vspace'></div><h3>Availability</h3>
<p>There are currently a few restrictions on the model checking <a class='wikilink' href='../ConfiguringPRISM/ComputationEngines.html'>engines</a> that can be used for some reward properties. The following table summarises the currently availability, where S, M and H denote the "sparse", "MTBDD", "hybrid" and "explicit" engines, respectively, for DTMCs, CTMCs and MDPs. For PTAs, support for rewards is currently quite restrictive; see the later section on "<a class='wikilink' href='PTAProperties.html'>PTA properties</a>" for details.
</p>
<div class='vspace'></div>
<table border='1' cellpadding='5' ><tr ><td > </td><td align='center'><code><strong>F</strong></code></td><td align='center'><code><strong>C</strong><=t</code></td><td align='center'><code><strong>C</strong></code></td><td align='left'><code><strong>I</strong>=t</code></td><td align='right'><code><strong>S</strong></code></td></tr>
<tr ><td align='center'><strong>DTMCs</strong></td><td align='center'>SMHE</td><td align='center'>SMHE</td><td align='center'>SMHE</td><td align='center'>SMHE</td><td align='right'>SMH-</td></tr>
<tr ><td align='center'><strong>CTMCs</strong></td><td align='center'>SMHE</td><td align='center'>SMHE</td><td align='center'>----</td><td align='center'>SMHE</td><td align='right'>SMH-</td></tr>
<tr ><td align='center'><strong>MDPs</strong></td><td align='center'>SM-E</td><td align='center'>S--E</td><td align='center'>----</td><td align='center'>SM--</td><td align='right'>----</td></tr>
</table><hr />
<h1>Non-Probabilistic Properties</h1>
<p>PRISM also supports most operators from the temporal logic CTL [<a class='wikilink' href='../Main/References.html#CE81'>CE81</a>], of which the probabilistic logics PCTL and CSL are an extension. CTL uses the <code><strong>A</strong></code> (for all) and <code><strong>E</strong></code> (there exists) operators, instead of the probabilistic <code><strong>P</strong></code> operator, to ask whether all (or some) paths from a state satisfy a particular path formula.
</p>
<p class='vspace'>For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock43'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">E</span> [ <span class="prismkeyword">F</span> "<span class="prismident">goal</span>" ]<br/>
<span class="prismkeyword">A</span> [ <span class="prismkeyword">F</span> "<span class="prismident">goal</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=43' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>mean "there exists a path that reaches a state labelled with <code>goal</code>"
and "all paths reach a state labelled with <code>goal</code>", respectively.
</p>
<p class='vspace'>Similarly:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock44'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">E</span> [ <span class="prismkeyword">G</span> "<span class="prismident">inv</span>" ]<br/>
<span class="prismkeyword">A</span> [ <span class="prismkeyword">G</span> "<span class="prismident">inv</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=44' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>state that some path (or all paths) satisfy <code><strong>G</strong> "inv"</code>, meaning that label <code>"inv"</code> holds in every state along the path.
</p>
<div class='vspace'></div><h3>Counterexamples and Witnesses</h3>
<p>If you check a property of the form <code>A [ G "inv" ]</code> and it is false, PRISM will generate a counterexample in the form of a path that reaches a state where <code>"inv"</code> is not true. This is displayed either in the simulator (from the GUI) or at the command-line. Similarly, if you check <code>E [ F "goal" ]</code> and the result is true, a witness (a path reaching a <code>"goal"</code> state) will be generated.
</p><hr />
<h1>Syntax And Semantics</h1>
<h3>Syntax</h3>
<p>The syntax of the PRISM property specification language subsumes various probabilistic temporal logics, including PCTL, CSL, (probabilistic) LTL, PCTL* and CTL. Informally, the syntax can be summarised as follows: a property can be any valid, well-typed PRISM <a class='wikilink' href='../ThePRISMLanguage/Expressions.html'>expression</a>, which (optionally) also includes the probabilistic operators discussed previously (<code><strong>P</strong></code>, <code><strong>S</strong></code> and <code><strong>R</strong></code>) and the non-probabilistic (CTL) ones <code><strong>A</strong></code> and <code><strong>E</strong></code>). This mean that any of the following operators can be used:
</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><li><code><strong>P</strong></code> (probabilistic operator)
</li><li><code><strong>S</strong></code> (steady-state operator)
</li><li><code><strong>R</strong></code> (reward operator)
</li><li><code><strong>A</strong></code> (for-all operator)
</li><li><code><strong>E</strong></code> (there-exists operator)
</li></ul><p class='vspace'>This allows you to write any property expressible in logics such as PCTL and CSL. For example, CSL allows you to nest <code><strong>P</strong></code> and <code><strong>S</strong></code> operators:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock45'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>><span class="prismnum">2</span> <span class="prismkeyword">S</span>><span class="prismnum">0.9</span>[ <span class="prismident">num_servers</span> >= <span class="prismnum">5</span> ] ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=45' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>"the probability of it taking more than 2 hours to get to a state from which the long-run probability of at least 5 servers being operational is >0.9"
</p>
<p class='vspace'>You can also express various arithmetic expressions such as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock46'>
<div class='sourceblocktext'><div class="prism"><span class="prismnum">1</span> - <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>[<span class="prismnum">3600</span>,<span class="prismnum">7200</span>] <span class="prismident">oper</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=46' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>"the probability that the system is <strong>not</strong> operational at any point during the second hour of operation"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock47'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>{"<span class="prismident">oper</span>"}=? [ <span class="prismkeyword">C</span><=<span class="prismident">t</span> ] / <span class="prismident">t</span><br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=47' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>"the expected fraction of time that the system is available (i.e. the expected interval availability) in the time interval [0, t]"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock48'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">fail_A</span> ] / <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">any_fail</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=48' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>"the (conditional) probability that component A eventually fails, given
that at least one component fails"
</p>
<div class='vspace'></div><h3>Semantics</h3>
<p>We omit a formal presentation of the semantics of the PRISM property language. The semantics of the probabilistic temporal logics that the language incorporates can be found from a variety of sources. See for example the pointers given in the <a class='urllink' href='http://www.prismmodelchecker.org/about.php'>About</a> and <a class='urllink' href='http://www.prismmodelchecker.org/doc/'>Documentation</a> sections of the PRISM website.
</p>
<p class='vspace'>It is worth, however, clarifying a few points specific to PRISM. A property is evaluated with respect to a particular state of a model. Depending on the type of the property, this value may either be a Boolean, an integer or a double. When performing model checking, PRISM usually has to actually compute the value for <em>all</em> states of the model but, for clarity, will by default report just a single value. Typically, this is the value for the (single) initial state of the model. For example, this:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock49'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=49' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>will report the probability, from the initial state of the model, of reaching an "error" state.
This:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock50'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>><span class="prismnum">0.5</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=50' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>will return <code>true</code> if and only if the probability, from the initial state, is greater than 0.5.
</p>
<p class='vspace'><strong>Note:</strong> This is contrast to older versions of PRISM, which treated numerical and Boolean-valued properties differently in this respect.
</p>
<p class='vspace'>For models with <a class='wikilink' href='../ThePRISMLanguage/MultipleInitialStates.html'>multiple initial states</a>, we need to adapt these definitions slightly. In this case, the two properties above will yield, respectively:
</p>
<div class='vspace'></div><ul><li>the range of values (over all initial states) of the probability of reaching "error"
<div class='vspace'></div></li><li><code>true</code> if and only if the probability is greater than 0.5 from <em>all</em> initial states.
</li></ul><p class='vspace'>You can also ask PRISM to return different values using <a class='wikilink' href='Filters.html'>filters</a>,
which are described in the next section.
</p><hr />
<h1>Filters</h1>
<p>As discussed above, when reporting the result of model checking a property, PRISM will by default return the value for the (single) initial state of the model. However, since PRISM in fact usually has to compute values for <em>all</em> states simultaneously, you can customise PRISM properties to obtain different results. This is done using <em>filters</em>.
</p>
<p class='vspace'>Filters are created using the <code>filter</code> keyword. They take the following form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock51'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">op</span>, <span class="prismident">prop</span>, <span class="prismident">states</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=51' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>where <code>op</code> is the filter <em>operator</em> (see below), <code>prop</code> is any PRISM property and <code>states</code> is a Boolean-valued expression identifying a set of states over which to apply the filter.
</p>
<p class='vspace'>In fact, the <code>states</code> argument is optional; if omitted, the filter is applied over all states. So, the following properties are equivalent:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock52'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">op</span>, <span class="prismident">prop</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">op</span>, <span class="prismident">prop</span>, <span class="prismkeyword">true</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=52' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Here's a simple example of a filter:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock53'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismkeyword">max</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], <span class="prismident">x</span>=<span class="prismnum">0</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=53' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>This gives the <em>maximum</em> value, starting from any state satisfying <code>x=0</code>, of the probability of reaching an "error" state.
</p>
<p class='vspace'>Here's another simple example,
which checks whether, <em>starting from any reachable state</em>,
we eventually reach a "done" state with probability 1.
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock54'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>>=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">done</span>" ])<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=54' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>We could modify this property slightly to instead check whether, from any state that satisfies the label "ready", we eventually reach a "done" state with probability 1. This could be done with either of the following two equivalent properties:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock55'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, "<span class="prismident">ready</span>" => <span class="prismkeyword">P</span>>=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">done</span>" ])<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>>=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">done</span>" ], "<span class="prismident">ready</span>")<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=55' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'><strong>Note:</strong> In older versions of PRISM, the property above could be written just as <code>"ready" => P>=1 [ F "done" ]</code> since the result was checked for all states by default, not just the <a class='wikilink' href='SyntaxAndSemantics.html'>initial state</a>. Now, you need to explicitly include a filter, as shown above, to achieve this.
</p>
<div class='vspace'></div><h3>Types of filter</h3>
<p>Most filters of the form <code>filter(op, prop, states)</code>
apply some operator <code>op</code> to the values of property <code>prop</code>
for all the states satisfying <code>states</code>,
resulting in a single value.
The full list of filter operators <code>op</code> in this category is:
</p>
<div class='vspace'></div><ul><li><code>min</code>: the minimum value of <code>prop</code> over states satisfying <code>states</code>
</li><li><code>max</code>: the maximum value of <code>prop</code> over states satisfying <code>states</code>
</li><li><code>count</code>: counts the number of states satisfying <code>states</code> for which <code>prop</code> is true
</li><li><code>sum</code> (or <code>+</code>): sums the value of <code>prop</code> for states satisfying <code>states</code>
</li><li><code>avg</code>: the average value of <code>prop</code> over states satisfying <code>states</code>
</li><li><code>first</code>: the value of <code>prop</code> for the first (lowest-indexed) state satisfying <code>states</code>
</li><li><code>range</code>: the range (interval) of values of <code>prop</code> over states satisfying <code>states</code>
</li><li><code>forall</code> (or <code>&</code>): returns <code>true</code> if <code>prop</code> is <code>true</code> for all states satisfying <code>states</code>
</li><li><code>exists</code> (or <code>|</code>): returns <code>true</code> if <code>prop</code> is <code>true</code> for some states satisfying <code>states</code>
</li><li><code>state</code>: returns the value for the single state satisfying <code>states</code> (if there is more than one, this is an error)
</li></ul><p class='vspace'>There are also a few filters that, rather than returning a single value, return different values for each state, like a normal PRISM property:
</p>
<div class='vspace'></div><ul><li><code>argmin</code>: returns <code>true</code> for the states satisfying <code>states</code> that yield the minimum value of <code>prop</code>
</li><li><code>argmax</code>: returns <code>true</code> for the states satisfying <code>states</code> that yield the maximum value of <code>prop</code>
</li><li><code>print</code>: does not change the result of <code>prop</code> but prints the (non-zero) values to the log
</li><li><code>printall</code>: like <code>print</code>, but displays <em>all</em> values, even for states where the value is zero
</li></ul><div class='vspace'></div><h3>More examples</h3>
<p>Here are some further illustrative examples of properties that use filters.
</p>
<p class='vspace'>Filters provide a quick way to <em>print</em> the results of a model checking query for several states. In most cases, for example, a <code>P=?</code> query just returns the probability from the initial state. To see the probability for all states satisfying <code>x>2</code>, use:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock56'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">print</span>, <span class="prismkeyword">P</span>=? [ ... ], <span class="prismident">x</span>><span class="prismnum">2</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=56' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Values are printed in the log (i.e. to the "Log" tab in the GUI or to the terminal from the command-line). For small models, you could omit the final <code>states</code> argument (<code>x>2</code> here) and view the probabilities from all states. You can also use PRISM's <a class='wikilink' href='../ConfiguringPRISM/OtherOptions.html'>verbose</a> mode to view values for all states, but filters provide an easier and more flexible solution.
<code>print</code> filters do not actually alter the result returned so, in the example above, PRISM will still return the probability for the initial state, in addition to printing other probabilities in the log.
</p>
<p class='vspace'>You can also use <code>print</code> filters to display lists of states. For example, this property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock57'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">print</span>, <span class="prismkeyword">filter</span>(<span class="prismident">argmax</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]))<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=57' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>prints the states which have the highest probability of reaching an error state.
However, you should exercise caution when using <code>argmax</code> (or <code>argmin</code>) on properties such as <code>P=? [ ... ]</code> (or <code>S=? [ ... ]</code> or <code>R=? [ ... ]</code>), whose results are only approximate due to the nature of the methods used to compute them (or because of round-off errors.)
</p>
<p class='vspace'>Another common use of filters is to display the value for a particular state of the model (rather than the initial state, which is used by default). To achieve this, use e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock58'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">state</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], <span class="prismident">x</span>=<span class="prismnum">2</span>&<span class="prismident">y</span>=<span class="prismnum">3</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=58' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>where <code>x=2&y=3</code> is assumed to specify one particular state.
A <code>state</code> filter will produce an error if the filter expression is not satisfied by exactly one state of the model.
</p>
<p class='vspace'>Filters can also be built up into more complex expressions. For example, the following two properties are equivalent:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock59'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">avg</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>")<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">sum</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>") / <span class="prismkeyword">filter</span>(<span class="prismident">count</span>, "<span class="prismkeyword">init</span>")<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=59' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>The <code>range</code> filter, unlike most PRISM expressions which are of type Boolean, integer or double, actually returns an interval: a pair of integers or doubles. For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock60'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">range</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">count</span>=<span class="prismnum">10</span> ], <span class="prismident">count</span>=<span class="prismnum">0</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=60' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>gives the range of all possible values for the probability of reach a state satisfying <code>count=10</code>, from all states satisfying <code>count=0</code>.
As will be described below, this kind of property also results from the use of old-style (<code>{...}</code>) filters and properties on models with multiple initial states.
</p>
<div class='vspace'></div><h3>Old-style filters</h3>
<p>In older versions of PRISM, filters were also available, but in a less expressive form. Previously, they were only usable on <code><strong>P</strong></code>, <code><strong>S</strong></code> or <code><strong>R</strong></code> properties and only a small set of filter operators were permitted. They were also specified in a different way, using braces (<code>{</code>...<code>}</code>). For compatibility with old properties files (and for compactness), these forms of filters are still allowed. These old-style forms of filters:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock61'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> {<span class="prismident">states</span>} ]<br/>
<span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> {<span class="prismident">states</span>}{<span class="prismkeyword">min</span>} ]<br/>
<span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> {<span class="prismident">states</span>}{<span class="prismkeyword">max</span>} ]<br/>
<span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> {<span class="prismident">states</span>}{<span class="prismkeyword">min</span>}{<span class="prismkeyword">max</span>} ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=61' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>are equivalent to:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock62'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">state</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismkeyword">min</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismkeyword">max</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">range</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=62' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Notice that the first of the four properties above (i.e. an old-style filter of the form <code>{states}</code> will result in an error if <code>states</code> is not satisfied by exactly one state of the model. Older versions of PRISM just gave you the value for the first state state satisfying the filter, without warning you about this. If you want to recreate the old behaviour, just use a <code>first</code> filter:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock63'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">first</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=63' type='text/plain'>[$[Get Code]]</a></div>
</div>
<div class='vspace'></div><h3>Default filters</h3>
<p>Finally, for completeness, we show what the <em>default</em> filters are in PRISM,
i.e. how the way that PRISM returns values from properties by default
could have been achieved equivalently using filters.
</p>
<p class='vspace'>Queries of the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock64'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>><span class="prismnum">0.5</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=64' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>are the same as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock65'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>><span class="prismnum">0.5</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>")<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=65' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>and queries of the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock66'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=66' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>are the same as either:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock67'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">state</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>")<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">range</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>")<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=67' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>for the cases where there the model has a single initial state
or multiple initial states, respectively.
</p><hr />
<h1>PTA Properties</h1>
<p>The classes of property that can be checked for PTAs are currently more restricted than for the other kinds of models that PRISM supports. This is because the model checking procedures are quite different for this type of model. We describe these restrictions here. The situation is also dependent on which of the PTA model checking <a class='wikilink' href='../ConfiguringPRISM/ComputationEngines.html#pta'>engines</a> is being used.
</p>
<p class='vspace'>For the "<strong>stochastic games</strong>" engine, we essentially only allow unbounded or time-bounded probabilistic reachability properties, i.e. properties of the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock68'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">Pmin</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
<span class="prismkeyword">Pmax</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
<span class="prismkeyword">Pmin</span>=? [ <span class="prismkeyword">F</span><=<span class="prismident">T</span> <span class="prismident">target</span> ]<br/>
<span class="prismkeyword">Pmax</span>=? [ <span class="prismkeyword">F</span><=<span class="prismident">T</span> <span class="prismident">target</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=68' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>where <code>target</code> is a Boolean-valued expression that does not include references to any clock variables and <code>T</code> is an integer-valued expression. The <code><strong>P</strong></code> operator cannot be nested and the <code><strong>S</strong></code> and <code><strong>R</strong></code> operators are not supported.
</p>
<p class='vspace'>The "<strong>backwards reachability</strong>" engine is similar but currently only handles maximum probabilities.
</p>
<p class='vspace'>For the "<strong>digital clocks</strong>" engine, there is slightly more flexibility,
e.g. until (<code><strong>U</strong></code>) properties are allowed, as are clock variables in expressions and arithmetic expressions such as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock69'>
<div class='sourceblocktext'><div class="prism"><span class="prismnum">1</span> - <span class="prismkeyword">Pmin</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=69' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>This engine, however, does not yet support time-bounded reachability properties and, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons
(e.g. <code>x<=5</code> is allowed, <code>x<5</code> is not).
</p>
<p class='vspace'>The digital clocks also has support for rewards:
it is possible to check reachability reward properties of the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock70'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">Rmin</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
<span class="prismkeyword">Rmax</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=70' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Reward structures specified in the model, though, must not depend on clock variables.
Formally, the class of PTAs with this kind of reward structure is sometime called <em>linearly priced PTAs</em> (see e.g. [<a class='wikilink' href='../Main/References.html#KNPS06'>KNPS06</a>].
</p>
<p class='vspace'>The digital clocks method is based on a language-level translation from a PTA model to an MDP one. If you want to see the MDP PRISM model that was generated, add the switch <code>-exportdigital digital.nm</code> when model checking property to export the model file to <code>digital.nm</code>.
</p><hr />
<h1>Properties Files</h1>
<h3>Constants</h3>
<p>Files containing properties to be analysed by PRISM can also contain constants, as is the case for model files.
These are defined in identical fashion, for example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock71'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">const</span> <span class="prismkeyword">int</span> <span class="prismident">k</span> = <span class="prismnum">7</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">T</span> = <span class="prismnum">9.5</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">p</span> = <span class="prismnum">0.01</span>;<br/>
<br/>
<span class="prismkeyword">P</span><<span class="prismident">p</span> [ <span class="prismkeyword">F</span><=<span class="prismident">T</span> <span class="prismident">x</span>=<span class="prismident">k</span> ];<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=71' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>As before, these constants can actually be left undefined and then later
assigned either a single value or a range of values using <a class='wikilink' href='../RunningPRISM/Experiments.html'>experiments</a>.
</p>
<p class='vspace'>In fact, values such as the probability bounds for the <code><strong>P</strong></code> or <code><strong>S</strong></code> operators (like <code><strong>P</strong></code> above)
and upper or lower bounds for the <code><strong>U</strong></code> operator (like <code> T</code> above)
can be arbitrary expressions, provided they are constant.
Furthermore, expressions in the properties file can also refer to constants previous defined in the model file.
</p>
<p class='vspace'><a name='labels' id='labels'></a>
</p><h3>Labels</h3>
<p>Another feature of properties files is <em>labels</em>. These are a way of defining sets of states that will be referred to in properties (they correspond to <em>atomic propositions</em> in a temporal logic setting). As described <a class='wikilink' href='../ThePRISMLanguage/FormulasAndLabels.html'>earlier</a>, labels can be defined in either model files or property files.
</p>
<p class='vspace'>Labels are defined using the keyword <code><strong>label</strong></code>, followed by a name (identifier) in double quotes, and then an expression which evaluates to a Boolean. Definition and usage of labels are illustrated in the following example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock72'>
<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/>
<br/>
<span class="prismkeyword">P</span>>=<span class="prismnum">0.99</span> [ "<span class="prismident">safe</span>" <span class="prismkeyword">U</span> "<span class="prismident">fail</span>" ];<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=72' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Two special cases are the <code>"init"</code> and <code>"deadlock"</code> labels which are always defined.
These are true in initial states of the model and states where deadlocks were found (and, usually, fixed by adding self-loops), respectively.
</p>
<p class='vspace'><a name='names' id='names'></a>
</p><h3>Property names</h3>
<p>For convenience, properties can be annotated with <em>names</em>, as shown in the following example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock73'>
<div class='sourceblocktext'><div class="prism">"<span class="prismident">safe</span>": <span class="prismkeyword">P</span><<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> <span class="prismident">temperature</span> > <span class="prismident">t_max</span> ];<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=73' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>which gives the name <code>"safe"</code> to the property. It is then possible to include named properties as sub-expressions of other properties, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock74'>
<div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismident">num_sensors</span>><span class="prismnum">0</span> => "<span class="prismident">safe</span>");<br/>
</div></div>
<div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&num=74' type='text/plain'>[$[Get Code]]</a></div>
</div>
<p class='vspace'>Notice that the syntax for referring to named properties is identical to the syntax for labels. For this reason, property names must be disjoint from those of any existing labels.
</p>
<p class='vspace'>You can refer to property names when using the command-line switch <a class='wikilink' href='../RunningPRISM/ModelChecking.html#cl'><code>-prop</code></a> to specify which property is to be model checked.
</p>
<div class='vspace'></div><h3>Properties files</h3>
<p>A PRISM properties file can contain any number of properties.
It is good practice, as shown in the examples above, to terminate each property with a semicolon. Currently, this is not enforced by PRISM (to prevent incompatibility with old properties files) but this may change in the future.
</p>
<p class='vspace'>Like model files, properties can also include any amount of white space (spaces, tabs, new lines, etc.) and C-style comments, which are both ignored.
The recommended file extension for PRISM properties is now <code>.props</code>.
Previously, though, the convention was to use extension <code>.pctl</code> for properties of DTMCs, MDPs or PTAs
and extension <code>.csl</code> for properties of CTMCs, so these are still also valid.
</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'>Property Specification</a></strong>
</p><ul><li><a class='wikilink' href='Main.html'>Introduction</a>
</li><li><a class='wikilink' href='IdentifyingASetOfStates.html'>Identifying A Set Of States</a>
</li><li><a class='wikilink' href='ThePOperator.html'>The P Operator</a>
</li><li><a class='wikilink' href='TheSOperator.html'>The S Operator</a>
</li><li><a class='wikilink' href='Reward-basedProperties.html'>Reward-based Properties</a>
</li><li><a class='wikilink' href='Non-probabilisticProperties.html'>Non-probabilistic Properties</a>
</li><li><a class='wikilink' href='SyntaxAndSemantics.html'>Syntax And Semantics</a>
</li><li><a class='wikilink' href='Filters.html'>Filters</a>
</li><li><a class='wikilink' href='PTAProperties.html'>PTA Properties</a>
</li><li><a class='wikilink' href='Multi-objectiveProperties.html'>Multi-objective Properties</a>
</li><li><a class='wikilink' href='PropertiesFiles.html'>Properties 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>
|