Go backward to
Syntax of Simple TLA
Go up to
Top
Go forward to
Additional Notation
Semantics of Simple TLA
s
[[
f
]]
<=>
f
(
forall
'
v
':
s
[[
v
]]/
v
)
s
[[
A
]]
t
<=>
A
(
forall
'
v
':
s
[[
v
]]/
v
,
t
[[
v
]]/
v'
)
<
s
0
,
s
1
, ...>[[
A
]]
<=>
s
0
[[
A
]]
s
1
|=
A
<=>
forall
s,t
in
St
:
s
[[
A
]]
t
s
[[
Enabled
A
]]
<=>
exists
t
in
St
:
s
[[
A
]]
t
<
s
0
,
s
1
, ...>[[
always
F
]]
<=>
forall
n
in
Nat
: <
s
n
,
s
n+1
, ...>[[
F
]]
sigma
[[
F
and
G
]]
<=>
sigma
[[
F
]]
and
sigma
[[
G
]]
sigma
[[
not
F
]]
<=>
not
sigma
[[
F
]]
|=
F
<=>
forall
sigma
in
St
^infinity:
sigma
[[
A
]]
t
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998