We’ve been implicitly using expressions up until now; we just haven’t clarified them. For our purposes, an expression is anything that follows a
\in. In this section we’ll cover some general expression modifiers.
We’ve used these for a while now:
/\ is and,
\/ is or. We can join expressions with them. The one subtlety is that this is the only case where TLA+ is whitespace sensitive. If you start a line with an indented junction, TLA+ considers that the start of a subclause. For example,
/\ TRUE \/ TRUE /\ FALSE \* (T \/ T) /\ F /\ TRUE \/ TRUE \/ FALSE \* (T /\ (T \/ F)) \/ TRUE \/ TRUE /\ FALSE \* T \/ (T /\ F)
Etc. As a general rule of thumb:
Generally if you mess this up the spec will crash, so you’re unlikely to get a logic bug through this.
Any expression can use LET-IN to add local operators and definitions to just that expression alone.
LET IsEven(x) == x % 2 = 0 IN IsEven(5) LET IsEven(x) == x % 2 = 0 Five == 5 IN IsEven(Five) LET IsEven(x) == LET Zero == 2 IN x % Zero = Zero Five == 5 IN IsEven(Five)
The whitespace does not matter: we can write
LET IsEven(x) == x % 2 = 0 Five == 5 IN IsEven(Five) and it will correctly parse it as two separate operators in the LET. You should use newlines though, because you care about legibility.
This is exactly what you expect it to be.
IsEven(x) == IF x % 2 = 0 THEN TRUE ELSE FALSE
As before, alignment doesn’t matter, but you should align them anyway unless you really hate your coworkers.
Case is mostly how you’d expect it to act, with one subtle difference.
CASE x = 1 -> TRUE  x = 2 -> TRUE  x = 3 -> 7  OTHER -> FALSE
OTHER is the default. If none of the cases match and you leave out an OTHER, TLC considers that an error. If more than one match, though, TLC will pick one for you and not branch. In other words, the following code
CASE TRUE -> FALSE  TRUE -> TRUE
May or may not be true. Be careful.
All parts of expressions are expressions or identifiers, so you can put expressions inside other expressions. Additionally, all expressions can be used inside PlusCal code.