Multiple steps A1, A2, ..., An can refine a single step as long as every Ai (except perhaps the last one) only changes low-level variables that do not occur in the high-level specification. (And conversely, a single step can then also refine multiple steps, see "stuttering variables" in .) Your toy example had only a single variable that you would naturally consider to be visible, otherwise the spec doesn't really have much meaning.
Yes, I was thinking of a "functional programming" style: the operators would not be TLA+ actions but would compute the result of the operation.
Again, these wouldn't be part of the operators but of the surrounding spec. The operators would be applied only when the enabling condition is satisfied.
Your operator could return a tuple or a record (in principle, you can rewrite any spec into one that has a single record-valued variable whose fields correspond to the variables of the original spec).
How practical and readable all this will be is a different story. Fundamentally, you are trying to write a "non-interleaving" specification that allows several actions to occur simultaneously. These are harder to write than the standard interleaving specs, and depending on what you are trying to model it may not be worth the effort. For example, whether two transitions of different nodes in a distributed system happen at the same time or in an arbitrary order doesn't matter because no other system component can observe the difference.
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/42CDE4B9-541F-4AAC-857F-49851CCB8F3B%40gmail.com.