model esop2b {

var i, j;

states l1,l3;

transition t1 := {
 from   := l1;
 to     := l1;
 guard  := 100<=j && j<=i-1;
 action := i'=i,j'=j-2;
};

transition t2 := {
 from   := l1;
 to     := l1;
 guard  := 100<=j && j>i-1;
 action := i'=i+1, j'=j;
};


transition t3 := {
 from   := l1;
 to     := l3;
 guard  := j<100;
 action := i'=i, j'=j;
};

}
strategy s1 {

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

}


// sans accel = l1 - > > {j>=98,j<=175,1>0,$>=0,i<177} 
// l3 - > > {j>=98,j<100,1>0,$>=0,i<177} 
// 6 it, 77 ms

// reps = idem 69 ms, 7 it

// accel = 82 ms, 1 it