LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
1: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
2: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
3: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
4: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
5: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
6: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
7: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
8: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
9: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
10: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
11: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
12: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
13: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
14: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
15: −15 + edgecount_post ≤ 015 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−15 + edgecount_0 ≤ 015 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
16: TRUE
17: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
2 25 2: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0
4 32 4: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0
7 39 7: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0
9 46 9: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0
13 53 13: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 3, 4, 9, 17, 23, 24 using the following ranking functions, which are bounded by −27.

17: 0
16: 0
11: 0
12: 0
13: 0
14: 0
15: 0
6: 0
7: 0
8: 0
9: 0
10: 0
3: 0
4: 0
5: 0
0: 0
2: 0
1: 0
17: −8
16: −9
11: −10
12: −10
13: −10
14: −10
15: −10
13_var_snapshot: −10
13*: −10
6: −11
7: −11
8: −11
9: −11
10: −11
7_var_snapshot: −11
7*: −11
9_var_snapshot: −11
9*: −11
3: −14
4: −14
5: −14
4_var_snapshot: −14
4*: −14
0: −15
2: −15
2_var_snapshot: −15
2*: −15
1: −16
Hints:
26 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
33 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
40 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
47 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
54 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
1 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
2 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
10 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
13 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
14 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
15 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
16 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
19 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
20 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
21 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
22 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
0 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
3 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
4 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
17 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
23 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
24 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

4 Location Addition

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

2* 28 2: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

5 Location Addition

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

2 26 2_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

6 Location Addition

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

4* 35 4: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

7 Location Addition

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

4 33 4_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

8 Location Addition

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

7* 42 7: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

9 Location Addition

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

7 40 7_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

10 Location Addition

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

9* 49 9: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

11 Location Addition

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

9 47 9_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

12 Location Addition

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

13* 56 13: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

13 Location Addition

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

13 54 13_var_snapshot: y_post + y_post ≤ 0y_posty_post ≤ 0y_0 + y_0 ≤ 0y_0y_0 ≤ 0x_post + x_post ≤ 0x_postx_post ≤ 0x_0 + x_0 ≤ 0x_0x_0 ≤ 0source_post + source_post ≤ 0source_postsource_post ≤ 0source_0 + source_0 ≤ 0source_0source_0 ≤ 0nodecount_post + nodecount_post ≤ 0nodecount_postnodecount_post ≤ 0nodecount_0 + nodecount_0 ≤ 0nodecount_0nodecount_0 ≤ 0j_post + j_post ≤ 0j_postj_post ≤ 0j_0 + j_0 ≤ 0j_0j_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0edgecount_post + edgecount_post ≤ 0edgecount_postedgecount_post ≤ 0edgecount_0 + edgecount_0 ≤ 0edgecount_0edgecount_0 ≤ 0

14 SCC Decomposition

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

14.1 SCC Subproblem 1/4

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

14.1.1 Transition Removal

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

0: −6⋅i_0 + 6⋅nodecount_0nodecount_post
2: −1 − 6⋅i_0 + 6⋅nodecount_0
2_var_snapshot: −12 + edgecount_post − 6⋅i_0 + 6⋅nodecount_0nodecount_post
2*: −6⋅i_0 + 6⋅nodecount_0
Hints:
26 lexWeak[ [1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 1, 0, 0, 0] ]
28 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0] ]
1 lexStrict[ [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
22 lexWeak[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 0, 0, 0] ]

14.1.2 Transition Removal

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

0: nodecount_0
2: edgecount_0
2_var_snapshot: 0
2*: edgecount_0 + edgecount_post
Hints:
26 lexStrict[ [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
28 lexStrict[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0] , [0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
22 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.1.3 Splitting Cut-Point Transitions

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

14.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 25.

14.1.3.1.1 Splitting Cut-Point Transitions

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

14.2 SCC Subproblem 2/4

Here we consider the SCC { 3, 4, 5, 4_var_snapshot, 4* }.

14.2.1 Transition Removal

We remove transition 5 using the following ranking functions, which are bounded by −689.

3: −2⋅edgecount_0edgecount_post − 47⋅i_0
4: −47⋅i_0
5: −2⋅edgecount_0edgecount_post − 47⋅i_0 + 3⋅nodecount_post
4_var_snapshot: −2⋅edgecount_0 − 47⋅i_0 + 3⋅nodecount_post
4*: 31 − 2⋅edgecount_0 − 47⋅i_0
Hints:
33 lexWeak[ [0, 0, 3, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 47, 0, 0, 0, 2] ]
35 lexWeak[ [0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 47, 0, 0, 0, 0] ]
2 lexWeak[ [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 47, 0, 47, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2] ]
5 lexStrict[ [0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 47, 0, 1, 0, 2] , [1, 0, 0, 3, 0, 0, 49, 0, 0, 0, 0, 0, 0, 0, 47, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
21 lexWeak[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 47, 0, 1, 0, 2] ]

14.2.2 Transition Removal

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

3: 1
4: edgecount_0
5: −5⋅nodecount_post
4_var_snapshot: −4⋅nodecount_post
4*: 0
Hints:
33 lexWeak[ [0, 0, 0, 4, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
35 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
2 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
21 lexStrict[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.2.3 Transition Removal

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

3: 0
4: edgecount_post
5: 0
4_var_snapshot: 0
4*: 0
Hints:
33 lexStrict[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.2.4 Splitting Cut-Point Transitions

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

14.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 32.

14.2.4.1.1 Splitting Cut-Point Transitions

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

14.3 SCC Subproblem 3/4

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

14.3.1 Transition Removal

We remove transition 10 using the following ranking functions, which are bounded by 75.

6: −61⋅i_0 + 61⋅nodecount_0
7: −61⋅i_0 + 61⋅nodecount_0
8: −61⋅i_0 + 61⋅nodecount_0
9: 4⋅edgecount_0 − 61⋅i_0 + 61⋅nodecount_0 − 3⋅nodecount_post
10: −30 + 3⋅edgecount_post − 61⋅i_0 + 61⋅nodecount_0
7_var_snapshot: −61⋅i_0 + 61⋅nodecount_0
7*: −61⋅i_0 + 61⋅nodecount_0
9_var_snapshot: 3⋅edgecount_post − 61⋅i_0 + 61⋅nodecount_0 − 3⋅nodecount_post
9*: 4⋅edgecount_0 − 61⋅i_0 + 61⋅nodecount_0
Hints:
40 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0] ]
42 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0] ]
47 lexWeak[ [3, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 61, 0, 0, 0, 0, 0, 0, 0, 0, 61, 3, 0, 0, 0] ]
49 lexWeak[ [0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 61, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 4, 0] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 61, 0, 0, 0, 0] ]
7 lexWeak[ [0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 61, 0, 61, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 0, 0, 0, 4, 0] ]
8 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0] ]
10 lexStrict[ [0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 61, 0, 0, 0, 0] , [0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
19 lexWeak[ [0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 0, 0, 0, 0, 61, 3, 0, 0, 0] ]
20 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0, 0, 0, 0, 0, 61, 0, 0, 0, 0] ]

14.3.2 Transition Removal

We remove transition 8 using the following ranking functions, which are bounded by −77.

6: −7 − 5⋅j_0
7: −4 − 5⋅j_0
8: −1 − 5⋅j_0nodecount_post
9: edgecount_0 − 5⋅j_0
10: −1 − edgecount_0 − 5⋅j_0
7_var_snapshot: −5⋅j_0nodecount_post
7*: −3 − 5⋅j_0
9_var_snapshot: −1 − edgecount_0 − 5⋅j_0
9*: −2 − 5⋅j_0nodecount_post
Hints:
40 lexWeak[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] ]
42 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] ]
47 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 1] ]
49 lexWeak[ [0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 1] ]
6 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0] ]
8 lexStrict[ [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 1, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
19 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 1] ]
20 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.3.3 Transition Removal

We remove transitions 40, 42, 47, 49, 6, 7, 19, 20 using the following ranking functions, which are bounded by −1.

