module ConcurrentProgram {
  var options: ??;
  var dec_x: integer;
  var inc_x: integer;
  var nondet_1: integer;
  var reset_x: integer;
  var x: integer;

  init {
    x = 0;

  }
  next {
    nondet_1' = x;
    if (x < 200) {
      inc_x' = (x + 1);
    } else {
      inc_x' = x;
    }
    if (x > 0) {
      dec_x' = (x - 1);
    } else {
      dec_x' = x;
    }
    if (x == 200) {
      reset_x' = 0;
    } else {
      reset_x' = x;
    }

  }
  invariant spec: ((0 <= x) && (x <= 200));

}
