LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0 ∧ −1 + tmp___4_post ≤ 0 ∧ −1 + tmp___4_0 ≤ 0
1: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0 ∧ −1 + tmp___4_post ≤ 0 ∧ −1 + tmp___4_0 ≤ 0
2: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0
3: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0
4: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0
5: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0 ∧ − tmp___3_post ≤ 0 ∧ − tmp___3_0 ≤ 0
6: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0
7: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0
8: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0
9: −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ 10 − nDim_0 ≤ 0
10: −1 + bDomain_post ≤ 0 ∧ 1 − bDomain_post ≤ 0 ∧ −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bDomain_0 ≤ 0 ∧ 1 − bDomain_0 ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ −10 + nDim_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
11: −1 + bDomain_post ≤ 0 ∧ 1 − bDomain_post ≤ 0 ∧ −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bDomain_0 ≤ 0 ∧ 1 − bDomain_0 ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ −10 + nDim_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
12: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0 ∧ − tmp___2_post ≤ 0 ∧ − tmp___2_0 ≤ 0
13: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
14: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
15: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
16: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
17: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0 ∧ bExists_0 ≤ 0 ∧ − bExists_0 ≤ 0
18: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0 ∧ −1 + tmp___1_post ≤ 0 ∧ −1 + tmp___1_0 ≤ 0
19: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
20: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0 ∧ bExists_0 ≤ 0 ∧ − bExists_0 ≤ 0
21: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
22: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
23: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
24: −1 + bSorted_post ≤ 0 ∧ 1 − bSorted_post ≤ 0 ∧ −10 + nDim_post ≤ 0 ∧ 10 − nDim_post ≤ 0 ∧ −1 + bSorted_0 ≤ 0 ∧ 1 − bSorted_0 ≤ 0 ∧ 10 − nDim_0 ≤ 0
25: TRUE
26: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
6 45 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0
10 52 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0
13 59 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0
21 66 21: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 5, 6, 7, 14, 38, 40, 43, 44 using the following ranking functions, which are bounded by −31.

26: 0
25: 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
5: 0
6: 0
7: 0
8: 0
9: 0
4: 0
3: 0
2: 0
0: 0
1: 0
26: −11
25: −12
10: −13
11: −13
10_var_snapshot: −13
10*: −13
12: −14
13: −14
14: −14
15: −14
16: −14
17: −14
18: −14
19: −14
20: −14
21: −14
22: −14
23: −14
24: −14
13_var_snapshot: −14
13*: −14
21_var_snapshot: −14
21*: −14
5: −17
6: −17
7: −17
8: −17
9: −17
6_var_snapshot: −17
6*: −17
4: −18
3: −19
2: −20
0: −21
1: −22

4 Location Addition

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

6* 48 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

5 Location Addition

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

6 46 6_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

6 Location Addition

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

10* 55 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

7 Location Addition

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

10 53 10_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

8 Location Addition

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

13* 62 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

9 Location Addition

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

13 60 13_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

10 Location Addition

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

21* 69 21: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

11 Location Addition

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

21 67 21_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___4_post + tmp___4_post ≤ 0 ∧ tmp___4_post − tmp___4_post ≤ 0 ∧ − tmp___4_0 + tmp___4_0 ≤ 0 ∧ tmp___4_0 − tmp___4_0 ≤ 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 ∧ − bSorted_post + bSorted_post ≤ 0 ∧ bSorted_post − bSorted_post ≤ 0 ∧ − bSorted_0 + bSorted_0 ≤ 0 ∧ bSorted_0 − bSorted_0 ≤ 0 ∧ − bExists_post + bExists_post ≤ 0 ∧ bExists_post − bExists_post ≤ 0 ∧ − bExists_0 + bExists_0 ≤ 0 ∧ bExists_0 − bExists_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

12 SCC Decomposition

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

12.1 SCC Subproblem 1/3

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

12.1.1 Transition Removal

We remove transition 15 using the following ranking functions, which are bounded by 113.

5: −11 + 52⋅nDim_0 − 52⋅ni_0
6: 30 + 52⋅nDim_0 − 52⋅ni_0
7: 52⋅nDim_0 − nDim_post − 52⋅ni_0
8: 52⋅nDim_0 − 52⋅ni_0
9: −10 + 52⋅nDim_0 + 2⋅nDim_post − 52⋅ni_0
6_var_snapshot: 52⋅nDim_0 + 2⋅nDim_post − 52⋅ni_0
6*: 52⋅nDim_0 + 4⋅nDim_post − 52⋅ni_0

12.1.2 Transition Removal

We remove transitions 46, 48, 8, 9, 10, 11, 12, 13, 42 using the following ranking functions, which are bounded by −31.

5: 0
6: −2⋅nDim_post
7: 2⋅nDim_0 − nDim_post
8: 2⋅nDim_0
9: −4⋅nDim_0
6_var_snapshot: −30
6*: −10

12.1.3 Splitting Cut-Point Transitions

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

12.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 45.

12.1.3.1.1 Splitting Cut-Point Transitions

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

12.2 SCC Subproblem 2/3

Here we consider the SCC { 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 13_var_snapshot, 13*, 21_var_snapshot, 21* }.

12.2.1 Transition Removal

We remove transition 39 using the following ranking functions, which are bounded by 36.

