Using PRISM – a probabilistic symbolic modelchecker
There are IEEE standards. There are implementations in hard- and software. There are implementations in software meant for simulation – and then there are models built to validate them. I’ll list some peculiarities of the PRISM modelchecker, as I started using it with only Java / C / C++ / php experience. The syntax is sometimes slightly obscure.
Formulas
What most programming languages call ‘functions’ or ‘methods’, is called a ‘formula’ in PRISM.; It can output either Boolean or int / double etc. So the following returns the Boolean:
formula p1 = j2=1 & k2=0;
Whereas this returns the int values:
formula p1 = j2=1 & k2=0 ? 1 : 0;
Notice that the last example uses an inline if-else statement: condition ? return_if_true : return_if_false.
Now why would you need this? Consider the following:
38 // state (0,0) 39 [] (j1=0 & k1=0) -> 1-q : (j1'=0) 40 + q*(1-p1) : (j1'=1) 41 + q*p1/w : (j1'=1) 42 + q*p1/w : (j1'=1) & (k1'=1) ...
We use a formula for p1, but if we were to use it as a Boolean value we’d get into trouble, PRISM cannot accept, for instance, the following:
40 + q & !p1 : (j1'=1)
… so we gate access to j1′ by means of a probability ‘q’ and a switch ‘p1’. When we use the inline if-else switch, we can use the first implementation as given in line 40, and it wil simply multiply by 1 or 0.