The semantics of CASE expressions in TLA+ is defined as a CHOOSE _expression_ [1]. For example,
CASE x >= 0 -> 1 [] x <= 0 -> 2
desugars to
CHOOSE v : (x > = 0 /\ v = 1) \/ (x <= 0 /\ v = 2)
If x=0, it could therefore evaluate to either 1 or 2.
Different TLA+ tools implement CASE statements in different ways. For example, TLC and the SMT backend of TLAPS regard them as nested IF expressions (and would evaluate the above example to 1 for x=0) but the Isabelle backend of TLAPS respects the CHOOSE semantics. For more details, see [2].
Because CASE is potentially confusing, at least one company working with TLA+ disallows the use of CASE altogether. We would welcome opinions (if possible backed up by data) on the use of CASE by the TLA+ community. For example:
- Did you assume that CASE expressions evaluated their branches sequentially?
- Do you frequently use CASE and would therefore mind CASE being deprecated and eventually eliminated from the language?
- Do you use CASE only when the different branches are non-overlapping (or if the expressions corresponding to overlapping branches are guaranteed to evaluate to the same value), so it could be seen as syntactic sugar for a nested IF _expression_?
Please add your opinions as a comment to [2].
Thanks,
Stephan
[1] Specifying Systems, section 16.1.4
[2] https://github.com/tlaplus/rfcs/issues/26