SYNOPSIS
LTSmin syntax for Simple Predicate Language formulae
DESCRIPTION
| Priority | Operator | Meaning |
|---|---|---|
0 |
true |
constant true |
0 |
false |
constant false |
0 |
maybe |
constant maybe |
1 |
* / % |
multiplication, division and remainder |
2 |
+ - |
addition, subtraction |
3 |
< <= > >= |
less than, less than or equal, greater than, greater than or equal |
4 |
== |
test operator (state variable name==number) |
4 |
?? |
enabledness operator (edge variable name ?? chunk) |
5 |
! |
Logical negation |
6 |
&& |
Logical and |
7 |
|| |
Logical or |
8 |
<-> |
Logical equivalence |
9 |
-> |
Logical implication |
EXAMPLE
init_0\.x == 4 && (user_1\.a\[3\] == 1 -> register_2\.y == 2)(Note the dot (.) and square braces ([ and ]) need to be escaped, as these symbols are used as keywords in the CTL and mu-calculus languages)
This predicate example could be used in the prom frontends, to search for states where either x is not equal to 4 in (instance 0) the init proctype, or the element three of array a in (instance 1 of) proctype user is non-zero, while y in (instance 2 of) proctype register is zero.
For variable naming consult the --labels option in the PINS tools.