LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: 1 − arg1P ≤ 0 ∧ 8 − arg2P ≤ 0 ∧ 6 − arg3P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 8 − arg2 ≤ 0 ∧ 6 − arg3 ≤ 0
2: 1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0
3: 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0
4: 1 − arg2P ≤ 0 ∧ 1 − arg2 ≤ 0
5: − arg1P ≤ 0 ∧ − arg1 ≤ 0
6: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
4 20 4: − x97 + x97 ≤ 0 ∧ x97 − x97 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x94 + x94 ≤ 0 ∧ x94 − x94 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x84 + x84 ≤ 0 ∧ x84 − x84 ≤ 0 ∧ − x83 + x83 ≤ 0 ∧ x83 − x83 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x66 + x66 ≤ 0 ∧ x66 − x66 ≤ 0 ∧ − x61 + x61 ≤ 0 ∧ x61 − x61 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x53 + x53 ≤ 0 ∧ x53 − x53 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x46 + x46 ≤ 0 ∧ x46 − x46 ≤ 0 ∧ − x45 + x45 ≤ 0 ∧ x45 − x45 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x43 + x43 ≤ 0 ∧ x43 − x43 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x35 + x35 ≤ 0 ∧ x35 − x35 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x33 + x33 ≤ 0 ∧ x33 − x33 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x28 + x28 ≤ 0 ∧ x28 − x28 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x13 + x13 ≤ 0 ∧ x13 − x13 ≤ 0 ∧ − x12 + x12 ≤ 0 ∧ x12 − x12 ≤ 0 ∧ − x114 + x114 ≤ 0 ∧ x114 − x114 ≤ 0 ∧ − x110 + x110 ≤ 0 ∧ x110 − x110 ≤ 0 ∧ − x106 + x106 ≤ 0 ∧ x106 − x106 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − 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 27 5: − x97 + x97 ≤ 0 ∧ x97 − x97 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x94 + x94 ≤ 0 ∧ x94 − x94 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x84 + x84 ≤ 0 ∧ x84 − x84 ≤ 0 ∧ − x83 + x83 ≤ 0 ∧ x83 − x83 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x66 + x66 ≤ 0 ∧ x66 − x66 ≤ 0 ∧ − x61 + x61 ≤ 0 ∧ x61 − x61 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x53 + x53 ≤ 0 ∧ x53 − x53 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x46 + x46 ≤ 0 ∧ x46 − x46 ≤ 0 ∧ − x45 + x45 ≤ 0 ∧ x45 − x45 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x43 + x43 ≤ 0 ∧ x43 − x43 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x35 + x35 ≤ 0 ∧ x35 − x35 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x33 + x33 ≤ 0 ∧ x33 − x33 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x28 + x28 ≤ 0 ∧ x28 − x28 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x13 + x13 ≤ 0 ∧ x13 − x13 ≤ 0 ∧ − x12 + x12 ≤ 0 ∧ x12 − x12 ≤ 0 ∧ − x114 + x114 ≤ 0 ∧ x114 − x114 ≤ 0 ∧ − x110 + x110 ≤ 0 ∧ x110 − x110 ≤ 0 ∧ − x106 + x106 ≤ 0 ∧ x106 − x106 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − 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, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 19 using the following ranking functions, which are bounded by −21.

6: 0
0: 0
1: 0
2: 0
3: 0
5: 0
4: 0
6: −8
0: −9
1: −10
2: −11
3: −12
5: −13
5_var_snapshot: −13
5*: −13
4: −16
4_var_snapshot: −16
4*: −16

4 Location Addition

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

4* 23 4: − x97 + x97 ≤ 0 ∧ x97 − x97 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x94 + x94 ≤ 0 ∧ x94 − x94 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x84 + x84 ≤ 0 ∧ x84 − x84 ≤ 0 ∧ − x83 + x83 ≤ 0 ∧ x83 − x83 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x66 + x66 ≤ 0 ∧ x66 − x66 ≤ 0 ∧ − x61 + x61 ≤ 0 ∧ x61 − x61 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x53 + x53 ≤ 0 ∧ x53 − x53 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x46 + x46 ≤ 0 ∧ x46 − x46 ≤ 0 ∧ − x45 + x45 ≤ 0 ∧ x45 − x45 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x43 + x43 ≤ 0 ∧ x43 − x43 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x35 + x35 ≤ 0 ∧ x35 − x35 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x33 + x33 ≤ 0 ∧ x33 − x33 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x28 + x28 ≤ 0 ∧ x28 − x28 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x13 + x13 ≤ 0 ∧ x13 − x13 ≤ 0 ∧ − x12 + x12 ≤ 0 ∧ x12 − x12 ≤ 0 ∧ − x114 + x114 ≤ 0 ∧ x114 − x114 ≤ 0 ∧ − x110 + x110 ≤ 0 ∧ x110 − x110 ≤ 0 ∧ − x106 + x106 ≤ 0 ∧ x106 − x106 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − 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.

