Model easy1¶
Cited in: [ChawdharyCGSY08].
Tag: complexity.
Figure¶
Source code¶
model main {
var x, y, z;
states start, lbl_11_1, lbl_9_1, stop;
transition t_23 := {
from := start;
to := lbl_11_1;
guard := z + 1 <= 0 || 1 <= z;
action := x' = 2, y' = 100;
};
transition t_22 := {
from := start;
to := lbl_9_1;
guard := 0 = z;
action := x' = 1, y' = 100;
};
transition t_19 := {
from := lbl_11_1;
to := lbl_9_1;
guard := x <= 39 && 0 = z;
action := x' = x + 1;
};
transition t_18 := {
from := lbl_11_1;
to := stop;
guard := 40 <= x;
action := ;
};
transition t_20 := {
from := lbl_11_1;
to := lbl_11_1;
guard := x <= 39 && z + 1 <= 0 || x <= 39 && 1 <= z;
action := x' = x + 2;
};
transition t_17 := {
from := lbl_9_1;
to := lbl_11_1;
guard := x <= 39 && z + 1 <= 0 || x <= 39 && 1 <= z;
action := x' = x + 2;
};
transition t_15 := {
from := lbl_9_1;
to := stop;
guard := 40 <= x;
action := ;
};
transition t_16 := {
from := lbl_9_1;
to := lbl_9_1;
guard := x <= 39 && 0 = z;
action := x' = x + 1;
};
}
strategy main_s {
Region init := {state = start};
}
Expected invariant¶
{ stop[v1, 100, v3] : v1 >= 40 and v1 <= 41; lbl_9_1[v1, 100, 0] : v1 >= 1 and v1 <= 40; lbl_11_1[v1, 100, v3] : v1 >= 2 and v1 <= 41 }
Results¶
- With Aspic: { lbl_11_1[x, 100, z] : x >= 2 and x <= 41; start[x, y, z]; stop[x, 100, z] : x >= 40 and x <= 41; lbl_9_1[x, 100, 0] : x >= 1 and x <= 40 } (0.06s), OK.
- With ISL: { stop[x__1, 100, z__1] : (exists (e0 = [(x__1)/2]: 2e0 = x__1 and z__1 >= 1 and x__1 <= 41 and x__1 >= 40)) or (exists (e0 = [(x__1)/2]: 2e0 = x__1 and z__1 <= -1 and x__1 <= 41 and x__1 >= 40)); stop[40, 100, 0]; lbl_9_1[x__1, 100, 0] : x__1 >= 2 and x__1 <= 40; lbl_9_1[1, 100, 0]; lbl_11_1[x__1, 100, z__1] : (exists (e0 = [(x__1)/2]: 2e0 = x__1 and z__1 >= 1 and x__1 <= 41 and x__1 >= 4)) or (exists (e0 = [(x__1)/2]: 2e0 = x__1 and z__1 <= -1 and x__1 <= 41 and x__1 >= 4)); lbl_11_1[2, 100, z__1] : z__1 >= 1 or z__1 <= -1; start[x, y, z] } (0.01s), OK.