LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

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

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
7 20 7: x98 + x98 ≤ 0x98x98 ≤ 0x93 + x93 ≤ 0x93x93 ≤ 0x66 + x66 ≤ 0x66x66 ≤ 0x59 + x59 ≤ 0x59x59 ≤ 0x52 + x52 ≤ 0x52x52 ≤ 0x45 + x45 ≤ 0x45x45 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x25 + x25 ≤ 0x25x25 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0
9 27 9: x98 + x98 ≤ 0x98x98 ≤ 0x93 + x93 ≤ 0x93x93 ≤ 0x66 + x66 ≤ 0x66x66 ≤ 0x59 + x59 ≤ 0x59x59 ≤ 0x52 + x52 ≤ 0x52x52 ≤ 0x45 + x45 ≤ 0x45x45 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x25 + x25 ≤ 0x25x25 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 3, 5, 6, 7, 13, 14, 15, 16, 19 using the following ranking functions, which are bounded by −23.

10: 0
0: 0
1: 0
9: 0
4: 0
6: 0
7: 0
8: 0
10: −9
0: −10
1: −11
9: −12
9_var_snapshot: −12
9*: −12
4: −15
6: −16
7: −17
7_var_snapshot: −17
7*: −17
8: −21

4 Location Addition

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

7* 23 7: x98 + x98 ≤ 0x98x98 ≤ 0x93 + x93 ≤ 0x93x93 ≤ 0x66 + x66 ≤ 0x66x66 ≤ 0x59 + x59 ≤ 0x59x59 ≤ 0x52 + x52 ≤ 0x52x52 ≤ 0x45 + x45 ≤ 0x45x45 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x25 + x25 ≤ 0x25x25 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

5 Location Addition

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

7 21 7_var_snapshot: x98 + x98 ≤ 0x98x98 ≤ 0x93 + x93 ≤ 0x93x93 ≤ 0x66 + x66 ≤ 0x66x66 ≤ 0x59 + x59 ≤ 0x59x59 ≤ 0x52 + x52 ≤ 0x52x52 ≤ 0x45 + x45 ≤ 0x45x45 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x25 + x25 ≤ 0x25x25 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

6 Location Addition

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

9* 30 9: x98 + x98 ≤ 0x98x98 ≤ 0x93 + x93 ≤ 0x93x93 ≤ 0x66 + x66 ≤ 0x66x66 ≤ 0x59 + x59 ≤ 0x59x59 ≤ 0x52 + x52 ≤ 0x52x52 ≤ 0x45 + x45 ≤ 0x45x45 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x25 + x25 ≤ 0x25x25 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

7 Location Addition

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

9 28 9_var_snapshot: x98 + x98 ≤ 0x98x98 ≤ 0x93 + x93 ≤ 0x93x93 ≤ 0x66 + x66 ≤ 0x66x66 ≤ 0x59 + x59 ≤ 0x59x59 ≤ 0x52 + x52 ≤ 0x52x52 ≤ 0x45 + x45 ≤ 0x45x45 ≤ 0x30 + x30 ≤ 0x30x30 ≤ 0x25 + x25 ≤ 0x25x25 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 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 { 9, 9_var_snapshot, 9* }.

8.1.1 Transition Removal

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

9: 1 + 3⋅arg1
9_var_snapshot: 3⋅arg1
9*: 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 27.

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 8, 9, 10, 11, 12 using the following ranking functions, which are bounded by 2.

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

8.2.2 Transition Removal

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

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

8.2.3 Transition Removal

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

7: 0
7_var_snapshot: 0
7*: 1

8.2.4 Splitting Cut-Point Transitions

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

8.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 20.

8.2.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert