The execution time of reachability graph expansion (msec.):40
No. of states: 12
 
*******************  The fault-intolerant program  *******************
No. of states: 12
 
*******************  The fault-tolerant program  *******************
 
----------  The actions of Process sender ----------
 
( cs == -1) && 
(  ( (  rs == 1 ) && (  bs == 1 ) && (  cr == -1 )  )  ) 
 -> set_rs_val0_cs_val1
  
( cs == -1) && 
(  ( (  rs == 1 ) && (  bs == 0 ) && (  cr == -1 )  )  ) 
 -> set_rs_val0_cs_val0
  
( cs == -1) && 
(  ( (  rs == 0 ) && (  bs == 0 ) && (  cr == 0 )  )  ) 
 -> set_rs_val1_bs_val1_cr_val_m1
  
( cs == -1) && 
(  ( (  rs == 0 ) && (  bs == 1 ) && (  cr == 1 )  )  ) 
 -> set_rs_val1_bs_val0_cr_val_m1
  
 
----------  The actions of Process receiver ----------
 
( cr == -1) && 
(  ( (  cs == 1 ) && (  rr == 0 ) && (  br == 0 )  )  ) 
 -> set_cs_val_m1_rr_val1_br_val1
  
( cr == -1) && 
(  ( (  cs == 0 ) && (  rr == 0 ) && (  br == 1 )  )  ) 
 -> set_cs_val_m1_rr_val1_br_val0
  
( cr == -1) && 
(  ( (  cs == -1 ) && (  rr == 1 ) && (  br == 1 )  )  ) 
 -> set_rr_val0_cr_val1
  
( cr == -1) && 
(  ( (  cs == -1 ) && (  rr == 1 ) && (  br == 0 )  )  ) 
 -> set_rr_val0_cr_val0
  
 
 
----------  The actions of Dummy Process  ----------
 
*************** After identifying ms states ***************
The execution time of Identify_ms (msec.):10
*************** After removing mt transitions ***************
The execution time of Remove_mt (msec.):40
No. of states in the reachability graph: 12
*************** After marking invariant states ***************
The execution time of Mark_Inv (msec.):0
*************** After solving deadlocks ***************
The execution time of solveDeadlock (msec.):881
No. of states: 12
 
*******************  The fault-tolerant program  *******************
No. of states: 12
 
*******************  The fault-tolerant program  *******************
 
----------  The actions of Process sender ----------
 
( cs == -1) && 
(  ( (  rs == 1 ) && (  bs == 1 ) && (  cr == -1 )  )  ) 
 -> set_rs_val0_cs_val1
  
( cs == -1) && 
(  ( (  rs == 1 ) && (  bs == 0 ) && (  cr == -1 )  )  ) 
 -> set_rs_val0_cs_val0
  
( cs == -1) && 
(  ( (  rs == 0 ) && (  bs == 0 ) && (  cr == 0 )  )  ) 
 -> set_rs_val1_bs_val1_cr_val_m1
  
( cs == -1) && 
(  ( (  rs == 0 ) && (  bs == 1 ) && (  cr == 1 )  )  ) 
 -> set_rs_val1_bs_val0_cr_val_m1
  
 
----------  The actions of Process receiver ----------
 
( cr == -1) && 
(  ( (  cs == 1 ) && (  rr == 0 ) && (  br == 0 )  )  ) 
 -> set_cs_val_m1_rr_val1_br_val1
  
( cr == -1) && 
(  ( (  cs == 0 ) && (  rr == 0 ) && (  br == 1 )  )  ) 
 -> set_cs_val_m1_rr_val1_br_val0
  
( cr == -1) && 
(  ( (  cs == -1 ) && (  rr == 1 ) && (  br == 1 )  )  ) 
 -> set_rr_val0_cr_val1
  
( cr == -1) && 
(  ( (  cs == -1 ) && (  rr == 1 ) && (  br == 0 )  )  ) 
 -> set_rr_val0_cr_val0
  
 
 
----------  The actions of Dummy Process  ----------
 
( rs == 0) && 
(  ( (  rr == 0 ) && (  bs == 1 ) && (  br == 0 ) && (  cs == -1 ) && (  cr == -1 )  )  ) 
 -> set_cs_val1
  
( rs == 0) && 
(  ( (  rr == 0 ) && (  bs == 0 ) && (  br == 1 ) && (  cs == -1 ) && (  cr == -1 )  )  ) 
 -> set_cs_val0
  
( rs == 0) && 
(  ( (  rr == 0 ) && (  bs == 1 ) && (  br == 1 ) && (  cs == -1 ) && (  cr == -1 )  )  ) 
 -> set_cr_val1
  
( rs == 0) && 
(  ( (  rr == 0 ) && (  bs == 0 ) && (  br == 0 ) && (  cs == -1 ) && (  cr == -1 )  )  ) 
 -> set_cr_val0