by T2Cert
0 | 0 | 1: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − x_0 + x_post ≤ 0 ∧ −1 + x_0 − x_post ≤ 0 ∧ 201 − x_post ≤ 0 ∧ x_0 − x_post ≤ 0 ∧ − x_0 + x_post ≤ 0 | |
1 | 1 | 0: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 | |
2 | 2 | 0: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 | |
3 | 3 | 2: | 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 |
The following invariants are asserted.
0: | TRUE |
1: | 201 − x_0 ≤ 0 ∧ 201 − x_post ≤ 0 |
2: | TRUE |
3: | TRUE |
The invariants are proved as follows.
0 | (0) | TRUE | ||
1 | (1) | 201 − x_0 ≤ 0 ∧ 201 − x_post ≤ 0 | ||
2 | (2) | TRUE | ||
3 | (3) | TRUE |
0 | 0 1 | |
1 | 1 0 | |
2 | 2 0 | |
3 | 3 2 |
0 | 4 | : | − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0 |
We remove transitions
, using the following ranking functions, which are bounded by −11.3: | 0 |
2: | 0 |
0: | 0 |
1: | 0 |
: | −4 |
: | −5 |
: | −6 |
: | −6 |
: | −6 |
: | −6 |
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
7 : − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_0 ≤ 0
The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.
5 : − x_post + x_post ≤ 0 ∧ x_post − x_post ≤ 0 ∧ − x_0 + x_0 ≤ 0 ∧ x_0 − x_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 804.: | −1 + 4⋅x_0 |
: | 1 + 4⋅x_0 |
: | −2 + 4⋅x_0 |
: | 4⋅x_0 |
We remove transitions 5, 7 using the following ranking functions, which are bounded by −1.
: | 0 |
: | 0 |
: | −1 |
: | 1 |
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