# Model determinant¶

Cited in: [AliasDFG10].

Tag: complexity.

## Source code¶

```model determinant {

var i, j, k, n;

states start, a, d, halt, b, c;

transition t0 := {
from   := start;
to     := a;
guard  := n >= 1;
action := ;
};

transition t1 := {
from   := a;
to     := d;
guard  := true;
action := k' = 1;
};

transition t3 := {
from   := d;
to     := halt;
guard  := k >= n;
action := i' = i;
};

transition t2 := {
from   := d;
to     := b;
guard  := k < n;
action := i' = k + 1;
};

transition t5 := {
from   := b;
to     := c;
guard  := i <= n;
action := j' = n;
};

transition t4 := {
from   := b;
to     := d;
guard  := i > n;
action := k' = k + 1;
};

transition t7 := {
from   := c;
to     := b;
guard  := j <= k;
action := i' = i + 1;
};

transition t6 := {
from   := c;
to     := c;
guard  := j > k;
action := j' = j - 1;
};

}

strategy determinant_s {

Region init := {state = start};

}```

## Expected invariant¶

`{ d[v1, v2, v3, v4] : v4 >= v3 and v3 >= 1; a[v1, v2, v3, v4] : v4 >= 1; halt[v1, v2, v3, v3] : v3 >= 1; b[v1, v2, v3, v4] : v4 >= -1 + v1 and v3 <= -1 + v1 and v4 >= 1 + v3 and v3 >= 1; c[v1, v2, v3, v4] : v4 >= v1 and v4 >= v2 and v3 >= 1 and v3 <= v2 and v3 <= -1 + v1 }`

## Results¶

• With Aspic: { start[i, j, k, n]; a[i, j, k, n] : n >= 1; halt[i, j, k, k] : k >= 1; b[i, j, k, n] : n >= -1 + i and k <= -1 + i and n >= 1 + k and k >= 1; c[i, j, k, n] : n >= i and n >= j and k >= 1 and k <= j and k <= -1 + i; d[i, j, k, n] : n >= k and n >= 1 and k >= 1 } (0.05s), OK.
• With ISL: { halt[i__1, j__1, 1, 1]; halt[i__1, -2 + i__1, -1 + i__1, -1 + i__1] : i__1 >= 3; start[i, j, k, n]; a[i__1, j__1, k__1, n__1] : n__1 >= 1; c[i__1, j__1, k__1, n__1] : n__1 >= 1 and n__1 >= i__1 and n__1 >= j__1 and k__1 >= 1 and n__1 >= 2 - i__1 + j__1 + k__1 and k__1 <= -1 + i__1 and k__1 <= j__1; c[i__1, j__1, -1 + i__1, j__1] : j__1 >= 1 and i__1 >= 2 and j__1 >= i__1; d[i__1, j__1, 1, n__1] : n__1 >= 1; d[i__1, j__1, 1 + j__1, -1 + i__1] : i__1 >= 3 and j__1 >= 1 and j__1 <= -2 + i__1; b[i__1, j__1, j__1, n__1] : n__1 >= 1 and n__1 >= -1 + i__1 and j__1 <= -2 + i__1 and j__1 >= 1; b[2, j__1, 1, n__1] : n__1 >= 2; b[i__1, -2 + i__1, -1 + i__1, n__1] : n__1 >= 1 and i__1 >= 3 and n__1 >= i__1 } (0.08s), OK.