# Model easy1¶

Cited in: [ChawdharyCGSY08].

Tag: complexity.

## 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.