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