LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0
1: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0
2: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0l_287_0 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0l_1519_0 ≤ 0
3: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0
4: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0j_36_post ≤ 0j_36_post ≤ 0j_39_post ≤ 0j_36_0 ≤ 0j_36_0 ≤ 0j_39_0 ≤ 0
5: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0l_287_0 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0j_36_post ≤ 0j_36_post ≤ 0j_39_post ≤ 0j_36_0 ≤ 0j_36_0 ≤ 0j_39_0 ≤ 0j_39_0 ≤ 0l_1429_0 ≤ 0
6: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0j_36_post ≤ 0j_36_post ≤ 0j_39_post ≤ 0j_36_0 ≤ 0j_36_0 ≤ 0j_39_0 ≤ 0j_39_0 ≤ 0
7: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0l_287_0 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0j_36_post ≤ 0j_36_post ≤ 0j_39_post ≤ 0j_36_0 ≤ 0j_36_0 ≤ 0j_39_0 ≤ 0j_39_0 ≤ 0l_855_0 ≤ 0
8: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0j_36_post ≤ 0j_36_post ≤ 0j_39_post ≤ 0j_36_0 ≤ 0j_36_0 ≤ 0j_39_0 ≤ 0j_39_0 ≤ 0
9: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0
10: h_28_post ≤ 0h_28_post ≤ 01 − l_27_post ≤ 0mt_20_post ≤ 0mt_20_post ≤ 0h_34_1 ≤ 0h_34_1 ≤ 0lt_10_1 ≤ 0lt_10_1 ≤ 0lt_17_1 ≤ 0lt_17_1 ≤ 0−1 + mt_18_1 ≤ 01 − mt_18_1 ≤ 0h_28_0 ≤ 0h_28_0 ≤ 01 − l_27_0 ≤ 0mt_20_0 ≤ 0mt_20_0 ≤ 0
11: TRUE
12: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 17 0: tp_44_post + tp_44_post ≤ 0tp_44_posttp_44_post ≤ 0tp_44_3 + tp_44_3 ≤ 0tp_44_3tp_44_3 ≤ 0tp_44_2 + tp_44_2 ≤ 0tp_44_2tp_44_2 ≤ 0tp_44_1 + tp_44_1 ≤ 0tp_44_1tp_44_1 ≤ 0tp_44_0 + tp_44_0 ≤ 0tp_44_0tp_44_0 ≤ 0tp_32_post + tp_32_post ≤ 0tp_32_posttp_32_post ≤ 0tp_32_2 + tp_32_2 ≤ 0tp_32_2tp_32_2 ≤ 0tp_32_1 + tp_32_1 ≤ 0tp_32_1tp_32_1 ≤ 0tp_32_0 + tp_32_0 ≤ 0tp_32_0tp_32_0 ≤ 0tp_30_post + tp_30_post ≤ 0tp_30_posttp_30_post ≤ 0tp_30_1 + tp_30_1 ≤ 0tp_30_1tp_30_1 ≤ 0tp_30_0 + tp_30_0 ≤ 0tp_30_0tp_30_0 ≤ 0tp_19_0 + tp_19_0 ≤ 0tp_19_0tp_19_0 ≤ 0t_45_post + t_45_post ≤ 0t_45_postt_45_post ≤ 0t_45_1 + t_45_1 ≤ 0t_45_1t_45_1 ≤ 0t_45_0 + t_45_0 ≤ 0t_45_0t_45_0 ≤ 0t_40_post + t_40_post ≤ 0t_40_postt_40_post ≤ 0t_40_0 + t_40_0 ≤ 0t_40_0t_40_0 ≤ 0t_38_post + t_38_post ≤ 0t_38_postt_38_post ≤ 0t_38_0 + t_38_0 ≤ 0t_38_0t_38_0 ≤ 0t_35_post + t_35_post ≤ 0t_35_postt_35_post ≤ 0t_35_2 + t_35_2 ≤ 0t_35_2t_35_2 ≤ 0t_35_1 + t_35_1 ≤ 0t_35_1t_35_1 ≤ 0t_35_0 + t_35_0 ≤ 0t_35_0t_35_0 ≤ 0t_14_0 + t_14_0 ≤ 0t_14_0t_14_0 ≤ 0t_1303_post + t_1303_post ≤ 0t_1303_postt_1303_post ≤ 0t_1303_0 + t_1303_0 ≤ 0t_1303_0t_1303_0 ≤ 0t_1057_post + t_1057_post ≤ 0t_1057_postt_1057_post ≤ 0t_1057_0 + t_1057_0 ≤ 0t_1057_0t_1057_0 ≤ 0sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_postsCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_1sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_43_0sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_postsCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_2sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_1sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_33_0sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_postsCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_29_0sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0sCALLSITERETURN_16_0sCALLSITERETURN_16_0 ≤ 0nd_7_post + nd_7_post ≤ 0nd_7_postnd_7_post ≤ 0nd_7_1 + nd_7_1 ≤ 0nd_7_1nd_7_1 ≤ 0nd_7_0 + nd_7_0 ≤ 0nd_7_0nd_7_0 ≤ 0mt_20_post + mt_20_post ≤ 0mt_20_postmt_20_post ≤ 0mt_20_0 + mt_20_0 ≤ 0mt_20_0mt_20_0 ≤ 0mt_18_post + mt_18_post ≤ 0mt_18_postmt_18_post ≤ 0mt_18_1 + mt_18_1 ≤ 0mt_18_1mt_18_1 ≤ 0mt_18_0 + mt_18_0 ≤ 0mt_18_0mt_18_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_1 + lt_17_1 ≤ 0lt_17_1lt_17_1 ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0lt_1256_post + lt_1256_post ≤ 0lt_1256_postlt_1256_post ≤ 0lt_1256_0 + lt_1256_0 ≤ 0lt_1256_0lt_1256_0 ≤ 0lt_10_post + lt_10_post ≤ 0lt_10_postlt_10_post ≤ 0lt_10_1 + lt_10_1 ≤ 0lt_10_1lt_10_1 ≤ 0lt_10_0 + lt_10_0 ≤ 0lt_10_0lt_10_0 ≤ 0l_855_post + l_855_post ≤ 0l_855_postl_855_post ≤ 0l_855_0 + l_855_0 ≤ 0l_855_0l_855_0 ≤ 0l_287_post + l_287_post ≤ 0l_287_postl_287_post ≤ 0l_287_0 + l_287_0 ≤ 0l_287_0l_287_0 ≤ 0l_27_post + l_27_post ≤ 0l_27_postl_27_post ≤ 0l_27_0 + l_27_0 ≤ 0l_27_0l_27_0 ≤ 0l_1519_post + l_1519_post ≤ 0l_1519_postl_1519_post ≤ 0l_1519_0 + l_1519_0 ≤ 0l_1519_0l_1519_0 ≤ 0l_1429_post + l_1429_post ≤ 0l_1429_postl_1429_post ≤ 0l_1429_0 + l_1429_0 ≤ 0l_1429_0l_1429_0 ≤ 0l_1304_post + l_1304_post ≤ 0l_1304_postl_1304_post ≤ 0l_1304_0 + l_1304_0 ≤ 0l_1304_0l_1304_0 ≤ 0l_1119_post + l_1119_post ≤ 0l_1119_postl_1119_post ≤ 0l_1119_1 + l_1119_1 ≤ 0l_1119_1l_1119_1 ≤ 0l_1119_0 + l_1119_0 ≤ 0l_1119_0l_1119_0 ≤ 0j_39_post + j_39_post ≤ 0j_39_postj_39_post ≤ 0j_39_0 + j_39_0 ≤ 0j_39_0j_39_0 ≤ 0j_36_post + j_36_post ≤ 0j_36_postj_36_post ≤ 0j_36_0 + j_36_0 ≤ 0j_36_0j_36_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0h_46_post + h_46_post ≤ 0h_46_posth_46_post ≤ 0h_46_1 + h_46_1 ≤ 0h_46_1h_46_1 ≤ 0h_46_0 + h_46_0 ≤ 0h_46_0h_46_0 ≤ 0h_37_post + h_37_post ≤ 0h_37_posth_37_post ≤ 0h_37_0 + h_37_0 ≤ 0h_37_0h_37_0 ≤ 0h_34_post + h_34_post ≤ 0h_34_posth_34_post ≤ 0h_34_2 + h_34_2 ≤ 0h_34_2h_34_2 ≤ 0h_34_1 + h_34_1 ≤ 0h_34_1h_34_1 ≤ 0h_34_0 + h_34_0 ≤ 0h_34_0h_34_0 ≤ 0h_28_post + h_28_post ≤ 0h_28_posth_28_post ≤ 0h_28_0 + h_28_0 ≤ 0h_28_0h_28_0 ≤ 0f_1323_post + f_1323_post ≤ 0f_1323_postf_1323_post ≤ 0f_1323_0 + f_1323_0 ≤ 0f_1323_0f_1323_0 ≤ 0fF_1324_post + fF_1324_post ≤ 0fF_1324_postfF_1324_post ≤ 0fF_1324_0 + fF_1324_0 ≤ 0fF_1324_0fF_1324_0 ≤ 0c_990_post + c_990_post ≤ 0c_990_postc_990_post ≤ 0c_990_0 + c_990_0 ≤ 0c_990_0c_990_0 ≤ 0c_98_post + c_98_post ≤ 0c_98_postc_98_post ≤ 0c_98_1 + c_98_1 ≤ 0c_98_1c_98_1 ≤ 0c_98_0 + c_98_0 ≤ 0c_98_0c_98_0 ≤ 0c_958_post + c_958_post ≤ 0c_958_postc_958_post ≤ 0c_958_1 + c_958_1 ≤ 0c_958_1c_958_1 ≤ 0c_958_0 + c_958_0 ≤ 0c_958_0c_958_0 ≤ 0c_901_post + c_901_post ≤ 0c_901_postc_901_post ≤ 0c_901_0 + c_901_0 ≤ 0c_901_0c_901_0 ≤ 0c_1481_post + c_1481_post ≤ 0c_1481_postc_1481_post ≤ 0c_1481_1 + c_1481_1 ≤ 0c_1481_1c_1481_1 ≤ 0c_1481_0 + c_1481_0 ≤ 0c_1481_0c_1481_0 ≤ 0c_1186_post + c_1186_post ≤ 0c_1186_postc_1186_post ≤ 0c_1186_0 + c_1186_0 ≤ 0c_1186_0c_1186_0 ≤ 0Flink_0 + Flink_0 ≤ 0Flink_0Flink_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 4, 5, 6, 7, 8, 9, 10, 15, 16 using the following ranking functions, which are bounded by −21.

12: 0
11: 0
0: 0
1: 0
2: 0
3: 0
9: 0
10: 0
4: 0
5: 0
6: 0
7: 0
8: 0
12: −9
11: −10
0: −11
1: −11
2: −11
3: −11
9: −11
10: −11
0_var_snapshot: −11
0*: −11
4: −12
5: −13
6: −14
7: −15
8: −16

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0* 20 0: tp_44_post + tp_44_post ≤ 0tp_44_posttp_44_post ≤ 0tp_44_3 + tp_44_3 ≤ 0tp_44_3tp_44_3 ≤ 0tp_44_2 + tp_44_2 ≤ 0tp_44_2tp_44_2 ≤ 0tp_44_1 + tp_44_1 ≤ 0tp_44_1tp_44_1 ≤ 0tp_44_0 + tp_44_0 ≤ 0tp_44_0tp_44_0 ≤ 0tp_32_post + tp_32_post ≤ 0tp_32_posttp_32_post ≤ 0tp_32_2 + tp_32_2 ≤ 0tp_32_2tp_32_2 ≤ 0tp_32_1 + tp_32_1 ≤ 0tp_32_1tp_32_1 ≤ 0tp_32_0 + tp_32_0 ≤ 0tp_32_0tp_32_0 ≤ 0tp_30_post + tp_30_post ≤ 0tp_30_posttp_30_post ≤ 0tp_30_1 + tp_30_1 ≤ 0tp_30_1tp_30_1 ≤ 0tp_30_0 + tp_30_0 ≤ 0tp_30_0tp_30_0 ≤ 0tp_19_0 + tp_19_0 ≤ 0tp_19_0tp_19_0 ≤ 0t_45_post + t_45_post ≤ 0t_45_postt_45_post ≤ 0t_45_1 + t_45_1 ≤ 0t_45_1t_45_1 ≤ 0t_45_0 + t_45_0 ≤ 0t_45_0t_45_0 ≤ 0t_40_post + t_40_post ≤ 0t_40_postt_40_post ≤ 0t_40_0 + t_40_0 ≤ 0t_40_0t_40_0 ≤ 0t_38_post + t_38_post ≤ 0t_38_postt_38_post ≤ 0t_38_0 + t_38_0 ≤ 0t_38_0t_38_0 ≤ 0t_35_post + t_35_post ≤ 0t_35_postt_35_post ≤ 0t_35_2 + t_35_2 ≤ 0t_35_2t_35_2 ≤ 0t_35_1 + t_35_1 ≤ 0t_35_1t_35_1 ≤ 0t_35_0 + t_35_0 ≤ 0t_35_0t_35_0 ≤ 0t_14_0 + t_14_0 ≤ 0t_14_0t_14_0 ≤ 0t_1303_post + t_1303_post ≤ 0t_1303_postt_1303_post ≤ 0t_1303_0 + t_1303_0 ≤ 0t_1303_0t_1303_0 ≤ 0t_1057_post + t_1057_post ≤ 0t_1057_postt_1057_post ≤ 0t_1057_0 + t_1057_0 ≤ 0t_1057_0t_1057_0 ≤ 0sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_postsCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_1sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_43_0sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_postsCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_2sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_1sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_33_0sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_postsCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_29_0sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0sCALLSITERETURN_16_0sCALLSITERETURN_16_0 ≤ 0nd_7_post + nd_7_post ≤ 0nd_7_postnd_7_post ≤ 0nd_7_1 + nd_7_1 ≤ 0nd_7_1nd_7_1 ≤ 0nd_7_0 + nd_7_0 ≤ 0nd_7_0nd_7_0 ≤ 0mt_20_post + mt_20_post ≤ 0mt_20_postmt_20_post ≤ 0mt_20_0 + mt_20_0 ≤ 0mt_20_0mt_20_0 ≤ 0mt_18_post + mt_18_post ≤ 0mt_18_postmt_18_post ≤ 0mt_18_1 + mt_18_1 ≤ 0mt_18_1mt_18_1 ≤ 0mt_18_0 + mt_18_0 ≤ 0mt_18_0mt_18_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_1 + lt_17_1 ≤ 0lt_17_1lt_17_1 ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0lt_1256_post + lt_1256_post ≤ 0lt_1256_postlt_1256_post ≤ 0lt_1256_0 + lt_1256_0 ≤ 0lt_1256_0lt_1256_0 ≤ 0lt_10_post + lt_10_post ≤ 0lt_10_postlt_10_post ≤ 0lt_10_1 + lt_10_1 ≤ 0lt_10_1lt_10_1 ≤ 0lt_10_0 + lt_10_0 ≤ 0lt_10_0lt_10_0 ≤ 0l_855_post + l_855_post ≤ 0l_855_postl_855_post ≤ 0l_855_0 + l_855_0 ≤ 0l_855_0l_855_0 ≤ 0l_287_post + l_287_post ≤ 0l_287_postl_287_post ≤ 0l_287_0 + l_287_0 ≤ 0l_287_0l_287_0 ≤ 0l_27_post + l_27_post ≤ 0l_27_postl_27_post ≤ 0l_27_0 + l_27_0 ≤ 0l_27_0l_27_0 ≤ 0l_1519_post + l_1519_post ≤ 0l_1519_postl_1519_post ≤ 0l_1519_0 + l_1519_0 ≤ 0l_1519_0l_1519_0 ≤ 0l_1429_post + l_1429_post ≤ 0l_1429_postl_1429_post ≤ 0l_1429_0 + l_1429_0 ≤ 0l_1429_0l_1429_0 ≤ 0l_1304_post + l_1304_post ≤ 0l_1304_postl_1304_post ≤ 0l_1304_0 + l_1304_0 ≤ 0l_1304_0l_1304_0 ≤ 0l_1119_post + l_1119_post ≤ 0l_1119_postl_1119_post ≤ 0l_1119_1 + l_1119_1 ≤ 0l_1119_1l_1119_1 ≤ 0l_1119_0 + l_1119_0 ≤ 0l_1119_0l_1119_0 ≤ 0j_39_post + j_39_post ≤ 0j_39_postj_39_post ≤ 0j_39_0 + j_39_0 ≤ 0j_39_0j_39_0 ≤ 0j_36_post + j_36_post ≤ 0j_36_postj_36_post ≤ 0j_36_0 + j_36_0 ≤ 0j_36_0j_36_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0h_46_post + h_46_post ≤ 0h_46_posth_46_post ≤ 0h_46_1 + h_46_1 ≤ 0h_46_1h_46_1 ≤ 0h_46_0 + h_46_0 ≤ 0h_46_0h_46_0 ≤ 0h_37_post + h_37_post ≤ 0h_37_posth_37_post ≤ 0h_37_0 + h_37_0 ≤ 0h_37_0h_37_0 ≤ 0h_34_post + h_34_post ≤ 0h_34_posth_34_post ≤ 0h_34_2 + h_34_2 ≤ 0h_34_2h_34_2 ≤ 0h_34_1 + h_34_1 ≤ 0h_34_1h_34_1 ≤ 0h_34_0 + h_34_0 ≤ 0h_34_0h_34_0 ≤ 0h_28_post + h_28_post ≤ 0h_28_posth_28_post ≤ 0h_28_0 + h_28_0 ≤ 0h_28_0h_28_0 ≤ 0f_1323_post + f_1323_post ≤ 0f_1323_postf_1323_post ≤ 0f_1323_0 + f_1323_0 ≤ 0f_1323_0f_1323_0 ≤ 0fF_1324_post + fF_1324_post ≤ 0fF_1324_postfF_1324_post ≤ 0fF_1324_0 + fF_1324_0 ≤ 0fF_1324_0fF_1324_0 ≤ 0c_990_post + c_990_post ≤ 0c_990_postc_990_post ≤ 0c_990_0 + c_990_0 ≤ 0c_990_0c_990_0 ≤ 0c_98_post + c_98_post ≤ 0c_98_postc_98_post ≤ 0c_98_1 + c_98_1 ≤ 0c_98_1c_98_1 ≤ 0c_98_0 + c_98_0 ≤ 0c_98_0c_98_0 ≤ 0c_958_post + c_958_post ≤ 0c_958_postc_958_post ≤ 0c_958_1 + c_958_1 ≤ 0c_958_1c_958_1 ≤ 0c_958_0 + c_958_0 ≤ 0c_958_0c_958_0 ≤ 0c_901_post + c_901_post ≤ 0c_901_postc_901_post ≤ 0c_901_0 + c_901_0 ≤ 0c_901_0c_901_0 ≤ 0c_1481_post + c_1481_post ≤ 0c_1481_postc_1481_post ≤ 0c_1481_1 + c_1481_1 ≤ 0c_1481_1c_1481_1 ≤ 0c_1481_0 + c_1481_0 ≤ 0c_1481_0c_1481_0 ≤ 0c_1186_post + c_1186_post ≤ 0c_1186_postc_1186_post ≤ 0c_1186_0 + c_1186_0 ≤ 0c_1186_0c_1186_0 ≤ 0Flink_0 + Flink_0 ≤ 0Flink_0Flink_0 ≤ 0

