module ChannelC {
  var buffer : [int]boolean;
  // Simulate unreliable behavior.
}

module ChannelD {
  var buffer : [int]boolean;
  // Perfect transmission.
}

module Sender {
  var current_message : int;
  var control_bit : boolean;
  var waiting_for_ack : boolean;
  // Send and retransmit logic.
}

module Receiver {
  var last_received_control_bit : boolean;
  // Receive message and send acknowledgement.
}

module main {
  instance S : Sender;
  instance R : Receiver;
  instance c : ChannelC;
  instance d : ChannelD;

  // main interaction logic.
}

control {
  // Model checking settings.
}
