SPEC
CTLSPEC
LTLSPEC
PSLSPEC COMPUTE
INVARSPEC
FAIRNESS

JUSTICE
COMPASSION
ISA
ASSIGN
CONSTRAINT
SIMPWFF
CTLWFF

LTLWFF
PSLWFF
COMPWFF
IN
MIN
MAX
process
array
of

boolean
integer
real
word
word1
bool
EX
AX
EF
AF
EG
AG

E
F
O
G
H
X
Y
Z
A
U
S
V
T
BU
EBF
ABF
EBG
ABG
case
esac
mod

next
init
union
in
xor
xnor
self
TRUE
FALSE


;**01l
MODULE

;**02l
DEFINE
CONSTANTS
VAR
IVAR
INIT
TRANS
INVAR

;**03l
ASSIGN
;**04l