12: −13 + 36⋅nDim_0 − 36⋅ni_0
13: −20⋅bSorted_0 + 22⋅bSorted_post + 36⋅nDim_0 + nDim_post − 36⋅ni_0
14: −1 − 11⋅bSorted_post + 36⋅nDim_0 − 36⋅ni_0
15: −11⋅bSorted_post + 36⋅nDim_0 − 36⋅ni_0
16: −20⋅bSorted_0 + 10⋅bSorted_post + 36⋅nDim_0 − 36⋅ni_0
17: −9⋅bSorted_post + 36⋅nDim_0 − 36⋅ni_0
18: −9⋅bSorted_0 + 36⋅nDim_0 − 36⋅ni_0
19: bSorted_0 + 36⋅nDim_0 − 36⋅ni_0
20: −9⋅bSorted_post + 36⋅nDim_0 − 36⋅ni_0
21: bSorted_0 + 36⋅nDim_0 − nDim_post − 36⋅ni_0
22: −9 + 36⋅nDim_0 − 36⋅ni_0
23: −9⋅bSorted_0 + 36⋅nDim_0 − 36⋅ni_0
24: −9⋅bSorted_0 + 10⋅bSorted_post + 36⋅nDim_0 − nDim_post − 36⋅ni_0
13_var_snapshot: −1 + bSorted_0 + 22⋅bSorted_post + 36⋅nDim_0 − 2⋅nDim_post − 36⋅ni_0
13*: 22⋅bSorted_post + 36⋅nDim_0 − 36⋅ni_0
21_var_snapshot: 10 − 9⋅bSorted_0 + 36⋅nDim_0 − nDim_post − 36⋅ni_0
21*: bSorted_0 − 10⋅bSorted_post + 36⋅nDim_0 − 36⋅ni_0

12.2.2 Transition Removal

We remove transition 36 using the following ranking functions, which are bounded by 47.

12: bSorted_post + 25⋅nDim_0 + nDim_post − 26⋅nj_0 − tmp___2_0
13: − bSorted_0 + 10⋅bSorted_post + 25⋅nDim_0 − 26⋅nj_0 − tmp___2_0
14: 10 + bSorted_post + 25⋅nDim_0 − 26⋅nj_0
15: 1 + bSorted_post + 25⋅nDim_0 + nDim_post − 26⋅nj_0
16: 1 + bSorted_0 + 26⋅nDim_0 + nDim_post − 26⋅nj_0
17: 1 + 26⋅nDim_0 − 26⋅nj_0
18: 26⋅nDim_0 − 26⋅nj_0
19: − bSorted_0 + 10⋅bSorted_post + 25⋅nDim_0 − 2⋅nDim_post − 26⋅nj_0 − tmp___2_0
20: 11⋅bSorted_post + 26⋅nDim_0 − 26⋅nj_0
21: 24 + 26⋅nDim_0 − 26⋅nj_0
22: 11⋅bSorted_0 + 26⋅nDim_0 − 26⋅nj_0
23: 12⋅bSorted_post + 26⋅nDim_0 − 26⋅nj_0
24: −88⋅bSorted_0 + 26⋅nDim_0 + 11⋅nDim_post − 26⋅nj_0
13_var_snapshot: − bSorted_0 + 10⋅bSorted_post + 25⋅nDim_0 − nDim_post − 26⋅nj_0 − tmp___2_0
13*: 10⋅bSorted_post + 25⋅nDim_0 − 26⋅nj_0 − tmp___2_0
21_var_snapshot: −87 + 26⋅nDim_0 + 11⋅nDim_post − 26⋅nj_0
21*: 25⋅bSorted_post + 26⋅nDim_0 − 26⋅nj_0

12.2.3 Transition Removal

We remove transitions 60, 62, 67, 69, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 37 using the following ranking functions, which are bounded by −52.

12: −30⋅bSorted_post
13: −11⋅bSorted_0 − 30⋅bSorted_post
14: −20⋅bSorted_post
15: − nDim_post
16: 0
17: 6⋅nDim_0
18: 50⋅bSorted_post
19: −1 − 11⋅bSorted_0 − 4⋅nDim_post
20: 10⋅bSorted_post + 6⋅nDim_0
21: 3⋅nDim_post
22: −9 + 6⋅nDim_0
23: 6⋅nDim_0 + 2⋅nDim_post
24: 20⋅bSorted_post − nDim_post
13_var_snapshot: −11⋅bSorted_0 − 4⋅nDim_post
13*: −30⋅bSorted_post − nDim_post
21_var_snapshot: 20⋅bSorted_post
21*: −40⋅bSorted_0 + 50⋅bSorted_post + 3⋅nDim_post

12.2.4 Splitting Cut-Point Transitions

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

12.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 59.

12.2.4.1.1 Splitting Cut-Point Transitions

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

12.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 66.

12.2.4.2.1 Splitting Cut-Point Transitions

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

12.3 SCC Subproblem 3/3

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

12.3.1 Transition Removal

We remove transition 41 using the following ranking functions, which are bounded by −38.

10: bDomain_0 − 4⋅ni_0
11: bDomain_0 − 2⋅bSorted_post − 4⋅ni_0
10_var_snapshot: −4⋅ni_0
10*: bDomain_0 + 3⋅bDomain_post − 2⋅bSorted_post − 4⋅ni_0

12.3.2 Transition Removal

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

10: 0
11: − bDomain_0 − bDomain_post
10_var_snapshot: − bDomain_post
10*: 1

12.3.3 Splitting Cut-Point Transitions

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

12.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 52.

12.3.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert