model ticket3i {



var p1 ,
    p2 ,
    p3,	
    t ,
    s ,
    a1 ,
    a2, 
    a3;

states normal;

 
transition t1  :=  {
	from :=normal;
	to:=normal;
	guard :=  p1 = 0
	;
	action := 
        a1' = t,
        t' = t+1,
        p1' = 1
	;
};

transition t2  :=  {
	from :=normal;
	to:=normal;
	guard :=  p1 = 1 && s >= a1
	;
	action := 
        p1' = 2
	;
};

transition t3  :=  {
	from :=normal;
	to:=normal;
	guard :=  p1 = 2
	;
	action := 
        s' = s+1,
        p1' = 0
	;
};

transition t4  :=  {
	from :=normal;
	to:=normal;
	guard :=  p2 = 0 
	;
	action :=         
	a2' = t,
        t' = t+1,
        p2' = 1
	;
};

transition t5  :=  {
	from :=normal;
	to:=normal;
	guard :=  p2 = 1 && s >= a2
	;
	action := 
        p2' = 2
	;
};

transition t6  :=  {
	from :=normal;
	to:=normal;
	guard :=  p2 = 2
	;
	action := 
        s'= s+1,
        p2' = 0
	;
};

transition t7  :=  {
	from :=normal;
	to:=normal;
	guard :=
  p3 = 0 
	;
	action := 
        a3' = t,
        t' = t+1,
        p3' = 1
	;
};

transition t8  :=  {
	from :=normal;
	to:=normal;
	guard :=
  p3 = 1 && s >= a3
	;
	action := 
        p3' = 2
	;
};

transition t9  :=  {
	from :=normal;
	to:=normal;
	guard :=
  p3 = 2
	;
	action := 
        s' = s+1,
        p3' = 0
	;
};


}


strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{state=normal && a1>=0 && a2>=0 && a3>=0 && t>=0 && s=t && p1=0 && p2=0 && p3=0};

Transitions tr := {t1,t2,t3,t4,t5,t6,t7,t8,t9};

Region reach := post*(init, tr);

	
}