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
}