Hi all
I'm reading Auxiliary Variables in TLA+ (
http://lamport.azurewebsites.net/pubs/auxiliary.pdf) to understand better
the technique of checking a low level spec satisfying a higher level spec.
There is a question concerning prophecy variables. In the module SendSetUndoP (p. 29) we add a prophecy array var
and check a Theorem
theorem SpecUP => SS!Spec
obviously to show that the spec specUP implements the lower level spec of the module SendSet.
Then it is said (p.29)
We should also check that condition (4.11) holds for each subaction A. To do this, we need to create a model with speci cation SpecU and have TLC check
the property:
[] [^ Choose => Ef \in [DOM->Pi] : PredChoose(f)
^ Send => Ef \in [DOM->Pi] : PredSend(f )
^ Rcv => Ef \in [DOM->Pi] : PredRcv(f )
^ AS \in subset y:Undo(S) ) => Ef \in [DOM->Pi] : PredUndo(f,S)
]vars
can someone explain why do we need to check this second condition?
or this is just the alternate option of how we check that the spec specUP implements the lower level spec of the module SendSet?
By proving this condition we show that Choose action is equivalent to ChooseP action, Send action is equivalent to SendP action, etc...
Thanks in advance.
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
.