LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: − arg1P ≤ 0 ∧ − arg1 ≤ 0
4: 1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0
6: 1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0
7: TRUE
8: 1 − arg2P ≤ 0 ∧ 1 − arg2 ≤ 0
9: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
1 18 1: − x63 + x63 ≤ 0 ∧ x63 − x63 ≤ 0 ∧ − x56 + x56 ≤ 0 ∧ x56 − x56 ≤ 0 ∧ − x49 + x49 ≤ 0 ∧ x49 − x49 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x22 + x22 ≤ 0 ∧ x22 − x22 ≤ 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 25 7: − x63 + x63 ≤ 0 ∧ x63 − x63 ≤ 0 ∧ − x56 + x56 ≤ 0 ∧ x56 − x56 ≤ 0 ∧ − x49 + x49 ≤ 0 ∧ x49 − x49 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x22 + x22 ≤ 0 ∧ x22 − x22 ≤ 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, 4, 6, 7, 8, 14, 15, 16, 17 using the following ranking functions, which are bounded by −21.

9: 0
0: 0
1: 0
4: 0
6: 0
7: 0
8: 0
9: −8
0: −9
1: −10
1_var_snapshot: −10
1*: −10
4: −13
6: −14
7: −15
7_var_snapshot: −15
7*: −15
8: −19

4 Location Addition

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

1* 21 1: − x63 + x63 ≤ 0 ∧ x63 − x63 ≤ 0 ∧ − x56 + x56 ≤ 0 ∧ x56 − x56 ≤ 0 ∧ − x49 + x49 ≤ 0 ∧ x49 − x49 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x22 + x22 ≤ 0 ∧ x22 − x22 ≤ 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.

1 19 1_var_snapshot: − x63 + x63 ≤ 0 ∧ x63 − x63 ≤ 0 ∧ − x56 + x56 ≤ 0 ∧ x56 − x56 ≤ 0 ∧ − x49 + x49 ≤ 0 ∧ x49 − x49 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x22 + x22 ≤ 0 ∧ x22 − x22 ≤ 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.

7* 28 7: − x63 + x63 ≤ 0 ∧ x63 − x63 ≤ 0 ∧ − x56 + x56 ≤ 0 ∧ x56 − x56 ≤ 0 ∧ − x49 + x49 ≤ 0 ∧ x49 − x49 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x22 + x22 ≤ 0 ∧ x22 − x22 ≤ 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.

7 26 7_var_snapshot: − x63 + x63 ≤ 0 ∧ x63 − x63 ≤ 0 ∧ − x56 + x56 ≤ 0 ∧ x56 − x56 ≤ 0 ∧ − x49 + x49 ≤ 0 ∧ x49 − x49 ≤ 0 ∧ − x42 + x42 ≤ 0 ∧ x42 − x42 ≤ 0 ∧ − x27 + x27 ≤ 0 ∧ x27 − x27 ≤ 0 ∧ − x22 + x22 ≤ 0 ∧ x22 − x22 ≤ 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 { 1, 1_var_snapshot, 1* }.

8.1.1 Transition Removal

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

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

8.1.2 Splitting Cut-Point Transitions

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

8.1.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 18.

8.1.2.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 { 7, 7_var_snapshot, 7* }.

8.2.1 Transition Removal

We remove transitions 9, 10, 11, 12, 13 using the following ranking functions, which are bounded by 3.

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

8.2.2 Transition Removal

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

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

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

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