You can access to a quick pdf summary about the tla+ language here: https://lamport.azurewebsites.net/tla/summary-standalone.pdf.

This is a web accessible version.

• module M :: Begins the module or submodule named M.
• extends M1, ..., Mn :: Incorporates declarations, definitions, assumptions, and theorems from modules M1, ..., Mn.
• constants C1, ..., Cn :: Declares constant parameters (rigid variables).
• variables x1, ..., xn :: Declares flexible variables.
• assume P :: Asserts P as an assumption.
• F(x1, ..., xn) == exp :: Defines operator F.
• f\[x ∈ S] == exp :: Defines function f with domain S.
• instance M with p1 <- e1, ..., pm <- em :: Instantiates module M with substitutions.
• N(x1, ..., xn) == instance M with p1 <- e1, ..., pm <- em :: Parameterized instantiation.
• theorem P :: Asserts that P can be proved.
• local def :: Makes definitions local.
• ==== :: Ends the current module or submodule.

\

Logic

* /, /, \~, =>, <=>, TRUE, FALSE, BOOLEAN * \A x ∈ S : p * \E x ∈ S : p * CHOOSE x ∈ S : p

Sets

* =, #, ∈, /∈, \cup, \cap, ⊆, * {e1, ..., en}, {x ∈ S : p}, {e : x ∈ S}, SUBSET S, UNION S

Functions

* f\[e], DOMAIN f, \[x ∈ S |-> e], \[S -> T], \[f EXCEPT !\[e1] = e2]

Records

* e.h, \[h1 |-> e1, ..., hn |-> en], \[h1: S1, ..., hn: Sn], \[r EXCEPT !.h = e]

Tuples

* e\[i], <\<e1, ..., en>>, S1 \X ... \X Sn

\

* IF p THEN e1 ELSE e2 * CASE p1 -> e1 \[] ... \[] pn -> en * CASE ... \[] OTHER -> e * LET d1 == e1 ... dn == en IN e * Conjunctions: /\ p1 ... /\ pn * Disjunctions: / p1 ... / pn

\

* e' :: Value of e in next state * \[A]\_e :: A / (e' = e) * <A>\_e :: A /\ (e' # e) * ENABLED A :: Step A is possible * UNCHANGED e :: e' = e * A \cdot B :: Composition of actions

\

* \[]F :: Always F * <>F :: Eventually F * WF\_e(A), SF\_e(A) :: Weak/Strong fairness * F \~> G :: F leads to G

\

Common infix operators: +, -, \*, /, ^, .., /, /, <=, >=, < , >, #, =|=, |=, ⊆, ⊂, @@, :>, %.

Postfix operators: ^+, ^\*, ^#

\

Operators have precedence ranges; overlapping ranges mean precedence unspecified. Examples:

* Prefix: \~ (4–4), ENABLED (4–15), UNCHANGED (4–15), \[] (4–15), <> (4–15) * Infix: => (1–1), / (3–3), / (3–3), = (5–5), # (5–5), < (5–5), > (5–5), \cup (8–8), \cap (8–8) * Postfix: ^+, ^\*, ^#, ' (15–15) \===== Operators Defined in Standard Modules ===== Naturals, Integers, Reals * +, -, \*, /, ^, .., \div, %, <=, >=, <, >, Infinity Sequences * \o, Head, Tail, Append, Len, Seq, SelectSeq, SubSeq FiniteSets * IsFiniteSet, Cardinality Bags * ⊕, BagIn, CopiesIn, SubBag, BagOfAll, EmptyBag, BagToSet, IsABag, BagCardinality, BagUnion, SetToBag RealTime * RTBound, RTnow, now TLC * :>, @@, Print, Assert, JavaTime, Permutations, SortSeq \===== ASCII Representation of Typeset Symbols ===== * / or \land * / or \lor * \~ or \lnot * # or /= :: not equal * ∈ :: \in * /∈ :: \notin * << :: \langle * >> :: \rangle * <=, >= :: <= or =<, >= or => * ⊆ :: \subseteq, ⊂ :: \subset * ⊇ :: \supseteq, ⊃ :: \supset * -> :: implication arrow * <- :: reverse arrow * \[] :: always * <> :: eventually * |-> :: maps-to * \div, \cdot, \circ, \bullet * x^y, x^\*, x^+, x^#''

---

This is the TLA+ Summary rewritten in DokuWiki-friendly notation.