CONSTANTS
  Data = {d1,d2}
  msgQLen = 2
  ackQLen = 2
  sbuffLen = 3
  rbuffLen = 3

SPECIFICATION AlternatingBit
CONSTRAINT Constraint

INVARIANT TypeInv
INVARIANT Reliable