Supporting Action Composition in TLC

[William Schultz]

As I understand it, TLC does not currently support the TLA+ action composition operator (mentioned in section 7.3 of Specifying Systems). It appears that it does have the ability to parse the operator within a spec, though. I am curious if there are any fundamental difficulties in implementing support for it. Perhaps it was never implemented simply because it was low priority or didn't seem useful enough for practical specs. I was recently working on a series of specifications where I may have found support for the composition operator useful. Essentially, I wanted to take one spec that modeled things at a fine grain of atomicity and compare it to a version of the spec where several lower level actions were executed as a single, coarse grained atomic step. I was able to manually implement the coarse grained version of the spec, but I felt it may have been easier and clearer if I was able to describe the coarse steps as the composition of fine grained steps. Any background information or thoughts on this would be appreciated. I can also open a Github issue if this might be a feasible feature to implement in the future.

[Leslie Lamport]

Action composition was not implemented in TLC because it was considered at best low priority.  I don't remember if it was difficult to implement or if I had my doubts about action composition being a good idea.  The specification that inspired Yuan Yu to build TLC actually used action composition, which suggests that it was difficult to implement in TLC.  However, it is a mathematically ugly operator for the same reason ENABLED is, and it's possible that I decided that ENABLED was a necessary evil but action composition wasn't. 

Leslie 

[William Schultz]

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.

[1] https://lamport.azurewebsites.net/tla/hiding-and-refinement.pdf

[Leslie Lamport]

For an indication of why ENABLED is ugly, see page 335 of "Specifying Systems".  For why it's necessary, you need to understand the concept of machine closure and why it's important, as well as the relation between WF/SF and machine closure.  I'm afraid I don't have time to explain that now; perhaps someone else will.

Note that ENABLED and \cdot (action composition) are not necessary in the sense that any particular instance of them can be written as an expression that doesn't use them.  For example, (x'=x+1)\cdot(x'=2* x)  equals \E y : (x' = y+1) /\ (y = 2*x).  Because of the importance of WF/SF in ensuring machine closure, requiring the user to do this translation would be a bad idea both because it would be inconvenient and permit errors in the translation.  This is less of an issue for \cdot.

Leslie 

[Leslie Lamport]

On Wednesday, May 6, 2020 at 9:43:49 AM UTC-7, William Schultz wrote: