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
=============================================================================