LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
10 41 10: − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_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, 8, 9, 10, 11, 12, 13, 19, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40 using the following ranking functions, which are bounded by −31.

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

3 Location Addition

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

10* 44 10: − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

4 Location Addition

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

10 42 10_var_snapshot: − x2_post + x2_post ≤ 0 ∧ x2_post − x2_post ≤ 0 ∧ − x2_0 + x2_0 ≤ 0 ∧ x2_0 − x2_0 ≤ 0 ∧ − x1_post + x1_post ≤ 0 ∧ x1_post − x1_post ≤ 0 ∧ − x1_0 + x1_0 ≤ 0 ∧ x1_0 − x1_0 ≤ 0 ∧ − x0_post + x0_post ≤ 0 ∧ x0_post − x0_post ≤ 0 ∧ − x0_0 + x0_0 ≤ 0 ∧ x0_0 − x0_0 ≤ 0 ∧ − oldX6_post + oldX6_post ≤ 0 ∧ oldX6_post − oldX6_post ≤ 0 ∧ − oldX6_0 + oldX6_0 ≤ 0 ∧ oldX6_0 − oldX6_0 ≤ 0 ∧ − oldX5_post + oldX5_post ≤ 0 ∧ oldX5_post − oldX5_post ≤ 0 ∧ − oldX5_0 + oldX5_0 ≤ 0 ∧ oldX5_0 − oldX5_0 ≤ 0 ∧ − oldX4_post + oldX4_post ≤ 0 ∧ oldX4_post − oldX4_post ≤ 0 ∧ − oldX4_0 + oldX4_0 ≤ 0 ∧ oldX4_0 − oldX4_0 ≤ 0 ∧ − oldX3_post + oldX3_post ≤ 0 ∧ oldX3_post − oldX3_post ≤ 0 ∧ − oldX3_0 + oldX3_0 ≤ 0 ∧ oldX3_0 − oldX3_0 ≤ 0 ∧ − oldX2_post + oldX2_post ≤ 0 ∧ oldX2_post − oldX2_post ≤ 0 ∧ − oldX2_0 + oldX2_0 ≤ 0 ∧ oldX2_0 − oldX2_0 ≤ 0 ∧ − oldX1_post + oldX1_post ≤ 0 ∧ oldX1_post − oldX1_post ≤ 0 ∧ − oldX1_0 + oldX1_0 ≤ 0 ∧ oldX1_0 − oldX1_0 ≤ 0 ∧ − oldX0_post + oldX0_post ≤ 0 ∧ oldX0_post − oldX0_post ≤ 0 ∧ − oldX0_0 + oldX0_0 ≤ 0 ∧ oldX0_0 − oldX0_0 ≤ 0

5 SCC Decomposition

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

5.1 SCC Subproblem 1/1

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

5.1.1 Transition Removal

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

9: −1 + 5⋅x2_0
10: −3 + 10⋅x2_0
11: 5⋅x2_0
12: 5⋅x2_0
10_var_snapshot: −4 + 10⋅x2_0
10*: −2 + 10⋅x2_0

5.1.2 Transition Removal

We remove transitions 42, 44, 14, 15, 16, 17, 18 using the following ranking functions, which are bounded by −5.

9: −2
10: −4
11: −1
12: 0
10_var_snapshot: −5
10*: −3

5.1.3 Splitting Cut-Point Transitions

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

5.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 41.

5.1.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert