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

[tlaplus] Re: Question about prophecy variables

The FIFOp module and FIFOp2 modules make no sense to me either.  I will investigate.

Leslie

On Saturday, February 29, 2020 at 1:28:29 PM UTC-8, ns wrote:
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

Untitled.png


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/4c98cb42-3da8-4178-8d1a-97e6464bd1c8%40googlegroups.com.