Hello, I am assuming that you are checking if the algorithm specified in module handshake1 refines the one of module alternation1 under the given refinement mapping. Your definition of formula Spec in module alternation1 contains fairness properties, whereas the PlusCal algorithm does not. And formula Spec in handshake1 doesn't contain fairness conditions either, so it's no wonder that it doesn't imply A!Spec. In fact, you anticipated the exercise at the end of section 6.6 of the hyperbook. Probably you changed something in the PlusCal algorithm of module alternation1, removing fairness conditions, and forgot to regenerate the corresponding TLA+ specification. Best regards, Stephan
|