LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0
1: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0
2: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ − l_1519_0 ≤ 0
3: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0
4: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0
5: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 ∧ − l_1429_0 ≤ 0
6: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0
7: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ − l_287_0 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0 ∧ − l_855_0 ≤ 0
8: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0 ∧ j_36_post ≤ 0 ∧ − j_36_post ≤ 0 ∧ j_39_post ≤ 0 ∧ j_36_0 ≤ 0 ∧ − j_36_0 ≤ 0 ∧ j_39_0 ≤ 0 ∧ − j_39_0 ≤ 0
9: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_20_0 ≤ 0
10: h_28_post ≤ 0 ∧ − h_28_post ≤ 0 ∧ 1 − l_27_post ≤ 0 ∧ mt_20_post ≤ 0 ∧ − mt_20_post ≤ 0 ∧ h_34_1 ≤ 0 ∧ − h_34_1 ≤ 0 ∧ lt_10_1 ≤ 0 ∧ − lt_10_1 ≤ 0 ∧ lt_17_1 ≤ 0 ∧ − lt_17_1 ≤ 0 ∧ −1 + mt_18_1 ≤ 0 ∧ 1 − mt_18_1 ≤ 0 ∧ h_28_0 ≤ 0 ∧ − h_28_0 ≤ 0 ∧ 1 − l_27_0 ≤ 0 ∧ mt_20_0 ≤ 0 ∧ − mt_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 ≤ 0 ∧ tp_44_post − tp_44_post ≤ 0 ∧ − tp_44_3 + tp_44_3 ≤ 0 ∧ tp_44_3 − tp_44_3 ≤ 0 ∧ − tp_44_2 + tp_44_2 ≤ 0 ∧ tp_44_2 − tp_44_2 ≤ 0 ∧ − tp_44_1 + tp_44_1 ≤ 0 ∧ tp_44_1 − tp_44_1 ≤ 0 ∧ − tp_44_0 + tp_44_0 ≤ 0 ∧ tp_44_0 − tp_44_0 ≤ 0 ∧ − tp_32_post + tp_32_post ≤ 0 ∧ tp_32_post − tp_32_post ≤ 0 ∧ − tp_32_2 + tp_32_2 ≤ 0 ∧ tp_32_2 − tp_32_2 ≤ 0 ∧ − tp_32_1 + tp_32_1 ≤ 0 ∧ tp_32_1 − tp_32_1 ≤ 0 ∧ − tp_32_0 + tp_32_0 ≤ 0 ∧ tp_32_0 − tp_32_0 ≤ 0 ∧ − tp_30_post + tp_30_post ≤ 0 ∧ tp_30_post − tp_30_post ≤ 0 ∧ − tp_30_1 + tp_30_1 ≤ 0 ∧ tp_30_1 − tp_30_1 ≤ 0 ∧ − tp_30_0 + tp_30_0 ≤ 0 ∧ tp_30_0 − tp_30_0 ≤ 0 ∧ − tp_19_0 + tp_19_0 ≤ 0 ∧ tp_19_0 − tp_19_0 ≤ 0 ∧ − t_45_post + t_45_post ≤ 0 ∧ t_45_post − t_45_post ≤ 0 ∧ − t_45_1 + t_45_1 ≤ 0 ∧ t_45_1 − t_45_1 ≤ 0 ∧ − t_45_0 + t_45_0 ≤ 0 ∧ t_45_0 − t_45_0 ≤ 0 ∧ − t_40_post + t_40_post ≤ 0 ∧ t_40_post − t_40_post ≤ 0 ∧ − t_40_0 + t_40_0 ≤ 0 ∧ t_40_0 − t_40_0 ≤ 0 ∧ − t_38_post + t_38_post ≤ 0 ∧ t_38_post − t_38_post ≤ 0 ∧ − t_38_0 + t_38_0 ≤ 0 ∧ t_38_0 − t_38_0 ≤ 0 ∧ − t_35_post + t_35_post ≤ 0 ∧ t_35_post − t_35_post ≤ 0 ∧ − t_35_2 + t_35_2 ≤ 0 ∧ t_35_2 − t_35_2 ≤ 0 ∧ − t_35_1 + t_35_1 ≤ 0 ∧ t_35_1 − t_35_1 ≤ 0 ∧ − t_35_0 + t_35_0 ≤ 0 ∧ t_35_0 − t_35_0 ≤ 0 ∧ − t_14_0 + t_14_0 ≤ 0 ∧ t_14_0 − t_14_0 ≤ 0 ∧ − t_1303_post + t_1303_post ≤ 0 ∧ t_1303_post − t_1303_post ≤ 0 ∧ − t_1303_0 + t_1303_0 ≤ 0 ∧ t_1303_0 − t_1303_0 ≤ 0 ∧ − t_1057_post + t_1057_post ≤ 0 ∧ t_1057_post − t_1057_post ≤ 0 ∧ − t_1057_0 + t_1057_0 ≤ 0 ∧ t_1057_0 − t_1057_0 ≤ 0 ∧ − sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0 ∧ sCALLSITERETURN_43_post − sCALLSITERETURN_43_post ≤ 0 ∧ − sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0 ∧ sCALLSITERETURN_43_1 − sCALLSITERETURN_43_1 ≤ 0 ∧ − sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0 ∧ sCALLSITERETURN_43_0 − sCALLSITERETURN_43_0 ≤ 0 ∧ − sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0 ∧ sCALLSITERETURN_33_post − sCALLSITERETURN_33_post ≤ 0 ∧ − sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0 ∧ sCALLSITERETURN_33_2 − sCALLSITERETURN_33_2 ≤ 0 ∧ − sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0 ∧ sCALLSITERETURN_33_1 − sCALLSITERETURN_33_1 ≤ 0 ∧ − sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0 ∧ sCALLSITERETURN_33_0 − sCALLSITERETURN_33_0 ≤ 0 ∧ − sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0 ∧ sCALLSITERETURN_29_post − sCALLSITERETURN_29_post ≤ 0 ∧ − sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0 ∧ sCALLSITERETURN_29_0 − sCALLSITERETURN_29_0 ≤ 0 ∧ − sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0 ∧ sCALLSITERETURN_16_0 − sCALLSITERETURN_16_0 ≤ 0 ∧ − nd_7_post + nd_7_post ≤ 0 ∧ nd_7_post − nd_7_post ≤ 0 ∧ − nd_7_1 + nd_7_1 ≤ 0 ∧ nd_7_1 − nd_7_1 ≤ 0 ∧ − nd_7_0 + nd_7_0 ≤ 0 ∧ nd_7_0 − nd_7_0 ≤ 0 ∧ − mt_20_post + mt_20_post ≤ 0 ∧ mt_20_post − mt_20_post ≤ 0 ∧ − mt_20_0 + mt_20_0 ≤ 0 ∧ mt_20_0 − mt_20_0 ≤ 0 ∧ − mt_18_post + mt_18_post ≤ 0 ∧ mt_18_post − mt_18_post ≤ 0 ∧ − mt_18_1 + mt_18_1 ≤ 0 ∧ mt_18_1 − mt_18_1 ≤ 0 ∧ − mt_18_0 + mt_18_0 ≤ 0 ∧ mt_18_0 − mt_18_0 ≤ 0 ∧ − lt_17_post + lt_17_post ≤ 0 ∧ lt_17_post − lt_17_post ≤ 0 ∧ − lt_17_1 + lt_17_1 ≤ 0 ∧ lt_17_1 − lt_17_1 ≤ 0 ∧ − lt_17_0 + lt_17_0 ≤ 0 ∧ lt_17_0 − lt_17_0 ≤ 0 ∧ − lt_1256_post + lt_1256_post ≤ 0 ∧ lt_1256_post − lt_1256_post ≤ 0 ∧ − lt_1256_0 + lt_1256_0 ≤ 0 ∧ lt_1256_0 − lt_1256_0 ≤ 0 ∧ − lt_10_post + lt_10_post ≤ 0 ∧ lt_10_post − lt_10_post ≤ 0 ∧ − lt_10_1 + lt_10_1 ≤ 0 ∧ lt_10_1 − lt_10_1 ≤ 0 ∧ − lt_10_0 + lt_10_0 ≤ 0 ∧ lt_10_0 − lt_10_0 ≤ 0 ∧ − l_855_post + l_855_post ≤ 0 ∧ l_855_post − l_855_post ≤ 0 ∧ − l_855_0 + l_855_0 ≤ 0 ∧ l_855_0 − l_855_0 ≤ 0 ∧ − l_287_post + l_287_post ≤ 0 ∧ l_287_post − l_287_post ≤ 0 ∧ − l_287_0 + l_287_0 ≤ 0 ∧ l_287_0 − l_287_0 ≤ 0 ∧ − l_27_post + l_27_post ≤ 0 ∧ l_27_post − l_27_post ≤ 0 ∧ − l_27_0 + l_27_0 ≤ 0 ∧ l_27_0 − l_27_0 ≤ 0 ∧ − l_1519_post + l_1519_post ≤ 0 ∧ l_1519_post − l_1519_post ≤ 0 ∧ − l_1519_0 + l_1519_0 ≤ 0 ∧ l_1519_0 − l_1519_0 ≤ 0 ∧ − l_1429_post + l_1429_post ≤ 0 ∧ l_1429_post − l_1429_post ≤ 0 ∧ − l_1429_0 + l_1429_0 ≤ 0 ∧ l_1429_0 − l_1429_0 ≤ 0 ∧ − l_1304_post + l_1304_post ≤ 0 ∧ l_1304_post − l_1304_post ≤ 0 ∧ − l_1304_0 + l_1304_0 ≤ 0 ∧ l_1304_0 − l_1304_0 ≤ 0 ∧ − l_1119_post + l_1119_post ≤ 0 ∧ l_1119_post − l_1119_post ≤ 0 ∧ − l_1119_1 + l_1119_1 ≤ 0 ∧ l_1119_1 − l_1119_1 ≤ 0 ∧ − l_1119_0 + l_1119_0 ≤ 0 ∧ l_1119_0 − l_1119_0 ≤ 0 ∧ − j_39_post + j_39_post ≤ 0 ∧ j_39_post − j_39_post ≤ 0 ∧ − j_39_0 + j_39_0 ≤ 0 ∧ j_39_0 − j_39_0 ≤ 0 ∧ − j_36_post + j_36_post ≤ 0 ∧ j_36_post − j_36_post ≤ 0 ∧ − j_36_0 + j_36_0 ≤ 0 ∧ j_36_0 − j_36_0 ≤ 0 ∧ − i_31_post + i_31_post ≤ 0 ∧ i_31_post − i_31_post ≤ 0 ∧ − i_31_0 + i_31_0 ≤ 0 ∧ i_31_0 − i_31_0 ≤ 0 ∧ − h_46_post + h_46_post ≤ 0 ∧ h_46_post − h_46_post ≤ 0 ∧ − h_46_1 + h_46_1 ≤ 0 ∧ h_46_1 − h_46_1 ≤ 0 ∧ − h_46_0 + h_46_0 ≤ 0 ∧ h_46_0 − h_46_0 ≤ 0 ∧ − h_37_post + h_37_post ≤ 0 ∧ h_37_post − h_37_post ≤ 0 ∧ − h_37_0 + h_37_0 ≤ 0 ∧ h_37_0 − h_37_0 ≤ 0 ∧ − h_34_post + h_34_post ≤ 0 ∧ h_34_post − h_34_post ≤ 0 ∧ − h_34_2 + h_34_2 ≤ 0 ∧ h_34_2 − h_34_2 ≤ 0 ∧ − h_34_1 + h_34_1 ≤ 0 ∧ h_34_1 − h_34_1 ≤ 0 ∧ − h_34_0 + h_34_0 ≤ 0 ∧ h_34_0 − h_34_0 ≤ 0 ∧ − h_28_post + h_28_post ≤ 0 ∧ h_28_post − h_28_post ≤ 0 ∧ − h_28_0 + h_28_0 ≤ 0 ∧ h_28_0 − h_28_0 ≤ 0 ∧ − f_1323_post + f_1323_post ≤ 0 ∧ f_1323_post − f_1323_post ≤ 0 ∧ − f_1323_0 + f_1323_0 ≤ 0 ∧ f_1323_0 − f_1323_0 ≤ 0 ∧ − fF_1324_post + fF_1324_post ≤ 0 ∧ fF_1324_post − fF_1324_post ≤ 0 ∧ − fF_1324_0 + fF_1324_0 ≤ 0 ∧ fF_1324_0 − fF_1324_0 ≤ 0 ∧ − c_990_post + c_990_post ≤ 0 ∧ c_990_post − c_990_post ≤ 0 ∧ − c_990_0 + c_990_0 ≤ 0 ∧ c_990_0 − c_990_0 ≤ 0 ∧ − c_98_post + c_98_post ≤ 0 ∧ c_98_post − c_98_post ≤ 0 ∧ − c_98_1 + c_98_1 ≤ 0 ∧ c_98_1 − c_98_1 ≤ 0 ∧ − c_98_0 + c_98_0 ≤ 0 ∧ c_98_0 − c_98_0 ≤ 0 ∧ − c_958_post + c_958_post ≤ 0 ∧ c_958_post − c_958_post ≤ 0 ∧ − c_958_1 + c_958_1 ≤ 0 ∧ c_958_1 − c_958_1 ≤ 0 ∧ − c_958_0 + c_958_0 ≤ 0 ∧ c_958_0 − c_958_0 ≤ 0 ∧ − c_901_post + c_901_post ≤ 0 ∧ c_901_post − c_901_post ≤ 0 ∧ − c_901_0 + c_901_0 ≤ 0 ∧ c_901_0 − c_901_0 ≤ 0 ∧ − c_1481_post + c_1481_post ≤ 0 ∧ c_1481_post − c_1481_post ≤ 0 ∧ − c_1481_1 + c_1481_1 ≤ 0 ∧ c_1481_1 − c_1481_1 ≤ 0 ∧ − c_1481_0 + c_1481_0 ≤ 0 ∧ c_1481_0 − c_1481_0 ≤ 0 ∧ − c_1186_post + c_1186_post ≤ 0 ∧ c_1186_post − c_1186_post ≤ 0 ∧ − c_1186_0 + c_1186_0 ≤ 0 ∧ c_1186_0 − c_1186_0 ≤ 0 ∧ − Flink_0 + Flink_0 ≤ 0 ∧ Flink_0 − Flink_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 ≤ 0 ∧ tp_44_post − tp_44_post ≤ 0 ∧ − tp_44_3 + tp_44_3 ≤ 0 ∧ tp_44_3 − tp_44_3 ≤ 0 ∧ − tp_44_2 + tp_44_2 ≤ 0 ∧ tp_44_2 − tp_44_2 ≤ 0 ∧ − tp_44_1 + tp_44_1 ≤ 0 ∧ tp_44_1 − tp_44_1 ≤ 0 ∧ − tp_44_0 + tp_44_0 ≤ 0 ∧ tp_44_0 − tp_44_0 ≤ 0 ∧ − tp_32_post + tp_32_post ≤ 0 ∧ tp_32_post − tp_32_post ≤ 0 ∧ − tp_32_2 + tp_32_2 ≤ 0 ∧ tp_32_2 − tp_32_2 ≤ 0 ∧ − tp_32_1 + tp_32_1 ≤ 0 ∧ tp_32_1 − tp_32_1 ≤ 0 ∧ − tp_32_0 + tp_32_0 ≤ 0 ∧ tp_32_0 − tp_32_0 ≤ 0 ∧ − tp_30_post + tp_30_post ≤ 0 ∧ tp_30_post − tp_30_post ≤ 0 ∧ − tp_30_1 + tp_30_1 ≤ 0 ∧ tp_30_1 − tp_30_1 ≤ 0 ∧ − tp_30_0 + tp_30_0 ≤ 0 ∧ tp_30_0 − tp_30_0 ≤ 0 ∧ − tp_19_0 + tp_19_0 ≤ 0 ∧ tp_19_0 − tp_19_0 ≤ 0 ∧ − t_45_post + t_45_post ≤ 0 ∧ t_45_post − t_45_post ≤ 0 ∧ − t_45_1 + t_45_1 ≤ 0 ∧ t_45_1 − t_45_1 ≤ 0 ∧ − t_45_0 + t_45_0 ≤ 0 ∧ t_45_0 − t_45_0 ≤ 0 ∧ − t_40_post + t_40_post ≤ 0 ∧ t_40_post − t_40_post ≤ 0 ∧ − t_40_0 + t_40_0 ≤ 0 ∧ t_40_0 − t_40_0 ≤ 0 ∧ − t_38_post + t_38_post ≤ 0 ∧ t_38_post − t_38_post ≤ 0 ∧ − t_38_0 + t_38_0 ≤ 0 ∧ t_38_0 − t_38_0 ≤ 0 ∧ − t_35_post + t_35_post ≤ 0 ∧ t_35_post − t_35_post ≤ 0 ∧ − t_35_2 + t_35_2 ≤ 0 ∧ t_35_2 − t_35_2 ≤ 0 ∧ − t_35_1 + t_35_1 ≤ 0 ∧ t_35_1 − t_35_1 ≤ 0 ∧ − t_35_0 + t_35_0 ≤ 0 ∧ t_35_0 − t_35_0 ≤ 0 ∧ − t_14_0 + t_14_0 ≤ 0 ∧ t_14_0 − t_14_0 ≤ 0 ∧ − t_1303_post + t_1303_post ≤ 0 ∧ t_1303_post − t_1303_post ≤ 0 ∧ − t_1303_0 + t_1303_0 ≤ 0 ∧ t_1303_0 − t_1303_0 ≤ 0 ∧ − t_1057_post + t_1057_post ≤ 0 ∧ t_1057_post − t_1057_post ≤ 0 ∧ − t_1057_0 + t_1057_0 ≤ 0 ∧ t_1057_0 − t_1057_0 ≤ 0 ∧ − sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0 ∧ sCALLSITERETURN_43_post − sCALLSITERETURN_43_post ≤ 0 ∧ − sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0 ∧ sCALLSITERETURN_43_1 − sCALLSITERETURN_43_1 ≤ 0 ∧ − sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0 ∧ sCALLSITERETURN_43_0 − sCALLSITERETURN_43_0 ≤ 0 ∧ − sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0 ∧ sCALLSITERETURN_33_post − sCALLSITERETURN_33_post ≤ 0 ∧ − sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0 ∧ sCALLSITERETURN_33_2 − sCALLSITERETURN_33_2 ≤ 0 ∧ − sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0 ∧ sCALLSITERETURN_33_1 − sCALLSITERETURN_33_1 ≤ 0 ∧ − sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0 ∧ sCALLSITERETURN_33_0 − sCALLSITERETURN_33_0 ≤ 0 ∧ − sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0 ∧ sCALLSITERETURN_29_post − sCALLSITERETURN_29_post ≤ 0 ∧ − sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0 ∧ sCALLSITERETURN_29_0 − sCALLSITERETURN_29_0 ≤ 0 ∧ − sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0 ∧ sCALLSITERETURN_16_0 − sCALLSITERETURN_16_0 ≤ 0 ∧ − nd_7_post + nd_7_post ≤ 0 ∧ nd_7_post − nd_7_post ≤ 0 ∧ − nd_7_1 + nd_7_1 ≤ 0 ∧ nd_7_1 − nd_7_1 ≤ 0 ∧ − nd_7_0 + nd_7_0 ≤ 0 ∧ nd_7_0 − nd_7_0 ≤ 0 ∧ − mt_20_post + mt_20_post ≤ 0 ∧ mt_20_post − mt_20_post ≤ 0 ∧ − mt_20_0 + mt_20_0 ≤ 0 ∧ mt_20_0 − mt_20_0 ≤ 0 ∧ − mt_18_post + mt_18_post ≤ 0 ∧ mt_18_post − mt_18_post ≤ 0 ∧ − mt_18_1 + mt_18_1 ≤ 0 ∧ mt_18_1 − mt_18_1 ≤ 0 ∧ − mt_18_0 + mt_18_0 ≤ 0 ∧ mt_18_0 − mt_18_0 ≤ 0 ∧ − lt_17_post + lt_17_post ≤ 0 ∧ lt_17_post − lt_17_post ≤ 0 ∧ − lt_17_1 + lt_17_1 ≤ 0 ∧ lt_17_1 − lt_17_1 ≤ 0 ∧ − lt_17_0 + lt_17_0 ≤ 0 ∧ lt_17_0 − lt_17_0 ≤ 0 ∧ − lt_1256_post + lt_1256_post ≤ 0 ∧ lt_1256_post − lt_1256_post ≤ 0 ∧ − lt_1256_0 + lt_1256_0 ≤ 0 ∧ lt_1256_0 − lt_1256_0 ≤ 0 ∧ − lt_10_post + lt_10_post ≤ 0 ∧ lt_10_post − lt_10_post ≤ 0 ∧ − lt_10_1 + lt_10_1 ≤ 0 ∧ lt_10_1 − lt_10_1 ≤ 0 ∧ − lt_10_0 + lt_10_0 ≤ 0 ∧ lt_10_0 − lt_10_0 ≤ 0 ∧ − l_855_post + l_855_post ≤ 0 ∧ l_855_post − l_855_post ≤ 0 ∧ − l_855_0 + l_855_0 ≤ 0 ∧ l_855_0 − l_855_0 ≤ 0 ∧ − l_287_post + l_287_post ≤ 0 ∧ l_287_post − l_287_post ≤ 0 ∧ − l_287_0 + l_287_0 ≤ 0 ∧ l_287_0 − l_287_0 ≤ 0 ∧ − l_27_post + l_27_post ≤ 0 ∧ l_27_post − l_27_post ≤ 0 ∧ − l_27_0 + l_27_0 ≤ 0 ∧ l_27_0 − l_27_0 ≤ 0 ∧ − l_1519_post + l_1519_post ≤ 0 ∧ l_1519_post − l_1519_post ≤ 0 ∧ − l_1519_0 + l_1519_0 ≤ 0 ∧ l_1519_0 − l_1519_0 ≤ 0 ∧ − l_1429_post + l_1429_post ≤ 0 ∧ l_1429_post − l_1429_post ≤ 0 ∧ − l_1429_0 + l_1429_0 ≤ 0 ∧ l_1429_0 − l_1429_0 ≤ 0 ∧ − l_1304_post + l_1304_post ≤ 0 ∧ l_1304_post − l_1304_post ≤ 0 ∧ − l_1304_0 + l_1304_0 ≤ 0 ∧ l_1304_0 − l_1304_0 ≤ 0 ∧ − l_1119_post + l_1119_post ≤ 0 ∧ l_1119_post − l_1119_post ≤ 0 ∧ − l_1119_1 + l_1119_1 ≤ 0 ∧ l_1119_1 − l_1119_1 ≤ 0 ∧ − l_1119_0 + l_1119_0 ≤ 0 ∧ l_1119_0 − l_1119_0 ≤ 0 ∧ − j_39_post + j_39_post ≤ 0 ∧ j_39_post − j_39_post ≤ 0 ∧ − j_39_0 + j_39_0 ≤ 0 ∧ j_39_0 − j_39_0 ≤ 0 ∧ − j_36_post + j_36_post ≤ 0 ∧ j_36_post − j_36_post ≤ 0 ∧ − j_36_0 + j_36_0 ≤ 0 ∧ j_36_0 − j_36_0 ≤ 0 ∧ − i_31_post + i_31_post ≤ 0 ∧ i_31_post − i_31_post ≤ 0 ∧ − i_31_0 + i_31_0 ≤ 0 ∧ i_31_0 − i_31_0 ≤ 0 ∧ − h_46_post + h_46_post ≤ 0 ∧ h_46_post − h_46_post ≤ 0 ∧ − h_46_1 + h_46_1 ≤ 0 ∧ h_46_1 − h_46_1 ≤ 0 ∧ − h_46_0 + h_46_0 ≤ 0 ∧ h_46_0 − h_46_0 ≤ 0 ∧ − h_37_post + h_37_post ≤ 0 ∧ h_37_post − h_37_post ≤ 0 ∧ − h_37_0 + h_37_0 ≤ 0 ∧ h_37_0 − h_37_0 ≤ 0 ∧ − h_34_post + h_34_post ≤ 0 ∧ h_34_post − h_34_post ≤ 0 ∧ − h_34_2 + h_34_2 ≤ 0 ∧ h_34_2 − h_34_2 ≤ 0 ∧ − h_34_1 + h_34_1 ≤ 0 ∧ h_34_1 − h_34_1 ≤ 0 ∧ − h_34_0 + h_34_0 ≤ 0 ∧ h_34_0 − h_34_0 ≤ 0 ∧ − h_28_post + h_28_post ≤ 0 ∧ h_28_post − h_28_post ≤ 0 ∧ − h_28_0 + h_28_0 ≤ 0 ∧ h_28_0 − h_28_0 ≤ 0 ∧ − f_1323_post + f_1323_post ≤ 0 ∧ f_1323_post − f_1323_post ≤ 0 ∧ − f_1323_0 + f_1323_0 ≤ 0 ∧ f_1323_0 − f_1323_0 ≤ 0 ∧ − fF_1324_post + fF_1324_post ≤ 0 ∧ fF_1324_post − fF_1324_post ≤ 0 ∧ − fF_1324_0 + fF_1324_0 ≤ 0 ∧ fF_1324_0 − fF_1324_0 ≤ 0 ∧ − c_990_post + c_990_post ≤ 0 ∧ c_990_post − c_990_post ≤ 0 ∧ − c_990_0 + c_990_0 ≤ 0 ∧ c_990_0 − c_990_0 ≤ 0 ∧ − c_98_post + c_98_post ≤ 0 ∧ c_98_post − c_98_post ≤ 0 ∧ − c_98_1 + c_98_1 ≤ 0 ∧ c_98_1 − c_98_1 ≤ 0 ∧ − c_98_0 + c_98_0 ≤ 0 ∧ c_98_0 − c_98_0 ≤ 0 ∧ − c_958_post + c_958_post ≤ 0 ∧ c_958_post − c_958_post ≤ 0 ∧ − c_958_1 + c_958_1 ≤ 0 ∧ c_958_1 − c_958_1 ≤ 0 ∧ − c_958_0 + c_958_0 ≤ 0 ∧ c_958_0 − c_958_0 ≤ 0 ∧ − c_901_post + c_901_post ≤ 0 ∧ c_901_post − c_901_post ≤ 0 ∧ − c_901_0 + c_901_0 ≤ 0 ∧ c_901_0 − c_901_0 ≤ 0 ∧ − c_1481_post + c_1481_post ≤ 0 ∧ c_1481_post − c_1481_post ≤ 0 ∧ − c_1481_1 + c_1481_1 ≤ 0 ∧ c_1481_1 − c_1481_1 ≤ 0 ∧ − c_1481_0 + c_1481_0 ≤ 0 ∧ c_1481_0 − c_1481_0 ≤ 0 ∧ − c_1186_post + c_1186_post ≤ 0 ∧ c_1186_post − c_1186_post ≤ 0 ∧ − c_1186_0 + c_1186_0 ≤ 0 ∧ c_1186_0 − c_1186_0 ≤ 0 ∧ − Flink_0 + Flink_0 ≤ 0 ∧ Flink_0 − Flink_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 ≤ 0 ∧ tp_44_post − tp_44_post ≤ 0 ∧ − tp_44_3 + tp_44_3 ≤ 0 ∧ tp_44_3 − tp_44_3 ≤ 0 ∧ − tp_44_2 + tp_44_2 ≤ 0 ∧ tp_44_2 − tp_44_2 ≤ 0 ∧ − tp_44_1 + tp_44_1 ≤ 0 ∧ tp_44_1 − tp_44_1 ≤ 0 ∧ − tp_44_0 + tp_44_0 ≤ 0 ∧ tp_44_0 − tp_44_0 ≤ 0 ∧ − tp_32_post + tp_32_post ≤ 0 ∧ tp_32_post − tp_32_post ≤ 0 ∧ − tp_32_2 + tp_32_2 ≤ 0 ∧ tp_32_2 − tp_32_2 ≤ 0 ∧ − tp_32_1 + tp_32_1 ≤ 0 ∧ tp_32_1 − tp_32_1 ≤ 0 ∧ − tp_32_0 + tp_32_0 ≤ 0 ∧ tp_32_0 − tp_32_0 ≤ 0 ∧ − tp_30_post + tp_30_post ≤ 0 ∧ tp_30_post − tp_30_post ≤ 0 ∧ − tp_30_1 + tp_30_1 ≤ 0 ∧ tp_30_1 − tp_30_1 ≤ 0 ∧ − tp_30_0 + tp_30_0 ≤ 0 ∧ tp_30_0 − tp_30_0 ≤ 0 ∧ − tp_19_0 + tp_19_0 ≤ 0 ∧ tp_19_0 − tp_19_0 ≤ 0 ∧ − t_45_post + t_45_post ≤ 0 ∧ t_45_post − t_45_post ≤ 0 ∧ − t_45_1 + t_45_1 ≤ 0 ∧ t_45_1 − t_45_1 ≤ 0 ∧ − t_45_0 + t_45_0 ≤ 0 ∧ t_45_0 − t_45_0 ≤ 0 ∧ − t_40_post + t_40_post ≤ 0 ∧ t_40_post − t_40_post ≤ 0 ∧ − t_40_0 + t_40_0 ≤ 0 ∧ t_40_0 − t_40_0 ≤ 0 ∧ − t_38_post + t_38_post ≤ 0 ∧ t_38_post − t_38_post ≤ 0 ∧ − t_38_0 + t_38_0 ≤ 0 ∧ t_38_0 − t_38_0 ≤ 0 ∧ − t_35_post + t_35_post ≤ 0 ∧ t_35_post − t_35_post ≤ 0 ∧ − t_35_2 + t_35_2 ≤ 0 ∧ t_35_2 − t_35_2 ≤ 0 ∧ − t_35_1 + t_35_1 ≤ 0 ∧ t_35_1 − t_35_1 ≤ 0 ∧ − t_35_0 + t_35_0 ≤ 0 ∧ t_35_0 − t_35_0 ≤ 0 ∧ − t_14_0 + t_14_0 ≤ 0 ∧ t_14_0 − t_14_0 ≤ 0 ∧ − t_1303_post + t_1303_post ≤ 0 ∧ t_1303_post − t_1303_post ≤ 0 ∧ − t_1303_0 + t_1303_0 ≤ 0 ∧ t_1303_0 − t_1303_0 ≤ 0 ∧ − t_1057_post + t_1057_post ≤ 0 ∧ t_1057_post − t_1057_post ≤ 0 ∧ − t_1057_0 + t_1057_0 ≤ 0 ∧ t_1057_0 − t_1057_0 ≤ 0 ∧ − sCALLSITERETURN_43_post + sCALLSITERETURN_43_post ≤ 0 ∧ sCALLSITERETURN_43_post − sCALLSITERETURN_43_post ≤ 0 ∧ − sCALLSITERETURN_43_1 + sCALLSITERETURN_43_1 ≤ 0 ∧ sCALLSITERETURN_43_1 − sCALLSITERETURN_43_1 ≤ 0 ∧ − sCALLSITERETURN_43_0 + sCALLSITERETURN_43_0 ≤ 0 ∧ sCALLSITERETURN_43_0 − sCALLSITERETURN_43_0 ≤ 0 ∧ − sCALLSITERETURN_33_post + sCALLSITERETURN_33_post ≤ 0 ∧ sCALLSITERETURN_33_post − sCALLSITERETURN_33_post ≤ 0 ∧ − sCALLSITERETURN_33_2 + sCALLSITERETURN_33_2 ≤ 0 ∧ sCALLSITERETURN_33_2 − sCALLSITERETURN_33_2 ≤ 0 ∧ − sCALLSITERETURN_33_1 + sCALLSITERETURN_33_1 ≤ 0 ∧ sCALLSITERETURN_33_1 − sCALLSITERETURN_33_1 ≤ 0 ∧ − sCALLSITERETURN_33_0 + sCALLSITERETURN_33_0 ≤ 0 ∧ sCALLSITERETURN_33_0 − sCALLSITERETURN_33_0 ≤ 0 ∧ − sCALLSITERETURN_29_post + sCALLSITERETURN_29_post ≤ 0 ∧ sCALLSITERETURN_29_post − sCALLSITERETURN_29_post ≤ 0 ∧ − sCALLSITERETURN_29_0 + sCALLSITERETURN_29_0 ≤ 0 ∧ sCALLSITERETURN_29_0 − sCALLSITERETURN_29_0 ≤ 0 ∧ − sCALLSITERETURN_16_0 + sCALLSITERETURN_16_0 ≤ 0 ∧ sCALLSITERETURN_16_0 − sCALLSITERETURN_16_0 ≤ 0 ∧ − nd_7_post + nd_7_post ≤ 0 ∧ nd_7_post − nd_7_post ≤ 0 ∧ − nd_7_1 + nd_7_1 ≤ 0 ∧ nd_7_1 − nd_7_1 ≤ 0 ∧ − nd_7_0 + nd_7_0 ≤ 0 ∧ nd_7_0 − nd_7_0 ≤ 0 ∧ − mt_20_post + mt_20_post ≤ 0 ∧ mt_20_post − mt_20_post ≤ 0 ∧ − mt_20_0 + mt_20_0 ≤ 0 ∧ mt_20_0 − mt_20_0 ≤ 0 ∧ − mt_18_post + mt_18_post ≤ 0 ∧ mt_18_post − mt_18_post ≤ 0 ∧ − mt_18_1 + mt_18_1 ≤ 0 ∧ mt_18_1 − mt_18_1 ≤ 0 ∧ − mt_18_0 + mt_18_0 ≤ 0 ∧ mt_18_0 − mt_18_0 ≤ 0 ∧ − lt_17_post + lt_17_post ≤ 0 ∧ lt_17_post − lt_17_post ≤ 0 ∧ − lt_17_1 + lt_17_1 ≤ 0 ∧ lt_17_1 − lt_17_1 ≤ 0 ∧ − lt_17_0 + lt_17_0 ≤ 0 ∧ lt_17_0 − lt_17_0 ≤ 0 ∧ − lt_1256_post + lt_1256_post ≤ 0 ∧ lt_1256_post − lt_1256_post ≤ 0 ∧ − lt_1256_0 + lt_1256_0 ≤ 0 ∧ lt_1256_0 − lt_1256_0 ≤ 0 ∧ − lt_10_post + lt_10_post ≤ 0 ∧ lt_10_post − lt_10_post ≤ 0 ∧ − lt_10_1 + lt_10_1 ≤ 0 ∧ lt_10_1 − lt_10_1 ≤ 0 ∧ − lt_10_0 + lt_10_0 ≤ 0 ∧ lt_10_0 − lt_10_0 ≤ 0 ∧ − l_855_post + l_855_post ≤ 0 ∧ l_855_post − l_855_post ≤ 0 ∧ − l_855_0 + l_855_0 ≤ 0 ∧ l_855_0 − l_855_0 ≤ 0 ∧ − l_287_post + l_287_post ≤ 0 ∧ l_287_post − l_287_post ≤ 0 ∧ − l_287_0 + l_287_0 ≤ 0 ∧ l_287_0 − l_287_0 ≤ 0 ∧ − l_27_post + l_27_post ≤ 0 ∧ l_27_post − l_27_post ≤ 0 ∧ − l_27_0 + l_27_0 ≤ 0 ∧ l_27_0 − l_27_0 ≤ 0 ∧ − l_1519_post + l_1519_post ≤ 0 ∧ l_1519_post − l_1519_post ≤ 0 ∧ − l_1519_0 + l_1519_0 ≤ 0 ∧ l_1519_0 − l_1519_0 ≤ 0 ∧ − l_1429_post + l_1429_post ≤ 0 ∧ l_1429_post − l_1429_post ≤ 0 ∧ − l_1429_0 + l_1429_0 ≤ 0 ∧ l_1429_0 − l_1429_0 ≤ 0 ∧ − l_1304_post + l_1304_post ≤ 0 ∧ l_1304_post − l_1304_post ≤ 0 ∧ − l_1304_0 + l_1304_0 ≤ 0 ∧ l_1304_0 − l_1304_0 ≤ 0 ∧ − l_1119_post + l_1119_post ≤ 0 ∧ l_1119_post − l_1119_post ≤ 0 ∧ − l_1119_1 + l_1119_1 ≤ 0 ∧ l_1119_1 − l_1119_1 ≤ 0 ∧ − l_1119_0 + l_1119_0 ≤ 0 ∧ l_1119_0 − l_1119_0 ≤ 0 ∧ − j_39_post + j_39_post ≤ 0 ∧ j_39_post − j_39_post ≤ 0 ∧ − j_39_0 + j_39_0 ≤ 0 ∧ j_39_0 − j_39_0 ≤ 0 ∧ − j_36_post + j_36_post ≤ 0 ∧ j_36_post − j_36_post ≤ 0 ∧ − j_36_0 + j_36_0 ≤ 0 ∧ j_36_0 − j_36_0 ≤ 0 ∧ − i_31_post + i_31_post ≤ 0 ∧ i_31_post − i_31_post ≤ 0 ∧ − i_31_0 + i_31_0 ≤ 0 ∧ i_31_0 − i_31_0 ≤ 0 ∧ − h_46_post + h_46_post ≤ 0 ∧ h_46_post − h_46_post ≤ 0 ∧ − h_46_1 + h_46_1 ≤ 0 ∧ h_46_1 − h_46_1 ≤ 0 ∧ − h_46_0 + h_46_0 ≤ 0 ∧ h_46_0 − h_46_0 ≤ 0 ∧ − h_37_post + h_37_post ≤ 0 ∧ h_37_post − h_37_post ≤ 0 ∧ − h_37_0 + h_37_0 ≤ 0 ∧ h_37_0 − h_37_0 ≤ 0 ∧ − h_34_post + h_34_post ≤ 0 ∧ h_34_post − h_34_post ≤ 0 ∧ − h_34_2 + h_34_2 ≤ 0 ∧ h_34_2 − h_34_2 ≤ 0 ∧ − h_34_1 + h_34_1 ≤ 0 ∧ h_34_1 − h_34_1 ≤ 0 ∧ − h_34_0 + h_34_0 ≤ 0 ∧ h_34_0 − h_34_0 ≤ 0 ∧ − h_28_post + h_28_post ≤ 0 ∧ h_28_post − h_28_post ≤ 0 ∧ − h_28_0 + h_28_0 ≤ 0 ∧ h_28_0 − h_28_0 ≤ 0 ∧ − f_1323_post + f_1323_post ≤ 0 ∧ f_1323_post − f_1323_post ≤ 0 ∧ − f_1323_0 + f_1323_0 ≤ 0 ∧ f_1323_0 − f_1323_0 ≤ 0 ∧ − fF_1324_post + fF_1324_post ≤ 0 ∧ fF_1324_post − fF_1324_post ≤ 0 ∧ − fF_1324_0 + fF_1324_0 ≤ 0 ∧ fF_1324_0 − fF_1324_0 ≤ 0 ∧ − c_990_post + c_990_post ≤ 0 ∧ c_990_post − c_990_post ≤ 0 ∧ − c_990_0 + c_990_0 ≤ 0 ∧ c_990_0 − c_990_0 ≤ 0 ∧ − c_98_post + c_98_post ≤ 0 ∧ c_98_post − c_98_post ≤ 0 ∧ − c_98_1 + c_98_1 ≤ 0 ∧ c_98_1 − c_98_1 ≤ 0 ∧ − c_98_0 + c_98_0 ≤ 0 ∧ c_98_0 − c_98_0 ≤ 0 ∧ − c_958_post + c_958_post ≤ 0 ∧ c_958_post − c_958_post ≤ 0 ∧ − c_958_1 + c_958_1 ≤ 0 ∧ c_958_1 − c_958_1 ≤ 0 ∧ − c_958_0 + c_958_0 ≤ 0 ∧ c_958_0 − c_958_0 ≤ 0 ∧ − c_901_post + c_901_post ≤ 0 ∧ c_901_post − c_901_post ≤ 0 ∧ − c_901_0 + c_901_0 ≤ 0 ∧ c_901_0 − c_901_0 ≤ 0 ∧ − c_1481_post + c_1481_post ≤ 0 ∧ c_1481_post − c_1481_post ≤ 0 ∧ − c_1481_1 + c_1481_1 ≤ 0 ∧ c_1481_1 − c_1481_1 ≤ 0 ∧ − c_1481_0 + c_1481_0 ≤ 0 ∧ c_1481_0 − c_1481_0 ≤ 0 ∧ − c_1186_post + c_1186_post ≤ 0 ∧ c_1186_post − c_1186_post ≤ 0 ∧ − c_1186_0 + c_1186_0 ≤ 0 ∧ c_1186_0 − c_1186_0 ≤ 0 ∧ − Flink_0 + Flink_0 ≤ 0 ∧ Flink_0 − Flink_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