module main
{
  var x : integer; // shared variable

  proc Inc = while true do if x<200 then x:=x+1 fi od;
  proc Dec = while true do if x>0 then x:=x-1 fi od;
  proc Reset = while true do if x=200 then x:=0 fi od;

  init {
    x = 100;
  }

  next {
    next(Inc); next(Dec); next(Reset);
  }

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