LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: TRUE
2: TRUE
3: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
4: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
5: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
6: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
7: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
8: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
9: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
10: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
11: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
12: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
13: −99 + arg1P ≤ 0 ∧ −99 + arg1 ≤ 0
14: TRUE
15: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
1 29 1: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2 36 2: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
3 43 3: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
4 50 4: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
5 57 5: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
6 64 6: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
7 71 7: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
8 78 8: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
9 85 9: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
10 92 10: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
11 99 11: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
12 106 12: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
13 113 13: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
14 120 14: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28 using the following ranking functions, which are bounded by −61.

15: 0
0: 0
1: 0
2: 0
3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: −16
0: −17
1: −18
2: −18
1_var_snapshot: −18
1*: −18
2_var_snapshot: −18
2*: −18
3: −21
3_var_snapshot: −21
3*: −21
4: −24
4_var_snapshot: −24
4*: −24
5: −27
5_var_snapshot: −27
5*: −27
6: −30
6_var_snapshot: −30
6*: −30
7: −33
7_var_snapshot: −33
7*: −33
8: −36
8_var_snapshot: −36
8*: −36
9: −39
9_var_snapshot: −39
9*: −39
10: −42
10_var_snapshot: −42
10*: −42
11: −45
11_var_snapshot: −45
11*: −45
12: −48
12_var_snapshot: −48
12*: −48
13: −51
13_var_snapshot: −51
13*: −51
14: −54
14_var_snapshot: −54
14*: −54

4 Location Addition

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

1* 32 1: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

5 Location Addition

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

1 30 1_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

6 Location Addition

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

2* 39 2: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

7 Location Addition

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

2 37 2_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

8 Location Addition

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

3* 46 3: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

9 Location Addition

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

3 44 3_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

10 Location Addition

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

4* 53 4: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

11 Location Addition

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

4 51 4_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

12 Location Addition

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

5* 60 5: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

13 Location Addition

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

5 58 5_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

14 Location Addition

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

6* 67 6: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

15 Location Addition

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

6 65 6_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

16 Location Addition

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

7* 74 7: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

17 Location Addition

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

7 72 7_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

18 Location Addition

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

8* 81 8: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

19 Location Addition

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

8 79 8_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

20 Location Addition

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

9* 88 9: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

21 Location Addition

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

9 86 9_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

22 Location Addition

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

10* 95 10: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

23 Location Addition

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

10 93 10_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

24 Location Addition

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

11* 102 11: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

25 Location Addition

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

11 100 11_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

26 Location Addition

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

12* 109 12: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

27 Location Addition

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

12 107 12_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

28 Location Addition

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

13* 116 13: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

29 Location Addition

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

13 114 13_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

30 Location Addition

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

14* 123 14: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

31 Location Addition

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

14 121 14_var_snapshot: − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

32 SCC Decomposition

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

32.1 SCC Subproblem 1/13

Here we consider the SCC { 14, 14_var_snapshot, 14* }.

32.1.1 Transition Removal

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

14: 1 + 3⋅arg1
14_var_snapshot: 3⋅arg1
14*: 2 + 3⋅arg1

32.1.2 Transition Removal

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

14: 0
14_var_snapshot: −1
14*: 1

32.1.3 Transition Removal

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

14: 0
14_var_snapshot: 0
14*: 1

32.1.4 Splitting Cut-Point Transitions

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

32.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 120.

32.1.4.1.1 Splitting Cut-Point Transitions

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

32.2 SCC Subproblem 2/13

Here we consider the SCC { 13, 13_var_snapshot, 13* }.

32.2.1 Transition Removal

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

13: −1 + 2⋅arg2 + arg3
13_var_snapshot: −2 + 2⋅arg2 + arg3
13*: 2⋅arg2 + arg3

32.2.2 Transition Removal

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

13: 0
13_var_snapshot: −1
13*: 1

32.2.3 Splitting Cut-Point Transitions

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

32.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 113.

32.2.3.1.1 Splitting Cut-Point Transitions

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

32.3 SCC Subproblem 3/13

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

32.3.1 Transition Removal

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

12: −1 + 2⋅arg2 + arg3
12_var_snapshot: −2 + 2⋅arg2 + arg3
12*: 2⋅arg2 + arg3

32.3.2 Transition Removal

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

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

32.3.3 Splitting Cut-Point Transitions

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

32.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 106.

32.3.3.1.1 Splitting Cut-Point Transitions

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

32.4 SCC Subproblem 4/13

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

32.4.1 Transition Removal

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

11: −1 + 2⋅arg2 + arg3
11_var_snapshot: −2 + 2⋅arg2 + arg3
11*: 2⋅arg2 + arg3

32.4.2 Transition Removal

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

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

