model apache1 {

var c, tk_sz;

states s1;

transition t1 := {
 from   := s1;
 to     := s1;
 guard  := c<tk_sz -1;
 action := tk_sz'=tk_sz,c'=c+1;
};

transition t2 := {
 from   := s1;
 to     := s1;
 guard  := c<tk_sz -1;
 action := tk_sz'=tk_sz,c'=c;
};



}

strategy s1 {

Region init := {state=s1 && tk_sz>0 && c=0};
Transitions ttt := {t1,t2};
Region reach := post*(init, ttt,1);


//Region bad := {c>tk_sz}; 
}

//meme resultat a savoir bad = empty 68ms sans accel 65 avec accel 80ms pour reps