Sometimes you may want to combine
either with labels, so that branching steps are possible. For example:
either Push: \* code or Pop: \* code end either After: \* code
However, you may also want some steps to only be possible in certain cases. For example, we might want that we can only pop a non-empty stack. Here are two ways of doing that:
either Push: \* code or if stack_not_empty() then Pop: \* code end if end either After: \* code
either Push: \* code or await stack_not_empty() Pop: \* code end either After: \* code
While the both will prevent you from running
stack_not_empty is false, they mean different things for the rest of your system. Here’s how TLC interprets each of them:
either, TLC checks two behaviors: “go to
Push” or “skip to
stack_not_emptymust be true. Since it’s false, the second branch can’t run, meaning only the first branch is possible. So there is only one possible behavior: “go to
In other words, in the
if spec, depending on the state of the stack, there are three possible behaviors:
After. In the
await spec, there’s only
Pop->After. Generally, the latter is what you want, so you should use
await in this case unless you’re sure that the skipping the
either is something you want.
One thing that does not work is putting the
either Push: \* code or Pop: await stack_not_empty() \* code end either After: \* code
This is because there’s nothing stopping TLC from reaching Pop; the
await only matters afterwards. In this case, if the stack is empty, there’s no way for TLC to run the
Pop step and no other processes to run instead, so this is a deadlock.
All of this, of course, assumes this is a single-process system. In a multiprocess system, other processes may potentially alter the stack, so
Pop is not an automatic deadlock.
We can also guard a process in the same way:
await condition; call process;
Similar to above, we can’t put the
await inside the process.. So we have to have an
await every time we want to call the process, which is error prone. While we can’t avoid this, we can ensure that we raise an error if we miss the guard:
process p() begin P: assert condition; \* code end
We still need to manually include the
await statements, but if we forget the assertion fails and spec is broken.