To read a TeX/ASCII file in ASCII, ignore everything up to and
including the \begin{spec}. The following abbreviations are used.
(See the LaTeX manual for the meaning of the \... commands.)
Additional abbreviations, used in a particular file, are listed at the
beginning of the file.
:xxx: --> \xxx, for any "xxx".
/\ --> \wedge (logical "and")
\/ --> \vee (logical "or")
~ --> \neg (logical negation)
=> --> \Rightarrow (implication)
:A: --> \forall (upside down "A")
:E: --> \exists (upside down "E")
[] --> \Box (TLA "always")
<> --> \Diamond (TLA "eventually")
~> --> \leadsto (TLA "leads to")
# --> \neq (not equal to)
|= --> \models (logical validity)
|- --> \vdash (logical entailment)
== --> "equals by definition" -- small \Delta on top of "="
-> --> \rightarrow
<- --> \leftarrow
|| --> \| ("parallel")
<< --> similar to \ltlt (much less than)
>> --> similar to \gtgt (much greater than)
[[ --> two close left brackets
]] --> two close right brackets
(+) --> \oplus
(-) --> \ominus
x subscript y is represented by
x_y or x_[y]
x superscript y is represented by
x^y or x^[y]
Backslash's ("\"s) at the beginning of a line are to be ignored.