Model while2¶
Cited in: [AliasDFG10].
Tag: complexity.
Figure¶
Source code¶
model main {
var N, i, j;
states start, lbl_6_2, lbl_7_2, stop;
transition t_25 := {
from := start;
to := lbl_6_2;
guard := 1 <= N;
action := i' = N, j' = N - 1;
};
transition t_18 := {
from := start;
to := stop;
guard := N <= 0;
action := i' = N;
};
transition t_20 := {
from := lbl_6_2;
to := lbl_7_2;
guard := j <= 0;
action := i' = i - 1;
};
transition t_21 := {
from := lbl_6_2;
to := lbl_6_2;
guard := 1 <= j;
action := j' = j - 1;
};
transition t_23 := {
from := lbl_7_2;
to := lbl_6_2;
guard := 1 <= N && 1 <= i;
action := j' = N - 1;
};
transition t_16 := {
from := lbl_7_2;
to := stop;
guard := i <= 0;
action := ;
};
transition t_22 := {
from := lbl_7_2;
to := lbl_7_2;
guard := N <= 0 && 1 <= i;
action := i' = i - 1, j' = N;
};
}
strategy main_s {
Region init := {state = start};
}
Expected invariant¶
{ stop[v1, v2, v3] : v2 <= v1 and v2 <= 0; lbl_7_2[v1, v2, 0] : v2 <= -1 + v1 and v2 >= 0; lbl_6_2[v1, v2, v3] : v3 >= 0 and v2 >= 1 and v2 <= v1 and v3 <= -1 + v1 }
Results¶
- With Aspic: { start[N, i, j]; lbl_6_2[N, i, j] : j >= 0 and i >= 1 and i <= N and j <= -1 + N; lbl_7_2[N, i, 0] : i <= -1 + N and i >= 0; stop[N, i, j] : i <= N and i <= 0 } (0.24s), OK.
- With ISL: { stop[N__1, N__1, j__1] : N__1 <= 0; stop[N__1, 0, 0] : N__1 >= 2; stop[1, 0, 0]; lbl_7_2[N__1, i__1, 0] : N__1 >= 1 and i__1 >= 0 and i__1 <= -2 + N__1; lbl_7_2[N__1, -1 + N__1, 0] : N__1 >= 2; lbl_7_2[1, 0, 0]; lbl_6_2[N__1, i__1, j__1] : N__1 >= 1 and i__1 <= -1 + N__1 and i__1 >= 1 and j__1 >= 0 and j__1 <= -1 + N__1; lbl_6_2[N__1, N__1, j__1] : N__1 >= 1 and j__1 <= -2 + N__1 and j__1 >= 0; lbl_6_2[N__1, N__1, -1 + N__1] : N__1 >= 1; start[N, i, j] } (0.07s), OK.