LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: 100 − i_0 ≤ 0
2: TRUE
3: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
4: 100 − i_0 ≤ 0
5: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
6: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
7: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
8: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
9: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
10: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
11: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
12: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
13: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
14: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
15: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
16: 100 − i_0 ≤ 0 ∧ 1 + i_0 ≤ 0
17: TRUE
18: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
2 28 2: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
6 35 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
10 42 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 2, 9, 12, 13, 14, 15, 22, 24, 25, 26, 27 using the following ranking functions, which are bounded by −29.

18: 0
17: 0
0: 0
2: 0
1: 0
10: 0
11: 0
14: 0
15: 0
16: 0
13: 0
12: 0
5: 0
6: 0
7: 0
8: 0
9: 0
3: 0
4: 0
18: −11
17: −12
0: −13
2: −13
2_var_snapshot: −13
2*: −13
1: −14
10: −15
11: −15
14: −15
15: −15
16: −15
10_var_snapshot: −15
10*: −15
13: −16
12: −17
5: −18
6: −18
7: −18
8: −18
9: −18
6_var_snapshot: −18
6*: −18
3: −19
4: −24

4 Location Addition

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

2* 31 2: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

5 Location Addition

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

2 29 2_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

6 Location Addition

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

6* 38 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

7 Location Addition

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

6 36 6_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

8 Location Addition

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

10* 45 10: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

9 Location Addition

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

10 43 10_var_snapshot: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − ret_check8_post + ret_check8_post ≤ 0 ∧ ret_check8_post − ret_check8_post ≤ 0 ∧ − ret_check8_0 + ret_check8_0 ≤ 0 ∧ ret_check8_0 − ret_check8_0 ≤ 0 ∧ − ret_check12_post + ret_check12_post ≤ 0 ∧ ret_check12_post − ret_check12_post ≤ 0 ∧ − ret_check12_0 + ret_check12_0 ≤ 0 ∧ ret_check12_0 − ret_check12_0 ≤ 0 ∧ − j_post + j_post ≤ 0 ∧ j_post − j_post ≤ 0 ∧ − j_0 + j_0 ≤ 0 ∧ j_0 − j_0 ≤ 0 ∧ − j6_post + j6_post ≤ 0 ∧ j6_post − j6_post ≤ 0 ∧ − j6_0 + j6_0 ≤ 0 ∧ j6_0 − j6_0 ≤ 0 ∧ − j10_post + j10_post ≤ 0 ∧ j10_post − j10_post ≤ 0 ∧ − j10_0 + j10_0 ≤ 0 ∧ j10_0 − j10_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0

10 SCC Decomposition

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

10.1 SCC Subproblem 1/3

Here we consider the SCC { 5, 6, 7, 8, 9, 6_var_snapshot, 6* }.

10.1.1 Transition Removal

We remove transitions 36, 38, 4, 5, 6, 7, 8, 10, 18 using the following ranking functions, which are bounded by −102.

5: −101
6: 0
7: 101⋅i_0
8: 0
9: 101
6_var_snapshot: 0
6*: 101

10.1.2 Splitting Cut-Point Transitions

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

10.1.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 35.

10.1.2.1.1 Splitting Cut-Point Transitions

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

10.2 SCC Subproblem 2/3

Here we consider the SCC { 10, 11, 14, 15, 16, 10_var_snapshot, 10* }.

10.2.1 Transition Removal

We remove transitions 43, 45, 11, 16, 17, 19, 20, 21, 23 using the following ranking functions, which are bounded by −1.

10: i_0
11: 0
14: − i_0
15: 0
16: 100
10_var_snapshot: 99
10*: −1 − i_0

10.2.2 Splitting Cut-Point Transitions

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

10.2.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 42.

10.2.2.1.1 Splitting Cut-Point Transitions

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

10.3 SCC Subproblem 3/3

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

10.3.1 Transition Removal

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

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

10.3.2 Transition Removal

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

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

10.3.3 Transition Removal

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

0: 0
2: 1
2_var_snapshot: 0
2*: 0

10.3.4 Splitting Cut-Point Transitions

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

10.3.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 28.

10.3.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert