LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 50 0: − 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
2 57 2: − 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 64 6: − 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 71 9: − 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 78 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 85 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
19 92 19: − 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
23 99 23: − 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
26 106 26: − 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 33, 45, 48, 49 using the following ranking functions, which are bounded by −31.

32: 0
31: 0
0: 0
1: 0
25: 0
26: 0
27: 0
28: 0
29: 0
30: 0
2: 0
3: 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
18: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
32: −6
31: −7
0: −8
1: −8
25: −8
27: −8
28: −8
29: −8
26: −8
30: −8
0_var_snapshot: −8
0*: −8
26_var_snapshot: −8
26*: −8
2: −11
3: −11
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
18: −11
19: −11
20: −11
21: −11
22: −11
23: −11
2_var_snapshot: −11
2*: −11
6_var_snapshot: −11
6*: −11
9_var_snapshot: −11
9*: −11
13_var_snapshot: −11
13*: −11
16_var_snapshot: −11
16*: −11
19_var_snapshot: −11
19*: −11
23_var_snapshot: −11
23*: −11
24: −24

3 Location Addition

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

0* 53 0: − 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.

0 51 0_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.

2* 60 2: − 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.

2 58 2_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.

6* 67 6: − 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.

6 65 6_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.

9* 74 9: − 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.

9 72 9_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.

13* 81 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

12 Location Addition

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

13 79 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

13 Location Addition

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

16* 88 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

14 Location Addition

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

16 86 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

15 Location Addition

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

19* 95 19: − 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.

19 93 19_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.

23* 102 23: − 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.

23 100 23_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.

26* 109 26: − 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.

26 107 26_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 { 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 2_var_snapshot, 2*, 6_var_snapshot, 6*, 9_var_snapshot, 9*, 13_var_snapshot, 13*, 16_var_snapshot, 16*, 19_var_snapshot, 19*, 23_var_snapshot, 23* }.

21.1.1 Transition Removal

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

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

21.1.2 Transition Removal

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

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

21.1.3 Transition Removal

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

2: 0
3: 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
18: 0
19: 0
20: 0
21: 0
22: 1
23: 1
2_var_snapshot: 0
2*: 0
6_var_snapshot: 0
6*: 0
9_var_snapshot: 0
9*: 0
13_var_snapshot: 0
13*: 0
16_var_snapshot: 0
16*: 0
19_var_snapshot: 0
19*: 0
23_var_snapshot: 1
23*: 1

21.1.4 Transition Removal

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

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

21.1.5 Transition Removal

We remove transitions 100, 27 using the following ranking functions, which are bounded by −2.

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

21.1.6 Transition Removal

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

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

21.1.7 Transition Removal

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

2: 0
3: 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
18: 0
19: 0
20: 1
21: 0
22: 0
23: 0
2_var_snapshot: 0
2*: 0
6_var_snapshot: 0
6*: 0
9_var_snapshot: 0
9*: 0
13_var_snapshot: 0
13*: 0
16_var_snapshot: 0
16*: 0
19_var_snapshot: 0
19*: 0
23_var_snapshot: 0
23*: 0

21.1.8 Transition Removal

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

2: 0
3: 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
18: 0
19: 0
20: 1
21: 0
22: 0
23: 0
2_var_snapshot: 0
2*: 0
6_var_snapshot: 0
6*: 0
9_var_snapshot: 0
9*: 0
13_var_snapshot: 0
13*: 0
16_var_snapshot: 0
16*: 0
19_var_snapshot: 0
19*: 0
23_var_snapshot: 0
23*: 0

21.1.9 Transition Removal

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

2: 0
3: 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
18: 1
19: 0
20: 0
21: 0
22: 0
23: 0
2_var_snapshot: 0
2*: 0
6_var_snapshot: 0
6*: 0
9_var_snapshot: 0
9*: 0
13_var_snapshot: 0
13*: 0
16_var_snapshot: 0
16*: 0
19_var_snapshot: 0
19*: 0
23_var_snapshot: 0
23*: 0

21.1.10 Transition Removal

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

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

21.1.11 Transition Removal

We remove transitions 65, 67, 3, 40 using the following ranking functions, which are bounded by −2.

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

21.1.12 Transition Removal

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

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

21.1.13 Transition Removal

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

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

21.1.14 Transition Removal

We remove transitions 13, 28 using the following ranking functions, which are bounded by 3.

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

21.1.15 Transition Removal

We remove transitions 79, 81, 15 using the following ranking functions, which are bounded by −14.

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

21.1.16 Transition Removal

We remove transitions 72, 74, 86, 88, 93, 95, 5, 6, 7, 10, 11, 12, 14, 16, 17, 18, 22, 25, 30, 32, 34 using the following ranking functions, which are bounded by −17.

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

21.1.17 Transition Removal

We remove transitions 58, 60, 1, 2, 9 using the following ranking functions, which are bounded by −4.

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

21.1.18 Splitting Cut-Point Transitions

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

21.1.18.1 Cut-Point Subproblem 1/7

Here we consider cut-point transition 57.

21.1.18.1.1 Splitting Cut-Point Transitions

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

21.1.18.2 Cut-Point Subproblem 2/7

Here we consider cut-point transition 64.

21.1.18.2.1 Splitting Cut-Point Transitions

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

21.1.18.3 Cut-Point Subproblem 3/7

Here we consider cut-point transition 71.

21.1.18.3.1 Splitting Cut-Point Transitions

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

21.1.18.4 Cut-Point Subproblem 4/7

Here we consider cut-point transition 78.

21.1.18.4.1 Splitting Cut-Point Transitions

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

21.1.18.5 Cut-Point Subproblem 5/7

Here we consider cut-point transition 85.

21.1.18.5.1 Splitting Cut-Point Transitions

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

21.1.18.6 Cut-Point Subproblem 6/7

Here we consider cut-point transition 92.

21.1.18.6.1 Splitting Cut-Point Transitions

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

21.1.18.7 Cut-Point Subproblem 7/7

Here we consider cut-point transition 99.

21.1.18.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, 25, 27, 28, 29, 26, 30, 0_var_snapshot, 0*, 26_var_snapshot, 26* }.

21.2.1 Transition Removal

We remove transition 46 using the following ranking functions, which are bounded by −2.

0: −2 − 14⋅i_0 + 14⋅n_0
1: −2 − 14⋅i_0 + 14⋅n_0
25: −11 − 14⋅i_0 + 14⋅n_0
27: −11 − 14⋅i_0 + 14⋅n_0
28: −2 − 14⋅i_0 + 14⋅n_0
29: −2 − 14⋅i_0 + 14⋅n_0
26: 1 − 14⋅i_0 + 14⋅n_0
30: −1 − 14⋅i_0 + 14⋅n_0
0_var_snapshot: −2 − 14⋅i_0 + 14⋅n_0
0*: −2 − 14⋅i_0 + 14⋅n_0
26_var_snapshot: −14⋅i_0 + 14⋅n_0
26*: 2 − 14⋅i_0 + 14⋅n_0

21.2.2 Transition Removal

We remove transitions 107, 109, 35, 43, 47 using the following ranking functions, which are bounded by −5.

0: 0
1: 0
25: −1
27: −1
28: 0
29: 0
26: −3
30: −5
0_var_snapshot: 0
0*: 0
26_var_snapshot: −4
26*: −2

21.2.3 Transition Removal

We remove transitions 36, 37, 38, 44 using the following ranking functions, which are bounded by −1.

0: 2 − 6⋅j_0 + 6⋅n_0
1: −6⋅j_0 + 6⋅n_0
25: −1
27: 0
28: −2 − 6⋅j_0 + 6⋅n_0
29: −1 − 6⋅j_0 + 6⋅n_0
26: 0
30: 0
0_var_snapshot: 1 − 6⋅j_0 + 6⋅n_0
0*: 3 − 6⋅j_0 + 6⋅n_0
26_var_snapshot: 0
26*: 0

21.2.4 Transition Removal

We remove transitions 51, 53, 0, 39, 41, 42 using the following ranking functions, which are bounded by −4.

0: −2
1: −4
25: 0
27: 0
28: 0
29: 1
26: 0
30: 0
0_var_snapshot: −3
0*: −1
26_var_snapshot: 0
26*: 0

21.2.5 Splitting Cut-Point Transitions

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

21.2.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 50.

21.2.5.1.1 Splitting Cut-Point Transitions

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

21.2.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 106.

21.2.5.2.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert