module CommunicationProtocol {
  type Bit = integer;

  var c: [integer]integer;
  var d: [integer]integer;
  var m: integer;
  var b: Bit;

  init {
    m = 0;
    b = 0;

  }
  next {
    if (c[m] == 1) {
      if (d[m] != b) {
        c' = c[m -> 1];
      } else {
        if (b == 0) {
          b' = 1;
        } else {
          b' = 0;
        }
      }
    }

  }
}
