Model counters4¶
Cited in: [GulwaniMC09] fig. 3 p. 6.
Tag: complexity.
Figure¶
Source code¶
model gulwani_mehra_chilimbi_popl09_06d {
var x, y, n, m, c;
states q;
transition t2 := {
from := q;
to := q;
guard := x >= n && y < m;
action := x' = x + 1, y' = y + 1, c' = c + 1;
};
transition t1 := {
from := q;
to := q;
guard := x < n;
action := x' = x + 1, y' = y + 1, c' = c + 1;
};
}
strategy gulwani_mehra_chilimbi_popl09_06d_s {
Region init := {state = q && x = 0 && y = 0 && c = 0 && n >= 0 && m >= 0};
}
Expected invariant¶
{ q[v1, v2, v3, v4, v5] : v5 <= v3 or (v5 >= 1 + v3 and v5 <= v4) }
Results¶
- With Aspic: { q[x, x, n, m, x] : x >= 0 and n >= 0 and m >= 0 and m >= x - n } (0.05s), failed.
- With ISL: { q[x__1, x__1, n__1, m__1, x__1] : (n__1 >= 1 and m__1 >= 0 and x__1 >= 1 and n__1 >= x__1) or (n__1 >= 1 and m__1 >= 0 and m__1 >= x__1 and n__1 <= -1 + x__1); q[0, 0, n, m, 0] : n >= 0 and m >= 0; q[x__1, x__1, 0, m__1, x__1] : x__1 >= 1 and m__1 >= 1 and m__1 >= x__1 } (0.02s), OK.