model esop2{

var i, j;

states l1,l3,l4;

transition t0 := {
 from   := l1;
 to     := l3;
 guard  := true;
 action := i'=i+2,j'=j-1;
};

transition t1 := {
 from   := l3;
 to     := l4;
 guard  := true;
 action := i'=i+2, j'=j-1;
};

transition t2 := {
 from   := l3;
 to     := l4;
 guard  := true;
 action := i'=i+2, j'=j-1;
};

transition t3 := {
 from   := l4;
 to     := l4;
 guard  := i<=j;
 action := i'=i+2, j'=j-1;
};



}

strategy s1 {

Region init := {state=l1 && i=1 && j=10};
Transitions ttt := {t0,t1,t2,t3};
Region reach := post*(init, ttt,1);


}
//source = http://www.di.ens.fr/~goubault/GOUBAULTpapers.html