LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 17 0: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0
2 24 2: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0
6 31 6: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0
7 38 7: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 2, 11, 13, 15, 16 using the following ranking functions, which are bounded by −23.

12: 0
11: 0
0: 0
1: 0
2: 0
3: 0
7: 0
8: 0
9: 0
10: 0
4: 0
6: 0
5: 0
12: −7
11: −8
0: −9
1: −9
0_var_snapshot: −9
0*: −9
2: −10
3: −10
7: −10
8: −10
9: −10
10: −10
2_var_snapshot: −10
2*: −10
7_var_snapshot: −10
7*: −10
4: −13
6: −13
6_var_snapshot: −13
6*: −13
5: −14
Hints:
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] ]
25 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] ]
32 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] ]
39 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 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 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] ]
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] ]
4 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] ]
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] ]
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] ]
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] ]
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] ]
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] ]
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] ]
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] ]
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] ]
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] ]
11 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] ]
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, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 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] ]

3 Location Addition

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

0* 20 0: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0

4 Location Addition

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

0 18 0_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0

5 Location Addition

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

2* 27 2: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0

6 Location Addition

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

2 25 2_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0

7 Location Addition

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

6* 34 6: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0

8 Location Addition

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

6 32 6_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0

9 Location Addition

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

7* 41 7: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0

10 Location Addition

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

7 39 7_var_snapshot: tmp_post + tmp_post ≤ 0tmp_posttmp_post ≤ 0tmp_0 + tmp_0 ≤ 0tmp_0tmp_0 ≤ 0t10_post + t10_post ≤ 0t10_postt10_post ≤ 0t10_0 + t10_0 ≤ 0t10_0t10_0 ≤ 0min9_post + min9_post ≤ 0min9_postmin9_post ≤ 0min9_0 + min9_0 ≤ 0min9_0min9_0 ≤ 0j7_post + j7_post ≤ 0j7_postj7_post ≤ 0j7_0 + j7_0 ≤ 0j7_0j7_0 ≤ 0i_post + i_post ≤ 0i_posti_post ≤ 0i_0 + i_0 ≤ 0i_0i_0 ≤ 0i8_post + i8_post ≤ 0i8_posti8_post ≤ 0i8_0 + i8_0 ≤ 0i8_0i8_0 ≤ 0N_0 + N_0 ≤ 0N_0N_0 ≤ 0N6_post + N6_post ≤ 0N6_postN6_post ≤ 0N6_0 + N6_0 ≤ 0N6_0N6_0 ≤ 0

11 SCC Decomposition

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

11.1 SCC Subproblem 1/3

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

11.1.1 Transition Removal

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

4: −1 + 4⋅N6_0 − 4⋅j7_0
6: 1 + 4⋅N6_0 − 4⋅j7_0
6_var_snapshot: 4⋅N6_0 − 4⋅j7_0
6*: 2 + 4⋅N6_0 − 4⋅j7_0
Hints:
32 lexWeak[ [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, 4, 0] ]
34 lexWeak[ [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, 4, 0] ]
3 lexStrict[ [0, 0, 0, 0, 4, 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, 4, 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] ]
10 lexWeak[ [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, 4, 0] ]

11.1.2 Transition Removal

We remove transitions 32, 34, 10 using the following ranking functions, which are bounded by −1.

