model main {

  var x, y, z;

  states start, lbl_7_1, stop;

  transition t_14 := {
    from   := start;
    to     := lbl_7_1;
    guard  := 1 <= z;
    action := x' = x + 1, y' = y - 1, z' = z - 1;
  };

  transition t_13 := {
    from   := start;
    to     := stop;
    guard  := z <= 0;
    action := ;
  };

  transition t_11 := {
    from   := lbl_7_1;
    to     := stop;
    guard  := z <= 0;
    action := ;
  };

  transition t_12 := {
    from   := lbl_7_1;
    to     := lbl_7_1;
    guard  := 1 <= z;
    action := x' = x + 1, y' = y - 1, z' = z - 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

{ lbl_7_1[v1, v2, v3] : v3 >= 0; stop[v1, v2, v3] : v3 <= 0 }