SYNOPSIS

LTSmin syntax for Simple Predicate Language formulae

DESCRIPTION

Table 1. Language’s operators and priority
Priority Operator Meaning

0

true

constant true

0

false

constant false

1

==

test operator (state variable name==number)

2

!

Logical negation

4

&&

Logical and

5

||

Logical or

6

<->

Logical equivalence

7

->

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.

SEE ALSO