---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/MCAlternatingBit.tla
---
--------------------------- MODULE MCAlternatingBit ----------------------------
EXTENDS AlternatingBit
INSTANCE ABCorrectness
CONSTANTS msgQLen, ackQLen
SeqConstraint ==
/\ Len(msgQ) <= msgQLen
/\ Len(ackQ) <= ackQLen
SentLeadsToRcvd == \A d \in Data: (sent = d) /\ (sBit /= sAck) ~> (rcvd = d)
================================================================================
ImpliedAction == [ABCNext]_cvars
TNext == WF_msgQ(~ABTypeInv')
TProp == \A d \in Data : (sent = d) => [](sent = d)
CSpec == ABSpec /\ TNext
\* DataPerm == Permutations(Data)
==============================================================