"STATE" keyword in TLA?

144 views

Skip to first unread message

ns

unread,

Mar 6, 2023, 6:16:29 PM3/6/23

to tlaplus

Toolbox turns the word "STATE" purple which suggests to me its a keyword, but one with which I'm not familiar. Anyone know what it's for?

Markus Alexander Kuppe

unread,

Mar 6, 2023, 7:04:02 PM3/6/23

to tlaplus

“STATE” is part of the TLA+ proof language: https://lamport.azurewebsites.net/tla/tla2-guide.pdf

Markus

Leslie Lamport

unread,

Mar 6, 2023, 7:16:57 PM3/6/23

to tlaplus

The keyword STATE is not mentioned in that document because I believe it is not recognized by TLAPS. It may be needed to reason about the temporal existential operator \EE, which TLAPS does not yet do, so it is treated as a keyword by the grammar.

Leslie