model main {

  var i, j, n, tmp;

  states start, lbl_13_1, lbl_9_1, lbl_14_2, stop;

  transition t_40 := {
    from   := start;
    to     := lbl_13_1;
    guard  := 1 <= n;
    action := i' = n, j' = 1;
  };

  transition t_39 := {
    from   := start;
    to     := lbl_9_1;
    guard  := 1 <= n;
    action := i' = n, j' = 0, tmp' = ?;
  };

  transition t_38 := {
    from   := start;
    to     := lbl_14_2;
    guard  := 0 = n;
    action := i' = n - 1, j' = 0;
  };

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

  transition t_33 := {
    from   := lbl_13_1;
    to     := lbl_9_1;
    guard  := j + 1 <= i;
    action := tmp' = ?;
  };

  transition t_32 := {
    from   := lbl_13_1;
    to     := lbl_14_2;
    guard  := i <= j;
    action := i' = i - 1;
  };

  transition t_34 := {
    from   := lbl_13_1;
    to     := lbl_13_1;
    guard  := j + 1 <= i;
    action := j' = j + 1;
  };

  transition t_25 := {
    from   := lbl_9_1;
    to     := lbl_13_1;
    guard  := true;
    action := j' = j + 1;
  };

  transition t_37 := {
    from   := lbl_14_2;
    to     := lbl_13_1;
    guard  := 1 <= i;
    action := j' = 1;
  };

  transition t_36 := {
    from   := lbl_14_2;
    to     := lbl_9_1;
    guard  := 1 <= i;
    action := j' = 0, tmp' = ?;
  };

  transition t_28 := {
    from   := lbl_14_2;
    to     := stop;
    guard  := i + 1 <= 0;
    action := ;
  };

  transition t_35 := {
    from   := lbl_14_2;
    to     := lbl_14_2;
    guard  := 0 = i;
    action := i' = i - 1, j' = 0;
  };

}

strategy main_s {

  Region init := {state = start};

}

{ lbl_13_1[v1, v2, v3, v4] : v2 >= 1 and v2 <= v1 and v3 >= v1; stop[v1, v2, v3, v4] : v3 >= v1 and v1 <= -1; lbl_14_2[v1, 1 + v1, v3, v4] : v3 >= 1 + v1 and v1 >= -1; lbl_9_1[v1, v2, v3, v4] : v3 >= v1 and v2 >= 0 and v2 <= -1 + v1 }