4 21 4_var_snapshot: − x97 + x97 ≤ 0 ∧ x97 − x97 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x94 + x94 ≤ 0 ∧ x94 − x94 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x84 + x84 ≤ 0 ∧ x84 − x84 ≤ 0 ∧ − x83 + x83 ≤ 0 ∧ x83 − x83 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x66 + x66 ≤ 0 ∧ x66 − x66 ≤ 0 ∧ − x61 + x61 ≤ 0 ∧ x61 − x61 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x53 + x53 ≤ 0 ∧ x53 − x53 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x46 + x46 ≤ 0 ∧ x46 − x46 ≤ 0 ∧ − x45 + x45 ≤ 0 ∧ x45 − x45 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x43 + x43 ≤ 0 ∧ x43 − x43 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x35 + x35 ≤ 0 ∧ x35 − x35 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x33 + x33 ≤ 0 ∧ x33 − x33 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x28 + x28 ≤ 0 ∧ x28 − x28 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x13 + x13 ≤ 0 ∧ x13 − x13 ≤ 0 ∧ − x12 + x12 ≤ 0 ∧ x12 − x12 ≤ 0 ∧ − x114 + x114 ≤ 0 ∧ x114 − x114 ≤ 0 ∧ − x110 + x110 ≤ 0 ∧ x110 − x110 ≤ 0 ∧ − x106 + x106 ≤ 0 ∧ x106 − x106 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − 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.

5* 30 5: − x97 + x97 ≤ 0 ∧ x97 − x97 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x94 + x94 ≤ 0 ∧ x94 − x94 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x84 + x84 ≤ 0 ∧ x84 − x84 ≤ 0 ∧ − x83 + x83 ≤ 0 ∧ x83 − x83 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x66 + x66 ≤ 0 ∧ x66 − x66 ≤ 0 ∧ − x61 + x61 ≤ 0 ∧ x61 − x61 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x53 + x53 ≤ 0 ∧ x53 − x53 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x46 + x46 ≤ 0 ∧ x46 − x46 ≤ 0 ∧ − x45 + x45 ≤ 0 ∧ x45 − x45 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x43 + x43 ≤ 0 ∧ x43 − x43 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x35 + x35 ≤ 0 ∧ x35 − x35 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x33 + x33 ≤ 0 ∧ x33 − x33 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x28 + x28 ≤ 0 ∧ x28 − x28 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x13 + x13 ≤ 0 ∧ x13 − x13 ≤ 0 ∧ − x12 + x12 ≤ 0 ∧ x12 − x12 ≤ 0 ∧ − x114 + x114 ≤ 0 ∧ x114 − x114 ≤ 0 ∧ − x110 + x110 ≤ 0 ∧ x110 − x110 ≤ 0 ∧ − x106 + x106 ≤ 0 ∧ x106 − x106 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − 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.

5 28 5_var_snapshot: − x97 + x97 ≤ 0 ∧ x97 − x97 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x94 + x94 ≤ 0 ∧ x94 − x94 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x84 + x84 ≤ 0 ∧ x84 − x84 ≤ 0 ∧ − x83 + x83 ≤ 0 ∧ x83 − x83 ≤ 0 ∧ − x78 + x78 ≤ 0 ∧ x78 − x78 ≤ 0 ∧ − x77 + x77 ≤ 0 ∧ x77 − x77 ≤ 0 ∧ − x76 + x76 ≤ 0 ∧ x76 − x76 ≤ 0 ∧ − x75 + x75 ≤ 0 ∧ x75 − x75 ≤ 0 ∧ − x68 + x68 ≤ 0 ∧ x68 − x68 ≤ 0 ∧ − x67 + x67 ≤ 0 ∧ x67 − x67 ≤ 0 ∧ − x66 + x66 ≤ 0 ∧ x66 − x66 ≤ 0 ∧ − x61 + x61 ≤ 0 ∧ x61 − x61 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x53 + x53 ≤ 0 ∧ x53 − x53 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x46 + x46 ≤ 0 ∧ x46 − x46 ≤ 0 ∧ − x45 + x45 ≤ 0 ∧ x45 − x45 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x43 + x43 ≤ 0 ∧ x43 − x43 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x35 + x35 ≤ 0 ∧ x35 − x35 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x33 + x33 ≤ 0 ∧ x33 − x33 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x28 + x28 ≤ 0 ∧ x28 − x28 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x13 + x13 ≤ 0 ∧ x13 − x13 ≤ 0 ∧ − x12 + x12 ≤ 0 ∧ x12 − x12 ≤ 0 ∧ − x114 + x114 ≤ 0 ∧ x114 − x114 ≤ 0 ∧ − x110 + x110 ≤ 0 ∧ x110 − x110 ≤ 0 ∧ − x106 + x106 ≤ 0 ∧ x106 − x106 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − 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 SCC Decomposition

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

8.1 SCC Subproblem 1/2

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

8.1.1 Transition Removal

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

5: −2 + 3⋅arg1
5_var_snapshot: −4 + 3⋅arg1
5*: 3⋅arg1

8.1.2 Transition Removal

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

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

8.1.3 Splitting Cut-Point Transitions

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

8.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 27.

8.1.3.1.1 Splitting Cut-Point Transitions

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

8.2 SCC Subproblem 2/2

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

8.2.1 Transition Removal

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

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

8.2.2 Transition Removal

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

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

8.2.3 Splitting Cut-Point Transitions

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

8.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 20.

8.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