[tlaplus] composing specifications

[ns <nedsri1988@xxxxxxxxx>]

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 SR == 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/689ec68a-2a5b-44d4-a380-0b033f28a42an%40googlegroups.com.