T_Abort_Send_P1=0 T_Abort_Send_P2=0 T_Abort_Send_P3=0
T_Abort_Send_P4=0 T_F1=0 T_F2=0 T_F3=0 T_F4=0 T_Recovery_Send_P1=0
T_Recovery_Send_P2=0 T_Recovery_Send_P3=0 T_Recovery_Send_P4=0
T_Respond1=0 T_Respond2=0 T_Respond3=0 T_Respond4=0 T_S1=0 T_S2=0
T_S3=0 T_S4=0 T_Validated=0 P3_AbortToken=0 P3_Abort_Send=0
P3_Recovery_1_2_2=0 P3_Recovery_1_3_3=0 P3_Recovery_4_3_3=0
P3_Recovery_4_4_4=0 P3_Recovery_5_4_4=0 P3_S1=0 P3_S2=0 P3_S4=0
P3_contacted_T=0 P3_stop=0 Pr_3_1_L=0 Pr_3_2_L=0 Pr_3_4_L=0
P2_AbortToken=0 P2_Abort_Send=0 P2_Recovery_1_1_1=0
P2_Recovery_1_1_2=0 P2_Recovery_1_3_2=0 P2_Recovery_1_3_3=0
P2_Recovery_1_4_3=0 P2_Recovery_4_3_3=0 P2_Recovery_4_4_3=0
P2_Recovery_4_4_4=0 P2_Recovery_4_5_4=0 P2_Recovery_5_4_4=0
P2_Recovery_5_5_4=0 P2_S1=0 P2_S3=0 P2_S4=0 P2_contacted_T=0 P2_stop=0
Pr_2_1_L=0 Pr_2_3_L=0 Pr_2_4_L=0 P4_AbortToken=0 P4_Abort_Send=0
P4_Recovery_3_3_3=0 P4_Recovery_4_4_4=0 P4_S1=0 P4_S2=0 P4_S3=0
P4_contacted_T=0 P4_stop=0 Pr_4_1_L=0 Pr_4_2_L=0 Pr_4_3_L=0
P1_AbortToken=0 P1_Recovery_1_1_1=0 P1_Recovery_1_1_2=0
P1_Recovery_1_1_3=0 P1_Recovery_1_3_2=0 P1_Recovery_1_3_3=0
P1_Recovery_1_3_4=0 P1_Recovery_1_4_3=0 P1_Recovery_1_4_4=0
P1_Recovery_4_3_3=0 P1_Recovery_4_3_4=0 P1_Recovery_4_4_3=0
P1_Recovery_4_4_4=0 P1_Recovery_4_4_5=0 P1_Recovery_4_5_4=0
P1_Recovery_4_5_5=0 P1_Recovery_5_4_4=0 P1_Recovery_5_4_5=0
P1_Recovery_5_5_4=0 P1_S2=0 P1_S3=0 P1_S4=0 P1_contacted_T=0 P1_stop=0
Pr_1_2_L=0 Pr_1_3_L=0 Pr_1_4_L=0

Pr_4_3_L=1 

Pr_3_1_L=1 Pr_3_2_L=1 Pr_2_3_L=2 Pr_1_3_L=2 

Pr_3_1_L=3 Pr_3_2_L=3 Pr_2_3_L=3 Pr_4_3_L=4 Pr_1_3_L=3 

Pr_3_4_L=3 Pr_4_2_L=1 Pr_1_3_L=4 

Pr_3_1_L=4 Pr_3_2_L=4 Pr_2_3_L=4 P4_Abort_Send=1 Pr_1_2_L=2 

T_Abort_Send_P4=1 T_Respond4=1 T_S4=1 Pr_3_4_L=4 P2_Recovery_1_3_2=1

T_Abort_Send_P2=1 T_F3=1 T_Respond2=1 T_S2=1 P3_Recovery_4_4_4=1
P3_contacted_T=1 Pr_2_1_L=4 Pr_4_1_L=4

T_Abort_Send_P3=1 T_Respond3=1 T_S3=1 P1_Recovery_4_4_4=1

T_Recovery_Send_P1=1 T_Respond1=1 T_Validated=1 P3_AbortToken=1
P3_stop=1

P1_S2=1 P1_S3=1 P1_S4=1