model henry_gdrgpl_19 {

  var x, d;

  states k;

  transition t3 := {
    from   := k;
    to     := k;
    guard  := x = 1000;
    action := d' = -1, x' = x + d;
  };

  transition t2 := {
    from   := k;
    to     := k;
    guard  := 1 <= x && x <= 999;
    action := x' = x + d;
  };

  transition t1 := {
    from   := k;
    to     := k;
    guard  := x = 0;
    action := d' = 1, x' = x + d;
  };

}

strategy henry_gdrgpl_19_s {

  Region init := {state = k && x = 0 && d = 1};

}

{ k[v1, v2] : v2 <= 1 and v2 >= -1 and v1 >= 0 and v2 >= -1999 + 2v1 }