model main {

  var i, j, k, tmp;

  states start, lbl_7_1, stop;

  transition t_17 := {
    from   := start;
    to     := lbl_7_1;
    guard  := i <= 100 && j <= k;
    action := i' = j, j' = i + 1, k' = k - 1, tmp' = i;
  };

  transition t_16 := {
    from   := start;
    to     := stop;
    guard  := 101 <= i || k + 1 <= j;
    action := ;
  };

  transition t_14 := {
    from   := lbl_7_1;
    to     := stop;
    guard  := 101 <= i || k + 1 <= j;
    action := ;
  };

  transition t_15 := {
    from   := lbl_7_1;
    to     := lbl_7_1;
    guard  := i <= 100 && j <= k;
    action := i' = j, j' = i + 1, k' = k - 1, tmp' = i;
  };

}

strategy main_s {

  Region init := {state = start};

}