157 lines
3.6 KiB
Markdown
157 lines
3.6 KiB
Markdown
# General tips
|
|
|
|
## Composite state
|
|
|
|
Modeling composite state as a struct requires updating
|
|
all items in every action, possibly using EXCEPT.
|
|
|
|
Instead, separate each field to its own variable, and
|
|
actions only update that variables.
|
|
|
|
|
|
## `THEOREM`
|
|
|
|
`THEOREM` declares the properties of the spec it belongs to.
|
|
However, TLC does not do anything with it,
|
|
so consider it as documentation. This is only used by TLAPS.
|
|
|
|
|
|
## PlusCal
|
|
### Macros
|
|
|
|
Macros, rather than [procedures](../core/07-concurrency.md), are the main form of statement reuse.
|
|
|
|
### Avoid `WHILE`
|
|
|
|
While creates one state for each iteration, which can lead
|
|
to an explosion of concurrency and the number of states.
|
|
|
|
That's fine when modeling queues, but better avoided for computations. Example
|
|
|
|
```pluscal
|
|
\* BAD
|
|
Double:
|
|
while i <= Len(seq) do
|
|
seq[i] := seq[i] * 2;
|
|
i := i + 1;
|
|
end while;
|
|
|
|
\* GOOD
|
|
[i \in 1..Len(seq) |-> seq[i] * 2]
|
|
```
|
|
|
|
### State sweeping
|
|
|
|
The practice of having a state variable control other state variables, as in, to increase the states generated with no
|
|
additional complexity.
|
|
|
|
```pluscal
|
|
\* Without
|
|
variable
|
|
seq \in [1..Size -> S]; \* Checks sequences of length 5
|
|
|
|
\* With state sweeping
|
|
variable
|
|
n \in 1..Size;
|
|
seq \in [1..n -> S]; \* Checks sequences of length 1 to 5
|
|
```
|
|
|
|
## TLA+
|
|
### `UNCHANGED`
|
|
|
|
Since TLA+ Next actions must define every change,
|
|
using `UNCHANGED` saves lots of typing.
|
|
|
|
### Helper actions
|
|
|
|
It can be convenient to split the next-state relations across
|
|
multiple actions, like this helper:
|
|
|
|
```tla+ code fragment
|
|
Trans(agent, a, b) ==
|
|
/\ pc[agent] = a
|
|
/\ pc' = [pc EXCEPT ![agent] = b]
|
|
\* used like:
|
|
Trans(agent, "state1", "state2")
|
|
```
|
|
|
|
### `@`
|
|
|
|
In a function update, `@` refers to the old value:
|
|
|
|
```tla+ code fragment
|
|
\* Verbose
|
|
f' = [f EXCEPT ![1][2].a = f[1][2].a + 1]
|
|
|
|
\* Clean
|
|
f' = [f EXCEPT ![1][2].a = @ + 1]
|
|
```
|
|
|
|
- `@` is the original value of the selected value before replacement
|
|
- it is also available in function assignments, which PlusCal converts to `EXCEPT:
|
|
- `counter[i] := @ + 1`
|
|
|
|
### Parameterized actions
|
|
|
|
```tla+ code fragment
|
|
\* Not parameterized
|
|
Add ==
|
|
\E w \in Worker: s' = s \union {w}
|
|
Remove ==
|
|
\E w \in Worker: s' = s \ {w}
|
|
Next == Add \/ Remove
|
|
|
|
\* Parameterized
|
|
Add(w) == s' = s \union {w}
|
|
Remove(w) == s' = s \ {w}
|
|
Next ==
|
|
\E in worker:
|
|
\/ Add(w)
|
|
\/ Remove(w)
|
|
```
|
|
|
|
This is better because we reuse the same value in multiple actions.
|
|
Imagine you want to add logging to every added or removed worker.
|
|
This is not easy in the first version (`w` may not be the same),
|
|
but easy in the second:
|
|
|
|
```tla+ code fragment
|
|
\* Parameterized
|
|
Add(w) == s' = s \union {w}
|
|
Remove(w) == s' = s \ {w}
|
|
Log(w) == log' = Append(log, w)
|
|
Next ==
|
|
\E in worker:
|
|
/\ \/ Add(w)
|
|
\/ Remove(w)
|
|
/\ Log(w)
|
|
```
|
|
|
|
### Secure refactorings with actions properties
|
|
|
|
```tla+ code fragment
|
|
\* Imagine we created an action including this:
|
|
OldAction(user) == seq' = seq \o <<user>>
|
|
\* The we refactor it:
|
|
NewAction(user) == seq' = Append(seq, user)
|
|
```
|
|
|
|
We can ensure these are equivalent by creating a property to check that:
|
|
|
|
```tla+ code fragment
|
|
\* It is always true that for all users in User the two actions return the same result,
|
|
\* all others vars remaining unchanged.
|
|
RefactorProp == [][
|
|
\A u \in User: OldAction(user) = NewAction(user)
|
|
]_vars
|
|
```
|
|
|
|
But we can go beyond equality to check that an action is a supserset of the old one:$
|
|
```tla+ code fragment
|
|
\* It is always true that for all users in User the two actions return the same result,
|
|
\* all others vars remaining unchanged.
|
|
RefactorProp == [][
|
|
\A u \in User: OldAction(user) => NewAction(user)
|
|
]_vars
|
|
```
|
|
|