---- MODULE MeolicVaja7MC ----

EXTENDS MeolicVaja7

CONSTANTS
  msgQLen,ackQLen,sbuffLen,rbuffLen

Constraint ==
  /\ Len(msgQ) <= msgQLen
  /\ Len(ackQ) <= ackQLen
  /\ Len(sbuff) <= sbuffLen
  /\ Len(rbuff) <= rbuffLen

====