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

[tlaplus] composing specifications

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 and Rcvr mentions where 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 (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/6a3a003f-c5bd-4bec-9f27-a7b1269fb553n%40googlegroups.com.