model jeannet_thesis_111 {

  var x, y;

  states i, d;

  transition t2 := {
    from   := i;
    to     := d;
    guard  := x >= 10;
    action := x' = x + 1;
  };

  transition t1 := {
    from   := i;
    to     := i;
    guard  := x <= 9;
    action := x' = x + 1;
  };

  transition t4 := {
    from   := d;
    to     := i;
    guard  := x <= 5;
    action := x' = x - 1;
  };

  transition t3 := {
    from   := d;
    to     := d;
    guard  := x >= 6;
    action := x' = x - 1;
  };

}

strategy jeannet_thesis_111_s {

  Region init := {state = i && x = 0};

}