[tlaplus] interface refinement

[s nedunuri <ss.nedunuri@xxxxxxxxx>]

I have a question or two regarding spec refinement. Suppose I can show that some component ComptL is a refinement of a component ComptH, that is 

      ComptL => \E x: ComptH

(Aside: I assume that this corresponds to establishing a simulation relation between ComptL and ComptH although I don't recall seeing that stated anywhere). Now if ComptH is part of some system, I would like to be able to conclude that replacing ComptH by ComptL in that system spec is also sound. I can definitely do this if the system is a simple composition of specs, eg System == ComptH /\ Env because then ComptL /\ Env => \E x: CmptH /\ Env. But what if my spec is something other than a simple asynchronous composition of Cmpt and Env. "Specifying Systems" covers a variety of cases and shows that even synchronous interleaved composition can be written as Cmpt /\ Env /\ <some additional conditions>, which still enables me to conclude that the replacement is sound. I've played around with various other compositions eg suppose I had 

System == ComptH_Init /\ Env_Init /\ [ComptH_Next /\ Env_Next]_vars

(ComptH and Env both tick at the same time). I believe that this can also be written as ComptH /\ Env /\ {some additional conditions}. Does anyone know if this is a general result and its always safe to substitute a refined component's Init and Next in the system spec?

Secondly, after watching the videos on Implementation with Refinement, I read Section 10.8 on Interface Refinement in Specifying Systems. The book seems to take a slightly different approach to things with an interface refinement module constraining the lower level variables as required by the higher level spec and then conjoining the higher level spec with a temporal existential to hide the higher level variables. After that I read the paper on Refinement Mappings which basically said that the temporal existential is no longer needed. If that's the case is 10.8 an "older style" of doing things? Also while on the subject I noticed that Specifying Systems is nearly 20 years old. Is there an update due any time in the near future?

thanks

-- 
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/164dafff-2860-4410-b5b5-83cadd3fccaen%40googlegroups.com.