Figure¶

Source code¶

model gonnord_thesis_083 {

  var x, y;

  states q1, q2;

  transition t3 := {
    from   := q1;
    to     := q2;
    guard  := x > 100;
    action := ;
  };

  transition t2 := {
    from   := q1;
    to     := q1;
    guard  := x <= 100;
    action := x' = x + 2;
  };

  transition t1 := {
    from   := q1;
    to     := q1;
    guard  := x <= 100;
    action := x' = x + 1, y' = y + 1;
  };

}

strategy gonnord_thesis_083_s {

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

}

Expected invariant¶

{ q1[v1, v2] : v2 <= v1 and v1 <= 102 and v2 >= 0; q2[v1, v2] : v2 <= v1 and v1 <= 102 and v2 >= 0 }

Results¶

• With Aspic: { q1[x, y] : y <= x and y >= 0 and x <= 102 and y <= 202 - x; q2[x, y] : x >= 101 and y <= x and y >= 0 and x <= 102 and y <= 202 - x } (0.05s), OK.
• With ISL: { q1[x__1, y__1] : exists (e0 = [(-x__1 + y__1)/2]: 2e0 = -x__1 + y__1 and x__1 <= 102 and y__1 <= 100 and y__1 >= 1 and y__1 <= -2 + x__1); q1[x__1, x__1] : x__1 >= 1 and x__1 <= 101; q1[x__1, 0] : exists (e0 = [(x__1)/2]: 2e0 = x__1 and x__1 >= 2 and x__1 <= 102); q1[0, 0]; q2[x__1, y__1] : exists (e0 = [(-x__1 + y__1)/2]: 2e0 = -x__1 + y__1 and x__1 >= 101 and y__1 <= 100 and y__1 >= 1 and y__1 <= -2 + x__1 and x__1 <= 102); q2[x__1, 0] : exists (e0 = [(x__1)/2]: 2e0 = x__1 and x__1 >= 101 and x__1 <= 102); q2[101, 101] } (0.01s), OK.