LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
3 51 3: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
5 58 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
7 65 7: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
13 72 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
16 79 16: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
20 86 20: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
22 93 22: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
24 100 24: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
25 107 25: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 24, 39, 42, 50 using the following ranking functions, which are bounded by −31.

32: 0
29: 0
0: 0
1: 0
2: 0
3: 0
18: 0
22: 0
30: 0
31: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
17: 0
19: 0
20: 0
21: 0
23: 0
24: 0
25: 0
26: 0
27: 0
28: 0
32: −6
29: −7
0: −8
1: −8
2: −8
3: −8
30: −8
31: −8
18: −8
22: −8
3_var_snapshot: −8
3*: −8
22_var_snapshot: −8
22*: −8
4: −11
5: −11
6: −11
7: −11
8: −11
9: −11
10: −11
11: −11
12: −11
13: −11
14: −11
15: −11
16: −11
17: −11
19: −11
20: −11
21: −11
23: −11
24: −11
25: −11
26: −11
27: −11
5_var_snapshot: −11
5*: −11
7_var_snapshot: −11
7*: −11
13_var_snapshot: −11
13*: −11
16_var_snapshot: −11
16*: −11
20_var_snapshot: −11
20*: −11
24_var_snapshot: −11
24*: −11
25_var_snapshot: −11
25*: −11
28: −24

3 Location Addition

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

3* 54 3: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

4 Location Addition

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

3 52 3_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

5 Location Addition

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

5* 61 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

6 Location Addition

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

5 59 5_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

7 Location Addition

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

7* 68 7: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

8 Location Addition

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

7 66 7_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

9 Location Addition

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

13* 75 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

10 Location Addition

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

13 73 13_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

11 Location Addition

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

16* 82 16: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

12 Location Addition

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

16 80 16_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

13 Location Addition

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

20* 89 20: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

14 Location Addition

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

20 87 20_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

15 Location Addition

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

22* 96 22: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

16 Location Addition

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

22 94 22_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

17 Location Addition

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

24* 103 24: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

18 Location Addition

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

24 101 24_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

19 Location Addition

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

25* 110 25: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

20 Location Addition

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

25 108 25_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − temp_post + temp_post ≤ 0 ∧ temp_post − temp_post ≤ 0 ∧ − temp_0 + temp_0 ≤ 0 ∧ temp_0 − temp_0 ≤ 0 ∧ − sum_post + sum_post ≤ 0 ∧ sum_post − sum_post ≤ 0 ∧ − sum_0 + sum_0 ≤ 0 ∧ sum_0 − sum_0 ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − k_post + k_post ≤ 0 ∧ k_post − k_post ≤ 0 ∧ − k_0 + k_0 ≤ 0 ∧ k_0 − k_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − imax_post + imax_post ≤ 0 ∧ imax_post − imax_post ≤ 0 ∧ − imax_0 + imax_0 ≤ 0 ∧ imax_0 − imax_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − dum_post + dum_post ≤ 0 ∧ dum_post − dum_post ≤ 0 ∧ − dum_0 + dum_0 ≤ 0 ∧ dum_0 − dum_0 ≤ 0 ∧ − big_post + big_post ≤ 0 ∧ big_post − big_post ≤ 0 ∧ − big_0 + big_0 ≤ 0 ∧ big_0 − big_0 ≤ 0

21 SCC Decomposition

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

21.1 SCC Subproblem 1/2

Here we consider the SCC { 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 19, 20, 21, 23, 24, 25, 26, 27, 5_var_snapshot, 5*, 7_var_snapshot, 7*, 13_var_snapshot, 13*, 16_var_snapshot, 16*, 20_var_snapshot, 20*, 24_var_snapshot, 24*, 25_var_snapshot, 25* }.

21.1.1 Transition Removal

We remove transition 30 using the following ranking functions, which are bounded by −1.

4: −5⋅i_0 + 5⋅n_0
5: −5⋅i_0 + 5⋅n_0
6: −5⋅i_0 + 5⋅n_0
7: −5⋅i_0 + 5⋅n_0
8: −5⋅i_0 + 5⋅n_0
9: −5⋅i_0 + 5⋅n_0
10: −5⋅i_0 + 5⋅n_0
11: −5⋅i_0 + 5⋅n_0
12: −5⋅i_0 + 5⋅n_0
13: −5⋅i_0 + 5⋅n_0
14: −5⋅i_0 + 5⋅n_0
15: −3 − 5⋅i_0 + 5⋅n_0
16: −5⋅i_0 + 5⋅n_0
17: −2 − 5⋅i_0 + 5⋅n_0
19: −1 − 5⋅i_0 + 5⋅n_0
20: −1 − 5⋅i_0 + 5⋅n_0
21: −5⋅i_0 + 5⋅n_0
23: −5 − 5⋅i_0 + 5⋅n_0
24: −5⋅i_0 + 5⋅n_0
25: −5 − 5⋅i_0 + 5⋅n_0
26: −5⋅i_0 + 5⋅n_0
27: −5⋅i_0 + 5⋅n_0
5_var_snapshot: −5⋅i_0 + 5⋅n_0
5*: −5⋅i_0 + 5⋅n_0
7_var_snapshot: −5⋅i_0 + 5⋅n_0
7*: −5⋅i_0 + 5⋅n_0
13_var_snapshot: −5⋅i_0 + 5⋅n_0
13*: −5⋅i_0 + 5⋅n_0
16_var_snapshot: −5⋅i_0 + 5⋅n_0
16*: −5⋅i_0 + 5⋅n_0
20_var_snapshot: −1 − 5⋅i_0 + 5⋅n_0
20*: −1 − 5⋅i_0 + 5⋅n_0
24_var_snapshot: −5⋅i_0 + 5⋅n_0
24*: −5⋅i_0 + 5⋅n_0
25_var_snapshot: −5 − 5⋅i_0 + 5⋅n_0
25*: −5 − 5⋅i_0 + 5⋅n_0

21.1.2 Transition Removal

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

4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 1
16: 0
17: 1
19: 1
20: 1
21: 0
23: 0
24: 0
25: 0
26: 0
27: 0
5_var_snapshot: 0
5*: 0
7_var_snapshot: 0
7*: 0
13_var_snapshot: 0
13*: 0
16_var_snapshot: 0
16*: 0
20_var_snapshot: 1
20*: 1
24_var_snapshot: 0
24*: 0
25_var_snapshot: 0
25*: 0

21.1.3 Transition Removal

We remove transition 27 using the following ranking functions, which are bounded by 1.

4: −22 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
5: −7⋅i_0 − 24⋅j_0 − 4⋅k_0
6: −21 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
7: −19 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
8: −17 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
9: −16 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
10: −15 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
11: −14 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
12: −13 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
13: −11 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
14: −9 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
15: −4 + 4⋅j_0 − 4⋅k_0
16: −6 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
17: −3 + 4⋅j_0 − 4⋅k_0
19: −2 + 4⋅j_0 − 4⋅k_0
20: 4⋅j_0 − 4⋅k_0
21: −8 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
23: −7 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
24: −2 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
25: −5 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
26: −4 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
27: −1 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
5_var_snapshot: −7⋅i_0 − 24⋅j_0 − 4⋅k_0
5*: 1 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
7_var_snapshot: −20 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
7*: −18 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
13_var_snapshot: −12 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
13*: −10 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
16_var_snapshot: −7 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
16*: −5 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
20_var_snapshot: −1 + 4⋅j_0 − 4⋅k_0
20*: 1 + 4⋅j_0 − 4⋅k_0
24_var_snapshot: −3 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
24*: −1 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
25_var_snapshot: −6 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0
25*: −4 − 7⋅i_0 − 24⋅j_0 − 4⋅k_0

21.1.4 Transition Removal

We remove transitions 87, 22, 23, 26, 28 using the following ranking functions, which are bounded by −4.

4: −20 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
5: 1 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
6: −20 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
7: −18 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
8: −17 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
9: −16 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
10: −15 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
11: −14 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
12: −13 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
13: −11 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
14: −9 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
15: −4
16: −6 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
17: −3
19: −2
20: 0
21: −8 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
23: −7 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
24: −2 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
25: −5 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
26: −4 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
27: −1 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
5_var_snapshot: −9⋅i_0 − 23⋅j_0 − 4⋅k_0
5*: 2 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
7_var_snapshot: −19 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
7*: −18 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
13_var_snapshot: −12 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
13*: −10 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
16_var_snapshot: −7 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
16*: −5 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
20_var_snapshot: −1
20*: 1
24_var_snapshot: −3 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
24*: −1 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
25_var_snapshot: −6 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0
25*: −4 − 9⋅i_0 − 23⋅j_0 − 4⋅k_0

21.1.5 Transition Removal

We remove transition 89 using the following ranking functions, which are bounded by −1.

4: −20 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
5: 1 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
6: −19 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
7: −17 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
8: −16 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
9: −15 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
10: −14 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
11: −13 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
12: −12 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
13: −12 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
14: −10 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
15: 0
16: −7 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
17: 0
19: 0
20: −1
21: −9 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
23: −8 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
24: −3 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
25: −7 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
26: −5 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
27: −1 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
5_var_snapshot: −7⋅i_0 − 23⋅j_0 − 3⋅k_0
5*: 2 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
7_var_snapshot: −18 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
7*: −16 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
13_var_snapshot: −12 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
13*: −11 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
16_var_snapshot: −8 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
16*: −6 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
20_var_snapshot: 0
20*: 0
24_var_snapshot: −4 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
24*: −2 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
25_var_snapshot: −7 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0
25*: −6 − 7⋅i_0 − 23⋅j_0 − 3⋅k_0

21.1.6 Transition Removal

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

4: − i_0 + n_0
5: − i_0 + n_0
6: − i_0 + n_0
7: − i_0 + n_0
8: − i_0 + n_0
9: − i_0 + n_0
10: − i_0 + n_0
11: − i_0 + n_0
12: − i_0 + n_0
13: − i_0 + n_0
14: − i_0 + n_0
15: 0
16: − i_0 + n_0
17: 0
19: 0
20: 0
21: − i_0 + n_0
23: −1 − i_0 + n_0
24: − i_0 + n_0
25: −1 − i_0 + n_0
26: − i_0 + n_0
27: − i_0 + n_0
5_var_snapshot: − i_0 + n_0
5*: − i_0 + n_0
7_var_snapshot: − i_0 + n_0
7*: − i_0 + n_0
13_var_snapshot: − i_0 + n_0
13*: − i_0 + n_0
16_var_snapshot: − i_0 + n_0
16*: − i_0 + n_0
20_var_snapshot: 0
20*: 0
24_var_snapshot: − i_0 + n_0
24*: − i_0 + n_0
25_var_snapshot: −1 − i_0 + n_0
25*: −1 − i_0 + n_0

21.1.7 Transition Removal

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

4: −13 − 16⋅j_0 + 16⋅n_0
5: 1 − 16⋅j_0 + 16⋅n_0
6: −12 − 16⋅j_0 + 16⋅n_0
7: −10 − 16⋅j_0 + 16⋅n_0
8: −9 − 16⋅j_0 + 16⋅n_0
9: −9 − 16⋅j_0 + 16⋅n_0
10: −8 − 16⋅j_0 + 16⋅n_0
11: −7 − 16⋅j_0 + 16⋅n_0
12: −7 − 16⋅j_0 + 16⋅n_0
13: −7 − 16⋅j_0 + 16⋅n_0
14: −6 − 16⋅j_0 + 16⋅n_0
15: 0
16: −3 − 16⋅j_0 + 16⋅n_0
17: 0
19: 0
20: 0
21: −5 − 16⋅j_0 + 16⋅n_0
23: −1 − 16⋅j_0 + 16⋅n_0
24: −1 − 16⋅j_0 + 16⋅n_0
25: −1 − 16⋅j_0 + 16⋅n_0
26: −1 − 16⋅j_0 + 16⋅n_0
27: −1 − 16⋅j_0 + 16⋅n_0
5_var_snapshot: −16⋅j_0 + 16⋅n_0
5*: 2 − 16⋅j_0 + 16⋅n_0
7_var_snapshot: −11 − 16⋅j_0 + 16⋅n_0
7*: −9 − 16⋅j_0 + 16⋅n_0
13_var_snapshot: −7 − 16⋅j_0 + 16⋅n_0
13*: −7 − 16⋅j_0 + 16⋅n_0
16_var_snapshot: −4 − 16⋅j_0 + 16⋅n_0
16*: −2 − 16⋅j_0 + 16⋅n_0
20_var_snapshot: 0
20*: 0
24_var_snapshot: −1 − 16⋅j_0 + 16⋅n_0
24*: −1 − 16⋅j_0 + 16⋅n_0
25_var_snapshot: −1 − 16⋅j_0 + 16⋅n_0
25*: −1 − 16⋅j_0 + 16⋅n_0

21.1.8 Transition Removal

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

