LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
6 54 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0
9 61 9: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0
14 68 14: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0
18 75 18: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0
19 82 19: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 23, 36, 48, 50, 52, 53 using the following ranking functions, which are bounded by −37.

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

3 Location Addition

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

6* 57 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

4 Location Addition

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

6 55 6_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

5 Location Addition

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

9* 64 9: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

6 Location Addition

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

9 62 9_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

7 Location Addition

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

14* 71 14: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

8 Location Addition

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

14 69 14_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

9 Location Addition

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

18* 78 18: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

10 Location Addition

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

18 76 18_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

11 Location Addition

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

19* 85 19: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

12 Location Addition

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

19 83 19_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___3_post + tmp___3_post ≤ 0 ∧ tmp___3_post − tmp___3_post ≤ 0 ∧ − tmp___3_0 + tmp___3_0 ≤ 0 ∧ tmp___3_0 − tmp___3_0 ≤ 0 ∧ − tmp___2_post + tmp___2_post ≤ 0 ∧ tmp___2_post − tmp___2_post ≤ 0 ∧ − tmp___2_0 + tmp___2_0 ≤ 0 ∧ tmp___2_0 − tmp___2_0 ≤ 0 ∧ − tmp___1_post + tmp___1_post ≤ 0 ∧ tmp___1_post − tmp___1_post ≤ 0 ∧ − tmp___1_0 + tmp___1_0 ≤ 0 ∧ tmp___1_0 − tmp___1_0 ≤ 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 ∧ − nj_post + nj_post ≤ 0 ∧ nj_post − nj_post ≤ 0 ∧ − nj_0 + nj_0 ≤ 0 ∧ nj_0 − nj_0 ≤ 0 ∧ − ni_post + ni_post ≤ 0 ∧ ni_post − ni_post ≤ 0 ∧ − ni_0 + ni_0 ≤ 0 ∧ ni_0 − ni_0 ≤ 0 ∧ − nDim_post + nDim_post ≤ 0 ∧ nDim_post − nDim_post ≤ 0 ∧ − nDim_0 + nDim_0 ≤ 0 ∧ nDim_0 − nDim_0 ≤ 0 ∧ − nDiff_post + nDiff_post ≤ 0 ∧ nDiff_post − nDiff_post ≤ 0 ∧ − nDiff_0 + nDiff_0 ≤ 0 ∧ nDiff_0 − nDiff_0 ≤ 0 ∧ − bGray_post + bGray_post ≤ 0 ∧ bGray_post − bGray_post ≤ 0 ∧ − bGray_0 + bGray_0 ≤ 0 ∧ bGray_0 − bGray_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0 ∧ − bAllDiff_post + bAllDiff_post ≤ 0 ∧ bAllDiff_post − bAllDiff_post ≤ 0 ∧ − bAllDiff_0 + bAllDiff_0 ≤ 0 ∧ bAllDiff_0 − bAllDiff_0 ≤ 0 ∧ − ___const_12_0 + ___const_12_0 ≤ 0 ∧ ___const_12_0 − ___const_12_0 ≤ 0

13 SCC Decomposition

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

13.1 SCC Subproblem 1/4

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

13.1.1 Transition Removal

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

8: −6 + 9⋅nDim_0 − 9⋅ni_0
9: 1 + 9⋅nDim_0 − 9⋅ni_0
10: −5 + 9⋅nDim_0 − 9⋅ni_0
11: −4 + 9⋅nDim_0 − 9⋅ni_0
12: −3 + 9⋅nDim_0 − 9⋅ni_0
13: −2 + 9⋅nDim_0 − 9⋅ni_0
16: −1 + 9⋅nDim_0 − 9⋅ni_0
9_var_snapshot: 9⋅nDim_0 − 9⋅ni_0
9*: 2 + 9⋅nDim_0 − 9⋅ni_0

13.1.2 Transition Removal

We remove transitions 62, 64, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 47 using the following ranking functions, which are bounded by −8.

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

13.1.3 Splitting Cut-Point Transitions

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

13.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 61.

13.1.3.1.1 Splitting Cut-Point Transitions

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

13.2 SCC Subproblem 2/4

Here we consider the SCC { 17, 18, 21, 22, 23, 24, 19, 20, 18_var_snapshot, 18*, 19_var_snapshot, 19* }.

13.2.1 Transition Removal

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

17: 12⋅nDim_0 − 12⋅ni_0
18: 12⋅nDim_0 − 12⋅ni_0
21: 12⋅nDim_0 − 12⋅ni_0
22: 12⋅nDim_0 − 12⋅ni_0
23: 12⋅nDim_0 − 12⋅ni_0
24: 12⋅nDim_0 − 12⋅ni_0
19: 10 + 12⋅nDim_0 − 12⋅ni_0
20: 8 + 12⋅nDim_0 − 12⋅ni_0
18_var_snapshot: 12⋅nDim_0 − 12⋅ni_0
18*: 12⋅nDim_0 − 12⋅ni_0
19_var_snapshot: 9 + 12⋅nDim_0 − 12⋅ni_0
19*: 11 + 12⋅nDim_0 − 12⋅ni_0

13.2.2 Transition Removal

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

17: −9 + 12⋅nDim_0 − 12⋅nj_0
18: 1 + 12⋅nDim_0 − 12⋅nj_0
21: −8 + 12⋅nDim_0 − 12⋅nj_0
22: −7 + 12⋅nDim_0 − 12⋅nj_0
23: −6 + 12⋅nDim_0 − 12⋅nj_0
24: −1 + 12⋅nDim_0 − 12⋅nj_0
19: −3 + 12⋅nDim_0 − 12⋅nj_0
20: −5 + 12⋅nDim_0 − 12⋅nj_0
18_var_snapshot: 12⋅nDim_0 − 12⋅nj_0
18*: 2 + 12⋅nDim_0 − 12⋅nj_0
19_var_snapshot: −4 + 12⋅nDim_0 − 12⋅nj_0
19*: −2 + 12⋅nDim_0 − 12⋅nj_0

13.2.3 Transition Removal

We remove transitions 76, 78, 83, 85, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 38 using the following ranking functions, which are bounded by −5.

17: 3
18: 1
21: 4
22: 5
23: 6
24: −1
19: −3
20: −5
18_var_snapshot: 0
18*: 2
19_var_snapshot: −4
19*: −2

13.2.4 Splitting Cut-Point Transitions

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

13.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 75.

13.2.4.1.1 Splitting Cut-Point Transitions

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

13.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 82.

13.2.4.2.1 Splitting Cut-Point Transitions

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

13.3 SCC Subproblem 3/4

Here we consider the SCC { 14, 15, 25, 26, 27, 28, 14_var_snapshot, 14* }.

13.3.1 Transition Removal

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

14: 5 + 10⋅nDim_0 − 10⋅ni_0
15: 3 + 10⋅nDim_0 − 10⋅ni_0
25: −3 + 10⋅nDim_0 − 10⋅ni_0
26: −2 + 10⋅nDim_0 − 10⋅ni_0
27: −1 + 10⋅nDim_0 − 10⋅ni_0
28: 10⋅nDim_0 − 10⋅ni_0
14_var_snapshot: 4 + 10⋅nDim_0 − 10⋅ni_0
14*: 6 + 10⋅nDim_0 − 10⋅ni_0

13.3.2 Transition Removal

We remove transitions 69, 71, 22, 39, 40, 41, 42, 43, 44, 45, 46 using the following ranking functions, which are bounded by −7.

14: −5
15: −7
25: −3
26: −2
27: −1
28: 0
14_var_snapshot: −6
14*: −4

13.3.3 Splitting Cut-Point Transitions

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

13.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 68.

13.3.3.1.1 Splitting Cut-Point Transitions

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

13.4 SCC Subproblem 4/4

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

13.4.1 Transition Removal

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

6: 2 + 4⋅nDim_0 − 4⋅ni_0
7: 4⋅nDim_0 − 4⋅ni_0
6_var_snapshot: 1 + 4⋅nDim_0 − 4⋅ni_0
6*: 3 + 4⋅nDim_0 − 4⋅ni_0

13.4.2 Transition Removal

We remove transitions 55, 57, 11 using the following ranking functions, which are bounded by −2.

6: 0
7: −2
6_var_snapshot: −1
6*: 1

13.4.3 Splitting Cut-Point Transitions

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

13.4.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 54.

13.4.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert