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