LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
3 17 3: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0
7 24 7: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 4, 6, 10, 12, 13, 15, 16 using the following ranking functions, which are bounded by −21.

11: 0
10: 0
0: 0
2: 0
3: 0
1: 0
6: 0
7: 0
8: 0
9: 0
4: 0
5: 0
11: −8
10: −9
0: −10
2: −10
3: −10
3_var_snapshot: −10
3*: −10
1: −11
6: −12
7: −12
8: −12
9: −12
7_var_snapshot: −12
7*: −12
4: −13
5: −14

3 Location Addition

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

3* 20 3: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0

4 Location Addition

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

3 18 3_var_snapshot: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0

5 Location Addition

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

7* 27 7: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0

6 Location Addition

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

7 25 7_var_snapshot: x6_post + x6_post ≤ 0x6_postx6_post ≤ 0x6_0 + x6_0 ≤ 0x6_0x6_0 ≤ 0x4_post + x4_post ≤ 0x4_postx4_post ≤ 0x4_0 + x4_0 ≤ 0x4_0x4_0 ≤ 0tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp___0_post + tmp___0_post ≤ 0tmp___0_posttmp___0_post ≤ 0tmp___0_0 + tmp___0_0 ≤ 0tmp___0_0tmp___0_0 ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0ret_foo7_post + ret_foo7_post ≤ 0ret_foo7_postret_foo7_post ≤ 0ret_foo7_0 + ret_foo7_0 ≤ 0ret_foo7_0ret_foo7_0 ≤ 0ret_foo5_post + ret_foo5_post ≤ 0ret_foo5_postret_foo5_post ≤ 0ret_foo5_0 + ret_foo5_0 ≤ 0ret_foo5_0ret_foo5_0 ≤ 0il_post + il_post ≤ 0il_postil_post ≤ 0il_0 + il_0 ≤ 0il_0il_0 ≤ 0___const_10_0 + ___const_10_0 ≤ 0___const_10_0___const_10_0 ≤ 0

7 SCC Decomposition

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

7.1 SCC Subproblem 1/2

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

7.1.1 Transition Removal

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

6: −4 + 7⋅___const_10_0 − 7⋅il_0
7: 2 + 7⋅___const_10_0 − 7⋅il_0
8: −1 + 7⋅___const_10_0 − 7⋅il_0
9: 7⋅___const_10_0 − 7⋅il_0
7_var_snapshot: 1 + 7⋅___const_10_0 − 7⋅il_0
7*: 2 + 7⋅___const_10_0 − 7⋅il_0

7.1.2 Transition Removal

We remove transitions 25, 27, 5, 7, 8, 9 using the following ranking functions, which are bounded by −5.

6: −1
7: −3
8: 0
9: −5
7_var_snapshot: −4
7*: −2

7.1.3 Splitting Cut-Point Transitions

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

7.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 24.

7.1.3.1.1 Splitting Cut-Point Transitions

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

7.2 SCC Subproblem 2/2

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

7.2.1 Transition Removal

We remove transition 14 using the following ranking functions, which are bounded by 4.

0: 1 + 5⋅___const_10_0 − 5⋅il_0
2: 5⋅___const_10_0 − 5⋅il_0
3: 3 + 5⋅___const_10_0 − 5⋅il_0
3_var_snapshot: 2 + 5⋅___const_10_0 − 5⋅il_0
3*: 4 + 5⋅___const_10_0 − 5⋅il_0

7.2.2 Transition Removal

We remove transitions 18, 20, 2, 3 using the following ranking functions, which are bounded by −4.

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

7.2.3 Transition Removal

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

0: tmp_0
2: 0
3: 0
3_var_snapshot: 0
3*: 0

7.2.4 Splitting Cut-Point Transitions

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

7.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 17.

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