LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
6 50 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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0
8 57 8: − 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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0
18 64 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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_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.

2 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 5, 6, 7, 44, 46, 48, 49 using the following ranking functions, which are bounded by −27.

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

3 Location Addition

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

6* 53 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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

4 Location Addition

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

6 51 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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_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.

8* 60 8: − 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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_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.

8 58 8_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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_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.

18* 67 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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_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.

18 65 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 ∧ − bNoCapture_post + bNoCapture_post ≤ 0 ∧ bNoCapture_post − bNoCapture_post ≤ 0 ∧ − bNoCapture_0 + bNoCapture_0 ≤ 0 ∧ bNoCapture_0 − bNoCapture_0 ≤ 0 ∧ − bDomain_post + bDomain_post ≤ 0 ∧ bDomain_post − bDomain_post ≤ 0 ∧ − bDomain_0 + bDomain_0 ≤ 0 ∧ bDomain_0 − bDomain_0 ≤ 0

9 SCC Decomposition

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

9.1 SCC Subproblem 1/2

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

9.1.1 Transition Removal

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

5: −4 + 19⋅nDim_0 − 19⋅ni_0
6: −4 + 19⋅nDim_0 − 19⋅ni_0
7: −4 + 19⋅nDim_0 − 19⋅ni_0
10: −4 + 19⋅nDim_0 − 19⋅ni_0
11: −4 + 19⋅nDim_0 − 19⋅ni_0
12: −4 + 19⋅nDim_0 − 19⋅ni_0
13: −4 + 19⋅nDim_0 − 19⋅ni_0
14: −4 + 19⋅nDim_0 − 19⋅ni_0
15: −4 + 19⋅nDim_0 − 19⋅ni_0
16: −4 + 19⋅nDim_0 − 19⋅ni_0
17: −4 + 19⋅nDim_0 − 19⋅ni_0
20: −4 + 19⋅nDim_0 − 19⋅ni_0
21: −4 + 19⋅nDim_0 − 19⋅ni_0
18: 13 + 19⋅nDim_0 − 19⋅ni_0
19: 11 + 19⋅nDim_0 − 19⋅ni_0
22: −3 + 19⋅nDim_0 − 19⋅ni_0
23: −2 + 19⋅nDim_0 − 19⋅ni_0
24: −1 + 19⋅nDim_0 − 19⋅ni_0
25: 19⋅nDim_0 − 19⋅ni_0
6_var_snapshot: −4 + 19⋅nDim_0 − 19⋅ni_0
6*: −4 + 19⋅nDim_0 − 19⋅ni_0
18_var_snapshot: 12 + 19⋅nDim_0 − 19⋅ni_0
18*: 14 + 19⋅nDim_0 − 19⋅ni_0

9.1.2 Transition Removal

We remove transitions 35, 36, 37, 39, 40, 41, 42, 43 using the following ranking functions, which are bounded by −3.

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

9.1.3 Transition Removal

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

5: −18 + 21⋅ni_0 − 21⋅nj_0
6: 1 + 21⋅ni_0 − 21⋅nj_0
7: −17 + 21⋅ni_0 − 21⋅nj_0
10: −16 + 21⋅ni_0 − 21⋅nj_0
11: −15 + 21⋅ni_0 − 21⋅nj_0
12: −14 + 21⋅ni_0 − 21⋅nj_0
13: −13 + 21⋅ni_0 − 21⋅nj_0
14: −12 + 21⋅ni_0 − 21⋅nj_0
15: −11 + 21⋅ni_0 − 21⋅nj_0
16: −10 + 21⋅ni_0 − 21⋅nj_0
17: −9 + 21⋅ni_0 − 21⋅nj_0
20: −9 + 21⋅ni_0 − 21⋅nj_0
21: −1 + 21⋅ni_0 − 21⋅nj_0
18: −24 + 3⋅ni_0 + 18⋅ni_post − 21⋅nj_0
19: −26 + 3⋅ni_0 + 18⋅ni_post − 21⋅nj_0
22: 0
23: 0
24: 0
25: 0
6_var_snapshot: 21⋅ni_0 − 21⋅nj_0
6*: 2 + 21⋅ni_0 − 21⋅nj_0
18_var_snapshot: −25 + 3⋅ni_0 + 18⋅ni_post − 21⋅nj_0
18*: −23 + 3⋅ni_0 + 18⋅ni_post − 21⋅nj_0

9.1.4 Transition Removal

We remove transition 34 using the following ranking functions, which are bounded by 14.

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

9.1.5 Transition Removal

We remove transitions 51, 53, 65, 67, 8, 9, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 31, 32, 33, 38 using the following ranking functions, which are bounded by −17.

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

9.1.6 Splitting Cut-Point Transitions

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

9.1.6.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 50.

9.1.6.1.1 Splitting Cut-Point Transitions

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

9.1.6.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 64.

9.1.6.2.1 Splitting Cut-Point Transitions

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

9.2 SCC Subproblem 2/2

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

9.2.1 Transition Removal

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

8: 2 + 4⋅nDim_0 − 4⋅ni_0
9: 4⋅nDim_0 − 4⋅ni_0
8_var_snapshot: 1 + 4⋅nDim_0 − 4⋅ni_0
8*: 3 + 4⋅nDim_0 − 4⋅ni_0

9.2.2 Transition Removal

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

8: 0
9: −2
8_var_snapshot: −1
8*: 1

9.2.3 Splitting Cut-Point Transitions

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

9.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 57.

9.2.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert