*************** After solving deadlocks ***************
The execution time of solveDeadlock (msec.):5278
No. of states: 768
 
*******************  The fault-tolerant program  *******************
No. of states: 768
 
******************************************************************
 
----------  The actions of Process P0 ----------
 
( c.0 == 1) && 
(  ( (  p.0 == 0 ) && (  sn.0 == 1 )  )  ) 
 -> set_c0_val0_sn0_val0
  
 
( c.0 == 1) && 
(  ( (  p.0 == 0 ) && (  sn.0 == 0 )  )  ) 
 -> set_c0_val0_sn0_val1
  
 
( c.0 == 1) && 
(  ( (  c.1 == 0 ) && (  c.2 == 0 ) && (  sn.0 == 1 ) && (  sn.1 == 0 ) && (  sn.2 == 0 ) && (  (  p.0 == 1 ) ||  (  p.0 == 2 )  )  )  ||  
( (  c.2 == 0 ) && (  sn.0 == 1 ) && (  sn.2 == 0 ) && (  p.0 == 2 )  )  || 
 ( (  c.1 == 0 ) && (  sn.0 == 0 ) && (  sn.1 == 1 ) && (  p.0 == 1 )  )  ||  
( (  c.2 == 0 ) && (  sn.0 == 0 ) && (  sn.2 == 1 ) && (  p.0 == 2 )  )  ||  
( (  c.1 == 0 ) && (  sn.0 == 1 ) && (  sn.1 == 0 ) && (  p.0 == 1 )  )  ||  
( (  c.1 == 0 ) && (  c.2 == 0 ) && (  sn.0 == 0 ) && (  sn.1 == 1 ) && (  sn.2 == 1 ) && (  (  p.0 == 1 ) ||  (  p.0 == 2 )  )  )  ) 
 -> set_c0_valcp0_sn0_valsnp0
  
 
( c.0 == 0) && 
(  ( (  c.1 == 1 ) && (  c.2 == 1 ) && (  sn.0 == 0 ) && (  sn.1 == 0 ) && (  sn.2 == 0 )  )  ||  
( (  c.1 == 1 ) && (  c.2 == 1 ) && (  sn.0 == 1 ) && (  sn.1 == 1 ) && (  sn.2 == 1 )  )  ) 
 -> set_c0_val1
  
 
 
----------  The actions of Process P1 ----------
 
( c.1 == 1) && 
(  ( (  c.p.1 == 0 ) && (  sn.1 == 0 ) && (  sn.p.1 == 1 )  )  ||  
( (  c.p.1 == 0 ) && (  sn.1 == 1 ) && (  sn.p.1 == 0 )  )  ) 
 -> set_c1_valcp1_sn1_valsnp1
  
 
( c.1 == 0) && 
(  ( (  sn.1 == 1 )  )  ||  ( (  sn.1 == 0 )  )  ) 
 -> set_c1_val1
  

----------  The actions of Process P2 ----------


( c.2 == 1) && 
(  ( (  c.p.2 == 0 ) && (  sn.2 == 0 ) && (  sn.p.2 == 1 )  )  ||  
( (  c.p.2 == 0 ) && (  sn.2 == 1 ) && (  sn.p.2 == 0 )  )  ) 
 -> set_c2_valcp2_sn2_valsnp2
  
 
( c.2 == 0) && 
(  ( (  sn.2 == 0 ) && (  c.3 == 1 ) && (  sn.3 == 0 ) && (  p.3 == 2 )  )  ||  
( (  sn.2 == 1 ) && (  c.3 == 1 ) && (  sn.3 == 1 ) && (  p.3 == 2 )  )  ) 
 -> set_c2_val1
  
 
 
----------  The actions of Process P3 ----------
 
( c.3 == 1) && 
(  ( (  c.p.3 == 0 ) && (  sn.3 == 0 ) && (  sn.p.3 == 1 )  )  ||  
( (  c.p.3 == 0 ) && (  sn.3 == 1 ) && (  sn.p.3 == 0 )  )  ) 
 -> set_c3_valcp3_sn3_valsnp3
  
 
( c.3 == 0) && 
(  ( (  sn.3 == 0 )  )  ||  ( (  sn.3 == 1 )  )  ) 
 -> set_c3_val1
  
 
 
 
----------  The actions of the high atomicity Process 0 ----------
 
 
( c0 == 1) && 
(  ( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 1 ) && (  sn3 == 0 ) && ( ( p0 == 2 ) || ( p0 == 1 )  )  && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 1 ) && (  sn1 == 0 ) && ( ( p0 == 2 ) || ( p0 == 1 )  )  && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 1 ) && (  sn2 == 0 ) && ( ( p0 == 2 ) || ( p0 == 1 )  )  && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> set_sn0_val0
  


( c0 == 1) && 
(  ( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 0 ) && (  sn2 == 0 ) && (  sn3 == 0 ) && ( ( p0 == 2 ) || ( p0 == 1 )  )  && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 1 ) && (  sn1 == 1 ) && (  sn2 == 1 ) && (  sn3 == 1 ) && ( ( p0 == 1 ) || ( p0 == 2 )  )  && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> set_p0_val0
  
 
( c0 == 1) && 
(  ( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 0 ) && (  sn2 == 1 ) && (  p0 == 2 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 1 ) && (  sn2 == 0 ) && (  p0 == 2 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn2 == 0 ) && (  sn3 == 1 ) && (  p0 == 2 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 1 ) && (  sn3 == 0 ) && (  p0 == 2 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn2 == 1 ) && (  sn3 == 0 ) && (  p0 == 2 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 0 ) && (  sn3 == 1 ) && (  p0 == 2 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> set_p0_val1
  


( c0 == 1) && 
(  ( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 1 ) && (  sn2 == 1 ) && (  sn3 == 1 ) && ( ( p0 == 2 ) || ( p0 == 1 )  )  && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> localReset
  
 
 
----------  The actions of the high atomicity Process 1 ----------
 
 
( c0 == 1) && 
(  ( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 1 ) && (  sn2 == 0 ) && (  sn3 == 0 ) && (  p0 == 1 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> set_sn1_val0
  
 
( c0 == 1) && 
(  ( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 0 ) && (  sn2 == 1 ) && (  p0 == 1 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ||  
( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 0 ) && (  sn3 == 1 ) && (  p0 == 1 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> set_sn1_val1
  
 
 
 
----------  The actions of the high atomicity Process 2 ----------
 
 
( c0 == 1) && 
(  ( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 1 ) && (  sn2 == 0 ) && (  sn3 == 1 ) && (  p0 == 1 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> set_sn2_val1
  
 
----------  The actions of the high atomicity Process 3 ----------



( c0 == 1) && 
(  ( (  c1 == 1 ) && (  c2 == 1 ) && (  c3 == 1 ) && (  sn0 == 0 ) && (  sn1 == 1 ) && (  sn2 == 1 ) && (  sn3 == 0 ) && (  p0 == 1 ) && (  p1 == 0 ) && (  p2 == 0 ) && (  p3 == 2 )  )  ) 
 -> set_sn3_val1