module LeaderElection {
  type Message = integer;

  var id: integer;
  var m: Message;

  input channel_in: Message;

  output channel_out: Message;

  init {
    channel_out = id;

  }
  next {
    if (m == id) {
    }
    if (m > id) {
      channel_out' = m;
    }

  }
}