4: −17 + 20⋅imax_0 − 20⋅j_0
5: 1 + 20⋅imax_0 − 20⋅j_0
6: −16 + 20⋅imax_0 − 20⋅j_0
7: −14 + 20⋅imax_0 − 20⋅j_0
8: −12 + 20⋅imax_0 − 20⋅j_0
9: −11 + 20⋅imax_0 − 20⋅j_0
10: −10 + 20⋅imax_0 − 20⋅j_0
11: −9 + 20⋅imax_0 − 20⋅j_0
12: −8 + 20⋅imax_0 − 20⋅j_0
13: −8 + 20⋅imax_0 − 20⋅j_0
14: −7 + 20⋅imax_0 − 20⋅j_0
15: 0
16: −4 + 20⋅imax_0 − 20⋅j_0
17: 0
19: 0
20: 0
21: −6 + 20⋅imax_0 − 20⋅j_0
23: −2 + 20⋅imax_0 − 20⋅j_0
24: −2 + 20⋅imax_0 − 20⋅j_0
25: −2 + 20⋅imax_0 − 20⋅j_0
26: −2 + 20⋅imax_0 − 20⋅j_0
27: −1 + 20⋅imax_0 − 20⋅j_0
5_var_snapshot: 20⋅imax_0 − 20⋅j_0
5*: 2 + 20⋅imax_0 − 20⋅j_0
7_var_snapshot: −15 + 20⋅imax_0 − 20⋅j_0
7*: −13 + 20⋅imax_0 − 20⋅j_0
13_var_snapshot: −8 + 20⋅imax_0 − 20⋅j_0
13*: −8 + 20⋅imax_0 − 20⋅j_0
16_var_snapshot: −5 + 20⋅imax_0 − 20⋅j_0
16*: −3 + 20⋅imax_0 − 20⋅j_0
20_var_snapshot: 0
20*: 0
24_var_snapshot: −2 + 20⋅imax_0 − 20⋅j_0
24*: −2 + 20⋅imax_0 − 20⋅j_0
25_var_snapshot: −2 + 20⋅imax_0 − 20⋅j_0
25*: −2 + 20⋅imax_0 − 20⋅j_0

21.1.9 Transition Removal

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

4: −16 − 18⋅j_0 + 18⋅n_0
5: 1 − 18⋅j_0 + 18⋅n_0
6: −15 − 18⋅j_0 + 18⋅n_0
7: −13 − 18⋅j_0 + 18⋅n_0
8: −11 − 18⋅j_0 + 18⋅n_0
9: −10 − 18⋅j_0 + 18⋅n_0
10: −9 − 18⋅j_0 + 18⋅n_0
11: −8 − 18⋅j_0 + 18⋅n_0
12: −7 − 18⋅j_0 + 18⋅n_0
13: −7 − 18⋅j_0 + 18⋅n_0
14: −6 − 18⋅j_0 + 18⋅n_0
15: 0
16: −3 − 18⋅j_0 + 18⋅n_0
17: 0
19: 0
20: 0
21: −5 − 18⋅j_0 + 18⋅n_0
23: −1 − 18⋅j_0 + 18⋅n_0
24: −1 − 18⋅j_0 + 18⋅n_0
25: −1 − 18⋅j_0 + 18⋅n_0
26: −1 − 18⋅j_0 + 18⋅n_0
27: −1 − 18⋅j_0 + 18⋅n_0
5_var_snapshot: −18⋅j_0 + 18⋅n_0
5*: 2 − 18⋅j_0 + 18⋅n_0
7_var_snapshot: −14 − 18⋅j_0 + 18⋅n_0
7*: −12 − 18⋅j_0 + 18⋅n_0
13_var_snapshot: −7 − 18⋅j_0 + 18⋅n_0
13*: −7 − 18⋅j_0 + 18⋅n_0
16_var_snapshot: −4 − 18⋅j_0 + 18⋅n_0
16*: −2 − 18⋅j_0 + 18⋅n_0
20_var_snapshot: 0
20*: 0
24_var_snapshot: −1 − 18⋅j_0 + 18⋅n_0
24*: −1 − 18⋅j_0 + 18⋅n_0
25_var_snapshot: −1 − 18⋅j_0 + 18⋅n_0
25*: −1 − 18⋅j_0 + 18⋅n_0

21.1.10 Transition Removal

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

4: −10 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
5: 2 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
6: −8 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
7: −6 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
8: −4 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
9: −20 − 4⋅i_0 + 4⋅j_0
10: −18 − 4⋅i_0 + 4⋅j_0
11: −16 − 4⋅i_0 + 4⋅j_0
12: −16 − 4⋅i_0 + 4⋅j_0
13: −16 − 4⋅i_0 + 4⋅j_0
14: −14 − 4⋅i_0 + 4⋅j_0
15: 0
16: −8 − 4⋅i_0 + 4⋅j_0
17: 0
19: 0
20: 0
21: −12 − 4⋅i_0 + 4⋅j_0
23: −7 − 4⋅i_0 + 4⋅j_0
24: −4 − 4⋅i_0 + 4⋅j_0
25: −7 − 4⋅i_0 + 4⋅j_0
26: −6 − 4⋅i_0 + 4⋅j_0
27: −2 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
5_var_snapshot: −4⋅i_0 − 14⋅j_0 + 18⋅n_0
5*: 4 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
7_var_snapshot: −6 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
7*: −5 − 4⋅i_0 − 14⋅j_0 + 18⋅n_0
13_var_snapshot: −16 − 4⋅i_0 + 4⋅j_0
13*: −16 − 4⋅i_0 + 4⋅j_0
16_var_snapshot: −10 − 4⋅i_0 + 4⋅j_0
16*: −6 − 4⋅i_0 + 4⋅j_0
20_var_snapshot: 0
20*: 0
24_var_snapshot: −5 − 4⋅i_0 + 4⋅j_0
24*: −4 − 4⋅i_0 + 4⋅j_0
25_var_snapshot: −7 − 4⋅i_0 + 4⋅j_0
25*: −7 − 4⋅i_0 + 4⋅j_0

21.1.11 Transition Removal

We remove transitions 59, 61, 66, 68, 3, 4, 6, 7, 9, 40, 41 using the following ranking functions, which are bounded by −2.

4: 3
5: 1
6: 6
7: 8
8: 10
9: −12 + 23⋅j_0 − 23⋅n_0
10: −11 + 23⋅j_0 − 23⋅n_0
11: −11 + 23⋅j_0 − 23⋅n_0
12: −10 + 23⋅j_0 − 23⋅n_0
13: −10 + 23⋅j_0 − 23⋅n_0
14: −9 + 23⋅j_0 − 23⋅n_0
15: 0
16: −6 + 23⋅j_0 − 23⋅n_0
17: 0
19: 0
20: 0
21: −8 + 23⋅j_0 − 23⋅n_0
23: 23⋅j_0 − 23⋅n_0
24: −3 + 23⋅j_0 − 23⋅n_0
25: 23⋅j_0 − 23⋅n_0
26: −5 + 23⋅j_0 − 23⋅n_0
27: −1
5_var_snapshot: 0
5*: 2
7_var_snapshot: 7
7*: 9
13_var_snapshot: −10 + 23⋅j_0 − 23⋅n_0
13*: −10 + 23⋅j_0 − 23⋅n_0
16_var_snapshot: −7 + 23⋅j_0 − 23⋅n_0
16*: −5 + 23⋅j_0 − 23⋅n_0
20_var_snapshot: 0
20*: 0
24_var_snapshot: −4 + 23⋅j_0 − 23⋅n_0
24*: −2 + 23⋅j_0 − 23⋅n_0
25_var_snapshot: 23⋅j_0 − 23⋅n_0
25*: 23⋅j_0 − 23⋅n_0

21.1.12 Transition Removal

We remove transitions 16, 34 using the following ranking functions, which are bounded by −6.

4: 0
5: 0
6: 0
7: 1
8: 0
9: −8 − 4⋅k_0 + 4⋅n_0
10: −7 − 4⋅k_0 + 4⋅n_0
11: −6 − 4⋅k_0 + 4⋅n_0
12: −5 − 4⋅k_0 + 4⋅n_0
13: −4 − 4⋅k_0 + 4⋅n_0
14: −2 − 4⋅k_0 + 4⋅n_0
15: 0
16: −3 + 4⋅i_0 − 4⋅k_0
17: 0
19: 0
20: 0
21: −5 + 4⋅i_0 − 4⋅k_0
23: 7 + 4⋅i_0 − 4⋅k_0
24: 1 + 4⋅i_0 − 4⋅k_0
25: 9 + 4⋅i_0 − 4⋅k_0
26: −1 + 4⋅i_0 − 4⋅k_0
27: 0
5_var_snapshot: 0
5*: 0
7_var_snapshot: 0
7*: 0
13_var_snapshot: −5 − 4⋅k_0 + 4⋅n_0
13*: −3 − 4⋅k_0 + 4⋅n_0
16_var_snapshot: −4 + 4⋅i_0 − 4⋅k_0
16*: −2 + 4⋅i_0 − 4⋅k_0
20_var_snapshot: 0
20*: 0
24_var_snapshot: 4⋅i_0 − 4⋅k_0
24*: 2 + 4⋅i_0 − 4⋅k_0
25_var_snapshot: 8 + 4⋅i_0 − 4⋅k_0
25*: 10 + 4⋅i_0 − 4⋅k_0

21.1.13 Transition Removal

We remove transitions 73, 75, 80, 82, 101, 103, 108, 110, 11, 12, 13, 14, 15, 17, 18, 19, 29, 32, 33, 35, 36, 38 using the following ranking functions, which are bounded by −13.

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

21.1.14 Splitting Cut-Point Transitions

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

21.1.14.1 Cut-Point Subproblem 1/7

Here we consider cut-point transition 58.

21.1.14.1.1 Splitting Cut-Point Transitions

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

21.1.14.2 Cut-Point Subproblem 2/7

Here we consider cut-point transition 65.

21.1.14.2.1 Splitting Cut-Point Transitions

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

21.1.14.3 Cut-Point Subproblem 3/7

Here we consider cut-point transition 72.

21.1.14.3.1 Splitting Cut-Point Transitions

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

21.1.14.4 Cut-Point Subproblem 4/7

Here we consider cut-point transition 79.

21.1.14.4.1 Splitting Cut-Point Transitions

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

21.1.14.5 Cut-Point Subproblem 5/7

Here we consider cut-point transition 86.

21.1.14.5.1 Splitting Cut-Point Transitions

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

21.1.14.6 Cut-Point Subproblem 6/7

Here we consider cut-point transition 100.

21.1.14.6.1 Splitting Cut-Point Transitions

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

21.1.14.7 Cut-Point Subproblem 7/7

Here we consider cut-point transition 107.

21.1.14.7.1 Splitting Cut-Point Transitions

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

21.2 SCC Subproblem 2/2

Here we consider the SCC { 0, 1, 2, 3, 30, 31, 18, 22, 3_var_snapshot, 3*, 22_var_snapshot, 22* }.

21.2.1 Transition Removal

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

0: −3⋅i_0 + 3⋅n_0
1: −3⋅i_0 + 3⋅n_0
2: −3⋅i_0 + 3⋅n_0
3: −3⋅i_0 + 3⋅n_0
30: −1 − 3⋅i_0 + 3⋅n_0
31: −3⋅i_0 + 3⋅n_0
18: 1 − 3⋅i_0 + 3⋅n_0
22: 2 − 3⋅i_0 + 3⋅n_0
3_var_snapshot: −3⋅i_0 + 3⋅n_0
3*: −3⋅i_0 + 3⋅n_0
22_var_snapshot: 1 − 3⋅i_0 + 3⋅n_0
22*: 2 − 3⋅i_0 + 3⋅n_0

21.2.2 Transition Removal

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

0: 1 − 13⋅j_0 + 13⋅n_0
1: −13⋅j_0 + 13⋅n_0
2: −13⋅j_0 + 13⋅n_0
3: 3 − 13⋅j_0 + 13⋅n_0
30: −1 − 13⋅j_0 + 13⋅n_0
31: −8 − 13⋅j_0 + 13⋅n_0
18: −5 − 13⋅j_0 + 13⋅n_0
22: −3 − 13⋅j_0 + 13⋅n_0
3_var_snapshot: 2 − 13⋅j_0 + 13⋅n_0
3*: 4 − 13⋅j_0 + 13⋅n_0
22_var_snapshot: −4 − 13⋅j_0 + 13⋅n_0
22*: −2 − 13⋅j_0 + 13⋅n_0

21.2.3 Transition Removal

We remove transitions 52, 54, 94, 96, 0, 2, 31, 43, 44, 45, 46, 47, 48, 49 using the following ranking functions, which are bounded by −11.

0: −5
1: −6
2: 0
3: −3
30: −7
31: −1
18: −11
22: −9
3_var_snapshot: −4
3*: −2
22_var_snapshot: −10
22*: −8

21.2.4 Splitting Cut-Point Transitions

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

21.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 51.

21.2.4.1.1 Splitting Cut-Point Transitions

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

21.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 93.

21.2.4.2.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert