Model wcet1¶
Cited in: [AliasDFG10].
Tag: complexity.
Figure¶
Source code¶
model main {
var i, j, n, tmp_1;
states start, stop, cut;
transition t_73 := {
from := start;
to := stop;
guard := 1 = n;
action := i' = n - 1, j' = 0, tmp_1' = 0;
};
transition t_70 := {
from := start;
to := cut;
guard := 2 <= n;
action := i' = n - 1, j' = 1, tmp_1' = 0;
};
transition t_69 := {
from := start;
to := stop;
guard := 1 = n;
action := i' = n - 1, j' = 0;
};
transition t_68 := {
from := start;
to := cut;
guard := 2 <= n;
action := i' = n - 1, j' = 0;
};
transition t_43 := {
from := start;
to := stop;
guard := n <= 0;
action := i' = n, j' = 0;
};
transition t_65 := {
from := cut;
to := stop;
guard := i <= 1 && n <= j + 1;
action := i' = i - 1, j' = 0, tmp_1' = j;
};
transition t_63 := {
from := cut;
to := stop;
guard := i <= 1 && j + 2 <= n;
action := i' = i - 1, j' = j + 1, tmp_1' = j;
};
transition t_61 := {
from := cut;
to := stop;
guard := i <= 1 && j <= 1;
action := i' = i - 1, j' = 0;
};
transition t_59 := {
from := cut;
to := stop;
guard := i <= 1 && 2 <= j;
action := i' = i - 1, j' = j - 1;
};
transition t_64 := {
from := cut;
to := cut;
guard := 2 <= i && n <= j + 1;
action := i' = i - 1, j' = 0, tmp_1' = j;
};
transition t_62 := {
from := cut;
to := cut;
guard := 2 <= i && j + 2 <= n;
action := i' = i - 1, j' = j + 1, tmp_1' = j;
};
transition t_60 := {
from := cut;
to := cut;
guard := 2 <= i && j <= 1;
action := i' = i - 1, j' = 0;
};
transition t_58 := {
from := cut;
to := cut;
guard := 2 <= i && 2 <= j;
action := i' = i - 1, j' = j - 1;
};
}
strategy main_s {
Region init := {state = start};
}
Expected invariant¶
{ stop[v1, v2, v3, v4] : v3 >= v1 + v2 and v2 >= 0 and v1 <= 0; cut[v1, v2, v3, v4] : v3 >= v1 + v2 and v3 >= 1 + v1 and v2 >= 0 and v1 >= 1 }
Results¶
- With Aspic: { start[i, j, n, tmp_1]; cut[i, j, n, tmp_1] : n >= i + j and n >= 1 + i and j >= 0 and i >= 1; stop[i, j, n, tmp_1] : n >= i + j and j >= 0 and i <= 0 } (0.08s), OK.
- With ISL: { start[i, j, n, tmp_1]; stop[0, j__1, n__1, tmp_1__1] : (n__1 >= 3 and j__1 >= 1) or (n__1 >= 3 and j__1 >= 1); stop[0, 0, 1, tmp_1__1]; stop[i__1, 0, i__1, tmp_1__1] : i__1 <= 0; stop[0, j__1, n__1, j__1] : (n__1 >= 3 and n__1 >= 2 + j__1 and j__1 >= 1) or (n__1 >= 3 and n__1 >= 2 + j__1 and j__1 >= 1); stop[0, 0, n__1, 1 - n__1] : n__1 >= 3; stop[0, 0, n__1, tmp_1__1] : (n__1 >= 3 and tmp_1__1 <= -2 + n__1 and tmp_1__1 <= 0) or n__1 >= 3 or (n__1 >= 3 and tmp_1__1 <= -2 + n__1 and tmp_1__1 <= 0) or n__1 >= 3 or (n__1 >= 3 and tmp_1__1 >= 0 and tmp_1__1 >= -1 + n__1) or (n__1 >= 3 and tmp_1__1 >= 0 and tmp_1__1 >= -1 + n__1); stop[0, j__1, 3 - j__1, -1 + j__1] : j__1 <= 0; stop[0, 0, n__1, -1 + n__1] : n__1 >= 3 or n__1 >= 3; stop[0, 0, 1, 0]; stop[0, 0, 2, 1]; stop[0, 1, 3, 0]; stop[0, j__1, n__1, -1 + j__1] : (n__1 >= 3 and n__1 >= 1 + j__1) or (n__1 >= 3 and j__1 >= 1 and n__1 >= 1 + j__1) or (n__1 >= 3 and n__1 >= 1 + j__1) or (n__1 >= 3 and j__1 >= 1 and n__1 >= 1 + j__1); stop[0, 0, 3, 0]; stop[0, 1, 2, 0]; stop[0, 0, 2, 0]; stop[0, 0, 2, tmp_1__1]; cut[i__1, j__1, n__1, tmp_1__1] : (n__1 >= 3 and n__1 >= 2 + i__1 and i__1 >= 1 and j__1 >= 0) or (n__1 >= 3 and n__1 >= 2 + i__1 and i__1 >= 1 and j__1 >= 0); cut[i__1, 0, 2 + i__1, 0] : i__1 >= 1; cut[i__1, j__1, n__1, -1 + j__1] : (n__1 >= 3 and n__1 >= 2 + i__1 and i__1 >= 1 and n__1 >= 1 + j__1) or (n__1 >= 3 and n__1 >= 2 + i__1 and i__1 >= 1 and n__1 >= 1 + j__1); cut[i__1, 1, 1 + i__1, 0] : i__1 >= 1; cut[i__1, 0, 1 + i__1, tmp_1__1] : i__1 >= 1; cut[i__1, j__1, 1 + i__1 - j__1, -1 + j__1] : j__1 <= -2 + i__1 and j__1 <= -1 and i__1 >= 1 and 2j__1 <= i__1 } (0.07s), failed.