model gonnord_thesis_93b {

  var x, z;

  states q;

  transition t2 := {
    from   := q;
    to     := q;
    guard  := true;
    action := z' = 0;
  };

  transition t1 := {
    from   := q;
    to     := q;
    guard  := x >= 2 * z;
    action := x' = x + 1, z' = z + 1;
  };

}

strategy gonnord_thesis_93b_s {

  Region init := {state = q && x = 0 && z = 0};

}

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