#define inv ((((((c[0] == c[p0]) && (c[4] == c[p0+4])) || ((c[0] ==1) && (c[p0] == 0)))  &&  (((c[1] == c[p1]) && (c[5] == c[p1+4])) || ((c[1] ==1) && (c[p1] == 0)))  &&  (((c[2] == c[p2]) && (c[6] == c[p2+4])) || ((c[2] ==1) && (c[p2] == 0)))  && (((c[3] == c[p3]) && (c[7] == c[p3+4])) || ((c[3] ==1) && (c[p3] == 0))) )) && ((p0 ==0) && (p1 == 0) && (p2 == 0) && (p3 == 2)) )


#define safety0 (!Z0 || X0) 
#define safety0p (!Z0p || X0p) 

#define safety2 (!Z2 || X2)
#define safety2p (!Z2p || X2p)

#define safety3 (!Z3 || X3)
#define safety3p (!Z3p || X3p)


#define X0 (c[3] == 1) && ( c[1] == 1 ) && (c[2] == 1) && (c[0] == 1) && ( c[4] == 1 ) && ((p0 == 2 ) || (p0 == 1)) 
#define Z0 (y0 == 1)

#define X0p (c[7] == 0) && ( c[1] == 1 )  && (c[2] == 1) && (c[0] == 1) && ( c[4] == 1 ) && ((p0 == 2 ) || (p0 == 1))
#define Z0p (y0p == 1)


#define X2 (c[3] == 1) && (c[2] == 1) && (c[4] == 1) && (c[0] == 1)  && ((p0 == 2 ) || (p0 == 1)) 
#define Z2 (y2 ==1)

#define X2p (c[7] == 0) && (c[2] == 1) && (c[4] == 1) && (c[0] == 1)  && ((p0 == 2 ) || (p0 == 1)) 
#define Z2p (y2p == 1)


#define X3 (c[3] == 1) && (c[2] == 1)
#define Z3 (y3 ==1)

#define X3p (c[7] == 0) && (c[2] == 1)
#define Z3p (y3p ==1)


/*
 [] safety
 [] (!inv -> <> inv)
 [] (<> inv)
*/



bool c[8];  

bool y3 =0, y2=0, y3p=0, y2p=0, y0 =0, y0p =0;

/* the cells of this array represent c0, c1, c2, c3, sn0, sn1, sn2, sn3 in order

		//  c0  ---> c[0]
		//  c1  ---> c[1]
		//  c2  ---> c[2]
		//  c3  ---> c[3]
		//  sn0  ---> c[4]
		//  sn1  ---> c[5]
		//  sn2  ---> c[6]
		//  sn3  ---> c[7]

*/

int p0 = 0;
int p1 = 0;
int p2 = 0;
int p3 = 2;




proctype  P0() {

do
:: atomic{ ((c[0] ==1) && (p0 == 0) ) ->  c[0] = 0; c[4] = !c[4];  
y0 = 0; y0p =0;  

}


:: atomic{ ((c[0] == 1) && (c[p0] == 0) && (c[4] != c[p0+4])) -> {c[0] = c[p0]; c[4] = c[p0+4]; 

if ::  (c[0] == 0) && (y0 ==1)  -> y0 = 0; y0p =0;

:: else skip;
fi; 

}
}


:: atomic{ ((c[0] == 0) && ((p1 != 0) || ((c[1] == 1) && (c[4] == c[5] ))) && ((p2 != 0) || ((c[2] == 1) && (c[4] == c[6])) ) ) 
-> c[0] = 1;  


if ::  (y2 == 0) && (y0 ==1) ->  y0 =0; 

:: else skip;
fi; 

if ::  (y2p == 0) && (y0p ==1)->  y0p =0;  
:: else skip;
fi; 



}



/* component-based action */


 :: atomic { ( ( y0 == 1 )   && ( ( y0p == 1 ) ||( c[5] == 0 ) ||( c[6] == 0 ))  )
 -> c[4] = 0;    y0 =0;  y0p = 0; y2 =0;  y2p = 0; }




:: atomic {(y2 == 1) && ( c[1] == 1 )  && (c[2] == 1)  && (c[0] == 1) && ( c[4] == 1 ) && ((p0 == 2 ) || (p0 == 1)) && (y0 == 0) -> y0 = 1;}

:: atomic {(y2p == 1) && ( c[1] == 1 )  && (c[2] == 1)  && (c[0] == 1) && ( c[4] == 1 ) && ((p0 == 2 ) || (p0 == 1)) && (y0p == 0) -> y0p = 1;}


od;
}



