Figure¶

Source code¶

model halbwachs_thesis_60 {

  var i, j;

  states k1, k3, k2;

  transition t2 := {
    from   := k1;
    to     := k3;
    guard  := i > 100;
    action := ;
  };

  transition t1 := {
    from   := k1;
    to     := k2;
    guard  := i <= 100;
    action := ;
  };

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

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

}

strategy halbwachs_thesis_60_s {

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

}

Expected invariant¶

{ k3[v1, v2] : v2 <= 51 }

Results¶

• With Aspic: { k2[i, j] : j >= 0 and i <= 100 and 2j <= i; k3[i, j] : i >= 101 and j >= 0 and 2j <= i; k1[i, j] : j >= 0 and 2j <= i } (0.04s), failed.
• With ISL: { k3[i__1, j__1] : (2j__1 = i__1 and i__1 >= 101 and i__1 <= 102) or (exists (e0 = [(i__1)/2], e1 = [(-i__1 + 2j__1)/4]: 2e0 = i__1 and 4e1 = -i__1 + 2j__1 and i__1 >= 101 and j__1 <= 50 and j__1 >= 1 and 2j__1 <= -4 + i__1 and i__1 <= 104)); k3[i__1, 0] : exists (e0 = [(i__1)/4]: 4e0 = i__1 and i__1 >= 101 and i__1 <= 104); k2[i__1, j__1] : (2j__1 = i__1 and i__1 >= 2 and i__1 <= 100) or (exists (e0 = [(i__1)/2], e1 = [(-i__1 + 2j__1)/4]: 2e0 = i__1 and 4e1 = -i__1 + 2j__1 and 2j__1 <= -4 + i__1 and i__1 <= 100 and j__1 >= 1)) or (exists (e0, e1, e2 = [(-i__1 + 2j__1 - 4e0 - 4e1)/4]: 4e2 = -i__1 + 2j__1 - 4e0 - 4e1 and i__1 <= 100 and e1 <= -1 and j__1 >= 3 and 4e1 >= 4 - i__1 + 2j__1 - 4e0 and e0 <= -1)) or (exists (e0, e1 = [(-i__1 + 2j__1 - 4e0)/4]: 4e1 = -i__1 + 2j__1 - 4e0 and e0 <= -1 and i__1 <= 100 and j__1 >= 3 and 4e0 >= 4 - i__1 + 2j__1)) or (exists (e0, e1 = [(-i__1 + 2j__1 + 4e0)/4]: 4e1 = -i__1 + 2j__1 + 4e0 and i__1 <= 100 and e0 >= 1 and j__1 >= 1 and 4e0 <= -4 + i__1 - 2j__1)) or (exists (e0, e1 = [(-i__1 + 2j__1 - 4e0)/4]: 4e1 = -i__1 + 2j__1 - 4e0 and i__1 <= 100 and j__1 >= 2 and e0 <= -1 and 4e0 >= 4 - i__1 + 2j__1)) or (exists (e0, e1 = [(-i__1 + 2j__1 - 4e0)/4]: 4e1 = -i__1 + 2j__1 - 4e0 and i__1 <= 100 and e0 <= -1 and j__1 >= 2 and 4e0 >= 4 - i__1 + 2j__1)) or (exists (e0, e1, e2 = [(-i__1 + 2j__1 + 4e0 - 4e1)/4]: 4e2 = -i__1 + 2j__1 + 4e0 - 4e1 and e1 <= -1 and j__1 >= 2 and i__1 <= 100 and 4e1 >= 4 - i__1 + 2j__1 + 4e0 and e0 >= 1)) or (exists (e0, e1 = [(i__1 - 2j__1 - 4e0)/4]: 4e1 = i__1 - 2j__1 - 4e0 and e0 >= 1 and 4e0 <= -4 + i__1 - 2j__1 and j__1 >= 1 and i__1 <= 100)) or (exists (e0, e1 = [(-i__1 + 2j__1 + 4e0)/4]: 4e1 = -i__1 + 2j__1 + 4e0 and i__1 <= 100 and j__1 >= 2 and e0 >= 1 and 4e0 <= -4 + i__1 - 2j__1)) or (exists (e0, e1 = [(-i__1 + 2j__1 - 4e0)/4]: 4e1 = -i__1 + 2j__1 - 4e0 and i__1 <= 100 and e0 <= -1 and j__1 >= 2 and 4e0 >= 4 - i__1 + 2j__1)) or (exists (e0, e1 = [(-i__1 + 2j__1 - 4e0)/4]: 4e1 = -i__1 + 2j__1 - 4e0 and e0 <= -1 and j__1 >= 3 and i__1 <= 100 and 4e0 >= 4 - i__1 + 2j__1)) or (exists (e0, e1 = [(-i__1 + 2j__1 + 4e0)/4]: 4e1 = -i__1 + 2j__1 + 4e0 and 4e0 <= -4 + i__1 - 2j__1 and e0 >= 1 and j__1 >= 2 and i__1 <= 100)) or (exists (e0, e1 = [(-i__1 + 2j__1 - 4e0)/4]: 4e1 = -i__1 + 2j__1 - 4e0 and e0 <= -1 and 4e0 >= 4 - i__1 + 2j__1 and j__1 >= 3 and i__1 <= 100)) or (exists (e0, e1, e2 = [(-i__1 + 2j__1 + 4e0 + 4e1)/4]: 4e2 = -i__1 + 2j__1 + 4e0 + 4e1 and i__1 <= 100 and e0 >= 1 and j__1 >= 1 and 4e1 <= -4 + i__1 - 2j__1 - 4e0 and e1 >= 1)) or (exists (e0, e1, e2 = [(-i__1 + 2j__1 + 4e0 - 4e1)/4]: 4e2 = -i__1 + 2j__1 + 4e0 - 4e1 and i__1 <= 100 and e0 >= 1 and e1 <= -1 and 4e1 >= 4 - i__1 + 2j__1 + 4e0 and j__1 >= 2)) or (exists (e0, e1 = [(-i__1 + 2j__1 + 4e0)/4]: 4e1 = -i__1 + 2j__1 + 4e0 and 4e0 <= -4 + i__1 - 2j__1 and j__1 >= 1 and e0 >= 1 and i__1 <= 100)) or (exists (e0, e1 = [(i__1 - 2j__1 + 4e0)/4]: 4e1 = i__1 - 2j__1 + 4e0 and j__1 >= 2 and i__1 <= 100 and 4e0 >= 4 - i__1 + 2j__1 and e0 <= -1)) or (exists (e0, e1 = [(-i__1 + 2j__1 + 4e0)/4]: 4e1 = -i__1 + 2j__1 + 4e0 and j__1 >= 1 and 4e0 <= -4 + i__1 - 2j__1 and e0 >= 1 and i__1 <= 100)) or (exists (e0, e1, e2 = [(-i__1 + 2j__1 + 4e0 + 4e1)/4]: 4e2 = -i__1 + 2j__1 + 4e0 + 4e1 and e0 >= 1 and i__1 <= 100 and e1 >= 1 and 4e1 <= -4 + i__1 - 2j__1 - 4e0 and j__1 >= 1)) or (exists (e0, e1 = [(-i__1 + 2j__1 + 4e0)/4]: 4e1 = -i__1 + 2j__1 + 4e0 and 4e0 <= -4 + i__1 - 2j__1 and j__1 >= 1 and e0 >= 1 and i__1 <= 100)) or (exists (e0, e1 = [(-i__1 + 2j__1 + 4e0)/4]: 4e1 = -i__1 + 2j__1 + 4e0 and i__1 <= 100 and j__1 >= 2 and e0 >= 1 and 4e0 <= -4 + i__1 - 2j__1)) or (exists (e0, e1, e2 = [(-i__1 + 2j__1 + 4e0 + 4e1)/4]: 4e2 = -i__1 + 2j__1 + 4e0 + 4e1 and j__1 >= 1 and 4e1 <= -4 + i__1 - 2j__1 - 4e0 and e1 >= 1 and i__1 <= 100 and e0 >= 1)) or (exists (e0, e1, e2 = [(-i__1 + 2j__1 - 4e0 + 4e1)/4]: 4e2 = -i__1 + 2j__1 - 4e0 + 4e1 and j__1 >= 2 and 4e1 <= -4 + i__1 - 2j__1 + 4e0 and e1 >= 1 and i__1 <= 100 and e0 <= -1)) or (exists (e0 = [(i__1)/2], e1 = [(-i__1 + 2j__1)/4]: 2e0 = i__1 and 4e1 = -i__1 + 2j__1 and 2j__1 <= -4 + i__1 and i__1 <= 100 and j__1 >= 2)); k2[i__1, 0] : (exists (e0 = [(i__1)/4]: 4e0 = i__1 and i__1 >= 4 and i__1 <= 100)) or (exists (e0, e1 = [(i__1 - 4e0)/4]: 4e1 = i__1 - 4e0 and e0 >= 1 and i__1 <= 100 and 4e0 <= -4 + i__1)) or (exists (e0, e1, e2 = [(i__1 - 4e0 - 4e1)/4]: 4e2 = i__1 - 4e0 - 4e1 and e0 >= 1 and e1 >= 1 and 4e1 <= -4 + i__1 - 4e0 and i__1 <= 100)); k2[0, 0]; k1[i__1, j__1] : (2j__1 = i__1 and i__1 >= 2 and i__1 <= 102) or (exists (e0 = [(i__1)/2], e1 = [(-i__1 + 2j__1)/4]: 2e0 = i__1 and 4e1 = -i__1 + 2j__1 and i__1 <= 104 and j__1 <= 50 and j__1 >= 1 and 2j__1 <= -4 + i__1)); k1[0, 0]; k1[i__1, 0] : exists (e0 = [(i__1)/4]: 4e0 = i__1 and i__1 >= 4 and i__1 <= 104) } (0.04s), OK.