Hello Gideon,
I am unable to reproduce your problem using the TLA+ modules attached to your message. Here's what I did: I launched TLC from handshake.1tla by creating a new model. I unchecked the box for deadlock checking (should be irrelevant) and entered Q!Spec as the only temporal property to check. The behavior spec is set to "Spec" (which refers to the formula Spec defined in module handshake1). TLC ran and reported no errors.
What properties did you check? Also, since the Consumer action is clearly executable in the state shown in your screen shot, are you sure you specified Spec as the behavior specification (and not Init and Next)?
Best, Stephan
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
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>
--
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><Capture.PNG>
|