module RingModule {
  var id: bv32;
  var m: bv32;
  var stopped: boolean;

  input incoming_m: bv32;

  output output_m: bv32;

  init {
    stopped = false;

  }
  next {
    if (!stopped) {
      if (m == id) {
        stopped' = true;
      } else {
        if (m > id) {
          output_m' = m;
        } else {
          output_m' = id;
        }
      }
    }
    m' = incoming_m;

  }
  invariant spec: (if (stopped) then (m == id) else true);

}
