TLA+ Cheatsheet

TLA+ Quick Start - contains enough to model almost anything

(* Comments *)

(* This is 
   multiline comment *)
\* This is single line comment

(* Module structure *)

---- MODULE <module> ----   \* Starts TLA+ module (should be in file <module>.tla)
====                        \* Ends TLA+ module (everything after that is ignored)

EXTENDS <module>            \* EXTEND (import) another TLA+ module
VARIABLES x, y, ...         \* declares variables x, y, ...
CONSTANTS x, y, ...         \* declares constants x, y, ... (should be defined in configuration)

Name == e                   \* defines operator Name without parameters, and with expression e as a body
Name(x, y, ...) == e        \* defines operator Name with parameters x, y, ..., and body e (may refer to x, y, ...)

(* Boolean logic *)

BOOLEAN                     \* the set of all booleans (same as {TRUE, FALSE})
TRUE                        \* Boolean true
FALSE                       \* Boolean false
~x                          \* not x; negation
x /\ y                      \* x and y; conjunction (can be also put at line start, in multi-line conjunctions)
x \/ y                      \* x or y; disjunction (can be also put at line start, in multi-line disjunctions)
x = y                       \* x equals y
x /= y                      \* x not equals y
x => y                      \* implication: y is true whenever x is true
x <=> y                     \* equivalence: x is true if and only if y is true

(* Integers *)              \* EXTENDS Integers (should extend standard module Integers)

Int                         \* the set of all integers (an infinite set)
1, -2, 1234567890           \* integer literals; integers are unbounded
a..b                        \* integer range: all integers between a and b inclusive
x + y, x - y, x * y         \* integer addition, subtraction, multiplication
x < y, x <= y               \* less than, less than or equal
x > y, x >= y               \* greater than, greater than or equal

(* Strings *)               

STRING                      \* the set of all finite strings (an infinite set)
"", "a", "hello, world"     \* string literals (can be compared for equality; otherwise uninterpreted)

(* Finite sets *)           \* EXTENDS FiniteSets (should extend standard module FiniteSets)

{a, b, c}                   \* set constructor: the set containing a, b, c
Cardinality(S)              \* number of elements in set S
x \in S                     \* x belongs to set S
x \notin S                  \* x does not belong to set S
S \subseteq T               \* is set S a subset of set T? true of all elements of S belong to T
S \union T                  \* union of sets S and T: all x belonging to S or T
S \intersect T              \* intersection of sets S and T: all x belonging to S and T
S \ T                       \* set difference, S less T: all x belonging to S but not T
{x \in S: P(x)}             \* set filter: selects all elements x in S such that P(x) is true
{e: x \in S}                \* set map: maps all elements x in set S to expression e (which may contain x)

(* Functions *) 

[x \in S |-> e]             \* function constructor: maps all keys x from set S to expression e (may refer to x) 
f[x]                        \* function application: the value of function f at key x
DOMAIN f                    \* function domain: the set of keys of function f
[f EXCEPT ![x] = e]         \* function f with key x remapped to expression e (may reference @, the original f[x])
[f EXCEPT ![x] = e1,        \* function f with multiple keys remapped: 
          ![y] = e2, ...]   \*   x to e1 (@ in e1 will be equal to f[x]), y to e2 (@ in e2 will be equal to f[y])
[S -> T]                    \* function set constructor: set of all functions with keys from S and values from T

(* Records *)

[x |-> e1, y |-> e2, ...]   \* record constructor: a record which field x equals to e1, field y equals to e2, ... 
r.x                         \* record field access: the value of field x of record r
[r EXCEPT !.x = e]          \* record r with field x remapped to expression e (may reference @, the original r.x)
[r EXCEPT !.x = e1,         \* record r with multiple fields remapped: 
          !.y = e2, ...]    \*   x to e1 (@ in e1 is equal to r.x), y to e2 (@ in e2 is equal to r.y)
[x: S, y: T, ...]           \* record set constructor: set of all records with field x from S, field y from T, ...

(* Sequences *)             \* EXTENDS Sequences (should extend standard module Sequences)

<<a, b, c>>                 \* sequence constructor: a sequence containing elements a, b, c
s[i]                        \* the ith element of the sequence s (1-indexed!)
s \o t                      \* the sequences s and t concatenated
Len(s)                      \* the length of sequence s
Append(s, x)                \* the sequence s with x added to the end
Head(s)                     \* the first element of sequence s

(* Tuples *)

<<a, b, c>>                 \* tuple constructor: a tuple of a,b,c (yes! the <<>> constructor is overloaded)
                            \* - sequence elements should be same type; tuple elements may have different types
t[i]                        \* the ith element of the tuple t (1-indexed!)
S \X T                      \* Cartesian product: set of all tuples <<x, y>>, where x is from S, y is from T

(* Quantifiers *)

\A x \in S: e               \* for all elements x in set S it holds that expression e is true
\E x \in S: e               \* there exists an element x in set S such that expression e is true

(* State changes *)

x', y'                      \* a primed variable (suffixed with ') denotes variable value in the next state 
UNCHANGED <<x,y>>           \* variables x, y are unchanged in the next state (same as x'=x /\ y'=y)

(* Control structures *)

LET x == e1 IN e2           \* introduces a local definition: every occurrence of x in e2 is replaced with e1
IF P THEN e1 ELSE e2        \* if P is true, then e1 should be true; otherwise e2 should be true

Apalache

# Running apalache

# A handy alias for calling Apalache
alias apalache="java -jar apalache-pkg-0.17.5-full.jar --nworkers=8"

# Typecheck
apalache typecheck <.tla file>

# Model check assuming a .cfg file with the same name as the .tla file is present
apalache check <.tla file>

# Model check assuming with a specific .cfg file
apalache check --config=<.cfg file> <.tla file>

# Model check an invariant Foo 
apalache check --inv=Foo <.tla file>

# Generate multiple (up to n) traces for invariant Foo
apalache check --view=<View Operator Name> --max-error=n --inv=Foo <.tla file>
(* Writing models with Apalache *)

EXTENDS Apalache       \* Import https://github.com/informalsystems/apalache/blob/unstable/src/tla/Apalache.tla

\* Makes Apalache understand that a function with keys in 1.maxSeqLen can be treated as a Sequence
FunAsSeq(fn, maxSeqLen) == SubSeq(fn, 1, maxSeqLen)

(*
Equivalent to the pseudocode:

x = initialValue
for element in arbitrary_ordering(S):
   x = CombinerFun(x, element)
return x

*)
FoldSet(CombinerFun, initialValue, S) \* For a set S

(*
Equivalent to the pseudocode:

x = initialValue
for element in sequential_ordering(S):
   x = CombinerFun(x, element)
return x

*)
FoldSeq(CombinerFun, initialValue, S) \* For a sequence S

TLC

# Running TLC

# A handy alias providing the JVM with 12GB of RAM (adjust accordingly) and using multiple threads
alias tlc="java -XX:+UseParallelGC -Xmx12g -cp tla2tools.jar tlc2.TLC -workers auto" 

# Model check with TLC
tlc -config <.config file> <.tla file> 

# Run TLC in simulation mode
tlc -config <.config file> -simulate <.tla file>

F.A.Q.

1. Does whitespace matter in TLA+?

Yes whitespace matters when AND’ing (/\), OR’ing (\/)

Foo == /\ x
       /\ \/ y
          \/ z

means

Foo == x and ( y or z)

Indentation defines precedence and must be tab or space aligned. The parser should complain if it not aligned.

2. …. coming soon.