Question about prophecy variables

37 views
Skip to first unread message

ns

unread,
Feb 29, 2020, 4:28:29 PM2/29/20
to tlaplus
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

Leslie Lamport

unread,
Feb 29, 2020, 7:46:49 PM2/29/20
to tlaplus
The FIFOp module and FIFOp2 modules make no sense to me either.  I will investigate.

Leslie

Leslie Lamport

unread,
Mar 2, 2020, 5:28:20 PM3/2/20
to tlaplus
When transcribing the FIFOp and FIFOp2 modules into the document, I somehow exchanged
"Get" and "Put" throughout the text.  I have corrected the document on the Web site.
Thank you for pointing out the error.  I hope whenever anyone finds something on
the Web site that seems to make no sense, he or she will ask me about it.

Leslie 
Reply all
Reply to author
Forward
0 new messages