6: 2⋅edgecount_0 + 10⋅nodecount_0 + nodecount_post
7: 2⋅edgecount_0edgecount_post + 10⋅nodecount_0
8: edgecount_0 + 10⋅nodecount_0
9: −3⋅edgecount_0 + 10⋅nodecount_0
10: nodecount_post
7_var_snapshot: 10⋅nodecount_0
7*: 2⋅edgecount_0 + 10⋅nodecount_0
9_var_snapshot: 0
9*: −30 + 10⋅nodecount_0
Hints:
40 lexStrict[ [1, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [1, 0, 0, 0, 0, 0, 0, 2, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
42 lexStrict[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 0] , [0, 0, 0, 0, 0, 0, 0, 2, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
47 lexStrict[ [0, 0, 0, 0, 0, 0, 3, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 3, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
49 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3] , [0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
6 lexStrict[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 2, 0] , [0, 0, 0, 1, 0, 0, 0, 2, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
7 lexStrict[ [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 1, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
19 lexStrict[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
20 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] , [0, 0, 0, 0, 0, 0, 0, 0, 10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.3.4 Splitting Cut-Point Transitions

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

14.3.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 39.

14.3.4.1.1 Splitting Cut-Point Transitions

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

14.3.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 46.

14.3.4.2.1 Splitting Cut-Point Transitions

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

14.4 SCC Subproblem 4/4

Here we consider the SCC { 11, 12, 13, 14, 15, 13_var_snapshot, 13* }.

14.4.1 Transition Removal

We remove transitions 15, 16, 18 using the following ranking functions, which are bounded by 17.

11: 4 + edgecount_0 + edgecount_post − 7⋅i_0 + nodecount_0 + nodecount_post + 7⋅source_0
12: 18 + edgecount_0 − 7⋅i_0 + nodecount_0 + nodecount_post + 7⋅source_0
13: −7 + edgecount_0 + 2⋅edgecount_post − 7⋅i_0 + nodecount_0 + nodecount_post + 7⋅source_0
14: −4 + 2⋅edgecount_0 + edgecount_post − 7⋅i_0 + nodecount_post + 7⋅source_0
15: 2⋅edgecount_0 + edgecount_post − 7⋅i_0 + 7⋅source_0
13_var_snapshot: −3 + 2⋅edgecount_0 + edgecount_post − 7⋅i_0 + nodecount_post + 7⋅source_0
13*: 24 + edgecount_0 − 7⋅i_0 + nodecount_0 + nodecount_post + 7⋅source_0
Hints:
54 lexWeak[ [0, 1, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 1, 0, 2, 0] ]
56 lexWeak[ [2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 7, 2, 0, 1, 0] ]
11 lexWeak[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 1, 0] ]
12 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 1, 0, 2, 0] ]
13 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0] ]
14 lexWeak[ [0, 0, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 7, 1, 0, 1, 0] ]
15 lexStrict[ [0, 0, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 7, 1, 0, 1, 0] , [0, 1, 0, 0, 0, 0, 0, 2, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
16 lexStrict[ [0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 1, 0] , [0, 1, 0, 0, 0, 0, 0, 2, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
18 lexStrict[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 1, 0, 2, 0] , [0, 1, 0, 1, 0, 0, 0, 2, 7, 0, 7, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.4.2 Transition Removal

We remove transitions 54, 56, 11, 12, 13 using the following ranking functions, which are bounded by −21.

11: 4⋅nodecount_post
12: edgecount_0 + 4⋅nodecount_post
13: edgecount_0
14: edgecount_0 − 4⋅nodecount_0
15: 5⋅nodecount_post
13_var_snapshot: −4⋅nodecount_0
13*: edgecount_0edgecount_post + 4⋅nodecount_post
Hints:
54 lexStrict[ [0, 0, 0, 0, 0, 0, 1, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
56 lexStrict[ [1, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] , [1, 0, 0, 4, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] , [0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
12 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] , [0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
13 lexStrict[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1] , [0, 0, 0, 4, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
14 lexWeak[ [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.4.3 Transition Removal

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

11: 0
12: 0
13: 0
14: 0
15: 1
13_var_snapshot: 0
13*: 0
Hints:
14 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.4.4 Splitting Cut-Point Transitions

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

14.4.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 53.

14.4.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert