# 2580 Tlaplus Syntax Cf31ead9 > TLA+ Syntax Reference - Skill: `tools-only/2580-tlaplus-syntax-cf31ead9` (Agent Skill, multi-file: 3 files) - Install (CLI): `npx skillmds@latest add tools-only/2580-tlaplus-syntax-cf31ead9` - Raw SKILL.md: https://api.skillmd.com/api/skills/tools-only/2580-tlaplus-syntax-cf31ead9/raw - Safety review: pending - Works with: Claude Code, Claude.ai, OpenAI Codex - Category: Research & Search - Author: tools-only (https://skillmd.com/u/tools-only) - Updated: 2026-09-22 - Page: https://skillmd.com/skills/tools-only/2580-tlaplus-syntax-cf31ead9 --- # TLA+ Syntax Reference ## Module Structure ```tla ---- MODULE ModuleName ---- EXTENDS StandardModules CONSTANTS ConstantDeclarations VARIABLES VariableDeclarations Definitions ==== ``` ## Standard Modules Common modules to extend: - **Naturals**: Natural numbers (0, 1, 2, ...), operators: +, -, *, /, %, ^, .., \div, \leq, \geq - **Integers**: All integers, includes Naturals - **Reals**: Real numbers - **Sequences**: Sequence operations (Seq, Len, Append, Head, Tail, SubSeq) - **FiniteSets**: Finite set operations (Cardinality, IsFiniteSet) - **TLC**: TLC-specific operators (Print, Assert, JavaTime) ## Variable Declarations ```tla VARIABLES x, y, z \* Group variables for convenience vars == <> ``` ## Constants ```tla CONSTANTS MaxValue, NumProcesses, Data ``` Constants are parameters that remain fixed during execution. ## Operators ### Boolean Operators - `/\` - AND (conjunction) - `\/` - OR (disjunction) - `~` - NOT (negation) - `=>` - Implies - `<=>` - Equivalence (if and only if) ### Comparison Operators - `=` - Equality - `#` or `/=` - Inequality - `<`, `>`, `\leq`, `\geq` - Ordering ### Set Operators - `\in` - Element of - `\notin` - Not element of - `\subseteq` - Subset or equal - `\cup` - Union - `\cap` - Intersection - `\` - Set difference - `SUBSET S` - Set of all subsets of S - `UNION S` - Union of all sets in S ### Set Construction ```tla {1, 2, 3} \* Explicit set {x \in S : P(x)} \* Set filter {e(x) : x \in S} \* Set map ``` ### Sequence Operators ```tla <<1, 2, 3>> \* Sequence literal Len(seq) \* Length seq[i] \* Index (1-based) Append(seq, elem) \* Append element Head(seq) \* First element Tail(seq) \* All but first SubSeq(seq, m, n) \* Subsequence from m to n seq1 \o seq2 \* Concatenation ``` ### Record Operators ```tla [field1 |-> value1, field2 |-> value2] \* Record literal record.field \* Field access [record EXCEPT !.field = newValue] \* Update field ``` ### Function Operators ```tla [x \in S |-> e(x)] \* Function definition f[x] \* Function application DOMAIN f \* Domain of function [f EXCEPT ![x] = newValue] \* Update function ``` ## Temporal Operators ### Action Operators - `[A]_v` - A or variables v unchanged (stuttering) - `<>_v` - A and variables v changed (non-stuttering) - `ENABLED A` - Action A is enabled - `UNCHANGED v` - Variables v remain unchanged - `v'` - Next-state value of v ### Temporal Logic Operators - `[]P` - Always P (globally) - `<>P` - Eventually P (finally) - `P ~> Q` - P leads to Q (P implies eventually Q) - `[][A]_v` - Always A or v unchanged - `WF_v(A)` - Weak fairness of A with respect to v - `SF_v(A)` - Strong fairness of A with respect to v ## Common Patterns ### Initial State Predicate ```tla Init == /\ x = 0 /\ y = {} /\ z = <<>> ``` ### Action Definition ```tla Action == /\ Precondition \* Guard/enabling condition /\ x' = x + 1 \* State update /\ UNCHANGED <> \* Other variables unchanged ``` ### Next State Relation ```tla Next == \/ Action1 \/ Action2 \/ Action3 ``` ### Specification ```tla Spec == Init /\ [][Next]_vars ``` With fairness: ```tla Spec == Init /\ [][Next]_vars /\ WF_vars(Action1) ``` ### Type Invariant ```tla TypeInvariant == /\ x \in Nat /\ y \in SUBSET Data /\ z \in Seq(Data) ``` ### Safety Property ```tla SafetyProperty == /\ x \leq MaxValue /\ Cardinality(y) \leq 10 ``` ### Liveness Property ```tla LivenessProperty == <>(x = MaxValue) \* Eventually x reaches MaxValue ``` ## Quantifiers ```tla \A x \in S : P(x) \* For all x in S, P(x) holds \E x \in S : P(x) \* There exists x in S such that P(x) ``` ## Conditional Expressions ```tla IF condition THEN expr1 ELSE expr2 CASE p1 -> e1 [] p2 -> e2 [] OTHER -> e3 ``` ## LET Definitions ```tla LET helper(x) == x + 1 constant == 42 IN helper(constant) ``` ## CHOOSE Operator ```tla CHOOSE x \in S : P(x) \* Arbitrarily choose x from S satisfying P ``` ## Common Idioms ### Nondeterministic Choice ```tla \E x \in S : /\ Condition(x) /\ var' = x /\ UNCHANGED other_vars ``` ### Parameterized Action ```tla Action(param) == /\ param \in ValidParams /\ var' = f(param) /\ UNCHANGED other_vars Next == \E p \in Params : Action(p) ``` ### Multiple Process Model ```tla VARIABLES pc, data Process(i) == /\ pc[i] = "ready" /\ pc' = [pc EXCEPT ![i] = "running"] /\ data' = data \cup {i} Next == \E i \in Processes : Process(i) ``` ### Message Passing ```tla VARIABLES messages Send(msg) == messages' = messages \cup {msg} Receive(msg) == /\ msg \in messages /\ messages' = messages \ {msg} ``` ### Mutex Lock ```tla VARIABLES lock, owner Acquire(proc) == /\ lock = FALSE /\ lock' = TRUE /\ owner' = proc Release(proc) == /\ lock = TRUE /\ owner = proc /\ lock' = FALSE /\ owner' = NULL ``` ## Comments ```tla \* Single line comment (* Multi-line comment *) ``` ## Operator Precedence (highest to lowest) 1. Function application: `f[x]`, record access: `r.field` 2. Prefix operators: `~`, `DOMAIN`, `SUBSET`, `UNION`, `ENABLED`, `UNCHANGED` 3. Postfix operators: `'` (prime) 4. Infix operators (left to right within same level): - `^` (exponentiation) - `*`, `/`, `\div`, `%` - `+`, `-`, `\o` (concatenation) - `..` (range) - Set operators: `\cap`, `\cup`, `\` - Comparison: `=`, `#`, `/=`, `<`, `>`, `\leq`, `\geq`, `\in`, `\notin`, `\subseteq` - `/\` (AND) - `\/` (OR) - `=>` (implies) - `<=>` (equivalence) 5. Temporal operators: `[]`, `<>`, `~>` 6. Quantifiers: `\A`, `\E` Use parentheses to clarify precedence when in doubt.