32.4.3 Splitting Cut-Point Transitions

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

32.4.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 99.

32.4.3.1.1 Splitting Cut-Point Transitions

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

32.5 SCC Subproblem 5/13

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

32.5.1 Transition Removal

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

10: −1 + 2⋅arg2 + arg3
10_var_snapshot: −2 + 2⋅arg2 + arg3
10*: 2⋅arg2 + arg3

32.5.2 Transition Removal

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

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

32.5.3 Splitting Cut-Point Transitions

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

32.5.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 92.

32.5.3.1.1 Splitting Cut-Point Transitions

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

32.6 SCC Subproblem 6/13

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

32.6.1 Transition Removal

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

9: −1 + 2⋅arg2 + arg3
9_var_snapshot: −2 + 2⋅arg2 + arg3
9*: 2⋅arg2 + arg3

32.6.2 Transition Removal

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

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

32.6.3 Splitting Cut-Point Transitions

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

32.6.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 85.

32.6.3.1.1 Splitting Cut-Point Transitions

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

32.7 SCC Subproblem 7/13

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

32.7.1 Transition Removal

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

8: −1 + 2⋅arg2 + arg3
8_var_snapshot: −2 + 2⋅arg2 + arg3
8*: 2⋅arg2 + arg3

32.7.2 Transition Removal

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

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

32.7.3 Splitting Cut-Point Transitions

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

32.7.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 78.

32.7.3.1.1 Splitting Cut-Point Transitions

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

32.8 SCC Subproblem 8/13

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

32.8.1 Transition Removal

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

7: 1 + 2⋅arg2 + arg3
7_var_snapshot: 2⋅arg2 + arg3
7*: 2 + 2⋅arg2 + arg3

32.8.2 Transition Removal

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

7: 0
7_var_snapshot: −1
7*: 1

32.8.3 Splitting Cut-Point Transitions

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

32.8.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 71.

32.8.3.1.1 Splitting Cut-Point Transitions

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

32.9 SCC Subproblem 9/13

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

32.9.1 Transition Removal

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

6: 1 + 2⋅arg2 + arg3
6_var_snapshot: 2⋅arg2 + arg3
6*: 2 + 2⋅arg2 + arg3

32.9.2 Transition Removal

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

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

32.9.3 Splitting Cut-Point Transitions

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

32.9.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 64.

32.9.3.1.1 Splitting Cut-Point Transitions

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

32.10 SCC Subproblem 10/13

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

32.10.1 Transition Removal

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

5: 1 + 2⋅arg2 + arg3
5_var_snapshot: 2⋅arg2 + arg3
5*: 2 + 2⋅arg2 + arg3

32.10.2 Transition Removal

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

5: 0
5_var_snapshot: −1
5*: 1

32.10.3 Splitting Cut-Point Transitions

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

32.10.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 57.

32.10.3.1.1 Splitting Cut-Point Transitions

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

32.11 SCC Subproblem 11/13

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

32.11.1 Transition Removal

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

4: 1 + 2⋅arg2 + arg3
4_var_snapshot: 2⋅arg2 + arg3
4*: 2 + 2⋅arg2 + arg3

32.11.2 Transition Removal

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

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

32.11.3 Splitting Cut-Point Transitions

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

32.11.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 50.

32.11.3.1.1 Splitting Cut-Point Transitions

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

32.12 SCC Subproblem 12/13

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

32.12.1 Transition Removal

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

3: 1 + 2⋅arg2 + arg3
3_var_snapshot: 2⋅arg2 + arg3
3*: 2 + 2⋅arg2 + arg3

32.12.2 Transition Removal

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

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

32.12.3 Splitting Cut-Point Transitions

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

32.12.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 43.

32.12.3.1.1 Splitting Cut-Point Transitions

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

32.13 SCC Subproblem 13/13

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

32.13.1 Transition Removal

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

1: 1 + 3⋅arg1
2: 3⋅arg1
1_var_snapshot: 3⋅arg1
1*: 2 + 3⋅arg1
2_var_snapshot: 3⋅arg1
2*: 3⋅arg1

32.13.2 Transition Removal

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

1: 3 − 3⋅arg1
2: 1 − arg2 − 2⋅arg3
1_var_snapshot: 3 − 3⋅arg1
1*: 4 − 3⋅arg1
2_var_snapshot: − arg2 − 2⋅arg3
2*: 2 − arg2 − 2⋅arg3

32.13.3 Transition Removal

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

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

32.13.4 Transition Removal

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

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

32.13.5 Splitting Cut-Point Transitions

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

32.13.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 29.

32.13.5.1.1 Splitting Cut-Point Transitions

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

32.13.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 36.

32.13.5.2.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert