by T2Cert
0 | 0 | 1: | 1 − copied_0 ≤ 0 ∧ − e_0 + olde_0 ≤ 0 ∧ n_0 − oldn_0 ≤ 0 ∧ − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 | |
0 | 1 | 2: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ copied_0 ≤ 0 ∧ −1 + copied_post ≤ 0 ∧ 1 − copied_post ≤ 0 ∧ − n_0 + oldn_post ≤ 0 ∧ n_0 − oldn_post ≤ 0 ∧ − e_0 + olde_post ≤ 0 ∧ e_0 − olde_post ≤ 0 ∧ 1 − e_0 ≤ 0 ∧ −100 + n_0 ≤ 0 ∧ −11 − n_0 + n_post ≤ 0 ∧ 11 + n_0 − n_post ≤ 0 ∧ −1 − e_0 + e_post ≤ 0 ∧ 1 + e_0 − e_post ≤ 0 ∧ copied_0 − copied_post ≤ 0 ∧ − copied_0 + copied_post ≤ 0 ∧ e_0 − e_post ≤ 0 ∧ − e_0 + e_post ≤ 0 ∧ n_0 − n_post ≤ 0 ∧ − n_0 + n_post ≤ 0 ∧ olde_0 − olde_post ≤ 0 ∧ − olde_0 + olde_post ≤ 0 ∧ oldn_0 − oldn_post ≤ 0 ∧ − oldn_0 + oldn_post ≤ 0 | |
2 | 2 | 0: | − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 | |
0 | 3 | 3: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ copied_0 ≤ 0 ∧ −1 + copied_post ≤ 0 ∧ 1 − copied_post ≤ 0 ∧ − n_0 + oldn_post ≤ 0 ∧ n_0 − oldn_post ≤ 0 ∧ − e_0 + olde_post ≤ 0 ∧ e_0 − olde_post ≤ 0 ∧ 1 − e_0 ≤ 0 ∧ 101 − n_0 ≤ 0 ∧ 10 − n_0 + n_post ≤ 0 ∧ −10 + n_0 − n_post ≤ 0 ∧ 1 − e_0 + e_post ≤ 0 ∧ −1 + e_0 − e_post ≤ 0 ∧ copied_0 − copied_post ≤ 0 ∧ − copied_0 + copied_post ≤ 0 ∧ e_0 − e_post ≤ 0 ∧ − e_0 + e_post ≤ 0 ∧ n_0 − n_post ≤ 0 ∧ − n_0 + n_post ≤ 0 ∧ olde_0 − olde_post ≤ 0 ∧ − olde_0 + olde_post ≤ 0 ∧ oldn_0 − oldn_post ≤ 0 ∧ − oldn_0 + oldn_post ≤ 0 | |
3 | 4 | 0: | − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 | |
0 | 5 | 4: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − e_0 ≤ 0 ∧ −100 + n_0 ≤ 0 ∧ −11 − n_0 + n_post ≤ 0 ∧ 11 + n_0 − n_post ≤ 0 ∧ −1 − e_0 + e_post ≤ 0 ∧ 1 + e_0 − e_post ≤ 0 ∧ e_0 − e_post ≤ 0 ∧ − e_0 + e_post ≤ 0 ∧ n_0 − n_post ≤ 0 ∧ − n_0 + n_post ≤ 0 ∧ − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 | |
4 | 6 | 0: | − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 | |
0 | 7 | 5: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − e_0 ≤ 0 ∧ 101 − n_0 ≤ 0 ∧ 10 − n_0 + n_post ≤ 0 ∧ −10 + n_0 − n_post ≤ 0 ∧ 1 − e_0 + e_post ≤ 0 ∧ −1 + e_0 − e_post ≤ 0 ∧ e_0 − e_post ≤ 0 ∧ − e_0 + e_post ≤ 0 ∧ n_0 − n_post ≤ 0 ∧ − n_0 + n_post ≤ 0 ∧ − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 | |
5 | 8 | 0: | − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 | |
6 | 9 | 0: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ −1 + e_post ≤ 0 ∧ 1 − e_post ≤ 0 ∧ copied_post ≤ 0 ∧ − copied_post ≤ 0 ∧ copied_0 − copied_post ≤ 0 ∧ − copied_0 + copied_post ≤ 0 ∧ e_0 − e_post ≤ 0 ∧ − e_0 + e_post ≤ 0 ∧ n_0 − n_post ≤ 0 ∧ − n_0 + n_post ≤ 0 ∧ − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 | |
7 | 10 | 6: | − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 |
The following invariants are asserted.
0: | − copied_post ≤ 0 ∧ − copied_0 ≤ 0 |
1: | − copied_post ≤ 0 ∧ 1 − copied_0 ≤ 0 |
2: | −1 + copied_post ≤ 0 ∧ 1 − copied_post ≤ 0 ∧ −1 + copied_0 ≤ 0 ∧ 1 − copied_0 ≤ 0 |
3: | −1 + copied_post ≤ 0 ∧ 1 − copied_post ≤ 0 ∧ −1 + copied_0 ≤ 0 ∧ 1 − copied_0 ≤ 0 |
4: | − copied_post ≤ 0 ∧ − copied_0 ≤ 0 |
5: | − copied_post ≤ 0 ∧ − copied_0 ≤ 0 |
6: | TRUE |
7: | TRUE |
The invariants are proved as follows.
0 | (0) | − copied_post ≤ 0 ∧ − copied_0 ≤ 0 | ||
1 | (1) | − copied_post ≤ 0 ∧ 1 − copied_0 ≤ 0 | ||
2 | (2) | −1 + copied_post ≤ 0 ∧ 1 − copied_post ≤ 0 ∧ −1 + copied_0 ≤ 0 ∧ 1 − copied_0 ≤ 0 | ||
3 | (3) | −1 + copied_post ≤ 0 ∧ 1 − copied_post ≤ 0 ∧ −1 + copied_0 ≤ 0 ∧ 1 − copied_0 ≤ 0 | ||
4 | (4) | − copied_post ≤ 0 ∧ − copied_0 ≤ 0 | ||
5 | (5) | − copied_post ≤ 0 ∧ − copied_0 ≤ 0 | ||
6 | (6) | TRUE | ||
7 | (7) | TRUE |
0 | 0 1 | |
0 | 1 2 | |
0 | 3 3 | |
0 | 5 4 | |
0 | 7 5 | |
2 | 2 0 | |
3 | 4 0 | |
4 | 6 0 | |
5 | 8 0 | |
6 | 9 0 | |
7 | 10 6 |
0 | 11 | : | − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0 |
We remove transitions
, , using the following ranking functions, which are bounded by −13.7: | 0 |
6: | 0 |
0: | 0 |
2: | 0 |
3: | 0 |
4: | 0 |
5: | 0 |
1: | 0 |
: | −5 |
: | −6 |
: | −7 |
: | −7 |
: | −7 |
: | −7 |
: | −7 |
: | −7 |
: | −7 |
: | −11 |
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
14 : − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
12 : − oldn_post + oldn_post ≤ 0 ∧ oldn_post − oldn_post ≤ 0 ∧ − oldn_0 + oldn_0 ≤ 0 ∧ oldn_0 − oldn_0 ≤ 0 ∧ − olde_post + olde_post ≤ 0 ∧ olde_post − olde_post ≤ 0 ∧ − olde_0 + olde_0 ≤ 0 ∧ olde_0 − olde_0 ≤ 0 ∧ − n_post + n_post ≤ 0 ∧ n_post − n_post ≤ 0 ∧ − n_0 + n_0 ≤ 0 ∧ n_0 − n_0 ≤ 0 ∧ − e_post + e_post ≤ 0 ∧ e_post − e_post ≤ 0 ∧ − e_0 + e_0 ≤ 0 ∧ e_0 − e_0 ≤ 0 ∧ − copied_post + copied_post ≤ 0 ∧ copied_post − copied_post ≤ 0 ∧ − copied_0 + copied_0 ≤ 0 ∧ copied_0 − copied_0 ≤ 0
We consider subproblems for each of the 1 SCC(s) of the program graph.
Here we consider the SCC {
, , , , , , }.We remove transitions
, using the following ranking functions, which are bounded by −719.: | −1 + 84⋅e_0 − 8⋅n_0 |
: | copied_post + 84⋅e_0 − 8⋅n_0 |
: | 1 + 84⋅e_0 − 8⋅n_0 |
: | 1 + 84⋅e_0 − 8⋅n_0 |
: | 1 + 84⋅e_0 − 8⋅n_0 |
: | −2 + 84⋅e_0 − 8⋅n_0 |
: | 84⋅e_0 − 8⋅n_0 |
We remove transition
using the following ranking functions, which are bounded by 19.: | 30⋅e_0 |
: | 1 + 30⋅e_0 |
: | copied_post + 30⋅e_0 |
: | 1 + 30⋅e_0 |
: | 10 + 30⋅e_0 |
: | −10 + 30⋅e_0 |
: | 30⋅e_0 |
We remove transitions
, , , using the following ranking functions, which are bounded by −4.: | −1 − 4⋅copied_0 |
: | 1 − 4⋅copied_0 |
: | −3⋅copied_0 |
: | 1 − 4⋅copied_0 |
: | 1 |
: | −2 − 4⋅copied_0 |
: | −4⋅copied_0 |
We remove transitions 12, using the following ranking functions, which are bounded by −3.
: | −2 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | −3 |
: | −1 |
We remove transition 14 using the following ranking functions, which are bounded by −1.
: | −1 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
: | 0 |
We consider 1 subproblems corresponding to sets of cut-point transitions as follows.
There remain no cut-point transition to consider. Hence the cooperation termination is trivial.
T2Cert