# Model multcounters1¶

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

Tag: complexity.

## Source code¶

```model gulwani_mehra_chilimbi_popl09_06e {

var x, y, n, m, c1, c2;

states q1, q2;

transition t1 := {
from   := q1;
to     := q2;
guard  := x < n;
action := ;
};

transition t3 := {
from   := q2;
to     := q1;
guard  := y >= m;
action := x' = x + 1, c2' = c2 + 1;
};

transition t2 := {
from   := q2;
to     := q1;
guard  := y < m;
action := y' = y + 1, c1' = c1 + 1;
};

}

strategy gulwani_mehra_chilimbi_popl09_06e_s {

Region init := {state = q1 && x = 0 && y = 0 && c1 = 0 && c2 = 0 && n >= 0 && m >= 0};

}```

## Expected invariant¶

`{ q2[v1, v2, v3, v4, v5, v6] : v6 <= v3 + v4 - v5; q1[v1, v2, v3, v4, v5, v6] : v6 <= v3 + v4 - v5 }`

## Results¶

• With Aspic: { q1[x, y, n, m, y, x] : m >= y and x >= 0 and y >= 0 and n >= 0 and m >= 0; q2[x, y, n, m, y, x] : x >= 0 and y >= 0 and m >= 0 and m >= y and n >= 1 + x } (0.04s), failed.
• With ISL: { q2[x__1, y__1, n__1, y__1, y__1, x__1] : n__1 >= 0 and y__1 >= 1 and n__1 >= 1 + x__1 and x__1 >= 1; q2[0, y__1, n__1, m__1, y__1, 0] : n__1 >= 1 and m__1 >= 0 and y__1 >= 1 and m__1 >= y__1; q2[x__1, 0, n__1, 0, 0, x__1] : n__1 >= 0 and n__1 >= 1 + x__1 and x__1 >= 1; q2[0, 0, n__1, m__1, 0, 0] : n__1 >= 1 and m__1 >= 0; q1[x__1, y__1, n__1, y__1, y__1, x__1] : n__1 >= 1 and y__1 >= 1 and n__1 >= x__1 and x__1 >= 1; q1[0, y__1, n__1, m__1, y__1, 0] : n__1 >= 1 and m__1 >= 1 and m__1 >= y__1 and y__1 >= 1; q1[x__1, 0, n__1, 0, 0, x__1] : n__1 >= 1 and n__1 >= x__1 and x__1 >= 1; q1[0, 0, n, m, 0, 0] : n >= 0 and m >= 0 } (0.03s), OK.