
module main
{
  var x : int;

  procedure action_A()
    modifies x;
  {
    x := 2 * x;
  }

  procedure action_B()
    modifies x;
  {
    x := x + 1;
  }

  init {
    x := 3;
  }

  next {
    either {
      call action_A();
    } or {
      call action_B();
    }
  }
}
