# Model jeannet3¶

Cited in: [Jeannet_thesis] fig. 4.2 p. 41.

Tag: fixpoint.

## Source code¶

model jeannet_thesis_041 {

var x, y;

states k1, err, k2, k3, k4;

transition t5 := {
from   := k1;
to     := err;
guard  := x < y;
action := ;
};

transition t1 := {
from   := k1;
to     := k2;
guard  := x >= y;
action := x' = x + 1;
};

transition t6 := {
from   := k2;
to     := err;
guard  := x < y;
action := ;
};

transition t2 := {
from   := k2;
to     := k3;
guard  := x >= y;
action := y' = y + 1;
};

transition t7 := {
from   := k3;
to     := err;
guard  := x < y;
action := ;
};

transition t3 := {
from   := k3;
to     := k4;
guard  := x >= y;
action := x' = x + 1;
};

transition t8 := {
from   := k4;
to     := err;
guard  := x < y;
action := ;
};

transition t4 := {
from   := k4;
to     := k1;
guard  := x >= y;
action := y' = y + 1;
};

}

strategy jeannet_thesis_041_s {

Region init := {state = k1 && x = 0 && y = 0};

}

{  }

## Results¶

• With Aspic: { k2[x, -1 + x] : x >= 1; k3[x, x] : x >= 1; k1[x, x] : x >= 0; k4[x, -1 + x] : x >= 2 } (0.05s), OK.
• With ISL: { k2[x__1, -1 + x__1] : exists (e0 = [(-1 + x__1)/2]: 2e0 = -1 + x__1 and x__1 >= 5); k2[3, 2]; k2[1, 0]; k1[x__1, x__1] : exists (e0 = [(x__1)/2]: 2e0 = x__1 and x__1 >= 4); k1[2, 2]; k1[0, 0]; k4[x__1, -1 + x__1] : (exists (e0 = [(-2 + x__1)/2]: 2e0 = -2 + x__1 and x__1 >= 4)) or (exists (e0, e1 = [(-2 + x__1 - 2e0)/2]: 2e1 = -2 + x__1 - 2e0 and 2e0 <= -4 + x__1 and e0 >= 1)) or (exists (e0, e1, e2 = [(-2 + x__1 - 2e0 - 2e1)/2]: 2e2 = -2 + x__1 - 2e0 - 2e1 and e1 >= 1 and 2e1 <= -4 + x__1 - 2e0 and e0 >= 1)); k4[2, 1]; k3[x__1, x__1] : exists (e0 = [(-1 + x__1)/2]: 2e0 = -1 + x__1 and x__1 >= 5); k3[3, 3]; k3[1, 1] } (0.01s), OK.