module main
{
  var x : int;

  process Inc
  {
    while true do
    {
      if x < 200 then
        x := x + 1;
      fi
    }
  }

  process Dec
  {
    while true do
    {
      if x > 0 then
        x := x - 1;
      fi
    }
  }

  process Reset
  {
    while true do
    {
      if x = 200 then
        x := 0;
      fi
    }
  }

  invariant x_between_0_and_200 : 0 <= x && x <= 200;
}
