module SendermainSystem {
  module Sender {
    var m : int; // message
    var b : bool; // control bit

    input send : bool; // signal to send message
    output c : int; // channel c

    init {
      m = 0;
      b = false;
      c = 0;
    }

    next {
      if (send) {
        c' = m;
      }
    }
  }

  module main {
    var m : int; // received message
    var b : bool; // received control bit
    var ack : bool; // acknowledgement

    input d : int; // channel d
    output receive : bool; // signal to receive message

    init {
      m = 0;
      b = false;
      ack = false;
      receive = false;
    }

    next {
      if (receive) {
        m' = d;
        b' = !b;
        ack' = b;
      }
    }
  }

  var c : int; // buffer for channel c
  var d : int; // buffer for channel d

  instance s : Sender(send, c);
  instance r : main(d, receive);

  init {
    c = 0;
    d = 0;
  }

  next {
    if (s.send) {
      d' = s.c;
    }

    if (r.receive) {
      c' = r.m;
    }
  }

  // Retransmission logic
  if (s.send && !r.receive) {
    s.send' = true;
  } else {
    s.send' = false;
  }
}