proctype P1() {

do

:: atomic{ ((c[1] ==1)  && (p1 == 1) ) -> c[1] = 0; c[5] = !c[5]; }

:: atomic{ ((c[1] == 1) && (c[p1] == 0) &&  (c[5] != c[p1+4]) )  -> c[1] = c[p1]; c[5] = c[p1+4];  }

:: atomic{ (c[1] == 0)   -> c[1] = 1;  }

od;

}




proctype P2() {

do


:: atomic{ ((c[2] ==1) && (p2 == 2) ) -> { c[2] = 0; c[6]= !c[6];  
y2 =0;  y0 =0; y3 =0; y3p =0;




if ::  ((y3p == 0) && (c[6] == 1)) && ((y2p ==1)|| (y0p ==1))-> y2p =0;  y0p =0;  y3p =0;
:: else skip;
fi;


}
 }



:: atomic{ ((c[2] == 1) && (c[p2] == 0) &&  (c[6] != c[p2+4])) -> {c[2] = c[p2]; c[6] = c[p2+4]; 

if ::  ((c[2] == 0) || (y3 == 0))  && ((y2 ==1) || (y0 ==1) || (y3 ==1)) -> y2 =0;  y0 =0; y3 =0;

:: else skip;
fi; 



if ::  ((y3p == 0) || (c[7] == 1) || (c[3] == 0) || (c[2] == 0)) && ((y2p ==1)|| (y0p ==1)|| (y3p ==1))-> y2p =0;  y0p =0;  y3p =0;
:: else skip;
fi; 
}
}


:: atomic{ ((c[2] == 0) && ((p3 != 2) || ((c[3] == 1) && (c[7] == c[6]))))     -> c[2] = 1; 

if ::  (y3 == 0) && ((y2 ==1)|| (y0 ==1)) -> y2 =0;  y0 =0; y3 =0;

:: else skip;
fi; 

if ::  (y3p == 0) && ((y2p ==1)|| (y0p ==1))-> y2p =0;  y0p =0;  y3p =0;
:: else skip;
fi; 



  }




:: atomic {(y3 == 1) && (c[2] == 1) && (c[4] == 1) && (c[0] == 1)  && ((p0 == 2 ) || (p0 == 1)) && (y2 == 0) -> y2 = 1;}

:: atomic {(y3p == 1) && (c[2] == 1) && (c[4] == 1) && (c[0] == 1)  && ((p0 == 2 ) || (p0 == 1))  && (y2p == 0) -> y2p = 1;}



od;

}


proctype P3() {

do

:: atomic{ ((c[3] ==1) && (p3 == 3) ) -> { c[3] = 0; c[7] = !c[7];  
y3 = 0; y2 = 0; 

if :: ((c[7] == 1) || (c[2] ==0)) && (y3p ==1) ->  y3p =0; y2p =0;
:: else skip;
fi;

}
}



:: atomic{ ((c[3] == 1) && (c[p3] == 0) &&  (c[7] != c[p3+4])) -> { 
c[3] = c[p3]; c[7] = c[p3+4];

if ::  ((c[3] == 0) || (c[2] ==0)) && (y3 ==1)  -> y3 = 0; y2 =0;
:: else skip;
fi; 

if :: ((c[7] == 1)  || (c[2] ==0)) && (y3p ==1)-> y3p =0; y2p =0;
:: else skip;
fi;

 
 

}
}


:: atomic{ (c[3] == 0)  -> c[3] = 1; 
if :: ((c[7] == 1)  || (c[2] ==0)) && (y3p ==1)-> y3p =0; y2p =0;
:: else skip;
fi;


}





:: atomic { (c[3] == 1 )  && (c[2] == 1) && ((c[6] ==0) || (c[7] ==0)) && (y3 == 0) -> y3 = 1; }


:: atomic { (c[7] == 0)  && (c[2] == 1) && (y3p == 0)  -> y3p = 1; }




od;

}




