LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
3 28 3: − 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 ∧ − 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 35 5: − 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 ∧ − 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
10 42 10: − 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 ∧ − 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, 2, 5, 7, 8, 10, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 using the following ranking functions, which are bounded by −31.

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

3 Location Addition

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

3* 31 3: − 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 ∧ − 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.

3 29 3_var_snapshot: − 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 ∧ − 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 Location Addition

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

5* 38 5: − 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 ∧ − 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

6 Location Addition

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

5 36 5_var_snapshot: − 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 ∧ − 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

7 Location Addition

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

10* 45 10: − 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 ∧ − 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

8 Location Addition

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

10 43 10_var_snapshot: − 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 ∧ − 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

9 SCC Decomposition

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

9.1 SCC Subproblem 1/3

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

9.1.1 Transition Removal

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

2: −1 + 4⋅x1_0
3: 1 + 4⋅x1_0
3_var_snapshot: 4⋅x1_0
3*: 2 + 4⋅x1_0

9.1.2 Transition Removal

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

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

9.1.3 Transition Removal

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

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

9.1.4 Splitting Cut-Point Transitions

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

9.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 28.

9.1.4.1.1 Splitting Cut-Point Transitions

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

9.2 SCC Subproblem 2/3

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

9.2.1 Transition Removal

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

4: −1 + 4⋅x0_0
5: 1 + 4⋅x0_0
5_var_snapshot: 4⋅x0_0
5*: 2 + 4⋅x0_0

9.2.2 Transition Removal

We remove transitions 36, 38, 4 using the following ranking functions, which are bounded by −1.

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

9.2.3 Splitting Cut-Point Transitions

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

9.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 35.

9.2.3.1.1 Splitting Cut-Point Transitions

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

9.3 SCC Subproblem 3/3

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

9.3.1 Transition Removal

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

9: −1 − 4⋅x0_0
10: 1 − 4⋅x0_0
10_var_snapshot: −4⋅x0_0
10*: 2 − 4⋅x0_0

9.3.2 Transition Removal

We remove transitions 43, 45, 9 using the following ranking functions, which are bounded by −2.

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

9.3.3 Splitting Cut-Point Transitions

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

9.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 42.

9.3.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert