model main {

  var n, x, y;

  states start, lbl_10_1, lbl_12_1, stop;

  transition t_35 := {
    from   := start;
    to     := lbl_10_1;
    guard  := 2 <= n;
    action := x' = n, y' = 2;
  };

  transition t_34 := {
    from   := start;
    to     := lbl_12_1;
    guard  := n <= 1 && 0 <= n;
    action := x' = n - 1, y' = 1;
  };

  transition t_22 := {
    from   := start;
    to     := stop;
    guard  := n + 1 <= 0;
    action := x' = n;
  };

  transition t_26 := {
    from   := lbl_10_1;
    to     := lbl_12_1;
    guard  := x <= y;
    action := x' = x - 1;
  };

  transition t_25 := {
    from   := lbl_10_1;
    to     := lbl_10_1;
    guard  := y + 1 <= x;
    action := y' = 2 * y;
  };

  transition t_31 := {
    from   := lbl_12_1;
    to     := lbl_10_1;
    guard  := 2 <= x;
    action := y' = 2;
  };

  transition t_29 := {
    from   := lbl_12_1;
    to     := stop;
    guard  := x + 1 <= 0;
    action := ;
  };

  transition t_30 := {
    from   := lbl_12_1;
    to     := lbl_12_1;
    guard  := x <= 1 && 0 <= x;
    action := x' = x - 1, y' = 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

{ lbl_12_1[v1, v2, v3] : v3 >= 1 and v2 >= -1 and v2 <= -1 + v1 and v3 >= 1 + v2; stop[v1, v2, v3] : v2 <= v1 and v2 <= -1; lbl_10_1[v1, v2, v3] : v3 >= 2 and v3 <= -2 + 2v2 and v2 <= v1 }