Dear Wan Azlan,
the term "equivalence" means that the two specifications imply each other, that is,
ABSpec => AB!ABCSpec and AB!ABCSpec => ABSpec.
In fact, you are only interested in proving the first implication, showing that the specification in module AlternatingBit refines the one in module ABCorrectness, or, as you say, that ABCorrectness is a higher abstraction of the function ensured by the alternating bit protocol.
I ran TLC on your modules, and everything works fine. Since you obtain a counter-example that ends in stuttering, this indicates that you did not include the fairness condition in the specification that TLC used for model checking. Perhaps you used just the initial state and next state predicates as the system specification instead of the full specification?
I'll assume here that you use TLC from the Toolbox. Here is what you need to do to check refinement:
1. From module MCAlternatingBit, select the menu "TLC Model Checker" and click on "New Model ...". Give the model an arbitrary name (by default, it is called "Model_1".) The model checker pane will open and display some errors. Don't panic: this just means that we need to fix some parameters before we can launch TLC.
2. On the left-hand side, you'll see a pane "What's the behavior spec?". Check the option "Temporal formula" and enter the name of the specification (ABSpec).
3. On the right-hand side, you'll see a pane "What is the model?". Here you have to specify fixed values for the parameters. I chose the following:
Data <- [model value] {d1,d2}
ackQLen <- 3
msgQLen <- 3
(Do a double-click on each of the three parameters. For the first one, I entered {d1,d2}, then chose "Set of model values" and accepted the default options. For the two others, I just entered 3 with default options, i.e. "Ordinary assignment".)
4. We now need to tell TLC what it should verify. In the lower left-hand field, click on "Properties", then "Add" and enter AB!ABCSpec as the property to check.
5. Now, we need to constrain the state space so that TLC respects the bounds on the queues. In the tab "Advanced Options", click on "State Constraint" and enter SeqConstraint.
6. Click on the green triangle in order to launch TLC. It should compute the state space, check the property and should display "No errors" after it stops. With my choices above, I get a diameter of 12, 3740 states found, and 528 distinct states.
If you use TLC from the command line and you are new to TLC, get the Toolbox. If you still use the command line, the instructions above and the book "Specifying Systems" should be enough to tell you how to successfully run TLC.
Hope this helps,
Stephan
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 specifi cation. In fact, it is typical in practice that we are called upon to check the correctness of a system
design without any formal specifi cation of what the system is supposed to do. In that case, we can write an ex-post facto specifi cation. Module ABCorrectness
in Figure 14.4 on the next page is such a specifi cation 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
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...@googlegroups.com.
Visit this group at
https://groups.google.com/group/tlaplus.
For more options, visit
https://groups.google.com/d/optout.
-- 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.<MCAlternatingBit.tla><ABCorrectness.tla><AlternatingBit.tla><PrintValues.tla>