4: −1
6: 1
6_var_snapshot: 0
6*: 2
Hints:
32 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] ]
34 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] ]
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, 0] , [0, 0, 0, 0, 0, 0, 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.1.3 Splitting Cut-Point Transitions

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

11.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 31.

11.1.3.1.1 Splitting Cut-Point Transitions

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

11.2 SCC Subproblem 2/3

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

11.2.1 Transition Removal

We remove transition 12 using the following ranking functions, which are bounded by 9.

2: 2 + 5⋅N6_0 − 5⋅j7_0
3: 5⋅N6_0 − 5⋅j7_0
7: −1 + 5⋅N6_0 − 5⋅j7_0
8: −1 + 5⋅N6_0 − 5⋅j7_0
9: −1 + 5⋅N6_0 − 5⋅j7_0
10: −1 + 5⋅N6_0 − 5⋅j7_0
2_var_snapshot: 1 + 5⋅N6_0 − 5⋅j7_0
2*: 3 + 5⋅N6_0 − 5⋅j7_0
7_var_snapshot: −1 + 5⋅N6_0 − 5⋅j7_0
7*: −1 + 5⋅N6_0 − 5⋅j7_0
Hints:
25 lexWeak[ [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, 5, 0] ]
27 lexWeak[ [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, 5, 0] ]
39 lexWeak[ [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, 5, 0] ]
41 lexWeak[ [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, 5, 0] ]
1 lexWeak[ [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, 5, 0] ]
4 lexWeak[ [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, 5, 0] ]
5 lexWeak[ [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, 5, 0] ]
6 lexWeak[ [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, 5, 0] ]
7 lexWeak[ [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, 5, 0] ]
8 lexWeak[ [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, 5, 0] ]
9 lexWeak[ [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, 5, 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, 5, 0, 0, 0, 0, 0, 0, 0, 0, 5, 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, 0, 0, 0, 0, 0, 0] ]

11.2.2 Transition Removal

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

2: −2 + 6⋅N6_0 − 6⋅i8_0
3: −4 + 6⋅N6_0 − 6⋅i8_0
7: 2 + 6⋅N6_0 − 6⋅i8_0
8: 6⋅N6_0 − 6⋅i8_0
9: −2 + 6⋅N6_0 − 6⋅i8_0
10: −1 + 6⋅N6_0 − 6⋅i8_0
2_var_snapshot: −3 + 6⋅N6_0 − 6⋅i8_0
2*: −1 + 6⋅N6_0 − 6⋅i8_0
7_var_snapshot: 1 + 6⋅N6_0 − 6⋅i8_0
7*: 3 + 6⋅N6_0 − 6⋅i8_0
Hints:
25 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, 6, 0] ]
27 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, 6, 0] ]
39 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, 6, 0] ]
41 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, 6, 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, 6, 0, 0, 0, 0, 6, 0] ]
4 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, 6, 0] ]
5 lexWeak[ [0, 0, 0, 6, 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, 6, 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, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 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, 6, 0, 0, 0, 0, 6, 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, 0, 0] ]

11.2.3 Transition Removal

We remove transitions 25, 27, 39, 41, 1, 4, 5, 6, 7, 8 using the following ranking functions, which are bounded by −3.

2: −1
3: −3
7: 3
8: 1
9: 5
10: 6
2_var_snapshot: −2
2*: 0
7_var_snapshot: 2
7*: 4
Hints:
25 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] ]
27 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] ]
39 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] ]
41 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] ]
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] ]
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] ]
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, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 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] ]
7 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] ]
8 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] ]

11.2.4 Splitting Cut-Point Transitions

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

11.2.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 24.

11.2.4.1.1 Splitting Cut-Point Transitions

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

11.2.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 38.

11.2.4.2.1 Splitting Cut-Point Transitions

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

11.3 SCC Subproblem 3/3

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

11.3.1 Transition Removal

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

0: 3⋅N_0 − 3⋅i_0
1: −2 + 3⋅N_0 − 3⋅i_0
0_var_snapshot: −1 + 3⋅N_0 − 3⋅i_0
0*: 3⋅N_0 − 3⋅i_0
Hints:
18 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 3, 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, 3, 0, 0, 0, 0, 3, 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, 3, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0] ]
14 lexStrict[ [0, 0, 0, 0, 3, 0, 3, 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, 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] ]

11.3.2 Transition Removal

We remove transitions 18, 20, 0 using the following ranking functions, which are bounded by −1.

0: 1
1: −1
0_var_snapshot: 0
0*: 2
Hints:
18 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] ]
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 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] ]

11.3.3 Splitting Cut-Point Transitions

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

11.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 17.

11.3.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert