Figure¶

Source code¶

model gonnord_thesis_031 {

  var i, j;

  states k1, k2;

  transition t3 := {
    from   := k1;
    to     := k2;
    guard  := i > 100;
    action := ;
  };

  transition t2 := {
    from   := k1;
    to     := k1;
    guard  := i <= 100;
    action := i' = i + 2, j' = j + 1;
  };

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

}

strategy gonnord_thesis_031_s {

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

}

Expected invariant¶

{ k2[v1, v2] : 2v2 <= v1 and v2 >= 0; k1[v1, v2] : 2v2 <= v1 and v2 >= 0 }

Results¶

• With Aspic: { k2[i, j] : i >= 101 and 2j <= i and j >= 0 and i <= 104 and 2j <= 204 - i; k1[i, j] : 2j <= i and j >= 0 and i <= 104 and 2j <= 204 - i } (0.05s), OK.
• With ISL: { k2[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)); k2[i__1, 0] : exists (e0 = [(i__1)/4]: 4e0 = i__1 and i__1 >= 101 and i__1 <= 104); 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.00s), OK.