What a module actually is
Every TLA+ file you've written so far has had this shape:
---- MODULE Name ----
...
====
A module is just a named container for definitions — the wrapper tools
need to know where one spec ends and another begins. EXTENDS Naturals (or
Sequences, FiniteSets, ...) pulls in another module's operators so you
can use them, exactly the way you've been doing since Chapter 0.1. There's
no more to modules than that — the interesting ideas from here on are
CONSTANT, VARIABLE, and what a state is.
Constants vs. variables
A CONSTANT is a value that's fixed for the whole run, but not baked
into the spec itself — you (or TLC's .cfg file) supply it from outside.
Think of it as a parameter: "however many servers there are" is a CONSTANT
if you want to check your spec against different numbers of servers without
editing the spec.
A VARIABLE is a value that's part of the system's state — it's
allowed to be different at different points in time. Everything you write
about a VARIABLE describes how it can change; a CONSTANT never
changes at all.
CONSTANT MaxRetries
VARIABLE attempts
A state is just an assignment
This is the single most important idea in this chapter, and you've been
using it informally since Chapter 0.1 without the vocabulary for it: a
state is an assignment of a specific value to every VARIABLE in the
spec. If a spec has one variable color, then color = "red" is a
state, completely. Add a second variable and a state becomes an assignment
to both — but for now, everything we write has exactly one.
Init: which states you can start in
Init is a predicate — true or false for a given state — describing the
starting state (or states; there can be more than one). You already know
how to write predicates about a value from Chapter 0.2, so this isn't new
syntax, just a new purpose for it:
VARIABLE color
TypeOK == color \in {"red", "green", "yellow"}
Init == color = "red"
TypeOK here is exactly what you'd expect from Chapter 1.4's preview: a
statement of what set color must always belong to. Init is stricter —
it doesn't just say what's possible, it says exactly where the system
begins.
What you'll do in this exercise
You'll declare color, write its TypeOK, and write Init for a traffic
light that always starts red. We haven't covered how color is allowed to
change yet — that's the entire subject of the next chapter — so this
exercise's Next is given to you as UNCHANGED color (a light that never
changes is a valid, if boring, system). TLC will check that your Init
only ever produces states satisfying TypeOK.