model bardin_thesis_041 {

  var x, y;

  states q1, q2;

  transition t3 := {
    from   := q1;
    to     := q2;
    guard  := x >= y;
    action := ;
  };

  transition t1 := {
    from   := q1;
    to     := q1;
    guard  := x >= 0;
    action := x' = x + 2;
  };

  transition t4 := {
    from   := q2;
    to     := q1;
    guard  := true;
    action := x' = x - y;
  };

  transition t2 := {
    from   := q2;
    to     := q2;
    guard  := true;
    action := x' = x + 1, y' = y + 1;
  };

}

strategy bardin_thesis_041_s {

  Region init := {state = q1 && x >= 0};

}