Model ax¶

Cited in: [AliasDFG10].

Tag: complexity.

Source code¶

```model ax {

var i, j, n;

states start, stop, lbl_7_1, cut;

transition t_26 := {
from   := start;
to     := stop;
guard  := n <= 1;
action := i' = 1, j' = 0;
};

transition t_24 := {
from   := start;
to     := lbl_7_1;
guard  := 2 <= n;
action := i' = 0, j' = 1;
};

transition t_20 := {
from   := lbl_7_1;
to     := stop;
guard  := n <= i + 2 && n <= j + 1;
action := i' = i + 1;
};

transition t_19 := {
from   := lbl_7_1;
to     := cut;
guard  := i + 3 <= n && n <= j + 1;
action := i' = i + 1;
};

transition t_18 := {
from   := lbl_7_1;
to     := lbl_7_1;
guard  := j + 2 <= n;
action := j' = j + 1;
};

transition t_23 := {
from   := cut;
to     := stop;
guard  := n <= i + 2 && n <= 1;
action := i' = i + 1, j' = 0;
};

transition t_21 := {
from   := cut;
to     := lbl_7_1;
guard  := 2 <= n;
action := j' = 1;
};

transition t_22 := {
from   := cut;
to     := cut;
guard  := i + 3 <= n && n <= 1;
action := i' = i + 1, j' = 0;
};

}

strategy ax_s {

Region init := {state = start};

}```

Expected invariant¶

`{ cut[v1, v2, 1 + v2] : v2 >= 1 + v1 and v1 >= 1; stop[v1, v2, v3] : v2 <= v1 and v2 >= -1 + v1 and v3 <= 1 + v2 and v1 >= 1; lbl_7_1[v1, v2, v3] : v3 >= 1 + v2 and v3 >= 2 + v1 and v2 >= 1 and v1 >= 0 }`

Results¶

• With Aspic: { start[i, j, n]; cut[i, j, 1 + j] : j >= 1 + i and i >= 1; lbl_7_1[i, j, n] : n >= 1 + j and n >= 2 + i and j >= 1 and i >= 0; stop[i, j, n] : j <= i and j >= -1 + i and n <= 1 + j and i >= 1 } (0.06s), OK.
• With ISL: { stop[i__1, i__1, 1 + i__1] : i__1 >= 2; stop[1, 0, n__1] : n__1 <= 1; stop[1, 1, 2]; cut[i__1, j__1, 1 + j__1] : j__1 >= 1 and i__1 >= 2 and j__1 >= 1 + i__1; cut[1, j__1, 1 + j__1] : j__1 >= 2; lbl_7_1[i__1, j__1, n__1] : n__1 >= 2 and j__1 >= 1 and n__1 >= 2 + i__1 and i__1 >= 1 and n__1 >= 1 + j__1; lbl_7_1[0, j__1, n__1] : n__1 >= 2 and j__1 >= 2 and n__1 >= 1 + j__1; lbl_7_1[0, 1, n__1] : n__1 >= 2; start[i, j, n] } (0.02s), OK.