model barber4 {




var 
  barber ,
  chair ,
  open ,
  p1 ,
  p2 ,
  p3 ,
  p4 ,
  p5 ;


states normal;

 
transition t1  :=  {
	from :=normal;
	to:=normal;
	guard :=  p1 = 0 && barber > 0
	;
	action := 
        barber' = barber-1,
        chair' = chair+1,
        p1' = 1
	;
};

transition t2 :=  {
	from :=normal;
	to:=normal;
	guard :=  p1 = 1 && open > 0
	;
	action := 
        open' = open-1,
        p1' = 0
	;
};

transition t3  :=  {
	from :=normal;
	to:=normal;
	guard :=  p2 = 0 && barber > 0
	;
	action := 
        barber' = barber-1,
        chair' = chair+1,
        p2' = 1
	;
};

transition t4  :=  {
	from :=normal;
	to:=normal;
	guard :=  p2 = 1 && open > 0
	;
	action := 
        open' = open-1,
        p2' = 0
	;
};

transition t5  :=  {
	from :=normal;
	to:=normal;
	guard :=  p3 = 0 && barber > 0
	;
	action := 
        barber' = barber-1,
        chair' = chair+1,
        p3' = 1
	;
};

transition t6 :=  {
	from :=normal;
	to:=normal;
	guard :=  p3 = 1 && open > 0
	;
	action := 
        open' = open-1,
        p3' = 0
	;
};

transition t7  :=  {
	from :=normal;
	to:=normal;
	guard :=  p4 = 0 && barber > 0
	;
	action := 
        barber' = barber-1,
        chair' = chair+1,
        p4' = 1
	;
};

transition t8  :=  {
	from :=normal;
	to:=normal;
	guard := p4 = 1 && open > 0
	;
	action := 
        open' = open-1,
        p4' = 0
	;
};

transition t9  :=  {
	from :=normal;
	to:=normal;
	guard := p5 = 0
	;
	action := 
        barber' = barber+1,
        p5' = 1
	;
};

transition t10  :=  {
	from :=normal;
	to:=normal;
	guard :=  p5 = 1 && chair > 0
	;
	action := 
        chair' = chair-1,
        p5' = 2
	;
};

transition t11  :=  {
	from :=normal;
	to:=normal;
	guard :=  p5 = 2
	;
	action := 
        open' = open+1,
        p5' = 3
	;
};

transition t12  :=  {
	from :=normal;
	to:=normal;
	guard :=  p5 = 3 && open = 0
	;
	action := 
        p5' = 0
	;
};

}

strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{state=normal && barber=0 && chair=0 && open=0 && p1=0 &&  p2=0 &&  p3=0 &&
	 p4=0 &&  p5=0 };

Transitions t := {t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12};

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

	
}