Model ax¶
Cited in: [AliasDFG10].
Tag: complexity.
Figure¶
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.