Figure¶

Source code¶

model jeannet_thesis_104 {

  var x, y, b0, b1;

  states k;

  transition t2 := {
    from   := k;
    to     := k;
    guard  := x >= y && b0 != b1;
    action := b0' = 1 - b1, b1' = b0, y' = y + 1;
  };

  transition t1 := {
    from   := k;
    to     := k;
    guard  := x >= y && b0 = b1;
    action := b0' = 1 - b1, b1' = b0, x' = x + 1;
  };

}

strategy jeannet_thesis_104_s {

  Region init := {state = k && x = 0 && y = 0 && b0 = 0 && b1 = 0};

}

Expected invariant¶

{ k[v1, v2, v3, v4] : v2 <= v1 }

Results¶

• With Aspic: { k[x, y, b0, b1] : y <= 1 + x } (0.05s), failed.
• With ISL: { k[x__1, y__1, b0__1, b1__1] : (exists (e0, e1, e2, e3 = [(x__1 + y__1 - b0__1 - b1__1 + 2e0 + 2e1 + 2e2)/2]: 2e3 = x__1 + y__1 - b0__1 - b1__1 + 2e0 + 2e1 + 2e2 and y__1 >= 1 - x__1 and y__1 <= 1 + x__1 and b1__1 <= -b0__1 and y__1 >= 2 and e1 >= 2 - y__1 + b1__1 - 2e0 and e1 >= -2e0 and x__1 >= 1)) or (exists (e0, e1 = [(x__1 + y__1 - b0__1 - b1__1 + 2e0)/2]: 2e1 = x__1 + y__1 - b0__1 - b1__1 + 2e0 and y__1 >= 1 - x__1 and y__1 <= 1 + x__1 and b1__1 <= -b0__1 and b1__1 <= -y__1 and y__1 >= 1 and x__1 >= 1)) or (exists (e0, e1 = [(x__1 + y__1 - b0__1 - b1__1 + 2e0)/2]: 2e1 = x__1 + y__1 - b0__1 - b1__1 + 2e0 and y__1 >= 1 - x__1 and y__1 <= 1 + x__1 and b1__1 <= -b0__1 and b1__1 >= y__1 and y__1 >= 1 and x__1 >= 1)) or (exists (e0, e1, e2, e3 = [(x__1 + y__1 - b0__1 - b1__1 + 2e0 + 2e1 + 2e2)/2]: 2e3 = x__1 + y__1 - b0__1 - b1__1 + 2e0 + 2e1 + 2e2 and y__1 >= 1 - x__1 and y__1 <= 1 + x__1 and b1__1 >= 2 - b0__1 and y__1 >= 2 and e1 >= 2 - y__1 + b1__1 - 2e0 and e1 >= -2e0 and x__1 >= 1)) or (exists (e0, e1 = [(x__1 + y__1 - b0__1 - b1__1 + 2e0)/2]: 2e1 = x__1 + y__1 - b0__1 - b1__1 + 2e0 and y__1 >= 1 - x__1 and y__1 <= 1 + x__1 and b1__1 >= 2 - b0__1 and b1__1 <= -y__1 and y__1 >= 1 and x__1 >= 1)) or (exists (e0, e1 = [(x__1 + y__1 - b0__1 - b1__1 + 2e0)/2]: 2e1 = x__1 + y__1 - b0__1 - b1__1 + 2e0 and y__1 >= 1 - x__1 and y__1 <= 1 + x__1 and b1__1 >= 2 - b0__1 and b1__1 >= y__1 and y__1 >= 1 and x__1 >= 1)); k[x__1, y__1, b0__1, 1 - b0__1] : (exists (e0, e1, e2, e3 = [(-1 + x__1 + y__1 + 2e0 + 2e1 + 2e2)/2]: 2e3 = -1 + x__1 + y__1 + 2e0 + 2e1 + 2e2 and y__1 >= 1 - x__1 and y__1 <= -1 + x__1 and y__1 >= 2 and e1 >= 3 - y__1 - b0__1 - 2e0 and e1 >= -2e0 and x__1 >= 1)) or (exists (e0, e1 = [(-1 + x__1 + y__1 + 2e0)/2]: 2e1 = -1 + x__1 + y__1 + 2e0 and y__1 >= 1 - x__1 and y__1 <= -1 + x__1 and b0__1 >= 1 + y__1 and y__1 >= 1 and x__1 >= 1)) or (exists (e0, e1 = [(-1 + x__1 + y__1 + 2e0)/2]: 2e1 = -1 + x__1 + y__1 + 2e0 and y__1 >= 1 - x__1 and y__1 <= -1 + x__1 and b0__1 <= 1 - y__1 and y__1 >= 1 and x__1 >= 1)); k[0, 1, b0__1, b1__1] : (exists (e0 = [(-1 - b0__1 + b1__1)/2]: 2e0 = -1 - b0__1 + b1__1 and b1__1 <= -b0__1 and b1__1 <= -1)) or (exists (e0 = [(-1 - b0__1 + b1__1)/2]: 2e0 = -1 - b0__1 + b1__1 and b1__1 <= -b0__1 and b1__1 >= 1)) or (exists (e0 = [(-1 - b0__1 + b1__1)/2]: 2e0 = -1 - b0__1 + b1__1 and b1__1 >= 2 - b0__1 and b1__1 <= -1)) or (exists (e0 = [(-1 - b0__1 + b1__1)/2]: 2e0 = -1 - b0__1 + b1__1 and b1__1 >= 2 - b0__1 and b1__1 >= 1)); k[0, 0, 0, 0]; k[x__1, 0, b0__1, 0] : (exists (e0 = [(x__1 - b0__1)/2]: 2e0 = x__1 - b0__1 and b0__1 <= 0 and x__1 >= 1)) or (exists (e0 = [(x__1 - b0__1)/2]: 2e0 = x__1 - b0__1 and b0__1 >= 2 and x__1 >= 1)); k[x__1, 0, 1, 0] : exists (e0 = [(-1 + x__1)/2]: 2e0 = -1 + x__1 and x__1 >= 1) } (0.09s), failed.