model main {

  var i, n;

  states start, lbl_3_2, stop;

  transition t_9 := {
    from   := start;
    to     := lbl_3_2;
    guard  := 2 <= i;
    action := i' = i - 1;
  };

  transition t_8 := {
    from   := start;
    to     := stop;
    guard  := i <= 1;
    action := ;
  };

  transition t_6 := {
    from   := lbl_3_2;
    to     := stop;
    guard  := i <= 1;
    action := ;
  };

  transition t_7 := {
    from   := lbl_3_2;
    to     := lbl_3_2;
    guard  := 2 <= i;
    action := i' = i - 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

{ lbl_3_2[v1, v2] : v1 >= 1; stop[v1, v2] : v1 <= 1 }