model hal79 {

var i,j;

states zero,one,two;

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

};

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

transition t2 := {
 from   := one;
 to     := one;
 guard  := i<=100;
 action := i'=i+2,j'=j+1;
};

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

strategy s1 {

Region init := {state=zero && i=0 && j=2};

//pas de region bad
}