Freeminded.org

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.