Figure¶

Source code¶

model halbwachs_thesis_60 {

  var i, j, k;

  states k1, k3, k2;

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

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

  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 && k = 0};

}

Expected invariant¶

{ k1[v1, v2, v3] : 4v3 = v1 + 2v2 }

Results¶

• With Aspic: { k1[i, j, k] : 4k = i + 2j and j >= 0 and 2j <= i; k3[i, j, k] : 4k = i + 2j and i >= 101 and j >= 0 and 2j <= i; k2[i, j, k] : 4k = 4 + i + 2j and j >= 0 and i <= 100 and 2j <= i } (0.06s), OK.
• With ISL: { k1[i__1, j__1, k__1] : (4k__1 = i__1 + 2j__1 and 2j__1 <= -4 + i__1 and i__1 <= 102 and j__1 >= 1) or (4k__1 = i__1 + 2j__1 and 2j__1 <= -8 + i__1 and i__1 <= 104 and j__1 >= 0) or (2j__1 = i__1 and 2k__1 = i__1 and i__1 <= 102 and i__1 >= 4) or (2j__1 = -4 + i__1 and 2k__1 = -2 + i__1 and i__1 <= 104 and i__1 >= 6); k1[2, 1, 1]; k1[4, 0, 1]; k1[0, 0, 0]; k3[i__1, j__1, k__1] : (4k__1 = i__1 + 2j__1 and 2j__1 <= -4 + i__1 and i__1 <= 102 and j__1 >= 1 and i__1 >= 101) or (4k__1 = i__1 + 2j__1 and 2j__1 <= -8 + i__1 and i__1 <= 104 and j__1 >= 0 and i__1 >= 101) or (2j__1 = i__1 and 2k__1 = i__1 and i__1 <= 102 and i__1 >= 101) or (2j__1 = -4 + i__1 and 2k__1 = -2 + i__1 and i__1 <= 104 and i__1 >= 101); k2[i__1, j__1, k__1] : (4k__1 = 4 + i__1 + 2j__1 and 2j__1 <= -4 + i__1 and i__1 <= 100 and j__1 >= 0) or (2j__1 = i__1 and 2k__1 = 2 + i__1 and i__1 <= 100 and i__1 >= 2); k2[0, 0, 1] } (0.04s), OK.