[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Supporting Action Composition in TLC



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 

On Wednesday, May 6, 2020 at 9:43:49 AM UTC-7, William Schultz wrote:
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.

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/905203d7-0ff1-47ff-854c-a2d543abcb69%40googlegroups.com.