model main {

  var tx, x, y;

  states start, lbl_10_1, lbl_9_1, stop;

  transition t_37 := {
    from   := start;
    to     := lbl_10_1;
    guard  := 0 <= tx && y <= x;
    action := y' = tx + y + 1;
  };

  transition t_36 := {
    from   := start;
    to     := lbl_9_1;
    guard  := 0 <= tx && y <= x;
    action := x' = x - tx - 1;
  };

  transition t_34 := {
    from   := start;
    to     := stop;
    guard  := 0 <= tx && x + 1 <= y;
    action := ;
  };

  transition t_21 := {
    from   := start;
    to     := stop;
    guard  := tx + 1 <= 0;
    action := ;
  };

  transition t_32 := {
    from   := lbl_10_1;
    to     := lbl_9_1;
    guard  := 0 <= tx && y <= x;
    action := x' = x - tx - 1;
  };

  transition t_31 := {
    from   := lbl_10_1;
    to     := stop;
    guard  := tx + 1 <= 0 && y <= x;
    action := ;
  };

  transition t_30 := {
    from   := lbl_10_1;
    to     := stop;
    guard  := x + 1 <= y;
    action := ;
  };

  transition t_33 := {
    from   := lbl_10_1;
    to     := lbl_10_1;
    guard  := 0 <= tx && y <= x;
    action := y' = tx + y + 1;
  };

  transition t_29 := {
    from   := lbl_9_1;
    to     := lbl_10_1;
    guard  := 0 <= tx && y <= x;
    action := y' = tx + y + 1;
  };

  transition t_27 := {
    from   := lbl_9_1;
    to     := stop;
    guard  := tx + 1 <= 0 && y <= x;
    action := ;
  };

  transition t_26 := {
    from   := lbl_9_1;
    to     := stop;
    guard  := x + 1 <= y;
    action := ;
  };

  transition t_28 := {
    from   := lbl_9_1;
    to     := lbl_9_1;
    guard  := 0 <= tx && y <= x;
    action := x' = x - tx - 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

{ lbl_10_1[v1, v2, v3] : v3 <= 1 + v1 + v2 and v1 >= 0; lbl_9_1[v1, v2, v3] : v3 <= 1 + v1 + v2 and v1 >= 0 }