5 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0 18 0_var_snapshot: tp_44_post + tp_44_post ≤ 0tp_44_posttp_44_post ≤ 0tp_44_3 + tp_44_3 ≤ 0tp_44_3tp_44_3 ≤ 0tp_44_2 + tp_44_2 ≤ 0tp_44_2tp_44_2 ≤ 0tp_44_1 + tp_44_1 ≤ 0tp_44_1tp_44_1 ≤ 0tp_44_0 + tp_44_0 ≤ 0tp_44_0tp_44_0 ≤ 0tp_32_post + tp_32_post ≤ 0tp_32_posttp_32_post ≤ 0tp_32_2 + tp_32_2 ≤ 0tp_32_2tp_32_2 ≤ 0tp_32_1 + tp_32_1 ≤ 0tp_32_1tp_32_1 ≤ 0tp_32_0 + tp_32_0 ≤ 0tp_32_0tp_32_0 ≤ 0tp_30_post + tp_30_post ≤ 0tp_30_posttp_30_post ≤ 0tp_30_1 + tp_30_1 ≤ 0tp_30_1tp_30_1 ≤ 0tp_30_0 + tp_30_0 ≤ 0tp_30_0tp_30_0 ≤ 0tp_19_0 + tp_19_0 ≤ 0tp_19_0tp_19_0 ≤ 0t_45_post + t_45_post ≤ 0t_45_postt_45_post ≤ 0t_45_1 + t_45_1 ≤ 0t_45_1t_45_1 ≤ 0t_45_0 + t_45_0 ≤ 0t_45_0t_45_0 ≤ 0t_40_post + t_40_post ≤ 0t_40_postt_40_post ≤ 0t_40_0 + t_40_0 ≤ 0t_40_0t_40_0 ≤ 0t_38_post + t_38_post ≤ 0t_38_postt_38_post ≤ 0t_38_0 + t_38_0 ≤ 0t_38_0t_38_0 ≤ 0t_35_post + t_35_post ≤ 0t_35_postt_35_post ≤ 0t_35_2 + t_35_2 ≤ 0t_35_2t_35_2 ≤ 0t_35_1 + t_35_1 ≤ 0t_35_1t_35_1 ≤ 0t_35_0 + t_35_0 ≤ 0t_35_0t_35_0 ≤ 0t_14_0 + t_14_0 ≤ 0t_14_0t_14_0 ≤ 0t_1303_post + t_1303_post ≤ 0t_1303_postt_1303_post ≤ 0t_1303_0 + t_1303_0 ≤ 0t_1303_0t_1303_0 ≤ 0t_1057_post + t_1057_post ≤ 0t_1057_postt_1057_post ≤ 0t_1057_0 + t_1057_0 ≤ 0t_1057_0t_1057_0 ≤ 0sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_postsCALLSITERETURN_43_post ≤ 0sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_1sCALLSITERETURN_43_1 ≤ 0sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_43_0sCALLSITERETURN_43_0 ≤ 0sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_postsCALLSITERETURN_33_post ≤ 0sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_2sCALLSITERETURN_33_2 ≤ 0sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_1sCALLSITERETURN_33_1 ≤ 0sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_33_0sCALLSITERETURN_33_0 ≤ 0sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_postsCALLSITERETURN_29_post ≤ 0sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_29_0sCALLSITERETURN_29_0 ≤ 0sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0sCALLSITERETURN_16_0sCALLSITERETURN_16_0 ≤ 0nd_7_post + nd_7_post ≤ 0nd_7_postnd_7_post ≤ 0nd_7_1 + nd_7_1 ≤ 0nd_7_1nd_7_1 ≤ 0nd_7_0 + nd_7_0 ≤ 0nd_7_0nd_7_0 ≤ 0mt_20_post + mt_20_post ≤ 0mt_20_postmt_20_post ≤ 0mt_20_0 + mt_20_0 ≤ 0mt_20_0mt_20_0 ≤ 0mt_18_post + mt_18_post ≤ 0mt_18_postmt_18_post ≤ 0mt_18_1 + mt_18_1 ≤ 0mt_18_1mt_18_1 ≤ 0mt_18_0 + mt_18_0 ≤ 0mt_18_0mt_18_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_1 + lt_17_1 ≤ 0lt_17_1lt_17_1 ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0lt_1256_post + lt_1256_post ≤ 0lt_1256_postlt_1256_post ≤ 0lt_1256_0 + lt_1256_0 ≤ 0lt_1256_0lt_1256_0 ≤ 0lt_10_post + lt_10_post ≤ 0lt_10_postlt_10_post ≤ 0lt_10_1 + lt_10_1 ≤ 0lt_10_1lt_10_1 ≤ 0lt_10_0 + lt_10_0 ≤ 0lt_10_0lt_10_0 ≤ 0l_855_post + l_855_post ≤ 0l_855_postl_855_post ≤ 0l_855_0 + l_855_0 ≤ 0l_855_0l_855_0 ≤ 0l_287_post + l_287_post ≤ 0l_287_postl_287_post ≤ 0l_287_0 + l_287_0 ≤ 0l_287_0l_287_0 ≤ 0l_27_post + l_27_post ≤ 0l_27_postl_27_post ≤ 0l_27_0 + l_27_0 ≤ 0l_27_0l_27_0 ≤ 0l_1519_post + l_1519_post ≤ 0l_1519_postl_1519_post ≤ 0l_1519_0 + l_1519_0 ≤ 0l_1519_0l_1519_0 ≤ 0l_1429_post + l_1429_post ≤ 0l_1429_postl_1429_post ≤ 0l_1429_0 + l_1429_0 ≤ 0l_1429_0l_1429_0 ≤ 0l_1304_post + l_1304_post ≤ 0l_1304_postl_1304_post ≤ 0l_1304_0 + l_1304_0 ≤ 0l_1304_0l_1304_0 ≤ 0l_1119_post + l_1119_post ≤ 0l_1119_postl_1119_post ≤ 0l_1119_1 + l_1119_1 ≤ 0l_1119_1l_1119_1 ≤ 0l_1119_0 + l_1119_0 ≤ 0l_1119_0l_1119_0 ≤ 0j_39_post + j_39_post ≤ 0j_39_postj_39_post ≤ 0j_39_0 + j_39_0 ≤ 0j_39_0j_39_0 ≤ 0j_36_post + j_36_post ≤ 0j_36_postj_36_post ≤ 0j_36_0 + j_36_0 ≤ 0j_36_0j_36_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0h_46_post + h_46_post ≤ 0h_46_posth_46_post ≤ 0h_46_1 + h_46_1 ≤ 0h_46_1h_46_1 ≤ 0h_46_0 + h_46_0 ≤ 0h_46_0h_46_0 ≤ 0h_37_post + h_37_post ≤ 0h_37_posth_37_post ≤ 0h_37_0 + h_37_0 ≤ 0h_37_0h_37_0 ≤ 0h_34_post + h_34_post ≤ 0h_34_posth_34_post ≤ 0h_34_2 + h_34_2 ≤ 0h_34_2h_34_2 ≤ 0h_34_1 + h_34_1 ≤ 0h_34_1h_34_1 ≤ 0h_34_0 + h_34_0 ≤ 0h_34_0h_34_0 ≤ 0h_28_post + h_28_post ≤ 0h_28_posth_28_post ≤ 0h_28_0 + h_28_0 ≤ 0h_28_0h_28_0 ≤ 0f_1323_post + f_1323_post ≤ 0f_1323_postf_1323_post ≤ 0f_1323_0 + f_1323_0 ≤ 0f_1323_0f_1323_0 ≤ 0fF_1324_post + fF_1324_post ≤ 0fF_1324_postfF_1324_post ≤ 0fF_1324_0 + fF_1324_0 ≤ 0fF_1324_0fF_1324_0 ≤ 0c_990_post + c_990_post ≤ 0c_990_postc_990_post ≤ 0c_990_0 + c_990_0 ≤ 0c_990_0c_990_0 ≤ 0c_98_post + c_98_post ≤ 0c_98_postc_98_post ≤ 0c_98_1 + c_98_1 ≤ 0c_98_1c_98_1 ≤ 0c_98_0 + c_98_0 ≤ 0c_98_0c_98_0 ≤ 0c_958_post + c_958_post ≤ 0c_958_postc_958_post ≤ 0c_958_1 + c_958_1 ≤ 0c_958_1c_958_1 ≤ 0c_958_0 + c_958_0 ≤ 0c_958_0c_958_0 ≤ 0c_901_post + c_901_post ≤ 0c_901_postc_901_post ≤ 0c_901_0 + c_901_0 ≤ 0c_901_0c_901_0 ≤ 0c_1481_post + c_1481_post ≤ 0c_1481_postc_1481_post ≤ 0c_1481_1 + c_1481_1 ≤ 0c_1481_1c_1481_1 ≤ 0c_1481_0 + c_1481_0 ≤ 0c_1481_0c_1481_0 ≤ 0c_1186_post + c_1186_post ≤ 0c_1186_postc_1186_post ≤ 0c_1186_0 + c_1186_0 ≤ 0c_1186_0c_1186_0 ≤ 0Flink_0 + Flink_0 ≤ 0Flink_0Flink_0 ≤ 0

6 SCC Decomposition

We consider subproblems for each of the 1 SCC(s) of the program graph.

6.1 SCC Subproblem 1/1

Here we consider the SCC { 0, 1, 2, 3, 9, 10, 0_var_snapshot, 0* }.

6.1.1 Transition Removal

We remove transitions 11, 12, 13 using the following ranking functions, which are bounded by 2.

0: 8⋅l_27_0 − 8⋅mt_18_0
1: 8⋅l_27_0 − 8⋅mt_18_0 − 2⋅mt_18_1
2: −3 + 8⋅l_27_0 − 8⋅lt_10_0
3: −4 + 8⋅l_27_0 − 8⋅lt_10_0
9: 3 + 8⋅l_27_0 − 8⋅lt_10_0 + 8⋅lt_17_0 − 8⋅mt_18_0
10: 8⋅l_27_0 − 8⋅mt_18_0 + 2⋅mt_18_1
0_var_snapshot: −1 + 8⋅l_27_0 − 8⋅mt_18_0
0*: −1 + 8⋅l_27_0 − 8⋅mt_18_0 + 2⋅mt_18_1

6.1.2 Transition Removal

We remove transitions 20, 0, 1, 2, 3, 14 using the following ranking functions, which are bounded by −2.

0: −2 + l_27_0 + 3⋅l_27_post
1: 0
2: mt_18_1
3: −2⋅mt_18_1
9: 0
10: l_27_0 + 3⋅l_27_post
0_var_snapshot: l_27_0
0*: −1 + l_27_0 + 3⋅l_27_post

6.1.3 Transition Removal

We remove transition 18 using the following ranking functions, which are bounded by 0.

0: mt_18_1
1: 0
2: 0
3: 0
9: 0
10: 0
0_var_snapshot: 0
0*: 0

6.1.4 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

6.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 17.

6.1.4.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert