Functions Basics

Fill in the five TODO assumptions in starter.tla so that every ASSUME statement is true, then click Run Model Checker.

Given: Squares == [n \in 1..5 |-> n * n], Alice == [name |-> "Alice", age |-> 30], Pair == <<7, 8>>.

1. Squares[4] is 16.
2. Alice's age is 30.
3. Alice is a record with a STRING name and a Nat age.
4. UpdatedSquares (defined for you as Squares with entry 1 changed to 100) maps 1 to 100, and still maps 2 to 4 — EXCEPT only touches the one entry you name.
5. The two elements of Pair add up to 15.