## 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 ( |

4 |
?? |
enabledness operator ( |

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.