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