model debug6 {

var  t,a;

states loc1;

transition t1 := {
 from   := loc1;
 to     := loc1;
 guard  := t<=4;
 action := t'=a,a'=t+1;
};

}

strategy s1 {

Region init := {state=loc1 && t=0 && a=2};
Transitions ttt := {t1};
Region reach := post*(init, ttt,1);

}

  // invar  = 

// avec delay 4 loc1 - > > {t+2a>=4,t+2>=a,$>=0,t<=a+1,1>0,a<=5} (6it)
// NH + upto loc1 - > > {t+2a>=4,t>=0,a<=5,1>0,$>=0} (4it)
// reps attrvertex = {a<=5,$>=0,1>0,a>=1,t>=0,t+2a>=4} (5it)
//accel =     = {t+2>=a,1>0,t+2a<=16,t<=a+1,t+2a>=4,$>=0} 1it
//ce qui est vrai !!
// nh + nouptos = loc1 - > > {$>=0,t+2a>=4,1>0,t>=0} idem bhrz...
// sriram = t+a-2>=0, a<=5