# Model gulwani3¶

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

Tag: complexity.

## Source code¶

```model gulwani_cav09_06 {

var x, y, n, i1, i2;

states q1, q2;

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

transition t3 := {
from   := q2;
to     := q1;
guard  := true;
action := x' = y + 1;
};

transition t2 := {
from   := q2;
to     := q2;
guard  := y < n;
action := i2' = i2 + 1, y' = y + 1;
};

}

strategy gulwani_cav09_06_s {

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

}```

## Expected invariant¶

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

## Results¶

• With Aspic: { q2[x, y, n, i1, 1 + y - i1] : n >= 1 + x and y >= x and i1 >= 1 and i1 <= 1 + x and n >= y; q1[x, y, n, i1, x - i1] : i1 <= x and i1 >= 0 and i1 <= n and i1 >= x - n and n >= 0 and 2i1 >= x - n } (0.06s), OK.
• With ISL: { q1[x__1, -1 + x__1, n__1, i1__1, x__1 - i1__1] : n__1 >= 0 and i1__1 >= 2 and i1__1 <= x__1 and n__1 >= -1 + x__1; q1[0, y, n, 0, 0] : n >= 0; q1[x__1, -1 + x__1, n__1, 1, -1 + x__1] : n__1 >= 0 and n__1 >= -1 + x__1 and x__1 >= 2; q1[1, 0, n__1, 1, 0] : n__1 >= 1; q2[x__1, y__1, n__1, i1__1, 1 + y__1 - i1__1] : n__1 >= 0 and i1__1 >= 2 and i1__1 <= 1 + y__1 and n__1 >= y__1; q2[0, y__1, n__1, 1, y__1] : n__1 >= 0 and n__1 >= y__1 and y__1 >= 1; q2[0, 0, n__1, 1, 0] : n__1 >= 1 } (0.04s), OK.