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

Re: [tlaplus] temporal properties



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 <gy94...@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...@xxxxxxxxxxxxxxxx.
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>