Re: [tlaplus] Proving equivalence of AlternatingBit to ABCorrectness

Dear Dr Stephan,

Thank you sir for your speedy response.

"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."

My understanding is that ABCorrectness, although without message channels and losing message action, is a higher abstraction of the alternating bit protocol module. This is from reading the following paragraph of the book.

"However, we don't have its specification. In fact, it is typical in practice that we are called upon to check the correctness of a system

design without any formal specification of what the system is supposed to do. In that case, we can write an ex-post facto specification. Module ABCorrectness

in Figure 14.4 on the next page is such a specification of correctness for the alternating bit protocol"

"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."

Sorry to throw you off track. Yes, variable hiding is not needed. I have reverted to the original and executed ABCSpecBar == AB!ABCSpec as per p. 228 in TLC

"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?"

Yes, I showed only the last state. I also attached the files used as requested

Initial

/\ ackQ = <<>>

/\ msgQ = <<>>

/\ rBit = 0

/\ rcvd = "d1"

/\ sAck = 0

/\ sBit = 0

/\ sent = "d1"

State=1

/\ ackQ = <<>>

/\ msgQ = <<<<1, "d1">>>>

/\ rBit = 0

/\ rcvd = "d1"

/\ sAck = 0

/\ sBit = 1

/\ sent = "d1"

State3 = Stuttering

Cheers!

-Wan-

On Wednesday, 7 June 2017 14:51:35 UTC+8, Stephan Merz wrote:

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

On 7 Jun 2017, at 04:35, Wan Azlan <wea...@xxxxxxxxx> wrote:

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...@googlegroups.com.
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.