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 specificationInit_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 defineSSndr ==\/ /\ buf' = Append(buf, ...)/\ SComm\/ /\ SCompute/\ UNCHANGED bufNS == 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,StephanOn 17 Mar 2022, at 05:11, ns <nedsr...@xxxxxxxxx> wrote:I have a question from reading Sec. 10.4.1 of the S.S. book There it talks about composition in the presence of shared updatable state. The example is of a Sender and Receiver system communicating using a shared buf. I understand that if you have a monolithic spec then it would be written InitSR /\ [][NextSR]_<<s,r,buf>> (ignoring fairness for now), where NextSR == Sndr \/ Rcvr, defined in the book, specifically Sndr mentions r and Rcvr mentions s where s and r are the sender and receiver state vars resp. He then (I assume) wants to defines the system as the composition of two components Cs /\ Cr, where Cs = Init_S /\ [][NS]_<<s,buf>> and Cr == Init_R /\ [][NR]_<<r,buf>>. So Cs /\ Cr == Init_S /\ Init_R /\ [][NS]_<<s,buf>> /\ [][NR]_<<r,buf>>. The form of say NS is given as Sndr \/ (sigma /\ (s'=s)), where sigma is calculated. The problem is that this still requires the component Cs know about r (and correspondingly Cr knows about s) How is this possible if Cs and Cr are two separate components? Does r represent the "environment" in an assume-guarantee setting?--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6a3a003f-c5bd-4bec-9f27-a7b1269fb553n%40googlegroups.com.