Model gulwani1_alt¶
Cited in: [Gulwani09] fig. 1b p. 3.
Tag: complexity.
Figure¶
Source code¶
model gulwani_cav09_03b {
var x, y, i1, i2, m;
states q;
transition t2 := {
from := q;
to := q;
guard := x < 100 && y >= m;
action := x' = x + 1, i2' = i2 + 1;
};
transition t1 := {
from := q;
to := q;
guard := x < 100 && y < m;
action := y' = y + 1, i1' = i1 + 1;
};
}
strategy gulwani_cav09_03b_s {
Region init := {state = q && x = 0 && y = 0 && m >= 0 && i1 = 0 && i2 = 0};
}
Expected invariant¶
{ q[v1, v2, v3, v4, v5] : v5 >= -100 + v3 + v4 }
Results¶
- With Aspic: { q[x, y, y, x, m] : x >= 0 and y >= 0 and m >= 0 and m >= y and x <= 100 } (0.06s), OK.
- With ISL: { q[x__1, y__1, y__1, x__1, y__1] : y__1 >= 1 and x__1 >= 1 and x__1 <= 100; q[0, y__1, y__1, 0, m__1] : m__1 >= 1 and y__1 >= 1 and m__1 >= y__1; q[x__1, 0, 0, x__1, 0] : x__1 <= 100 and x__1 >= 1; q[0, 0, 0, 0, m] : m >= 0 } (0.01s), OK.