Thank you, that's helpful background information. I would be curious to know what you mean when you say that ENABLED and action composition are "mathematically ugly" operators. From a cursory glance, I might guess that you consider them "ugly" because they are in some way an "extension" to a more primitive core of TLA. For example, in the Action Operators section (16.2.3) of Specifying Systems, you give definitions for ENABLED and the composition operator, both of which cannot be defined in terms of existing constructs. Their definitions also appear to rely on quantification over states, which seems distinct from other action operator definitions.It seems that most common, practically useful TLA formulas can be written in terms of the prime construct (') and the box operator (☐). ENABLED and action composition introduce exceptions to this. Temporal operators like \EE would seem to be another exception, but perhaps you have similar opinions on their aesthetics based on your "stone in the soup" comments from [1].I also recall that the definitions of weak and strong fairness are given in terms of ENABLED, so perhaps that was one motivator for inclusion of the "necessary evil", but I am mostly conjecturing here.