LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
1: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
2: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
3: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
4: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
5: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
6: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
7: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
8: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
9: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
10: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
11: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
12: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
13: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
14: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − edgecount_0 ≤ 0−5 + nodecount_0 ≤ 05 − nodecount_0 ≤ 0source_0 ≤ 0
15: −5 + edgecount_post ≤ 05 − edgecount_post ≤ 0−5 + nodecount_post ≤ 05 − nodecount_post ≤ 0source_post ≤ 0source_post ≤ 0−5 + edgecount_0 ≤ 05 − 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:
0 25 0: 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
6 39 6: 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 46 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
11 53 11: 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 1, 4, 6, 12, 20, 23, 24 using the following ranking functions, which are bounded by −27.

17: 0
16: 0
0: 0
1: 0
13: 0
14: 0
15: 0
7: 0
8: 0
10: 0
11: 0
12: 0
5: 0
6: 0
9: 0
2: 0
4: 0
3: 0
17: −8
16: −9
0: −10
1: −10
13: −10
14: −10
15: −10
0_var_snapshot: −10
0*: −10
7: −11
8: −11
10: −11
11: −11
12: −11
7_var_snapshot: −11
7*: −11
11_var_snapshot: −11
11*: −11
5: −14
6: −14
9: −14
6_var_snapshot: −14
6*: −14
2: −15
4: −15
4_var_snapshot: −15
4*: −15
3: −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, 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] ]
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 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] ]
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] ]
3 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] ]
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] ]
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, 0] ]
9 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] ]
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] ]
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] ]
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] ]
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] ]
17 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] ]
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, 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, 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] ]
1 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] ]
6 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] ]
12 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] ]
20 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.

0* 28 0: 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.

0 26 0_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.

6* 42 6: 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.

6 40 6_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.

7* 49 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

11 Location Addition

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

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

12 Location Addition

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

11* 56 11: 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.

11 54 11_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 { 2, 4, 4_var_snapshot, 4* }.

14.1.1 Transition Removal

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

2: edgecount_post − 6⋅i_0 + 6⋅nodecount_0
4: −1 − 6⋅i_0 + 6⋅nodecount_0
4_var_snapshot: −2 − edgecount_post − 6⋅i_0 + 6⋅nodecount_0 + nodecount_post
4*: −6⋅i_0 + 6⋅nodecount_0
Hints:
33 lexWeak[ [0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 6, 0, 1, 0, 0] ]
35 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] ]
2 lexStrict[ [1, 0, 0, 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] , [1, 0, 0, 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, 0, 0, 1, 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, 1, 0, 0] ]

14.1.2 Transition Removal

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

2: edgecount_0
4: −5 + 2⋅edgecount_0
4_var_snapshot: 0
4*: 2⋅edgecount_0
Hints:
33 lexStrict[ [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, 0, 0, 0, 0] , [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, 0, 0, 0, 0] ]
35 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, 2, 0] , [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, 0, 0, 0, 0] ]
22 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, 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] ]

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

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 { 5, 6, 9, 6_var_snapshot, 6* }.

14.2.1 Transition Removal

We remove transition 7 using the following ranking functions, which are bounded by −79.

5: −6 + edgecount_post − 17⋅i_0 − 2⋅nodecount_post
6: −17⋅i_0
9: edgecount_0 + edgecount_post − 17⋅i_0 − 2⋅nodecount_post
6_var_snapshot: edgecount_post − 17⋅i_0 − 2⋅nodecount_post
6*: edgecount_post − 17⋅i_0
Hints:
40 lexWeak[ [1, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 17, 1, 0, 0, 0] ]
42 lexWeak[ [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, 17, 0, 0, 0, 0] ]
3 lexWeak[ [0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 17, 0, 17, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 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, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 17, 1, 0, 0, 0] , [0, 1, 2, 0, 0, 0, 18, 0, 0, 0, 0, 0, 0, 0, 17, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 17, 1, 0, 0, 1] ]

14.2.2 Transition Removal

We remove transitions 42, 3, 15 using the following ranking functions, which are bounded by −6.

5: 2⋅nodecount_post
6: 0
9: −1 − nodecount_post
6_var_snapshot: nodecount_post
6*: 5
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, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
42 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, 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, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
15 lexStrict[ [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, 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] ]

14.2.3 Transition Removal

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

5: 0
6: edgecount_0
9: 0
6_var_snapshot: 0
6*: 0
Hints:
40 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, 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] ]

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

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 { 7, 8, 10, 11, 12, 7_var_snapshot, 7*, 11_var_snapshot, 11* }.

14.3.1 Transition Removal

We remove transition 13 using the following ranking functions, which are bounded by 15.

7: edgecount_0 − 21⋅i_0 + 21⋅nodecount_0 + 2⋅nodecount_post
8: edgecount_post − 21⋅i_0 + 21⋅nodecount_0
10: edgecount_0edgecount_post − 21⋅i_0 + 21⋅nodecount_0
11: edgecount_post − 21⋅i_0 + 21⋅nodecount_0nodecount_post
12: edgecount_0 − 21⋅i_0 + 21⋅nodecount_0nodecount_post
7_var_snapshot: −21⋅i_0 + 21⋅nodecount_0
7*: edgecount_0 + 3⋅edgecount_post − 21⋅i_0 + 21⋅nodecount_0
11_var_snapshot: edgecount_post − 21⋅i_0 + 21⋅nodecount_0nodecount_post
11*: −5 − edgecount_post − 21⋅i_0 + 21⋅nodecount_0
Hints:
47 lexWeak[ [0, 0, 0, 2, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 0, 0, 0] ]
49 lexWeak[ [0, 3, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 21, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 0, 0, 1] ]
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, 1, 21, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 1, 0, 0] ]
56 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, 21, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 1, 0, 0] ]
5 lexWeak[ [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 1, 0, 0] ]
8 lexWeak[ [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, 21, 0, 0, 0, 0, 21, 0, 1, 0, 0] ]
9 lexWeak[ [1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 21, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 0, 0, 1] ]
10 lexWeak[ [3, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 21, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 0, 0, 0, 0, 3, 0, 0, 1] ]
11 lexWeak[ [0, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 1, 0, 1] ]
13 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, 21, 0, 0, 0, 0, 21, 0, 1, 0, 0] , [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 21, 0, 0, 0, 0, 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.2 Transition Removal

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

7: 15 − 2⋅edgecount_0edgecount_post − 20⋅j_0 − 4⋅nodecount_post
8: −20⋅j_0 − 6⋅nodecount_post
10: −2⋅edgecount_0 − 20⋅j_0nodecount_post
11: −20⋅j_0
12: −2⋅edgecount_0 − 20⋅j_0
7_var_snapshot: edgecount_post − 20⋅j_0 − 4⋅nodecount_post
7*: −2⋅edgecount_0edgecount_post − 20⋅j_0
11_var_snapshot: −5 − 20⋅j_0
11*: 2⋅edgecount_post − 20⋅j_0nodecount_post
Hints:
47 lexWeak[ [0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 20, 0, 0, 0, 0, 0, 1, 0, 0] ]
49 lexWeak[ [0, 0, 0, 4, 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, 20, 0, 0, 0, 0, 0, 1, 0, 2] ]
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, 20, 0, 0, 0, 0, 0, 0, 0, 0] ]
56 lexWeak[ [0, 2, 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, 20, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexWeak[ [1, 0, 0, 2, 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, 20, 0, 0, 0, 0, 0, 0, 0, 0] ]
8 lexWeak[ [2, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 20, 0, 20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0] ]
9 lexWeak[ [0, 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, 20, 0, 0, 0, 0, 0, 0, 0, 2] ]
10 lexWeak[ [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, 20, 0, 1, 0, 2] ]
11 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, 1, 0, 0, 0, 0, 0, 20, 0, 0, 0, 0, 0, 0, 0, 2] , [0, 0, 0, 0, 0, 0, 22, 0, 0, 0, 0, 0, 0, 0, 20, 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.3 Transition Removal

We remove transitions 47, 49, 54, 5, 8, 9, 10 using the following ranking functions, which are bounded by −21.

7: −3⋅edgecount_post
8: −1 − 3⋅edgecount_postnodecount_post
10: 2⋅nodecount_0 + nodecount_post
11: nodecount_0
12: −3⋅edgecount_post + 2⋅nodecount_post
7_var_snapshot: −3⋅edgecount_postnodecount_post
7*: −5 − 3⋅edgecount_post + 2⋅nodecount_post
11_var_snapshot: 0
11*: nodecount_0 + nodecount_post
Hints:
47 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, 3, 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, 0, 0, 0, 0, 0, 0, 0] ]
49 lexStrict[ [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, 0, 0, 0, 0, 0, 3, 0, 0] , [3, 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, 0, 0, 0, 0, 0, 0, 0, 0] ]
54 lexStrict[ [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, 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] ]
56 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5 lexStrict[ [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, 3, 0, 0] , [3, 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] ]
8 lexStrict[ [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, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 1, 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, 0, 0, 0, 0, 0] ]
9 lexStrict[ [0, 3, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
10 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, 2, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0] , [3, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.3.4 Transition Removal

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

7: 0
8: 0
10: 0
11: −1
12: 0
7_var_snapshot: 0
7*: 0
11_var_snapshot: 0
11*: 0
Hints:
56 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] ]

14.3.5 Splitting Cut-Point Transitions

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

14.3.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 46.

14.3.5.1.1 Splitting Cut-Point Transitions

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

14.3.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 53.

14.3.5.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 { 0, 1, 13, 14, 15, 0_var_snapshot, 0* }.

14.4.1 Transition Removal

We remove transitions 18, 19, 21 using the following ranking functions, which are bounded by −26.

0: 1 + 4⋅edgecount_0 − 11⋅i_0 + 11⋅source_0
1: −1 + edgecount_0 + edgecount_post − 11⋅i_0 + nodecount_0 + nodecount_post + 11⋅source_0
13: 13 + edgecount_0 − 11⋅i_0 + nodecount_0 − 2⋅nodecount_post + 11⋅source_0
14: 2 + edgecount_0 − 11⋅i_0 + nodecount_0 + 11⋅source_0
15: edgecount_0 + edgecount_post − 11⋅i_0 + nodecount_0 + 11⋅source_0
0_var_snapshot: edgecount_0 + edgecount_post − 11⋅i_0 + nodecount_0 + nodecount_post + 11⋅source_0
0*: −3 + 4⋅edgecount_0 − 11⋅i_0 + nodecount_0 + 11⋅source_0
Hints:
26 lexWeak[ [1, 0, 1, 0, 0, 0, 0, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 11, 1, 0, 1, 0] ]
28 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 4, 0] ]
0 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 11, 1, 0, 1, 0] ]
14 lexWeak[ [0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 1, 0] ]
16 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 11, 0, 11, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 4, 0] ]
17 lexWeak[ [0, 1, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 2, 1, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 1, 0] ]
18 lexStrict[ [0, 1, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 2, 1, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 1, 0] , [0, 1, 0, 0, 0, 0, 0, 1, 0, 1, 0, 11, 0, 0, 0, 0, 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 11, 0, 0, 1, 0] , [0, 1, 0, 0, 0, 0, 0, 1, 0, 1, 0, 11, 0, 0, 0, 0, 0, 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, 11, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 11, 1, 0, 1, 0] , [0, 1, 0, 1, 0, 0, 0, 1, 10, 0, 11, 11, 0, 0, 0, 0, 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 26, 28, 0, 14, 16 using the following ranking functions, which are bounded by −11.

0: edgecount_post
1: −1 − 2⋅edgecount_0
13: 2⋅nodecount_post
14: 5
15: 3⋅nodecount_post
0_var_snapshot: −2⋅edgecount_0
0*: 0
Hints:
26 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2] , [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] ]
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, 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 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, 2] , [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, 0, 0, 0, 0, 0, 0] ]
14 lexStrict[ [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, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
16 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 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, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

14.4.3 Transition Removal

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

0: 0
1: 0
13: 0
14: 0
15: edgecount_post
0_var_snapshot: 0
0*: 0
Hints:
17 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, 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] ]

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

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