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