MODULE CELL(xpos,inSLP,initwg,initen,intihh,initptc,initci,WGleft,WGright,WGtop,WGbottom,WGlefttop,WGrighttop,WGbottomleft,WGbottomright,HHleft,HHright,HHtop,HHbottom,HHlefttop,HHrighttop,HHbottomleft,HHbottomright,hhleft,hhright,hhtop,hhbottom,hhlefttop,hhrighttop,hhbottomleft,hhbottomright) 
 VAR 
	 SLP :boolean; 
	 wg : boolean;
	 WG : boolean;
	 en : boolean;
	 EN : boolean;
	 hh : boolean;
	 HH : boolean;
	 ptc : boolean;
	 PTC : boolean;
	 PH : boolean;
	 SMO : boolean;
	 ci : boolean;
	 CI : boolean;
	 CIA : boolean;
	 CIR : boolean;
 ASSIGN 
	 init(SLP) := inSLP; 
	 init(WG)  := 0;
	 init(EN)  := 0;
	 init(HH)  := 0;
	 init(PTC) := 0;
	 init(PH)  := 0;
	 init(SMO) := 0;
	 init(CI)  := 0;
	 init(CIA) := 0;
	 init(CIR) := 0;
	 next(SLP) := inSLP; 
	 next(wg) := (CIA & inSLP & !CIR)|(wg & (CIA|inSLP) & !CIR);
	 next(WG) := wg;
	 next(en) := !inSLP & (WGleft|WGright|WGtop|WGbottom|WGlefttop|WGrighttop|WGbottomleft|WGbottomright) ;
	 next(EN) := en;
	 next(HH) := hh;
	 next(ptc) := CIA & !EN & !CIR;
	 next(PTC) := ptc |(PTC & !HHleft & !HHright & !HHtop & !HHbottom & !HHlefttop & !HHrighttop & !HHbottomleft & !HHbottomright);
	 next(PH) := PTC & (HHleft | HHright | HHtop | HHbottom | HHlefttop | HHrighttop | HHbottomleft & HHbottomright);
	 next(SMO) := !PTC|HHleft | HHright | HHtop | HHbottom | HHlefttop | HHrighttop | HHbottomleft | HHbottomright;
	 next(ci) := !EN;
	 next(CI) := ci;
	 next(CIA) := CI & (SMO | hhleft |hhright|hhtop|hhbottom|hhlefttop|hhrighttop|hhbottomleft|hhbottomright);
	 next(CIR) := CI & !SMO &!hhleft &!hhright&!hhtop&!hhbottom&!hhlefttop&!hhrighttop&!hhbottomleft&!hhbottomright;
 TRANS 
	 next(hh) = 0 | next(hh) = 1 
 DEFINE
	 p1_1 := !wg&!WG& en& EN& hh& HH&!ptc&!PTC&!PH& SMO&!ci&!CI&!CIA&!CIR;
	 p1_2 := !wg&!WG&!en& EN&!hh&!HH& ptc& PTC& PH& SMO& ci& CI& CIA&!CIR;
	 p1_3 := !wg&!WG&!en&!EN&!hh&!HH&!ptc& PTC&!PH&!SMO& ci& CI&!CIA& CIR;
	 p1_4 :=  wg& WG&!en&!EN&!hh&!HH& ptc& PTC& PH& SMO& ci& CI& CIA&!CIR;
	 p2_1 := !wg&!WG& en& EN& hh& HH&!ptc&!PTC&!PH& SMO&!ci&!CI&!CIA&!CIR;
	 p2_2 := !wg&!WG& en& EN& hh& HH&!ptc&!PTC&!PH& SMO&!ci&!CI&!CIA&!CIR;
	 p2_3 :=  wg& WG&!en&!EN&!hh&!HH& ptc& PTC& PH& SMO& ci& CI& CIA&!CIR;
	 p2_4 :=  wg& WG&!en&!EN&!hh&!HH& ptc& PTC& PH& SMO& ci& CI& CIA&!CIR;

MODULE COUNTER
 VAR
	 CT:0..6;
 ASSIGN
	 init(CT) :=0;
	 next(CT) :=((CT+1) mod 7);

