In TLA+, a function maps every element of its domain to a value. They're similar to dictionaries or maps in programming languages.
f == [x \in 1..3 |-> x * 2]
This creates a function where f[1] = 2, f[2] = 4, f[3] = 6.
Use square brackets:
f[1] \* returns 2
The DOMAIN operator returns the set of inputs a function is defined on:
DOMAIN f \* returns {1, 2, 3}[S -> T] \* the set of all functions from S to T
Example: [{"a", "b"} -> BOOLEAN] is the set of all functions mapping "a" and "b" to TRUE or FALSE.
f' = [f EXCEPT ![2] = 10]
This creates a new function identical to f but with f'[2] = 10.
You can use @ to refer to the old value:
f' = [f EXCEPT ![2] = @ + 1]The spec models a simple key-value store using TLA+ functions.