[tlaplus] Question about prophecy variables

[ns <nedsri1988@xxxxxxxxx>]

Hello, I was reading about prophecy variables in the paper Hiding, Refinement, and Auxiliary Variables" and I have to admit I'm mystified as to what the def of module FIFO2 is trying to say

Why is GetP effectively carrying out a Put action? While I can see how SpecP might implement Spec I don't see how \EE p: SpecP is equivalent to Spec

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/1c0c31dd-8a4f-40b3-8812-251d5f779fca%40googlegroups.com.