LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 3

Transitions: (pre-variables and post-variables)

0	0	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2P ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0
1	1	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1 + arg2 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg1P + arg2 ≤ 0 ∧ arg1P − arg2 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ arg2 − arg3P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ arg2 − arg4P ≤ 0 ∧ − arg2 + arg4P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0
2	2	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ arg4 ≤ 0 ∧ − arg1P + arg2 ≤ 0 ∧ arg1P − arg2 ≤ 0 ∧ arg1 − arg2P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0
2	3	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ 1 − arg3P + arg3 ≤ 0 ∧ −1 + arg3P − arg3 ≤ 0 ∧ 1 + arg3 − arg4P ≤ 0 ∧ −1 − arg3 + arg4P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2	4	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ 1 − arg3P + arg3 ≤ 0 ∧ −1 + arg3P − arg3 ≤ 0 ∧ 1 + arg3 − arg4P ≤ 0 ∧ −1 − arg3 + arg4P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2	5	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ −1 − arg3P + arg3 ≤ 0 ∧ 1 + arg3P − arg3 ≤ 0 ∧ −1 + arg3 − arg4P ≤ 0 ∧ 1 − arg3 + arg4P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
3	6	0:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

1	7	1:	− arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2	14	2:	− arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 6 using the following ranking functions, which are bounded by −13.

3:	0
0:	0
1:	0
2:	0
3:	−4
0:	−5
1:	−6
2:	−6
1_var_snapshot:	−6
1*:	−6
2_var_snapshot:	−6
2*:	−6

3 Location Addition

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

1* 10 1: − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

4 Location Addition

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

1 8 1_var_snapshot: − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

5 Location Addition

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

2* 17 2: − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

6 Location Addition

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

2 15 2_var_snapshot: − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

7 SCC Decomposition

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

7.1 SCC Subproblem 1/1

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

7.1.1 Transition Removal

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

1:	−2 + 4⋅arg1
2:	4⋅arg2 − 4⋅arg3
1_var_snapshot:	−3 + 4⋅arg1
1*:	−1 + 4⋅arg1
2_var_snapshot:	4⋅arg2 − 4⋅arg3
2*:	4⋅arg2 − 4⋅arg3

7.1.2 Transition Removal

We remove transitions 8, 10, 2, 4 using the following ranking functions, which are bounded by −3.

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

7.1.3 Splitting Cut-Point Transitions

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

7.1.3.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 7.

7.1.3.1.1 Splitting Cut-Point Transitions

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

7.1.3.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 14.

7.1.3.2.1 Fresh Variable Addition

The new variable __snapshot_2_arg4P is introduced. The transition formulas are extended as follows:

8:	__snapshot_2_arg4P ≤ __snapshot_2_arg4P ∧ __snapshot_2_arg4P ≤ __snapshot_2_arg4P
15:	__snapshot_2_arg4P ≤ arg4P ∧ arg4P ≤ __snapshot_2_arg4P
17:	__snapshot_2_arg4P ≤ __snapshot_2_arg4P ∧ __snapshot_2_arg4P ≤ __snapshot_2_arg4P
3:	__snapshot_2_arg4P ≤ __snapshot_2_arg4P ∧ __snapshot_2_arg4P ≤ __snapshot_2_arg4P
5:	__snapshot_2_arg4P ≤ __snapshot_2_arg4P ∧ __snapshot_2_arg4P ≤ __snapshot_2_arg4P

7.1.3.2.2 Fresh Variable Addition

The new variable __snapshot_2_arg4 is introduced. The transition formulas are extended as follows:

8:	__snapshot_2_arg4 ≤ __snapshot_2_arg4 ∧ __snapshot_2_arg4 ≤ __snapshot_2_arg4
15:	__snapshot_2_arg4 ≤ arg4 ∧ arg4 ≤ __snapshot_2_arg4
17:	__snapshot_2_arg4 ≤ __snapshot_2_arg4 ∧ __snapshot_2_arg4 ≤ __snapshot_2_arg4
3:	__snapshot_2_arg4 ≤ __snapshot_2_arg4 ∧ __snapshot_2_arg4 ≤ __snapshot_2_arg4
5:	__snapshot_2_arg4 ≤ __snapshot_2_arg4 ∧ __snapshot_2_arg4 ≤ __snapshot_2_arg4

7.1.3.2.3 Fresh Variable Addition

The new variable __snapshot_2_arg3P is introduced. The transition formulas are extended as follows:

8:	__snapshot_2_arg3P ≤ __snapshot_2_arg3P ∧ __snapshot_2_arg3P ≤ __snapshot_2_arg3P
15:	__snapshot_2_arg3P ≤ arg3P ∧ arg3P ≤ __snapshot_2_arg3P
17:	__snapshot_2_arg3P ≤ __snapshot_2_arg3P ∧ __snapshot_2_arg3P ≤ __snapshot_2_arg3P
3:	__snapshot_2_arg3P ≤ __snapshot_2_arg3P ∧ __snapshot_2_arg3P ≤ __snapshot_2_arg3P
5:	__snapshot_2_arg3P ≤ __snapshot_2_arg3P ∧ __snapshot_2_arg3P ≤ __snapshot_2_arg3P

7.1.3.2.4 Fresh Variable Addition

The new variable __snapshot_2_arg3 is introduced. The transition formulas are extended as follows:

8:	__snapshot_2_arg3 ≤ __snapshot_2_arg3 ∧ __snapshot_2_arg3 ≤ __snapshot_2_arg3
15:	__snapshot_2_arg3 ≤ arg3 ∧ arg3 ≤ __snapshot_2_arg3
17:	__snapshot_2_arg3 ≤ __snapshot_2_arg3 ∧ __snapshot_2_arg3 ≤ __snapshot_2_arg3
3:	__snapshot_2_arg3 ≤ __snapshot_2_arg3 ∧ __snapshot_2_arg3 ≤ __snapshot_2_arg3
5:	__snapshot_2_arg3 ≤ __snapshot_2_arg3 ∧ __snapshot_2_arg3 ≤ __snapshot_2_arg3

7.1.3.2.5 Fresh Variable Addition

The new variable __snapshot_2_arg2P is introduced. The transition formulas are extended as follows:

8:	__snapshot_2_arg2P ≤ __snapshot_2_arg2P ∧ __snapshot_2_arg2P ≤ __snapshot_2_arg2P
15:	__snapshot_2_arg2P ≤ arg2P ∧ arg2P ≤ __snapshot_2_arg2P
17:	__snapshot_2_arg2P ≤ __snapshot_2_arg2P ∧ __snapshot_2_arg2P ≤ __snapshot_2_arg2P
3:	__snapshot_2_arg2P ≤ __snapshot_2_arg2P ∧ __snapshot_2_arg2P ≤ __snapshot_2_arg2P
5:	__snapshot_2_arg2P ≤ __snapshot_2_arg2P ∧ __snapshot_2_arg2P ≤ __snapshot_2_arg2P

7.1.3.2.6 Fresh Variable Addition

The new variable __snapshot_2_arg2 is introduced. The transition formulas are extended as follows:

8:	__snapshot_2_arg2 ≤ __snapshot_2_arg2 ∧ __snapshot_2_arg2 ≤ __snapshot_2_arg2
15:	__snapshot_2_arg2 ≤ arg2 ∧ arg2 ≤ __snapshot_2_arg2
17:	__snapshot_2_arg2 ≤ __snapshot_2_arg2 ∧ __snapshot_2_arg2 ≤ __snapshot_2_arg2
3:	__snapshot_2_arg2 ≤ __snapshot_2_arg2 ∧ __snapshot_2_arg2 ≤ __snapshot_2_arg2
5:	__snapshot_2_arg2 ≤ __snapshot_2_arg2 ∧ __snapshot_2_arg2 ≤ __snapshot_2_arg2

7.1.3.2.7 Fresh Variable Addition

The new variable __snapshot_2_arg1P is introduced. The transition formulas are extended as follows:

8:	__snapshot_2_arg1P ≤ __snapshot_2_arg1P ∧ __snapshot_2_arg1P ≤ __snapshot_2_arg1P
15:	__snapshot_2_arg1P ≤ arg1P ∧ arg1P ≤ __snapshot_2_arg1P
17:	__snapshot_2_arg1P ≤ __snapshot_2_arg1P ∧ __snapshot_2_arg1P ≤ __snapshot_2_arg1P
3:	__snapshot_2_arg1P ≤ __snapshot_2_arg1P ∧ __snapshot_2_arg1P ≤ __snapshot_2_arg1P
5:	__snapshot_2_arg1P ≤ __snapshot_2_arg1P ∧ __snapshot_2_arg1P ≤ __snapshot_2_arg1P

7.1.3.2.8 Fresh Variable Addition

The new variable __snapshot_2_arg1 is introduced. The transition formulas are extended as follows:

8:	__snapshot_2_arg1 ≤ __snapshot_2_arg1 ∧ __snapshot_2_arg1 ≤ __snapshot_2_arg1
15:	__snapshot_2_arg1 ≤ arg1 ∧ arg1 ≤ __snapshot_2_arg1
17:	__snapshot_2_arg1 ≤ __snapshot_2_arg1 ∧ __snapshot_2_arg1 ≤ __snapshot_2_arg1
3:	__snapshot_2_arg1 ≤ __snapshot_2_arg1 ∧ __snapshot_2_arg1 ≤ __snapshot_2_arg1
5:	__snapshot_2_arg1 ≤ __snapshot_2_arg1 ∧ __snapshot_2_arg1 ≤ __snapshot_2_arg1

7.1.3.2.9 Invariant Updates

The following invariants are asserted.

0:	TRUE
1:	TRUE
2:	1 − arg4 ≤ 0 ∨ 1 ≤ 0 ∨ − arg4 ≤ 0
3:	TRUE
1:	FALSE
2:	1 − arg4 ≤ 0 ∨ 1 − __snapshot_2_arg3 + arg3 ≤ 0 ∧ 1 − __snapshot_2_arg3 ≤ 0 ∧ − arg4 ≤ 0 ∨ − arg4 ≤ 0
1_var_snapshot:	1 ≤ 0
1*:	1 ≤ 0
2_var_snapshot:	− __snapshot_2_arg3 + arg3 ≤ 0 ∧ 1 − __snapshot_2_arg3 + arg3 − arg4 ≤ 0 ∧ 1 − arg4 ≤ 0 ∨ − __snapshot_2_arg3 + arg3 ≤ 0 ∧ − arg4 ≤ 0
2*:	1 ≤ 0 ∨ 1 − __snapshot_2_arg3 + arg3 ≤ 0 ∧ 1 − __snapshot_2_arg3 ≤ 0 ∧ − arg4 ≤ 0

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(3)	TRUE
1	(0)	TRUE
2	(1)	TRUE
3	(2)	1 − arg4 ≤ 0
8	(1)	TRUE
9	(2)	1 ≤ 0
10	(2)	1 ≤ 0
11	(2)	− arg4 ≤ 0
12	(2)	1 − arg4 ≤ 0
13	(2_var_snapshot)	− __snapshot_2_arg3 + arg3 ≤ 0 ∧ 1 − __snapshot_2_arg3 + arg3 − arg4 ≤ 0 ∧ 1 − arg4 ≤ 0
18	(2*)	1 ≤ 0
19	(2*)	1 − __snapshot_2_arg3 + arg3 ≤ 0 ∧ 1 − __snapshot_2_arg3 ≤ 0 ∧ − arg4 ≤ 0
20	(2)	1 − __snapshot_2_arg3 + arg3 ≤ 0 ∧ 1 − __snapshot_2_arg3 ≤ 0 ∧ − arg4 ≤ 0
21	(2_var_snapshot)	− __snapshot_2_arg3 + arg3 ≤ 0 ∧ − arg4 ≤ 0
22	(2_var_snapshot)	− __snapshot_2_arg3 + arg3 ≤ 0 ∧ − arg4 ≤ 0
30	(1)	TRUE
31	(2)	1 ≤ 0
32	(2)	1 ≤ 0
33	(2)	− arg4 ≤ 0
34	(2)	− arg4 ≤ 0
35	(2_var_snapshot)	− __snapshot_2_arg3 + arg3 ≤ 0 ∧ − arg4 ≤ 0
38	(2*)	1 ≤ 0
39	(2*)	1 − __snapshot_2_arg3 + arg3 ≤ 0 ∧ 1 − __snapshot_2_arg3 ≤ 0 ∧ − arg4 ≤ 0

initial node: 0
cover edges:

8 → 2

21 → 22

30 → 2

33 → 11

35 → 22

39 → 19

transition edges:

0	6 1
1	0 2
2	1 3
3	2 8
3	3 9
3	4 10
3	5 11
3	14 12
11	2 30
11	3 31
11	4 32
11	5 33
11	14 34
12	15 13
13	3 18
13	5 19
19	17 20
20	15 21
20	15 22
22	3 38
22	5 39
34	15 35

7.1.3.2.10 Transition Removal

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

1:	__snapshot_2_arg3
2:	arg3
1_var_snapshot:	__snapshot_2_arg3
1*:	__snapshot_2_arg3
2_var_snapshot:	__snapshot_2_arg3
2*:	__snapshot_2_arg3

7.1.3.2.11 Transition Removal

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

1:	−1
2:	−2
1_var_snapshot:	−3
1*:	−4
2_var_snapshot:	−5
2*:	−6

7.1.3.2.12 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert

version: 1.0

8	→ 2
21	→ 22
30	→ 2
33	→ 11
35	→ 22
39	→ 19