Re: [tlaplus] Request for comment: CASE expressions

- Did you assume that CASE expressions evaluated their branches sequentially?

Yes, I assumed they desugared to nested IF/THEN/ELSE expressions with the final ELSE optionally replaced by an Assert(FALSE) for runtime failure purposes (whatever that means formally).

- Do you frequently use CASE and would therefore mind CASE being deprecated and eventually eliminated from the language?

I did use it relatively recently for defining the transition function of a finite automaton. This could have been written as a bunch of IF/THEN/ELSE blocks instead. Would I mind terribly much if it were removed from the language? I guess not. However, currently we have to import the TLC module to access the Assert operator, so that is kind of messy for cases where the final ELSE is undefined. TLA+ also already feels lacking when it comes to enum support, given that almost every spec has them but we don't have good ways to define and match over them. Removing our closest thing to a switch statement might make that worse, unless it were somehow replaced with real support for enums in 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_?

I guess I don't really understand this question, sometimes it is easier to write checks in ways that overlap but due to execution order one takes precedence over the other, so roughly like:

ASSUME P \subseteq Q

op(e) ==

IF e \in P THEN f(e)

ELSE IF e \in Q THEN g(e)

ELSE Assert(FALSE)

One final thing I will say about CASE expressions is that they are very difficult to parse; ex:

This is due both to dangling-else ambiguity and their interaction with vertically-aligned conjunction/disjunction lists.

Andrew Helwer

On Wed, Jun 10, 2026 at 12:03 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/d8112d8f-2a2e-4b7e-9130-8d932adef9e9n%40googlegroups.com.