LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
1: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0
2: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
3: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
4: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
5: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
6: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
7: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
8: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
9: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
10: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0 ∧ Sorted5_0 ≤ 0 ∧ − Sorted5_0 ≤ 0
11: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
12: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
13: 1 + fact3_post ≤ 0 ∧ 1 + factor_post ≤ 0 ∧ −1 − factor_post ≤ 0 ∧ 101 − Index2_0 ≤ 0 ∧ 1 + fact3_0 ≤ 0 ∧ 1 + factor_0 ≤ 0 ∧ −1 − factor_0 ≤ 0
14: TRUE
15: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
1 22 1: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
2 29 2: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
9 36 9: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 3, 4, 7, 8, 18, 20, 21 using the following ranking functions, which are bounded by −23.

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

4 Location Addition

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

1* 25 1: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

5 Location Addition

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

1 23 1_var_snapshot: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

6 Location Addition

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

2* 32 2: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

7 Location Addition

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

2 30 2_var_snapshot: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

8 Location Addition

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

9* 39 9: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

9 Location Addition

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

9 37 9_var_snapshot: − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − factor_post + factor_post ≤ 0 ∧ factor_post − factor_post ≤ 0 ∧ − factor_0 + factor_0 ≤ 0 ∧ factor_0 − factor_0 ≤ 0 ∧ − fact3_post + fact3_post ≤ 0 ∧ fact3_post − fact3_post ≤ 0 ∧ − fact3_0 + fact3_0 ≤ 0 ∧ fact3_0 − fact3_0 ≤ 0 ∧ − Temp6_post + Temp6_post ≤ 0 ∧ Temp6_post − Temp6_post ≤ 0 ∧ − Temp6_0 + Temp6_0 ≤ 0 ∧ Temp6_0 − Temp6_0 ≤ 0 ∧ − Sorted5_post + Sorted5_post ≤ 0 ∧ Sorted5_post − Sorted5_post ≤ 0 ∧ − Sorted5_0 + Sorted5_0 ≤ 0 ∧ Sorted5_0 − Sorted5_0 ≤ 0 ∧ − Index7_post + Index7_post ≤ 0 ∧ Index7_post − Index7_post ≤ 0 ∧ − Index7_0 + Index7_0 ≤ 0 ∧ Index7_0 − Index7_0 ≤ 0 ∧ − Index2_post + Index2_post ≤ 0 ∧ Index2_post − Index2_post ≤ 0 ∧ − Index2_0 + Index2_0 ≤ 0 ∧ Index2_0 − Index2_0 ≤ 0

10 SCC Decomposition

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

10.1 SCC Subproblem 1/2

Here we consider the SCC { 1, 6, 7, 8, 9, 10, 11, 12, 13, 1_var_snapshot, 1*, 9_var_snapshot, 9* }.

10.1.1 Transition Removal

We remove transition 19 using the following ranking functions, which are bounded by −695.

1: 1 − 7⋅i8_0
6: −3 − 7⋅i8_0
7: −4 − 7⋅i8_0
8: −2 − 7⋅i8_0
9: 2⋅factor_0 − 7⋅i8_0
10: 1 + 2⋅factor_post − 7⋅i8_0
11: 2⋅factor_post − 7⋅i8_0
12: 2⋅factor_0 − 7⋅i8_0
13: 2⋅factor_post − 7⋅i8_0
1_var_snapshot: −7⋅i8_0
1*: 2 − 7⋅i8_0
9_var_snapshot: 2 + 2⋅factor_0 + 2⋅factor_post − 7⋅i8_0
9*: 2⋅factor_post − 7⋅i8_0

10.1.2 Transition Removal

We remove transition 16 using the following ranking functions, which are bounded by −695.

1: −7⋅Index7_0 + 4⋅fact3_post + 2⋅factor_0
6: −3 − 7⋅Index7_0
7: −7⋅Index7_0 + 4⋅fact3_post
8: −7⋅Index7_0 + 4⋅factor_0
9: −5 − 7⋅Index7_0 − 6⋅factor_post
10: −7⋅Index7_0 + 4⋅fact3_post + 4⋅factor_0
11: −7⋅Index7_0 + 3⋅factor_post
12: −2 − 7⋅Index7_0
13: −7⋅Index7_0 + factor_post
1_var_snapshot: −3 − 7⋅Index7_0 + 4⋅fact3_post
1*: −1 − 7⋅Index7_0 + 4⋅fact3_post
9_var_snapshot: −7⋅Index7_0
9*: −7⋅Index7_0 + 4⋅factor_0 − 6⋅factor_post

10.1.3 Transition Removal

We remove transitions 23, 25, 37, 39, 5, 9, 10, 11, 12, 13, 14, 15, 17 using the following ranking functions, which are bounded by −5.

1: 3⋅factor_post
6: −2⋅fact3_post + factor_0 + factor_post
7: −2 − 2⋅fact3_post + factor_0
8: 2 − 5⋅fact3_0 − 2⋅fact3_post + factor_0 + 3⋅factor_post
9: −4 − 5⋅fact3_0 − 2⋅fact3_post
10: −1 + 4⋅factor_0
11: −5⋅fact3_0 − 2⋅fact3_post + factor_0
12: Index2_0 − 5⋅fact3_0 − 2⋅fact3_post + factor_0
13: −2⋅fact3_post + factor_0
1_var_snapshot: 4⋅factor_0
1*: −2⋅fact3_post + factor_0 + 3⋅factor_post
9_var_snapshot: −2⋅fact3_post
9*: −5⋅fact3_0 − 2⋅fact3_post + 3⋅factor_post

10.1.4 Transition Removal

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

1: 0
6: 0
7: − fact3_post
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
1_var_snapshot: 0
1*: 0
9_var_snapshot: 0
9*: 0

10.1.5 Splitting Cut-Point Transitions

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

10.1.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 22.

10.1.5.1.1 Splitting Cut-Point Transitions

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

10.1.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 36.

10.1.5.2.1 Splitting Cut-Point Transitions

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

10.2 SCC Subproblem 2/2

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

10.2.1 Transition Removal

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

0: −4⋅Index2_0 + 3⋅factor_0 + factor_post
2: −2 − 4⋅Index2_0
2_var_snapshot: −4⋅Index2_0 + 3⋅factor_0
2*: −4⋅Index2_0 + factor_post

10.2.2 Transition Removal

We remove transitions 30, 32, 2 using the following ranking functions, which are bounded by −2.

0: fact3_0 + factor_0
2: 0
2_var_snapshot: factor_0
2*: 1

10.2.3 Splitting Cut-Point Transitions

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

10.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 29.

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