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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
2 24 2: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
6 31 6: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_0 ≤ 0
7 38 7: − tmp_post + tmp_post ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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

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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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 ≤ 0 ∧ tmp_post − tmp_post ≤ 0 ∧ − tmp_0 + tmp_0 ≤ 0 ∧ tmp_0 − tmp_0 ≤ 0 ∧ − t10_post + t10_post ≤ 0 ∧ t10_post − t10_post ≤ 0 ∧ − t10_0 + t10_0 ≤ 0 ∧ t10_0 − t10_0 ≤ 0 ∧ − min9_post + min9_post ≤ 0 ∧ min9_post − min9_post ≤ 0 ∧ − min9_0 + min9_0 ≤ 0 ∧ min9_0 − min9_0 ≤ 0 ∧ − j7_post + j7_post ≤ 0 ∧ j7_post − j7_post ≤ 0 ∧ − j7_0 + j7_0 ≤ 0 ∧ j7_0 − j7_0 ≤ 0 ∧ − i_post + i_post ≤ 0 ∧ i_post − i_post ≤ 0 ∧ − i_0 + i_0 ≤ 0 ∧ i_0 − i_0 ≤ 0 ∧ − i8_post + i8_post ≤ 0 ∧ i8_post − i8_post ≤ 0 ∧ − i8_0 + i8_0 ≤ 0 ∧ i8_0 − i8_0 ≤ 0 ∧ − N_0 + N_0 ≤ 0 ∧ N_0 − N_0 ≤ 0 ∧ − N6_post + N6_post ≤ 0 ∧ N6_post − N6_post ≤ 0 ∧ − N6_0 + N6_0 ≤ 0 ∧ N6_0 − N6_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

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

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

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

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

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

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: −1 + 4⋅N_0 − 4⋅i_0
1: −3 + 4⋅N_0 − 4⋅i_0
0_var_snapshot: −2 + 4⋅N_0 − 4⋅i_0
0*: 4⋅N_0 − 4⋅i_0

11.3.2 Transition Removal

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

0: 0
1: −2
0_var_snapshot: −1
0*: 1

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