model main {

  var x, y;

  states start, lbl_9_1, lbl_8_1, stop;

  transition t_25 := {
    from   := start;
    to     := lbl_9_1;
    guard  := y + 3 <= x && 0 <= y;
    action := y' = y + 1;
  };

  transition t_24 := {
    from   := start;
    to     := lbl_8_1;
    guard  := x + 3 <= y && 0 <= x;
    action := x' = x + 1;
  };

  transition t_23 := {
    from   := start;
    to     := stop;
    guard  := x <= y + 2 && 0 <= x && y <= x + 2 && 0 <= y;
    action := ;
  };

  transition t_13 := {
    from   := start;
    to     := stop;
    guard  := x + 1 <= 0 || y + 1 <= 0;
    action := ;
  };

  transition t_21 := {
    from   := lbl_9_1;
    to     := lbl_8_1;
    guard  := x + 3 <= y;
    action := x' = x + 1;
  };

  transition t_20 := {
    from   := lbl_9_1;
    to     := stop;
    guard  := x <= y + 2 && y <= x + 2;
    action := ;
  };

  transition t_22 := {
    from   := lbl_9_1;
    to     := lbl_9_1;
    guard  := y + 3 <= x;
    action := y' = y + 1;
  };

  transition t_19 := {
    from   := lbl_8_1;
    to     := lbl_9_1;
    guard  := y + 3 <= x;
    action := y' = y + 1;
  };

  transition t_17 := {
    from   := lbl_8_1;
    to     := stop;
    guard  := x <= y + 2 && y <= x + 2;
    action := ;
  };

  transition t_18 := {
    from   := lbl_8_1;
    to     := lbl_8_1;
    guard  := x + 3 <= y;
    action := x' = x + 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

{ lbl_9_1[v1, v2] : v2 <= -2 + v1 and v2 >= 1; lbl_8_1[v1, v2] : v1 >= 1 and v2 >= 2 + v1 }