LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ −2 + nDim_0 ≤ 0 ∧ 2 − nDim_0 ≤ 0
1: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ −2 + nDim_0 ≤ 0 ∧ 2 − nDim_0 ≤ 0
2: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ −2 + nDim_0 ≤ 0 ∧ 2 − nDim_0 ≤ 0
3: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ −2 + nDim_0 ≤ 0 ∧ 2 − nDim_0 ≤ 0
4: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
5: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0 ∧ −1 + tmp___1_post ≤ 0 ∧ −1 + tmp___1_0 ≤ 0
6: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
7: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
8: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
9: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0 ∧ −1 + tmp___1_post ≤ 0 ∧ −1 + tmp___1_0 ≤ 0
10: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
11: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
12: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
13: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
14: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
15: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
16: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
17: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
18: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
19: −2 + nDim_post ≤ 0 ∧ 2 − nDim_post ≤ 0 ∧ 2 − nDim_0 ≤ 0
20: TRUE
21: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 34 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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
2 41 2: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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
13 48 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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
17 55 17: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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
18 62 18: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 17, 18, 19, 25, 30, 32, 33 using the following ranking functions, which are bounded by −41.

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

4 Location Addition

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

0* 37 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

5 Location Addition

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

0 35 0_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

6 Location Addition

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

2* 44 2: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

7 Location Addition

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

2 42 2_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

8 Location Addition

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

13* 51 13: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

9 Location Addition

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

13 49 13_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

10 Location Addition

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

17* 58 17: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

11 Location Addition

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

17 56 17_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

12 Location Addition

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

18* 65 18: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

13 Location Addition

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

18 63 18_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 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 ∧ − nk_post + nk_post ≤ 0 ∧ nk_post − nk_post ≤ 0 ∧ − nk_0 + nk_0 ≤ 0 ∧ nk_0 − nk_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

14 SCC Decomposition

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

14.1 SCC Subproblem 1/2

Here we consider the SCC { 13, 14, 16, 17, 18, 19, 13_var_snapshot, 13*, 17_var_snapshot, 17*, 18_var_snapshot, 18* }.

14.1.1 Transition Removal

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

13: 8 + 12⋅nDim_0 − 12⋅ni_0
14: 6 + 12⋅nDim_0 − 12⋅ni_0
16: 12⋅nDim_0 − 12⋅ni_0
17: 12⋅nDim_0 − 12⋅ni_0
18: 12⋅nDim_0 − 12⋅ni_0
19: 12⋅nDim_0 − 12⋅ni_0
13_var_snapshot: 12⋅nDim_0 + 4⋅nDim_post − 12⋅ni_0
13*: 10 + 12⋅nDim_0 − 12⋅ni_0
17_var_snapshot: 12⋅nDim_0 − 12⋅ni_0
17*: 12⋅nDim_0 − 12⋅ni_0
18_var_snapshot: 12⋅nDim_0 − 12⋅ni_0
18*: 12⋅nDim_0 − 12⋅ni_0

14.1.2 Transition Removal

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

13: −1 − 5⋅nj_0
14: −1 − nDim_post − 5⋅nj_0
16: 5⋅nDim_0 − 5⋅nj_0
17: 3 + 5⋅nDim_0 − 5⋅nj_0
18: 5⋅nDim_0 − 5⋅nj_0
19: 1 + 5⋅nDim_0 − 5⋅nj_0
13_var_snapshot: − nDim_post − 5⋅nj_0
13*: −5⋅nj_0
17_var_snapshot: 2 + 5⋅nDim_0 − 5⋅nj_0
17*: 4 + 5⋅nDim_0 − 5⋅nj_0
18_var_snapshot: 5⋅nDim_0 − 5⋅nj_0
18*: 5⋅nDim_0 − 5⋅nj_0

14.1.3 Transition Removal

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

13: nDim_0 − 4⋅nk_0
14: −1 + nDim_0 − nDim_post − 4⋅nk_0
16: −2 + 4⋅nDim_0 + 2⋅nDim_post − 4⋅nk_0
17: 4⋅nDim_0 − 4⋅nk_0
18: 4 + 4⋅nDim_0 − 4⋅nk_0
19: 3⋅nDim_0 − nDim_post − 4⋅nk_0
13_var_snapshot: nDim_0 − nDim_post − 4⋅nk_0
13*: 2⋅nDim_0 − 4⋅nk_0
17_var_snapshot: 3⋅nDim_0 − 4⋅nk_0
17*: −4 + 4⋅nDim_0 + 2⋅nDim_post − 4⋅nk_0
18_var_snapshot: 4⋅nDim_0 + 2⋅nDim_post − 4⋅nk_0
18*: 1 + 4⋅nDim_0 + 2⋅nDim_post − 4⋅nk_0

14.1.4 Transition Removal

We remove transitions 49, 56, 58, 63, 65, 16, 20, 22, 23, 27 using the following ranking functions, which are bounded by −9.

13: −6
14: −1 − 4⋅nDim_post
16: −2 + 2⋅nDim_0 + 2⋅nDim_post
17: −2 + 2⋅nDim_post
18: 2⋅nDim_0 + 3⋅nDim_post
19: − nDim_post
13_var_snapshot: −4⋅nDim_post
13*: −2 − nDim_post
17_var_snapshot: 0
17*: 2⋅nDim_post
18_var_snapshot: 2⋅nDim_0 + 2⋅nDim_post
18*: 2⋅nDim_0 + 4⋅nDim_post

14.1.5 Transition Removal

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

13: 0
14: 0
16: 0
17: 0
18: 0
19: 0
13_var_snapshot: 0
13*: 1
17_var_snapshot: 0
17*: 0
18_var_snapshot: 0
18*: 0

14.1.6 Splitting Cut-Point Transitions

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

14.1.6.1 Cut-Point Subproblem 1/3

Here we consider cut-point transition 48.

14.1.6.1.1 Splitting Cut-Point Transitions

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

14.1.6.2 Cut-Point Subproblem 2/3

Here we consider cut-point transition 55.

14.1.6.2.1 Splitting Cut-Point Transitions

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

14.1.6.3 Cut-Point Subproblem 3/3

Here we consider cut-point transition 62.

14.1.6.3.1 Splitting Cut-Point Transitions

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

14.2 SCC Subproblem 2/2

Here we consider the SCC { 0, 1, 2, 3, 0_var_snapshot, 0*, 2_var_snapshot, 2* }.

14.2.1 Transition Removal

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

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

14.2.2 Transition Removal

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

0: − nDim_post − 7⋅nj_0
1: −2⋅nDim_0 − nDim_post − 7⋅nj_0
2: −2 + 4⋅nDim_0 − 7⋅nj_0
3: nDim_0 − 7⋅nj_0
0_var_snapshot: −2 − nDim_post − 7⋅nj_0
0*: −7⋅nj_0
2_var_snapshot: 4⋅nDim_0 − 2⋅nDim_post − 7⋅nj_0
2*: 4⋅nDim_0 − 7⋅nj_0

14.2.3 Transition Removal

We remove transitions 35, 37, 42, 44, 0, 1, 28 using the following ranking functions, which are bounded by −9.

0: −4 − nDim_post
1: −5⋅nDim_post
2: nDim_0
3: − nDim_post
0_var_snapshot: −3⋅nDim_0 − nDim_post
0*: − nDim_0 − nDim_post
2_var_snapshot: 0
2*: 2⋅nDim_0

14.2.4 Splitting Cut-Point Transitions

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

14.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 34.

14.2.4.1.1 Splitting Cut-Point Transitions

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

14.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 41.

14.2.4.2.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert