Model counters2¶

Cited in: [GulwaniMC09] fig. 3 p. 6.

Tag: complexity.

Source code¶

```model gulwani_mehra_chilimbi_popl09_06b {

var x, n, c;

states q1, q2;

transition t2 := {
from   := q1;
to     := q2;
guard  := true;
action := ;
};

transition t1 := {
from   := q1;
to     := q1;
guard  := x < n;
action := x' = x + 1, c' = c + 1;
};

transition t3 := {
from   := q2;
to     := q2;
guard  := x < n;
action := x' = x + 1, c' = c + 1;
};

}

strategy gulwani_mehra_chilimbi_popl09_06b_s {

Region init := {state = q1 && x = 0 && c = 0 && n >= 0};

}```

Expected invariant¶

`{ q2[v1, v2, v3] : v3 <= v2; q1[v1, v2, v3] : v3 <= v2 }`

Results¶

• With Aspic: { q2[x, n, x] : n >= 0 and x >= 0 and n >= x; q1[x, n, x] : n >= 0 and n >= x and x >= 0 } (0.05s), OK.
• With ISL: { q2[x__1, n__1, x__1] : (n__1 >= 1 and x__1 >= 1 and n__1 >= x__1) or (n__1 >= 1 and x__1 >= 1 and n__1 >= x__1) or (n__1 >= 0 and n__1 >= x__1 and x__1 >= 2); q2[0, n__1, 0] : n__1 >= 0; q1[x__1, n__1, x__1] : n__1 >= 1 and x__1 >= 1 and n__1 >= x__1; q1[0, n, 0] : n >= 0 } (0.00s), OK.