model t4 {
var t__0, i, j, n;

states P,Q;

 transition t4 := {
  from   := P;
  to     := P;
  guard  := (0 <= n-i-1) && (j<=n-1);
  action := t__0'=j, i'=i+1,j'=j;
 };


 transition thop := {
  from   := P;
  to     := Q;
  guard  := true;
  action := i'=i;
 };




 transition t6 := {
  from   := Q;
  to     := Q;
  guard  := (i>=n) && (j<=n-1);
  action := t__0'=j+1, i'=1,j'=j+1;
 };

 transition thop2 := {
  from   := Q;
  to     := P;
  guard  := true;
  action := i'=i;
 };


}
strategy s1 {
Region init := {state = P && n>=0 && j=1 && i=1 && t__0 =1 };
Transitions ttt := {t4,thop,t6,thop2};
Region reach := post*(init, ttt,1);

}
//avec delay 3 invariant strictement + gros