Learn · All the Ways It Can Break

growing

Values Before Variables

TLA+ becomes much smaller when sets, functions, records, and sequences are ordinary values first.

formal-methods, tla-plus, tlc, sets, functions, learn

You will run TLA+ expressions in TLC's evaluator, distinguish sets from sequences, use functions as finite maps, construct records, and read a functional update. Experienced readers can use the final section to connect these forms to extensional equality and state fingerprinting. The next chapter puts the expressions inside a complete module.

Start with a small world

Download tla2tools.jar from the official TLA+ 1.7.4 release and place it in an empty directory. Java 11 or newer is sufficient for this route. Start the evaluator:

java -cp tla2tools.jar tlc2.REPL

The prompt accepts TLA+ expressions. Try these one at a time:

{1, 2, 3} \union {3, 4}
{job_a, job_b} \ {job_b}
<<"accept", "start">> \o <<"publish">>
[phase |-> "running", canceled |-> FALSE]

The evaluator should produce {1, 2, 3, 4}, {job_a}, a three-element sequence, and a record. Names such as job_a are model values: finite atoms whose internal representation does not matter.

Extensional equality — two sets are equal when they contain the same members, and two functions are equal when they return the same value for every input. See the value sections of Leslie Lamport's Specifying Systems.

Prediction — distinguish a function from the storage used to implement one.

A function is a map you can apply

Enter:

LET phase == [job \in {job_a, job_b} |-> "queued"]
IN phase[job_a]

The result is "queued". TLA+ functions subsume many structures programmers meet separately: a tuple is a function over 1..n, and a record is a function whose domain is a set of field names. The syntax remains specialized because it makes intent readable.

A function update returns a new value:

LET old == [job \in {job_a, job_b} |-> "queued"]
    new == [old EXCEPT ![job_a] = "running"]
IN <<old[job_a], new[job_a], new[job_b]>>

The result is <<"queued", "running", "queued">>. The expression changed neither old nor an external store. It defined new by saying that it agrees with old everywhere except at job_a. This is the shape later used in an action: phase' will receive the new function.

Sets admit choices; sequences remember order

Use a set when membership matters and order does not. Use a sequence when position and repetition matter:

{ "retry", "retry" }
<<"retry", "retry">>

The first value contains one member because sets discard duplicates. The second has length two. A pending-job pool may be a set if the model observes only eligibility. A delivery history must be a sequence if two deliveries or their order can change the future.

This is the first abstraction test from Chapter 2 in executable form. Choosing a set is not a performance decision. It asserts that multiplicity and order cannot affect the modeled observation. If that assertion is false, the model has already erased a possible failure.

Under the hood: equality makes states revisitable

TLC explores a graph. It needs to decide whether a newly produced state has already been seen. A state whose variables are mathematical values has a clear equality relation: equal sets ignore enumeration order; equal functions agree on their domains and results; equal sequences agree position by position.

The implementation uses fingerprints and collision safeguards rather than performing a philosophical comparison from scratch at every edge. The modeler's obligation remains semantic: choose values whose equality preserves the distinctions the claim needs. Storage identity, allocation order, and object addresses do not enter unless the specification explicitly models them.

Lessons

TLA+ expressions denote values; they do not execute container mutations.
Sets preserve membership, while sequences preserve order and multiplicity.
A bounded function is a finite map and can be applied with brackets.
EXCEPT constructs a new function that differs at named locations.
The choice of value shape is already an abstraction claim.

Practice

Retrieval. Write expressions for a two-member job set, a two-event sequence, and a record with phase and canceled fields.
Discrimination. Should an at-most-once publication model represent published job identities as a set or a sequence? Name one question that would reverse your answer.
Transfer. Define a function mapping node_a and node_b to 0, then define a second function in which only node_b maps to 1. Evaluate both.

Worked answers

{job_a, job_b}; <<"accept", "start">>; [phase |-> "running", canceled |-> FALSE].
A set is enough when the observation is only whether a job ever published. Use a sequence when the claim asks whether it published twice or which publication occurred first.
LET old = [node \in {node_a, node_b} |-> 0] new = [old EXCEPT ![node_b] = 1] IN <<old, new>>.

References

Leslie Lamport. Specifying Systems. Addison-Wesley, 2002. — values, expressions, functions, and the TLA+ language
TLA+ Foundation. TLA+ 1.7.4 release. — the versioned TLC evaluator used in this chapter
TLA+ Foundation. TLA+ documentation. — current installation and tooling routes

← Green Has a Boundary A Module Names Its World →

Before TLA+ describes a system changing, it describes values. {job_a, job_b} is a set. [job \in Jobs |-> "queued"] is a function. [phase |-> "running", canceled |-> FALSE] is a record. <<"accept", "start">> is a sequence. None is a mutable container. Each expression denotes one complete value. That choice is more than notation. A checker needs states it can compare, hash, and revisit. Whole mathematical values make equality explicit. An update expression constructs another function; it does not secretly alter the old one. Later, a primed variable will name the value in the next state. This chapter first makes the values themselves familiar.