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