MODULE main
 VAR
	cell1_1  : CELL(1,FALSE,FALSE,TRUE,TRUE,FALSE,FALSE,cell4_1.WG,cell2_1.WG,cell1_4.WG,cell1_2.WG,cell4_4.WG,cell2_4.WG,cell4_2.WG,cell2_2.WG,cell4_1.HH,cell2_1.HH,cell1_4.HH,cell1_2.HH,cell4_4.HH,cell2_4.HH,cell4_2.HH,cell2_2.HH,cell4_1.hh,cell2_1.hh,cell1_4.hh,cell1_2.hh,cell4_4.hh,cell2_4.hh,cell4_2.hh,cell2_2.hh);
	cell1_2  : CELL(2,FALSE,FALSE,FALSE,FALSE,TRUE,TRUE,cell4_2.WG,cell2_2.WG,cell1_1.WG,cell1_3.WG,cell4_1.WG,cell2_1.WG,cell4_3.WG,cell2_3.WG,cell4_2.HH,cell2_2.HH,cell1_1.HH,cell1_3.HH,cell4_1.HH,cell2_1.HH,cell4_3.HH,cell2_3.HH,cell4_2.hh,cell2_2.hh,cell1_1.hh,cell1_3.hh,cell4_1.hh,cell2_1.hh,cell4_3.hh,cell2_3.hh);
	cell1_3  : CELL(3,TRUE,FALSE,FALSE,FALSE,TRUE,TRUE,cell4_3.WG,cell2_3.WG,cell1_2.WG,cell1_4.WG,cell4_2.WG,cell2_2.WG,cell4_4.WG,cell2_4.WG,cell4_3.HH,cell2_3.HH,cell1_2.HH,cell1_4.HH,cell4_2.HH,cell2_2.HH,cell4_4.HH,cell2_4.HH,cell4_3.hh,cell2_3.hh,cell1_2.hh,cell1_4.hh,cell4_2.hh,cell2_2.hh,cell4_4.hh,cell2_4.hh);
	cell1_4  : CELL(4,TRUE,TRUE,FALSE,FALSE,TRUE,TRUE,cell4_4.WG,cell2_4.WG,cell1_3.WG,cell1_1.WG,cell4_3.WG,cell2_3.WG,cell4_1.WG,cell2_1.WG,cell4_4.HH,cell2_4.HH,cell1_3.HH,cell1_1.HH,cell4_3.HH,cell2_3.HH,cell4_1.HH,cell2_1.HH,cell4_4.hh,cell2_4.hh,cell1_3.hh,cell1_1.hh,cell4_3.hh,cell2_3.hh,cell4_1.hh,cell2_1.hh);
	cell2_1  : CELL(1,FALSE,FALSE,TRUE,TRUE,FALSE,FALSE,cell1_1.WG,cell3_1.WG,cell2_4.WG,cell2_2.WG,cell1_4.WG,cell3_4.WG,cell1_2.WG,cell3_2.WG,cell1_1.HH,cell3_1.HH,cell2_4.HH,cell2_2.HH,cell1_4.HH,cell3_4.HH,cell1_2.HH,cell3_2.HH,cell1_1.hh,cell3_1.hh,cell2_4.hh,cell2_2.hh,cell1_4.hh,cell3_4.hh,cell1_2.hh,cell3_2.hh);
	cell2_2  : CELL(2,FALSE,FALSE,FALSE,FALSE,TRUE,TRUE,cell1_2.WG,cell3_2.WG,cell2_1.WG,cell2_3.WG,cell1_1.WG,cell3_1.WG,cell1_3.WG,cell3_3.WG,cell1_2.HH,cell3_2.HH,cell2_1.HH,cell2_3.HH,cell1_1.HH,cell3_1.HH,cell1_3.HH,cell3_3.HH,cell1_2.hh,cell3_2.hh,cell2_1.hh,cell2_3.hh,cell1_1.hh,cell3_1.hh,cell1_3.hh,cell3_3.hh);
	cell2_3  : CELL(3,TRUE,FALSE,FALSE,FALSE,TRUE,TRUE,cell1_3.WG,cell3_3.WG,cell2_2.WG,cell2_4.WG,cell1_2.WG,cell3_2.WG,cell1_4.WG,cell3_4.WG,cell1_3.HH,cell3_3.HH,cell2_2.HH,cell2_4.HH,cell1_2.HH,cell3_2.HH,cell1_4.HH,cell3_4.HH,cell1_3.hh,cell3_3.hh,cell2_2.hh,cell2_4.hh,cell1_2.hh,cell3_2.hh,cell1_4.hh,cell3_4.hh);
	cell2_4  : CELL(4,TRUE,TRUE,FALSE,FALSE,TRUE,TRUE,cell1_4.WG,cell3_4.WG,cell2_3.WG,cell2_1.WG,cell1_3.WG,cell3_3.WG,cell1_1.WG,cell3_1.WG,cell1_4.HH,cell3_4.HH,cell2_3.HH,cell2_1.HH,cell1_3.HH,cell3_3.HH,cell1_1.HH,cell3_1.HH,cell1_4.hh,cell3_4.hh,cell2_3.hh,cell2_1.hh,cell1_3.hh,cell3_3.hh,cell1_1.hh,cell3_1.hh);
	cell3_1  : CELL(1,FALSE,FALSE,TRUE,TRUE,FALSE,FALSE,cell2_1.WG,cell4_1.WG,cell3_4.WG,cell3_2.WG,cell2_4.WG,cell4_4.WG,cell2_2.WG,cell4_2.WG,cell2_1.HH,cell4_1.HH,cell3_4.HH,cell3_2.HH,cell2_4.HH,cell4_4.HH,cell2_2.HH,cell4_2.HH,cell2_1.hh,cell4_1.hh,cell3_4.hh,cell3_2.hh,cell2_4.hh,cell4_4.hh,cell2_2.hh,cell4_2.hh);
	cell3_2  : CELL(2,FALSE,FALSE,FALSE,FALSE,TRUE,TRUE,cell2_2.WG,cell4_2.WG,cell3_1.WG,cell3_3.WG,cell2_1.WG,cell4_1.WG,cell2_3.WG,cell4_3.WG,cell2_2.HH,cell4_2.HH,cell3_1.HH,cell3_3.HH,cell2_1.HH,cell4_1.HH,cell2_3.HH,cell4_3.HH,cell2_2.hh,cell4_2.hh,cell3_1.hh,cell3_3.hh,cell2_1.hh,cell4_1.hh,cell2_3.hh,cell4_3.hh);
	cell3_3  : CELL(3,TRUE,FALSE,FALSE,FALSE,TRUE,TRUE,cell2_3.WG,cell4_3.WG,cell3_2.WG,cell3_4.WG,cell2_2.WG,cell4_2.WG,cell2_4.WG,cell4_4.WG,cell2_3.HH,cell4_3.HH,cell3_2.HH,cell3_4.HH,cell2_2.HH,cell4_2.HH,cell2_4.HH,cell4_4.HH,cell2_3.hh,cell4_3.hh,cell3_2.hh,cell3_4.hh,cell2_2.hh,cell4_2.hh,cell2_4.hh,cell4_4.hh);
	cell3_4  : CELL(4,TRUE,TRUE,FALSE,FALSE,TRUE,TRUE,cell2_4.WG,cell4_4.WG,cell3_3.WG,cell3_1.WG,cell2_3.WG,cell4_3.WG,cell2_1.WG,cell4_1.WG,cell2_4.HH,cell4_4.HH,cell3_3.HH,cell3_1.HH,cell2_3.HH,cell4_3.HH,cell2_1.HH,cell4_1.HH,cell2_4.hh,cell4_4.hh,cell3_3.hh,cell3_1.hh,cell2_3.hh,cell4_3.hh,cell2_1.hh,cell4_1.hh);
	cell4_1  : CELL(1,FALSE,FALSE,TRUE,TRUE,FALSE,FALSE,cell3_1.WG,cell1_1.WG,cell4_4.WG,cell4_2.WG,cell3_4.WG,cell1_4.WG,cell3_2.WG,cell1_2.WG,cell3_1.HH,cell1_1.HH,cell4_4.HH,cell4_2.HH,cell3_4.HH,cell1_4.HH,cell3_2.HH,cell1_2.HH,cell3_1.hh,cell1_1.hh,cell4_4.hh,cell4_2.hh,cell3_4.hh,cell1_4.hh,cell3_2.hh,cell1_2.hh);
	cell4_2  : CELL(2,FALSE,FALSE,FALSE,FALSE,TRUE,TRUE,cell3_2.WG,cell1_2.WG,cell4_1.WG,cell4_3.WG,cell3_1.WG,cell1_1.WG,cell3_3.WG,cell1_3.WG,cell3_2.HH,cell1_2.HH,cell4_1.HH,cell4_3.HH,cell3_1.HH,cell1_1.HH,cell3_3.HH,cell1_3.HH,cell3_2.hh,cell1_2.hh,cell4_1.hh,cell4_3.hh,cell3_1.hh,cell1_1.hh,cell3_3.hh,cell1_3.hh);
	cell4_3  : CELL(3,TRUE,FALSE,FALSE,FALSE,TRUE,TRUE,cell3_3.WG,cell1_3.WG,cell4_2.WG,cell4_4.WG,cell3_2.WG,cell1_2.WG,cell3_4.WG,cell1_4.WG,cell3_3.HH,cell1_3.HH,cell4_2.HH,cell4_4.HH,cell3_2.HH,cell1_2.HH,cell3_4.HH,cell1_4.HH,cell3_3.hh,cell1_3.hh,cell4_2.hh,cell4_4.hh,cell3_2.hh,cell1_2.hh,cell3_4.hh,cell1_4.hh);
	cell4_4  : CELL(4,TRUE,TRUE,FALSE,FALSE,TRUE,TRUE,cell3_4.WG,cell1_4.WG,cell4_3.WG,cell4_1.WG,cell3_3.WG,cell1_3.WG,cell3_1.WG,cell1_1.WG,cell3_4.HH,cell1_4.HH,cell4_3.HH,cell4_1.HH,cell3_3.HH,cell1_3.HH,cell3_1.HH,cell1_1.HH,cell3_4.hh,cell1_4.hh,cell4_3.hh,cell4_1.hh,cell3_3.hh,cell1_3.hh,cell3_1.hh,cell1_1.hh);
	CT  : COUNTER; 
LTLSPEC  !F (cell1_1.p1_1= 1& cell1_1.p1_1 = 1& cell1_2.p1_2 = 1& cell1_3.p1_3 = 1& cell1_4.p1_4 = 1& cell2_1.p1_1 = 1& cell2_2.p1_2 = 1& cell2_3.p1_3 = 1& cell2_4.p1_4 = 1& cell3_1.p1_1 = 1& cell3_2.p1_2 = 1& cell3_3.p1_3 = 1& cell3_4.p1_4 = 1& cell4_1.p1_1 = 1& cell4_2.p1_2 = 1& cell4_3.p1_3 = 1& cell4_4.p1_4 = 1& CT.CT = 6)