model hal79b {

var x,y;

states zero,one,two;

transition t0 := {
 from := zero;
 to := one;
 guard :=true;
 action := x'=0,y'=0;

};

transition t1 := {
 from   := one;
 to     := one;
 guard  := x<=100;
 action := x'=x+2;
};

transition t2 := {
 from   := one;
 to     := one;
 guard  := x<=100;
 action := x'=x+1,y'=y+1;
};

transition t3 := {
 from   := one;
 to     := two;
 guard  := x>100;
 action := x'=x;
};
}

strategy s1 {

Region init := {state=zero};

//pas de region bad
}