LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0
1: i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0
2: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ 50 − i11_0 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ 50 − i13_0 ≤ 0
3: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ 50 − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ 50 − i11_0 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ 50 − i13_0 ≤ 0
4: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ 50 − i11_0 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0 ∧ 50 − i13_0 ≤ 0
5: i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
6: i_post ≤ 0 ∧ − i_post ≤ 0 ∧ i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ i_0 ≤ 0 ∧ − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0
7: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ 50 − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ 50 − i11_0 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
8: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ 50 − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0 ∧ 50 − i11_0 ≤ 0 ∧ i13_1 ≤ 0 ∧ − i13_1 ≤ 0
9: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0
10: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0
11: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ 50 − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
12: i7_1 ≤ 0 ∧ − i7_1 ≤ 0 ∧ 50 − i7_0 ≤ 0 ∧ 50 − i_0 ≤ 0 ∧ i9_1 ≤ 0 ∧ − i9_1 ≤ 0 ∧ 50 − i9_0 ≤ 0 ∧ i11_1 ≤ 0 ∧ − i11_1 ≤ 0
13: TRUE
14: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 20 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0
4 27 4: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0
5 34 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0
8 41 8: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0
9 48 9: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0
12 55 12: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 1, 4, 7, 10, 13, 16, 18, 19 using the following ranking functions, which are bounded by −33.

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

4 Location Addition

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

0* 23 0: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

5 Location Addition

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

0 21 0_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

6 Location Addition

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

4* 30 4: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

7 Location Addition

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

4 28 4_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

8 Location Addition

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

5* 37 5: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

9 Location Addition

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

5 35 5_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

10 Location Addition

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

8* 44 8: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

11 Location Addition

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

8 42 8_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

12 Location Addition

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

9* 51 9: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

13 Location Addition

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

9 49 9_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

14 Location Addition

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

12* 58 12: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

15 Location Addition

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

12 56 12_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp___0_post + tmp___0_post ≤ 0 ∧ tmp___0_post − tmp___0_post ≤ 0 ∧ − tmp___0_0 + tmp___0_0 ≤ 0 ∧ tmp___0_0 − tmp___0_0 ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i9_post + i9_post ≤ 0 ∧ i9_post − i9_post ≤ 0 ∧ − i9_1 + i9_1 ≤ 0 ∧ i9_1 − i9_1 ≤ 0 ∧ − i9_0 + i9_0 ≤ 0 ∧ i9_0 − i9_0 ≤ 0 ∧ − i7_post + i7_post ≤ 0 ∧ i7_post − i7_post ≤ 0 ∧ − i7_1 + i7_1 ≤ 0 ∧ i7_1 − i7_1 ≤ 0 ∧ − i7_0 + i7_0 ≤ 0 ∧ i7_0 − i7_0 ≤ 0 ∧ − i13_post + i13_post ≤ 0 ∧ i13_post − i13_post ≤ 0 ∧ − i13_1 + i13_1 ≤ 0 ∧ i13_1 − i13_1 ≤ 0 ∧ − i13_0 + i13_0 ≤ 0 ∧ i13_0 − i13_0 ≤ 0 ∧ − i11_post + i11_post ≤ 0 ∧ i11_post − i11_post ≤ 0 ∧ − i11_1 + i11_1 ≤ 0 ∧ i11_1 − i11_1 ≤ 0 ∧ − i11_0 + i11_0 ≤ 0 ∧ i11_0 − i11_0 ≤ 0

16 SCC Decomposition

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

16.1 SCC Subproblem 1/6

Here we consider the SCC { 2, 4, 4_var_snapshot, 4* }.

16.1.1 Transition Removal

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

2: −1 − 4⋅i_0
4: 1 − 4⋅i_0
4_var_snapshot: −4⋅i_0
4*: 2 − 4⋅i_0

16.1.2 Transition Removal

We remove transitions 30, 15 using the following ranking functions, which are bounded by −1.

2: − i11_0
4: i13_0
4_var_snapshot: 0
4*: i13_0 + i7_0

16.1.3 Transition Removal

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

2: 0
4: i11_0
4_var_snapshot: 0
4*: 0

16.1.4 Splitting Cut-Point Transitions

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

16.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 27.

16.1.4.1.1 Splitting Cut-Point Transitions

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

16.2 SCC Subproblem 2/6

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

16.2.1 Transition Removal

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

7: −1 − 4⋅i13_0
8: 1 − 4⋅i13_0
8_var_snapshot: −4⋅i13_0
8*: 2 − 4⋅i13_0

16.2.2 Transition Removal

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

7: − i11_0
8: i9_0
8_var_snapshot: 0
8*: i7_0 + i9_0

16.2.3 Transition Removal

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

7: 0
8: i9_0
8_var_snapshot: 0
8*: 0

16.2.4 Splitting Cut-Point Transitions

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

16.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 41.

16.2.4.1.1 Splitting Cut-Point Transitions

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

16.3 SCC Subproblem 3/6

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

16.3.1 Transition Removal

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

11: −1 − 4⋅i11_0
12: 1 − 4⋅i11_0
12_var_snapshot: −4⋅i11_0
12*: 2 − 4⋅i11_0

16.3.2 Transition Removal

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

11: −1
12: i_0
12_var_snapshot: 0
12*: 1 + i_0

16.3.3 Splitting Cut-Point Transitions

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

16.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 55.

16.3.3.1.1 Splitting Cut-Point Transitions

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

16.4 SCC Subproblem 4/6

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

16.4.1 Transition Removal

We remove transition 11 using the following ranking functions, which are bounded by −200.

9: −1 − 4⋅i_0
10: −3 − 4⋅i_0
9_var_snapshot: −2 − 4⋅i_0
9*: −4⋅i_0

16.4.2 Transition Removal

We remove transitions 49, 6 using the following ranking functions, which are bounded by −1.

9: i7_0
10: − i7_0
9_var_snapshot: 0
9*: 2⋅i7_0

16.4.3 Transition Removal

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

9: −1
10: 0
9_var_snapshot: 0
9*: 0

16.4.4 Splitting Cut-Point Transitions

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

16.4.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 48.

16.4.4.1.1 Splitting Cut-Point Transitions

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

16.5 SCC Subproblem 5/6

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

16.5.1 Transition Removal

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

5: 2 − 4⋅i9_0
6: −4⋅i9_0
5_var_snapshot: 1 − 4⋅i9_0
5*: 3 − 4⋅i9_0

16.5.2 Transition Removal

We remove transitions 35, 37, 3 using the following ranking functions, which are bounded by −1.

5: i7_0
6: −1
5_var_snapshot: 0
5*: 2⋅i7_0

16.5.3 Splitting Cut-Point Transitions

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

16.5.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 34.

16.5.3.1.1 Splitting Cut-Point Transitions

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

16.6 SCC Subproblem 6/6

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

16.6.1 Transition Removal

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

0: 2 − 4⋅i7_0
1: −4⋅i7_0
0_var_snapshot: 1 − 4⋅i7_0
0*: 3 − 4⋅i7_0

16.6.2 Transition Removal

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

0: 0
1: −2
0_var_snapshot: −1
0*: 1

16.6.3 Transition Removal

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

0: 0
1: 0
0_var_snapshot: 0
0*: 1

16.6.4 Splitting Cut-Point Transitions

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

16.6.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 20.

16.6.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert