LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: −1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0h_14_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0
1: h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0
2: TRUE
3: h_23_post ≤ 0h_23_post ≤ 0i_21_post ≤ 0i_21_post ≤ 0i_21_0 ≤ 0i_21_0 ≤ 0h_23_0 ≤ 0h_23_0 ≤ 0
4: 1 − l_20_0 ≤ 0rv_24_0 ≤ 0
5: −1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0
6: 2 − l_20_0 ≤ 0rv_24_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0−2 + i_21_1 ≤ 02 − i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0
7: 2 − l_20_0 ≤ 0rv_24_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0−2 + i_21_1 ≤ 02 − i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0−1 − i_91_0 ≤ 0
8: 2 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0
9: 2 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
10: 2 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0
11: 2 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0a_145_post ≤ 01 − i_181_0 ≤ 0
12: 2 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0a_145_post ≤ 0f_211_0 ≤ 0
13: −1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 01 − i_16_1 ≤ 0
14: −1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 01 − i_16_1 ≤ 01 − i_259_0 ≤ 0
16: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
6 29 6: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0
9 36 9: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0
10 43 10: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0
13 50 13: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 2, 3, 6, 7, 8, 9, 13, 17, 18, 21, 22, 26, 27, 28 using the following ranking functions, which are bounded by −33.

16: 0
2: 0
3: 0
4: 0
5: 0
13: 0
14: 0
0: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
1: 0
16: −12
2: −13
3: −14
4: −15
5: −16
13: −17
14: −17
13_var_snapshot: −17
13*: −17
0: −20
6: −21
7: −21
6_var_snapshot: −21
6*: −21
8: −24
9: −25
10: −25
11: −25
12: −25
9_var_snapshot: −25
9*: −25
10_var_snapshot: −25
10*: −25
1: −31

4 Location Addition

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

6* 32 6: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

5 Location Addition

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

6 30 6_var_snapshot: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

6 Location Addition

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

9* 39 9: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

7 Location Addition

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

9 37 9_var_snapshot: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

8 Location Addition

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

10* 46 10: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

9 Location Addition

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

10 44 10_var_snapshot: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

10 Location Addition

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

13* 53 13: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

11 Location Addition

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

13 51 13_var_snapshot: tp_26_post + tp_26_post ≤ 0tp_26_posttp_26_post ≤ 0tp_26_0 + tp_26_0 ≤ 0tp_26_0tp_26_0 ≤ 0t_25_post + t_25_post ≤ 0t_25_postt_25_post ≤ 0t_25_0 + t_25_0 ≤ 0t_25_0t_25_0 ≤ 0st_22_post + st_22_post ≤ 0st_22_postst_22_post ≤ 0st_22_1 + st_22_1 ≤ 0st_22_1st_22_1 ≤ 0st_22_0 + st_22_0 ≤ 0st_22_0st_22_0 ≤ 0st_15_0 + st_15_0 ≤ 0st_15_0st_15_0 ≤ 0rv_24_post + rv_24_post ≤ 0rv_24_postrv_24_post ≤ 0rv_24_0 + rv_24_0 ≤ 0rv_24_0rv_24_0 ≤ 0rv_17_post + rv_17_post ≤ 0rv_17_postrv_17_post ≤ 0rv_17_0 + rv_17_0 ≤ 0rv_17_0rv_17_0 ≤ 0rv_13_post + rv_13_post ≤ 0rv_13_postrv_13_post ≤ 0rv_13_0 + rv_13_0 ≤ 0rv_13_0rv_13_0 ≤ 0rt_11_post + rt_11_post ≤ 0rt_11_postrt_11_post ≤ 0rt_11_2 + rt_11_2 ≤ 0rt_11_2rt_11_2 ≤ 0rt_11_1 + rt_11_1 ≤ 0rt_11_1rt_11_1 ≤ 0rt_11_0 + rt_11_0 ≤ 0rt_11_0rt_11_0 ≤ 0r_45_post + r_45_post ≤ 0r_45_postr_45_post ≤ 0r_45_0 + r_45_0 ≤ 0r_45_0r_45_0 ≤ 0r_38_post + r_38_post ≤ 0r_38_postr_38_post ≤ 0r_38_0 + r_38_0 ≤ 0r_38_0r_38_0 ≤ 0r_261_post + r_261_post ≤ 0r_261_postr_261_post ≤ 0r_261_0 + r_261_0 ≤ 0r_261_0r_261_0 ≤ 0r_255_post + r_255_post ≤ 0r_255_postr_255_post ≤ 0r_255_0 + r_255_0 ≤ 0r_255_0r_255_0 ≤ 0r_249_post + r_249_post ≤ 0r_249_postr_249_post ≤ 0r_249_0 + r_249_0 ≤ 0r_249_0r_249_0 ≤ 0nd_12_post + nd_12_post ≤ 0nd_12_postnd_12_post ≤ 0nd_12_1 + nd_12_1 ≤ 0nd_12_1nd_12_1 ≤ 0nd_12_0 + nd_12_0 ≤ 0nd_12_0nd_12_0 ≤ 0l_20_post + l_20_post ≤ 0l_20_postl_20_post ≤ 0l_20_0 + l_20_0 ≤ 0l_20_0l_20_0 ≤ 0i_98_post + i_98_post ≤ 0i_98_posti_98_post ≤ 0i_98_0 + i_98_0 ≤ 0i_98_0i_98_0 ≤ 0i_91_0 + i_91_0 ≤ 0i_91_0i_91_0 ≤ 0i_259_0 + i_259_0 ≤ 0i_259_0i_259_0 ≤ 0i_232_0 + i_232_0 ≤ 0i_232_0i_232_0 ≤ 0i_21_post + i_21_post ≤ 0i_21_posti_21_post ≤ 0i_21_1 + i_21_1 ≤ 0i_21_1i_21_1 ≤ 0i_21_0 + i_21_0 ≤ 0i_21_0i_21_0 ≤ 0i_181_0 + i_181_0 ≤ 0i_181_0i_181_0 ≤ 0i_16_post + i_16_post ≤ 0i_16_posti_16_post ≤ 0i_16_1 + i_16_1 ≤ 0i_16_1i_16_1 ≤ 0i_16_0 + i_16_0 ≤ 0i_16_0i_16_0 ≤ 0i_156_post + i_156_post ≤ 0i_156_posti_156_post ≤ 0i_156_0 + i_156_0 ≤ 0i_156_0i_156_0 ≤ 0i_134_post + i_134_post ≤ 0i_134_posti_134_post ≤ 0i_134_0 + i_134_0 ≤ 0i_134_0i_134_0 ≤ 0i_128_post + i_128_post ≤ 0i_128_posti_128_post ≤ 0i_128_0 + i_128_0 ≤ 0i_128_0i_128_0 ≤ 0i_123_0 + i_123_0 ≤ 0i_123_0i_123_0 ≤ 0i_110_post + i_110_post ≤ 0i_110_posti_110_post ≤ 0i_110_0 + i_110_0 ≤ 0i_110_0i_110_0 ≤ 0h_23_post + h_23_post ≤ 0h_23_posth_23_post ≤ 0h_23_0 + h_23_0 ≤ 0h_23_0h_23_0 ≤ 0h_14_post + h_14_post ≤ 0h_14_posth_14_post ≤ 0h_14_0 + h_14_0 ≤ 0h_14_0h_14_0 ≤ 0f_233_0 + f_233_0 ≤ 0f_233_0f_233_0 ≤ 0f_211_0 + f_211_0 ≤ 0f_211_0f_211_0 ≤ 0f_195_0 + f_195_0 ≤ 0f_195_0f_195_0 ≤ 0a_69_post + a_69_post ≤ 0a_69_posta_69_post ≤ 0a_69_1 + a_69_1 ≤ 0a_69_1a_69_1 ≤ 0a_69_0 + a_69_0 ≤ 0a_69_0a_69_0 ≤ 0a_254_post + a_254_post ≤ 0a_254_posta_254_post ≤ 0a_254_1 + a_254_1 ≤ 0a_254_1a_254_1 ≤ 0a_254_0 + a_254_0 ≤ 0a_254_0a_254_0 ≤ 0a_220_post + a_220_post ≤ 0a_220_posta_220_post ≤ 0a_220_0 + a_220_0 ≤ 0a_220_0a_220_0 ≤ 0a_204_post + a_204_post ≤ 0a_204_posta_204_post ≤ 0a_204_0 + a_204_0 ≤ 0a_204_0a_204_0 ≤ 0a_189_post + a_189_post ≤ 0a_189_posta_189_post ≤ 0a_189_0 + a_189_0 ≤ 0a_189_0a_189_0 ≤ 0a_165_post + a_165_post ≤ 0a_165_posta_165_post ≤ 0a_165_0 + a_165_0 ≤ 0a_165_0a_165_0 ≤ 0a_164_post + a_164_post ≤ 0a_164_posta_164_post ≤ 0a_164_1 + a_164_1 ≤ 0a_164_1a_164_1 ≤ 0a_164_0 + a_164_0 ≤ 0a_164_0a_164_0 ≤ 0a_145_post + a_145_post ≤ 0a_145_posta_145_post ≤ 0a_145_0 + a_145_0 ≤ 0a_145_0a_145_0 ≤ 0a_144_post + a_144_post ≤ 0a_144_posta_144_post ≤ 0a_144_0 + a_144_0 ≤ 0a_144_0a_144_0 ≤ 0a_109_post + a_109_post ≤ 0a_109_posta_109_post ≤ 0a_109_1 + a_109_1 ≤ 0a_109_1a_109_1 ≤ 0a_109_0 + a_109_0 ≤ 0a_109_0a_109_0 ≤ 0___const_101_0 + ___const_101_0 ≤ 0___const_101_0___const_101_0 ≤ 0___const_100_0 + ___const_100_0 ≤ 0___const_100_0___const_100_0 ≤ 0

12 SCC Decomposition

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

12.1 SCC Subproblem 1/3

Here we consider the SCC { 13, 14, 13_var_snapshot, 13* }.

12.1.1 Transition Removal

We remove transition 19 using the following ranking functions, which are bounded by −5.

13: 1 − 4⋅i_16_0 + 4⋅i_259_0
14: 1 − 4⋅i_16_0 + 4⋅i_259_0 + 2⋅rv_13_0
13_var_snapshot: −4⋅i_16_0 + 4⋅i_259_0
13*: −4⋅i_16_0 + 4⋅i_259_0 + 2⋅rv_13_0

12.1.2 Transition Removal

We remove transitions 51, 53, 20 using the following ranking functions, which are bounded by −3.

13: −2
14: 0
13_var_snapshot: −3⋅i_16_1
13*: −1

12.1.3 Splitting Cut-Point Transitions

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

12.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 50.

12.1.3.1.1 Splitting Cut-Point Transitions

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

12.2 SCC Subproblem 2/3

Here we consider the SCC { 9, 10, 11, 12, 9_var_snapshot, 9*, 10_var_snapshot, 10* }.

12.2.1 Splitting Cut-Point Transitions

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

12.2.1.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 36.

12.2.1.1.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0−1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0h_14_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0
1: h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0
2: TRUE
3: h_23_post ≤ 0h_23_post ≤ 0i_21_post ≤ 0i_21_post ≤ 0i_21_0 ≤ 0i_21_0 ≤ 0h_23_0 ≤ 0h_23_0 ≤ 0
4: 1 ≤ 01 − l_20_0 ≤ 0rv_24_0 ≤ 0
5: 1 ≤ 0−1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0
6: 1 ≤ 02 − l_20_0 ≤ 0rv_24_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0−2 + i_21_1 ≤ 02 − i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0
7: 1 ≤ 02 − l_20_0 ≤ 0rv_24_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0−2 + i_21_1 ≤ 02 − i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0−1 − i_91_0 ≤ 0
8: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0
9: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
10: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0
11: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0a_145_post ≤ 01 − i_181_0 ≤ 0
12: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0a_145_post ≤ 0f_211_0 ≤ 0
13: 1 ≤ 0−1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 01 − i_16_1 ≤ 0
14: 1 ≤ 0−1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 01 − i_16_1 ≤ 01 − i_259_0 ≤ 0
16: TRUE
9: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
10: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0
11: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0a_145_post ≤ 01 − i_181_0 ≤ 0
12: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0a_145_post ≤ 0f_211_0 ≤ 0
9_var_snapshot: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
9*: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
10_var_snapshot: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0
10*: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

12.2.1.1.2 Transition Removal

We remove transition 37 using the following ranking functions, which are bounded by −10.

9: −1
10: −2
11: −3
12: −4
9_var_snapshot: −5
9*: −6
10_var_snapshot: −7
10*: −8

12.2.1.1.3 Splitting Cut-Point Transitions

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

12.2.1.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 43.

12.2.1.2.1 Invariant Updates

The following invariants are asserted.

0: 1 ≤ 0−1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0h_14_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0
1: h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0
2: TRUE
3: h_23_post ≤ 0h_23_post ≤ 0i_21_post ≤ 0i_21_post ≤ 0i_21_0 ≤ 0i_21_0 ≤ 0h_23_0 ≤ 0h_23_0 ≤ 0
4: 1 ≤ 01 − l_20_0 ≤ 0rv_24_0 ≤ 0
5: 1 ≤ 0−1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0
6: 1 ≤ 02 − l_20_0 ≤ 0rv_24_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0−2 + i_21_1 ≤ 02 − i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0
7: 1 ≤ 02 − l_20_0 ≤ 0rv_24_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0−2 + i_21_1 ≤ 02 − i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0−1 − i_91_0 ≤ 0
8: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0
9: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
10: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0
11: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0a_145_post ≤ 01 − i_181_0 ≤ 0
12: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0a_145_post ≤ 0f_211_0 ≤ 0
13: 1 ≤ 0−1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 01 − i_16_1 ≤ 0
14: 1 ≤ 0−1 + rv_13_0 ≤ 01 − rv_13_0 ≤ 0h_14_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 01 − i_16_1 ≤ 01 − i_259_0 ≤ 0
16: TRUE
9: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
10: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0
11: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0a_145_post ≤ 01 − i_181_0 ≤ 0
12: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0a_145_post ≤ 0f_211_0 ≤ 0
9_var_snapshot: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
9*: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 01 − i_16_1 ≤ 0a_145_0 ≤ 0
10_var_snapshot: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0
10*: 1 ≤ 02 − rv_13_0 ≤ 0−2 + a_69_post ≤ 02 − a_69_post ≤ 0i_21_1 ≤ 0−2 + a_69_0 ≤ 02 − a_69_0 ≤ 0h_14_post ≤ 0i_98_post ≤ 0rt_11_1 ≤ 0st_22_1 ≤ 01 − i_16_0 ≤ 0h_14_0 ≤ 0i_98_0 ≤ 0rv_17_post ≤ 0rv_17_post ≤ 0rv_17_0 ≤ 0rv_17_0 ≤ 0a_145_0 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

12.2.1.2.2 Transition Removal

We remove transition 44 using the following ranking functions, which are bounded by −10.

9: −1
10: −2
11: −3
12: −4
9_var_snapshot: −5
9*: −6
10_var_snapshot: −7
10*: −8

12.2.1.2.3 Splitting Cut-Point Transitions

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

12.3 SCC Subproblem 3/3

Here we consider the SCC { 6, 7, 6_var_snapshot, 6* }.

12.3.1 Transition Removal

We remove transition 4 using the following ranking functions, which are bounded by −12.

6: a_69_0 − 7⋅i_21_0 + 7⋅i_91_0
7: a_69_post − 7⋅i_21_0 + 7⋅i_91_0
6_var_snapshot: −7⋅i_21_0 − 2⋅i_21_1 + 7⋅i_91_0
6*: a_69_0 + a_69_post − 7⋅i_21_0 + 7⋅i_91_0

12.3.2 Transition Removal

We remove transitions 30, 32, 5 using the following ranking functions, which are bounded by −3.

6: i_21_1
7: 1
6_var_snapshot: −2⋅a_69_post
6*: 0

12.3.3 Splitting Cut-Point Transitions

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

12.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 29.

12.3.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert