| Dear Wan,
first of all, the two specifications are not equivalent: ABCorrectness contains fewer details (it does not specify the message or acknowledgement channels), so you cannot expect it to imply the specification in module AlternatingBit.
How you can check that the specification in module AlternatingBit implies the one in ABCorrectness is explained in chapter 14 of the book (p.228). In fact, your renaming of variables is unnecessary: the idea is that the behaviors satisfying formula ABSpec also satisfy formula ABCSpec. I do not understand why you say that some variables of module ABCorrectness (but not the others) are hidden. And I do not see why your renaming of variables would change anything.
Finally, a counter-example to a temporal property is a trace (ending in a loop), not a single state. The state that you indicate in your message appears to be perfectly valid and does not help me understand the problem that you encounter. If you cannot debug the issue yourself, could you please provide the full TLA+ modules that you are using?
Regards, Stephan
Hello, Dear TLA+ experts,
From Chapter 14 of the book, I am trying to "prove" (is this the correct term?) the AlternatingBit specification is equivalent to ABCorrectness specification but ran into temporal property error.
In ABCorrectness, I edited, the occurrance of sBit, rBit and sAck with hsBit, hrBit and hsAck, respectively, as these are hidden. I then mapped hsBit, hrBit and hsAck with the corresponding variables sBit, rBit and sAck from AlternatingBit spec. However I got the following errors shown below. I always thought that AlternatingBit and ABCorrectness are supposed to be equivalent but it seems that ABCorrectness is "one-state lagging" the execution of AlternatingBit. The model check code is attached below.
Can someone point out my mistake?
Thanks in advance.
-Wan-
ErrorState == /\ ackQ = <<>> /\ msgQ = <<<<1, "d1">>>> /\ rBit = 0 /\ rcvd = "d1" /\ sAck = 0 /\ sBit = 1 /\ sent = "d1"
--------------------------- MODULE MCAlternatingBit ------------------------- EXTENDS AlternatingBit
CONSTANTS msgQLen, ackQLen
SeqConstraint == /\ Len(msgQ) \leq msgQLen /\ Len(ackQ) \leq ackQLen
osBit == sBit osAck == sAck orBit == rBit
AB == INSTANCE ABCorrectness WITH hsBit<-osBit, hsAck<-osAck, hrBit<-orBit ABPropertyToTest == AB!ABCSpec THEOREM ABSpec => AB!ABCSpec
=============================================================================
--
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 https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|