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

Proving equivalence of AlternatingBit to ABCorrectness

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.


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