Figure¶

Source code¶

model jeannet_thesis_016 {

  var i, j;

  states k1, k3, k2;

  transition t2 := {
    from   := k1;
    to     := k3;
    guard  := i + j > 20;
    action := ;
  };

  transition t1 := {
    from   := k1;
    to     := k2;
    guard  := i + j <= 20;
    action := ;
  };

  transition t4 := {
    from   := k2;
    to     := k1;
    guard  := i < 10;
    action := i' = i + 2, j' = j + 1;
  };

  transition t3 := {
    from   := k2;
    to     := k1;
    guard  := i >= 10;
    action := i' = i + 4;
  };

}

strategy jeannet_thesis_016_s {

  Region init := {state = k1 && i = 2 && j = 0};

}

Expected invariant¶

{ k2[v1, v2] : 2v2 <= -2 + v1 and v2 <= 4 }

Results¶

• With Aspic: { k2[i, j] : 2j <= -2 + i and j <= 4 and j <= 20 - i; k3[i, j] : j <= 4 and j >= 21 - i; k1[i, j] : j <= 4 and 2j <= -2 + i } (0.05s), OK.
• With ISL: { k3[i__1, 4] : exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 <= 20 and i__1 >= 17); k2[i__1, j__1] : 2j__1 = -2 + i__1 and i__1 <= 11 and i__1 >= 4; k2[i__1, 4] : (exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 >= 14 and i__1 <= 16)) or (exists (e0, e1 = [(10 - i__1 + 4e0)/4]: 4e1 = 10 - i__1 + 4e0 and 4e0 <= -14 + i__1 and e0 >= 1 and i__1 <= 16)) or (exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 <= 16 and i__1 >= 14)) or (exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 >= 14 and i__1 <= 16)) or (exists (e0, e1 = [(-10 + i__1 - 4e0)/4]: 4e1 = -10 + i__1 - 4e0 and i__1 <= 16 and 4e0 <= -14 + i__1 and e0 >= 1)) or (exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 <= 16 and i__1 >= 14)) or (exists (e0, e1 = [(10 - i__1 + 4e0)/4]: 4e1 = 10 - i__1 + 4e0 and 4e0 <= -14 + i__1 and i__1 <= 16 and e0 >= 1)) or (exists (e0, e1, e2 = [(10 - i__1 + 4e0 + 4e1)/4]: 4e2 = 10 - i__1 + 4e0 + 4e1 and e0 >= 1 and e1 >= 1 and i__1 <= 16 and 4e1 <= -14 + i__1 - 4e0)); k2[2, 0]; k1[i__1, j__1] : 2j__1 = -2 + i__1 and i__1 <= 11 and i__1 >= 4; k1[i__1, 4] : exists (e0 = [(-2 + i__1)/4]: 4e0 = -2 + i__1 and i__1 <= 20 and i__1 >= 14); k1[2, 0] } (0.02s), OK.