model main {

  var N, j, k, m, tmp;

  states start, lbl_20_1, lbl_21_1, lbl_4_3, stop;

  transition t_79 := {
    from   := start;
    to     := lbl_20_1;
    guard  := 4 <= N;
    action := j' = 2, k' = 0, m' = 2;
  };

  transition t_78 := {
    from   := start;
    to     := lbl_21_1;
    guard  := 4 <= N;
    action := j' = N, k' = 0, m' = 2;
  };

  transition t_77 := {
    from   := start;
    to     := lbl_20_1;
    guard  := 3 <= N;
    action := j' = 1, k' = 0, m' = 1;
  };

  transition t_76 := {
    from   := start;
    to     := lbl_21_1;
    guard  := 3 <= N;
    action := j' = N, k' = 0, m' = 1;
  };

  transition t_51 := {
    from   := start;
    to     := stop;
    guard  := N <= 2;
    action := ;
  };

  transition t_63 := {
    from   := lbl_20_1;
    to     := lbl_21_1;
    guard  := 2 * j + k + 4 <= N;
    action := j' = N, m' = 2 * j + 2;
  };

  transition t_61 := {
    from   := lbl_20_1;
    to     := lbl_21_1;
    guard  := 2 * j + k + 3 <= N;
    action := j' = N, m' = 2 * j + 1;
  };

  transition t_60 := {
    from   := lbl_20_1;
    to     := lbl_4_3;
    guard  := N <= 2 * j + k + 2;
    action := k' = k + 1, tmp' = k;
  };

  transition t_64 := {
    from   := lbl_20_1;
    to     := lbl_20_1;
    guard  := 2 * j + k + 4 <= N;
    action := j' = 2 * j + 2, m' = 2 * j + 2;
  };

  transition t_62 := {
    from   := lbl_20_1;
    to     := lbl_20_1;
    guard  := 2 * j + k + 3 <= N;
    action := j' = 2 * j + 1, m' = 2 * j + 1;
  };

  transition t_69 := {
    from   := lbl_21_1;
    to     := lbl_20_1;
    guard  := 2 * j + k + 4 <= N;
    action := j' = 2 * j + 2, m' = 2 * j + 2;
  };

  transition t_67 := {
    from   := lbl_21_1;
    to     := lbl_20_1;
    guard  := 2 * j + k + 3 <= N;
    action := j' = 2 * j + 1, m' = 2 * j + 1;
  };

  transition t_65 := {
    from   := lbl_21_1;
    to     := lbl_4_3;
    guard  := N <= 2 * j + k + 2;
    action := k' = k + 1, tmp' = k;
  };

  transition t_68 := {
    from   := lbl_21_1;
    to     := lbl_21_1;
    guard  := 2 * j + k + 4 <= N;
    action := j' = N, m' = 2 * j + 2;
  };

  transition t_66 := {
    from   := lbl_21_1;
    to     := lbl_21_1;
    guard  := 2 * j + k + 3 <= N;
    action := j' = N, m' = 2 * j + 1;
  };

  transition t_74 := {
    from   := lbl_4_3;
    to     := lbl_20_1;
    guard  := k + 4 <= N;
    action := j' = 2, m' = 2;
  };

  transition t_73 := {
    from   := lbl_4_3;
    to     := lbl_21_1;
    guard  := k + 4 <= N;
    action := j' = N, m' = 2;
  };

  transition t_72 := {
    from   := lbl_4_3;
    to     := lbl_20_1;
    guard  := k + 3 <= N;
    action := j' = 1, m' = 1;
  };

  transition t_71 := {
    from   := lbl_4_3;
    to     := lbl_21_1;
    guard  := k + 3 <= N;
    action := j' = N, m' = 1;
  };

  transition t_56 := {
    from   := lbl_4_3;
    to     := stop;
    guard  := N <= k + 1;
    action := ;
  };

  transition t_70 := {
    from   := lbl_4_3;
    to     := lbl_4_3;
    guard  := k + 2 = N;
    action := j' = 0, k' = k + 1, m' = 0, tmp' = k;
  };

}

strategy main_s {

  Region init := {state = start};

}

{ lbl_20_1[v1, v2, v3, v2, v5] : v3 >= 0 and v3 <= -2 + v1 - v2 and v2 >= 1; lbl_21_1[v1, v1, v3, v4, v5] : v3 >= 0 and v4 <= -2 + v1 - v3 and v4 >= 1; lbl_4_3[v1, v2, v3, v4, -1 + v3] : 3v4 >= 3 - v1 + v2 and v4 <= -1 + v1 - v3 and v4 >= -1 + v1 - v2 - v3 and v3 >= 1 and v4 <= v2 and v2 <= v1 }