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

*From*: Wan Azlan <wear...@xxxxxxxxx>*Date*: Tue, 6 Jun 2017 19:35:27 -0700 (PDT)

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

=============================================================================

**Follow-Ups**:**Re: [tlaplus] Proving equivalence of AlternatingBit to ABCorrectness***From:*Stephan Merz

- Prev by Date:
**Re: TLA+ theory blog post series + new subreddit** - Next by Date:
**Re: [tlaplus] Proving equivalence of AlternatingBit to ABCorrectness** - Previous by thread:
**Re: [tlaplus] Seq({"xxx"}) is not enumerable** - Next by thread:
**Re: [tlaplus] Proving equivalence of AlternatingBit to ABCorrectness** - Index(es):