# Model microsoftex7¶

Cited in: [GulwaniZ10] fig. 3 p. 3.

Tag: complexity.

## Figure¶ ## Source code¶

```model gulwani_zuleger_pldi10_03b {

var n, m, j;

states q1, q2;

transition t1b := {
from   := q1;
to     := q2;
guard  := j > n;
action := ;
};

transition t1a := {
from   := q1;
to     := q2;
guard  := j < n;
action := ;
};

transition t3 := {
from   := q2;
to     := q1;
guard  := j <= m;
action := j' = j + 1;
};

transition t2 := {
from   := q2;
to     := q1;
guard  := j > m;
action := j' = 0;
};

}

strategy gulwani_zuleger_pldi10_03b_s {

Region init := {state = q1 && 0 < n && n < m && j = n + 1};

}```

## Expected invariant¶

`{ q2[v1, v2, v3] : v1 >= 1 and v3 <= 1 + v2 and v3 >= 0 and v2 >= 1 + v1; q1[v1, v2, v3] : v3 >= 0 and v3 <= 1 + v2 and v1 >= 1 and v2 >= 1 + v1 }`

## Results¶

• With Aspic: { q2[n, m, j] : n >= 1 and j <= 1 + m and j >= 0 and m >= 1 + n; q1[n, m, j] : j >= 0 and j <= 1 + m and n >= 1 and m >= 1 + n } (0.05s), OK.
• With ISL: { q2[n__1, m__1, j__1] : (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 <= 1 + m__1 and j__1 <= -1 + n__1) or (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 >= 1 + n__1 and j__1 <= 1 + m__1) or (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 <= -1 + n__1) or (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 >= 1 + n__1 and j__1 <= 1 + m__1); q2[n__1, m__1, 0] : n__1 >= 1 and m__1 >= 1 + n__1; q2[n__1, m__1, 1 + n__1] : n__1 >= 1 and m__1 >= 1 + n__1; q1[n__1, m__1, j__1] : (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 <= n__1) or (n__1 >= 1 and m__1 >= 1 + n__1 and j__1 >= 2 + n__1 and j__1 <= 1 + m__1); q1[n__1, m__1, 0] : n__1 >= 1 and m__1 >= 1 + n__1; q1[n, m, 1 + n] : n >= 1 and m >= 1 + n } (2.93s), failed.