model main {

  var ell, i, j, k;

  states start, lbl_7_2, stop;

  transition t_16 := {
    from   := start;
    to     := lbl_7_2;
    guard  := i <= 100 && j <= k;
    action := ell' = i, i' = j, j' = i + 1, k' = k - 1;
  };

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

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

  transition t_14 := {
    from   := lbl_7_2;
    to     := lbl_7_2;
    guard  := i <= 100 && j <= k;
    action := ell' = i, i' = j, j' = i + 1, k' = k - 1;
  };

}

strategy main_s {

  Region init := {state = start};

}