# Model terminator¶

Cited in: [CookPR06] fig. 3 p. 4.

Tag: complexity.

## Source code¶

```model cook_podelski_rybalchenko_pldi06_04 {

var x0, z0, x, z, n, c1, c2;

states q1, q2;

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

transition t3 := {
from   := q2;
to     := q1;
guard  := z <= x;
action := z' = z + 1, c2' = c2 + 1;
};

transition t2 := {
from   := q2;
to     := q1;
guard  := z > x;
action := x' = x + 1, c1' = c1 + 1;
};

}

strategy cook_podelski_rybalchenko_pldi06_04_s {

Region init := {state = q1 && x = x0 && z = z0 && c1 = 0 && c2 = 0 && n >= x0 && n >= z0};

}```

## Expected invariant¶

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

## Results¶

• With Aspic: { q1[x0, z0, x, z, n, -x0 + x, -z0 + z] : n >= z0 and n >= x0 and n >= z and z >= z0 and x >= x0; q2[x0, z0, x, z, n, -x0 + x, -z0 + z] : n >= z and n >= 1 + x and z >= z0 and n >= z0 and x >= x0 } (0.08s), failed.
• With ISL: { q1[x0__1, z0__1, x__1, z__1, n__1, -x0__1 + x__1, -z0__1 + z__1] : (n__1 >= 1 + x0__1 and n__1 >= z0__1 and z__1 >= 1 + x0__1 + z0__1 - x__1 and n__1 >= 1 + x__1 and z__1 <= 1 + x__1 and z__1 >= z0__1 and x__1 >= x0__1) or (n__1 >= 1 + x0__1 and n__1 >= z0__1 and z__1 >= 1 + x0__1 + z0__1 - x__1 and n__1 >= x__1 and z__1 >= x__1 and z__1 >= z0__1 and x__1 >= x0__1); q1[x0, z0, x0, z0, n, 0, 0] : n >= x0 and n >= z0; q2[x0__1, z0__1, x__1, z__1, n__1, -x0__1 + x__1, -z0__1 + z__1] : n__1 >= x0__1 and n__1 >= z0__1 and n__1 >= 1 + x__1 and z__1 >= z0__1 and x__1 >= x0__1 and z__1 >= 1 + x0__1 + z0__1 - x__1; q2[x0__1, z0__1, x0__1, z0__1, n__1, 0, 0] : n__1 >= 1 + x0__1 and n__1 >= z0__1 } (0.25s), failed.