Model microsoftex2¶
Cited in: [GulwaniZ10] fig. 2 p. 4.
Tag: complexity.
Figure¶
Source code¶
model gulwani_zuleger_pldi10_04a {
var n, n0, m, i;
states q1, q2;
transition t1 := {
from := q1;
to := q2;
guard := n > 0 && m > 0;
action := n' = n - 1, m' = m - 1, i' = i + 1;
};
transition t3 := {
from := q2;
to := q1;
guard := true;
action := ;
};
transition t2 := {
from := q2;
to := q2;
guard := true;
action := n' = n - 1, m' = m + 1;
};
}
strategy gulwani_zuleger_pldi10_04a_s {
Region init := {state = q1 && n > 0 && m > 0 && n = n0 && i = 0};
}
Expected invariant¶
{ q2[v1, v2, v3, v4] : v4 <= v2; q1[v1, v2, v3, v4] : v4 <= v2 }
Results¶
- With Aspic: { q2[n, n0, m, i] : i >= 1 and i <= -n + n0 and i <= n0 and m >= 0 and 2i >= 1 - n + n0 - m; q1[n, n0, m, i] : m >= 0 and i >= 0 and i <= -n + n0 and n0 >= 1 and 2i >= 1 - n + n0 - m } (0.04s), failed.
- With ISL: { q2[n__1, n0__1, m__1, i__1] : n0__1 >= 1 and 2i__1 >= 1 - n__1 + n0__1 - m__1 and n0__1 >= 1 + n__1 and i__1 >= 1 and i__1 <= -n__1 + n0__1; q1[n__1, n0__1, m__1, i__1] : n0__1 >= 1 and 2i__1 >= 1 - n__1 + n0__1 - m__1 and n0__1 >= 1 + n__1 and i__1 >= 1 and i__1 <= -n__1 + n0__1; q1[n, n, m, 0] : n >= 1 and m >= 1 } (0.00s), failed.