| Hello, the only references to the variables r and s in the sender's (respectively receiver's) next-state action shown in the text occur in UNCHANGED clauses, and they are inherited from the monolithic specification of the system. It seems to me that in the compositional specification Init_S /\ [][NS]_<<s,buf>> /\ Init_R /\ [][NR]_<<r,buf>> these references can be dropped from the specifications of the components' next-state actions. For example, we can define SSndr == \/ /\ buf' = Append(buf, ...) /\ SComm \/ /\ SCompute /\ UNCHANGED buf NS == SSndr \/ (sigma /\ s'=s) assuming of course that r does not appear in the formulas SComm and SCompute. The definitions of does not involve r either (and symmetrically for the receiver and the variable s) so the only shared variable between the specifications of the sender and the receiver is buf, as expected. This being said, Leslie has often insisted that writing monolithic specifications is much easier than writing compositional ones (and of course TLC only accepts monolithic specs). Regards, Stephan
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/3828185C-CDBE-4184-9216-3DAD983236AE%40gmail.com. |