proctype Pseudo0() {

do

/*
:: atomic { ( c[0] == 1) && 
( ( ( c[1] == 1 ) && (  c[2] == 1 ) && (  c[3] == 1 ) && ( c[4] == 1 ) && ( ( p0 == 2 ) || ( p0 == 1 )  )  )  && (( c[7] == 0 ) || ( c[5] == 0 ) || ( c[6] == 0 ))  )
 -> c[4] = 0; }
*/


:: atomic{ ( (c[0] == 1) &&  (  c[1] == 1 ) && (  c[2] == 1 ) && (  c[3] == 1 ) && ( ( p0 == 2 ) || ( p0 == 1))   ) &&
(
(( c[4] == 0 ) && ( c[5] == 0 ) && ( c[6] == 0 ) && ( c[7] == 0 )) ||
(( c[4] == 1 ) && ( c[5] == 1 ) && ( c[6] == 1 ) && ( c[7] == 1 ))
) 
 -> p0 = 0;  }




:: atomic{
( c[0] == 1) && (c[1] == 1 ) && (  c[2] == 1 ) && (  c[3] == 1 ) && ( c[4] == 0 ) && (  p0 == 2 ) && (
(( c[4] == 0 ) && ( c[5] == 0 ) && ( c[6] == 1 )) ||
(( c[4] == 0 ) && ( c[5] == 1 ) && ( c[6] == 0 )) ||
(( c[4] == 0 ) && ( c[5] == 0 ) && ( c[7] == 1 )) ||
(( c[4] == 0 ) && ( c[5] == 1 ) && ( c[7] == 0 )) ||
(( c[4] == 0 ) && ( c[6] == 1 ) && ( c[7] == 0 )) ||
(( c[4] == 0 ) && ( c[5] == 0 ) && ( c[7] == 1 ))
)  -> p0 = 1; }





:: atomic{
( c[0] == 1) && 
(  ( (  c[1] == 1 ) && (  c[2] == 1 ) && (  c[3] == 1 ) && ( c[4] == 0 ) && ( c[5] == 1 ) && ( c[6] == 1 ) && ( c[7] == 1 ) && ( ( p0 == 2 ) || ( p0 == 1 )  )  )  ) 
 -> {c[0] =1; c[4] = 1; p0 = 0;

 }
}
od;

}


proctype Pseudo1() {

do

:: atomic{
( c[0] == 1) && 
(  ( (  c[1] == 1 ) && (  c[2] == 1 ) && (  c[3] == 1 ) && ( c[4] == 0 ) && ( c[5] == 1 ) && ( c[6] == 0 ) && ( c[7] == 0 ) && (  p0 == 1 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> c[5] =0;


 }


:: atomic{  
( c[0] == 1) && ( c[1] == 1 ) && (  c[2] == 1 ) && (  c[3] == 1 ) && ( c[4] == 0 ) && ( c[5] == 0 ) && (  p0 == 1 ) &&
(( c[6] == 1 ) || ( c[7] == 1 ))
-> c[5] = 1; }




od;

}



proctype Pseudo2() {

do

:: atomic {
( c[0] == 1) && 
(  ( (  c[1] == 1 ) && (  c[2] == 1 ) && (  c[3] == 1 ) && ( c[4] == 0 ) && ( c[5] == 1 ) && ( c[6] == 0 ) && ( c[7] == 1 ) && (  p0 == 1 )  )  ) 
 -> {c[6] = 1; 
}
}
 


od;

}


proctype Pseudo3() {

do

:: atomic {
( c[0] == 1) && 
(  ( (  c[1] == 1 ) && ( c[2] == 1 ) && (  c[3] == 1 ) && ( c[4] == 0 ) && ( c[5] == 1 ) && ( c[6] == 1 ) && ( c[7] == 0 ) && (  p0 == 1 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> {c[7] = 1;
 }
}

od;

}

proctype Faults() {

  

if 

:: atomic { (true) -> c[0] = 0;  }
:: atomic {(true) -> c[0] = 1;  }
:: atomic {(true) -> c[1] = 0; }
:: atomic {(true) -> c[1] = 1;  }



:: atomic { (true) -> c[2] = 0;  }
:: atomic {(true) -> c[2] = 1;  }
:: atomic {(true) -> c[3] = 0; }
:: atomic {(true) -> c[3] = 1;  }



:: atomic { (true) -> c[4] = 0;  }
:: atomic {(true) -> c[4] = 1;  }
:: atomic {(true) -> c[5] = 0; }
:: atomic {(true) -> c[5] = 1;  }


:: atomic { (true) -> c[6] = 0;  }
:: atomic {(true) -> c[6] = 1;  }
:: atomic {(true) -> c[7] = 0; }
:: atomic {(true) -> c[7] = 1;  }


:: atomic{ (true) ->  p0 = 0;   }
:: atomic{ (true) ->  p0 = 1;  }
:: atomic{ (true) ->  p0 = 2; }

/*
:: atomic{ (true) -> c[0] = 1; c[1] = 1; c[2] = 1; c[3] = 1; p0 = 0; }
:: atomic{ (true) -> c[0] = 1; c[1] = 1; c[2] = 1; c[3] = 1; p0 = 1; }
:: atomic{ (true) -> c[0] = 1; c[1] = 1; c[2] = 1; c[3] = 1; p0 = 2; }
*/
fi;

}

init{


run Faults();  


run P0(); run P1(); run P2(); run P3(); 

run Pseudo0();  run Pseudo1();
 run Pseudo2();
run Pseudo3();

/*
assert(inv) 
*/
}