Re: [tlaplus] temporal properties

Recompiling to PlusCal fixed it (with no fairness anywhere0; but when I add the same fairness to both alternationa1 and handshake1, I get "temporal properties were violated".

What's wrong?

Thanks

On Tuesday, March 11, 2014 10:13:31 AM UTC-7, Stephan Merz wrote:

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

On 10 Mar 2014, at 19:25, Gideon Yuval <gy9...@xxxxxxxxx> wrote:

I copied the alternation &handshake (enclosed) from the book. Model gives me "Temporal properties were violated." . Am I doing anything obviously wrong?

Thanks

/Gideon

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

<alternation1.tla>
<handshake1.tla>