model review4 {

var i,j,a,k,k1,i0;

states s1,s2,out;

transition t1 := {
 from   := s1;
 to     := s2;
 guard  := i<5;
 action :=  j'=0,a'=a,i'=i,k'=k+1,k1'=k1;// 
};

transition t2 := {
 from   := s2;
 to     := s1;
 guard  :=  j=10 ;
 action :=  i'=i+1,a'=a,j'=j,k'=k,k1'=k1;// 
};

transition t4 := {
 from   := s2;
 to     := s2;
 guard  :=  j<=9 && i<=2 ;
 action :=  j'=j+1,a'=a,i'=i,k'=k,k1'=k1;// 
};

transition t5 := {
 from   := s2;
 to     := s2;
 guard  :=  j<=9 && i>2 ;
 action :=  a'=a+2,j'=j+1,i'=i,k'=k,k1'=k1+1;// 
};

transition tout := {
 from   := s1;
 to     := out;
 guard  :=  i=5 &&j=10;
 action :=  i'=i,j'=j,a'=a,k'=k,k1'=k1;// 
};



}

strategy s1 {

Region init := {state = s1 && 0=i &&  i=i0 && 0<=a && a<=5 &&k=0 &&k1=0 && j=0};
//Region bad := {state=out && k1<20};
}