Figure¶

Source code¶

model gonnord_thesis_034 {

  var l, t, x;

  states L, N;

  transition t2 := {
    from   := L;
    to     := N;
    guard  := true;
    action := x' = 0;
  };

  transition t1 := {
    from   := L;
    to     := L;
    guard  := x <= 9;
    action := x' = x + 1, t' = t + 1, l' = l + 1;
  };

  transition t4 := {
    from   := N;
    to     := L;
    guard  := x >= 50;
    action := x' = 0;
  };

  transition t3 := {
    from   := N;
    to     := N;
    guard  := true;
    action := x' = x + 1, t' = t + 1;
  };

}

strategy gonnord_thesis_034_s {

  Region init := {state = L && x = 0 && t = 0 && l = 0};

}

Expected invariant¶

{ L[v1, v2, v3] : v2 >= -50 + 6v1; N[v1, v2, v3] : v2 >= -50 + 6v1 }

Results¶

• With Aspic: { L[l, t, x] : 5x >= 6l - t and x <= 10 and x >= 0 and x <= l; N[l, t, x] : x <= 50 - 6l + t and x <= -l + t and x >= 0 and l >= 0 } (0.05s), OK.
• With ISL: { L[l__1, t__1, x__1] : (exists (e0, e1: x__1 <= 10 and x__1 <= l__1 and 10e1 <= 9l__1 - 10t__1 + x__1 + 10e0 and e1 <= -1 + l__1 - t__1 + e0 and 50e1 >= 50 + 51l__1 - 51t__1 + 50e0 and x__1 >= 0)) or (exists (e0, e1: 10e1 <= 10 + 9l__1 - 10t__1 + x__1 + 10e0 and x__1 >= 0 and x__1 <= 10 and x__1 <= -1 + l__1 and e1 <= -1 + l__1 - t__1 + e0 and 50e1 >= 50 + 51l__1 - 51t__1 + 50e0)) or (x__1 <= -1 + l__1 and x__1 >= -10 + l__1 and t__1 >= 50 + l__1 and x__1 <= 10 and x__1 >= 0); L[l__1, l__1, l__1] : l__1 >= 1 and l__1 <= 10; L[0, 0, 0]; L[l__1, t__1, l__1] : t__1 >= 50 + l__1 and l__1 <= 10 and l__1 >= 0; N[l__1, t__1, x__1] : (exists (e0, e1, e2, e3, e4, e5, e6: 10e6 <= 10 + 10e0 - 10e1 + 9e5 and e5 <= -1 + l__1 - t__1 + e2 - e3 + e4 and e5 >= l__1 - t__1 + e4 and e5 >= 1 and e6 <= -1 + e0 - e1 + e5 and e6 >= e5 and e6 <= -1 + e4 and 50e6 >= 51l__1 - 51t__1 + x__1 + 50e0 - 50e1 + 50e2 - 50e3 + 50e4 and e5 <= l__1 and 9e5 <= 9l__1 - 10t__1 + 10e2 - 10e3 + 10e4)) or (exists (e0, e1, e2: 10e2 <= 10 + 9l__1 + 10e0 - 10e1 and e2 <= -2 + t__1 and 50e2 >= 51l__1 - t__1 + x__1 + 50e0 - 50e1 and l__1 >= 1 and e2 <= -1 + l__1 + e0 - e1 and e2 >= l__1)) or (exists (e0, e1: 50e1 >= 51l__1 - 51t__1 + x__1 + 50e0 and l__1 >= 0 and 10e1 <= 9l__1 - 10t__1 + 10e0 and e1 <= -1 + l__1 - t__1 + e0 and t__1 >= l__1)) or (exists (e0, e1: 10e1 <= 10 + 9l__1 - 10t__1 + 10e0 and t__1 >= l__1 and 50e1 >= 51l__1 - 51t__1 + x__1 + 50e0 and l__1 >= 1 and e1 <= -1 + l__1 - t__1 + e0)) or (exists (e0, e1, e2, e3, e4, e5: e5 >= 1 - l__1 + t__1 - e2 + e3 + e4 and e4 >= 0 and 10e5 <= 10e0 - 10e1 + 9e4 and e5 <= -1 + e0 - e1 + e4 and e5 >= e4 and e5 <= -l__1 + t__1 + e4 and 50e3 >= 51l__1 - 51t__1 + x__1 + 50e0 - 50e1 + 50e2 and e4 <= l__1 and 10e5 >= -9l__1 + 10t__1 - 10e2 + 10e3 + 9e4)) or (exists (e0, e1, e2: 50e2 >= 51l__1 - t__1 + x__1 + 50e0 - 50e1 and l__1 >= 0 and 10e2 <= 9l__1 + 10e0 - 10e1 and e2 <= -1 + l__1 + e0 - e1 and e2 >= l__1 and e2 <= -1 + t__1)) or (exists (e0, e1, e2: e2 >= 1 and 50e2 <= -51l__1 + 51t__1 - x__1 - 50e0 + 50e1 and l__1 >= 0 and 10e2 >= -9l__1 + 10t__1 - 10e0 + 10e1 and e2 >= 1 - l__1 + t__1 - e0 + e1 and e2 <= -l__1 + t__1)) or (exists (e0, e1, e2, e3, e4, e5, e6, e7: e6 >= 1 and e6 <= 10 and e7 >= 1 + e6 and e5 >= 1 - l__1 + t__1 - e2 + e3 + e4 and e6 <= e4 and 10e7 >= -10e0 + 10e1 - 9e4 + 10e5 + 9e6 and e7 >= 1 - e0 + e1 - e4 + e5 + e6 and e7 <= -e4 + e5 + e6 and e5 <= -l__1 + t__1 + e4 and 50e7 <= -51l__1 + 51t__1 - x__1 - 50e0 + 50e1 - 50e2 + 50e3 + 50e6 and e4 <= l__1 and 10e5 >= -9l__1 + 10t__1 - 10e2 + 10e3 + 9e4)) or (exists (e0, e1, e2, e3, e4, e5: 10e5 <= 10 + 10e0 - 10e1 + 9e4 and e4 <= l__1 and e5 >= 1 - l__1 + t__1 - e2 + e3 + e4 and e4 >= 1 and e5 <= -1 + e0 - e1 + e4 and 10e5 >= -9l__1 + 10t__1 - 10e2 + 10e3 + 9e4 and e5 >= e4 and e5 <= -l__1 + t__1 + e4 and 50e3 >= 51l__1 - 51t__1 + x__1 + 50e0 - 50e1 + 50e2)) or (exists (e0, e1, e2: 10e2 <= 10 + 9l__1 + 10e0 - 10e1 and e2 >= l__1 and 50e2 >= 51l__1 - t__1 + x__1 + 50e0 - 50e1 and l__1 >= 1 and e2 <= -1 + l__1 + e0 - e1 and e2 <= -1 + t__1)) or (exists (e0, e1, e2, e3: e3 >= 1 and e3 <= 10 and e3 <= -1 + e2 and 50e3 >= 51l__1 - 51t__1 + x__1 + 50e0 - 50e1 + 50e2 and e3 <= l__1 and 9e3 <= 9l__1 - 10t__1 + 10e0 - 10e1 + 10e2 and e3 <= -1 + l__1 - t__1 + e0 - e1 + e2 and e3 >= l__1 - t__1 + e2)) or (exists (e0, e1, e2, e3, e4: e3 >= 1 and e3 <= 10 and e4 >= 1 + e3 and 50e4 <= -51l__1 + t__1 - x__1 - 50e0 + 50e1 + 50e2 + 50e3 and e3 <= l__1 and 10e4 >= -9l__1 - 10e0 + 10e1 + 10e2 + 9e3 and e4 >= 1 - l__1 - e0 + e1 + e2 + e3 and e4 <= -l__1 + e2 + e3 and e2 <= -1 + t__1)) or (exists (e0, e1, e2, e3, e4, e5, e6, e7, e8, e9: 10e7 >= -9l__1 + 10t__1 - 10e4 + 10e5 + 9e6 and e8 >= 0 and 10e9 <= 10e0 - 10e1 + 9e8 and e9 <= -1 + e0 - e1 + e8 and e9 >= e8 and e6 <= l__1 and e7 >= 1 - l__1 + t__1 - e4 + e5 + e6 and e8 <= e6 and 10e9 >= -10e2 + 10e3 - 9e6 + 10e7 + 9e8 and e9 >= 1 - e2 + e3 - e6 + e7 + e8 and e9 <= -e6 + e7 + e8 and e7 <= -l__1 + t__1 + e6 and 50e5 >= 51l__1 - 51t__1 + x__1 + 50e0 - 50e1 + 50e2 - 50e3 + 50e4)) or (exists (e0, e1, e2, e3, e4, e5, e6: e4 <= -1 + t__1 and e5 >= 0 and 10e6 <= 10e0 - 10e1 + 9e5 and e6 <= -1 + e0 - e1 + e5 and e6 >= e5 and e6 <= -l__1 + e4 + e5 and 50e4 >= 51l__1 - t__1 + x__1 + 50e0 - 50e1 + 50e2 - 50e3 and e5 <= l__1 and 10e6 >= -9l__1 - 10e2 + 10e3 + 10e4 + 9e5 and e6 >= 1 - l__1 - e2 + e3 + e4 + e5)) or (exists (e0, e1, e2, e3, e4, e5, e6: e5 <= -1 + l__1 - t__1 + e2 - e3 + e4 and e5 >= 0 and 10e6 <= 10e0 - 10e1 + 9e5 and e6 <= -1 + e0 - e1 + e5 and e6 >= e5 and e5 >= l__1 - t__1 + e4 and e6 <= -1 + e4 and 50e6 >= 51l__1 - 51t__1 + x__1 + 50e0 - 50e1 + 50e2 - 50e3 + 50e4 and e5 <= l__1 and 9e5 <= 9l__1 - 10t__1 + 10e2 - 10e3 + 10e4)) or (exists (e0, e1, e2: 50e2 >= 51l__1 - t__1 + x__1 + 50e0 - 50e1 and l__1 >= 0 and 10e2 <= 9l__1 + 10e0 - 10e1 and e2 <= -1 + l__1 + e0 - e1 and e2 >= l__1 and e2 <= -2 + t__1)) or (exists (e0, e1, e2, e3, e4, e5, e6: e6 >= 1 and e5 >= 1 - l__1 + t__1 - e2 + e3 + e4 and e4 >= 0 and 10e6 >= -10e0 + 10e1 - 9e4 + 10e5 and e6 >= 1 - e0 + e1 - e4 + e5 and e6 <= -e4 + e5 and e5 <= -l__1 + t__1 + e4 and 50e6 <= -51l__1 + 51t__1 - x__1 - 50e0 + 50e1 - 50e2 + 50e3 and e4 <= l__1 and 10e5 >= -9l__1 + 10t__1 - 10e2 + 10e3 + 9e4)) or (exists (e0, e1, e2, e3: e3 >= 1 and 50e3 <= -51l__1 + t__1 - x__1 - 50e0 + 50e1 + 50e2 and l__1 >= 0 and 10e3 >= -9l__1 - 10e0 + 10e1 + 10e2 and e3 >= 1 - l__1 - e0 + e1 + e2 and e3 <= -l__1 + e2 and e2 <= -1 + t__1)) or (exists (e0, e1, e2: e2 <= -l__1 + t__1 and e2 >= 2 and 50e2 <= -51l__1 + 51t__1 - x__1 - 50e0 + 50e1 and l__1 >= 0 and 10e2 >= -9l__1 + 10t__1 - 10e0 + 10e1 and e2 >= 1 - l__1 + t__1 - e0 + e1)) or (exists (e0, e1, e2, e3: e3 >= 1 and e3 <= 10 and e3 >= l__1 - t__1 + e2 and e3 <= -2 + e2 and 50e3 >= 51l__1 - 51t__1 + x__1 + 50e0 - 50e1 + 50e2 and e3 <= l__1 and 9e3 <= 9l__1 - 10t__1 + 10e0 - 10e1 + 10e2 and e3 <= -1 + l__1 - t__1 + e0 - e1 + e2)) or (exists (e0, e1, e2, e3, e4, e5, e6, e7, e8, e9: 10e9 <= 10 + 10e0 - 10e1 + 9e8 and e6 <= l__1 and 10e7 >= -9l__1 + 10t__1 - 10e4 + 10e5 + 9e6 and e8 >= 1 and e9 <= -1 + e0 - e1 + e8 and e9 >= e8 and e7 >= 1 - l__1 + t__1 - e4 + e5 + e6 and e8 <= e6 and 10e9 >= -10e2 + 10e3 - 9e6 + 10e7 + 9e8 and e9 >= 1 - e2 + e3 - e6 + e7 + e8 and e9 <= -e6 + e7 + e8 and e7 <= -l__1 + t__1 + e6 and 50e5 >= 51l__1 - 51t__1 + x__1 + 50e0 - 50e1 + 50e2 - 50e3 + 50e4)) or (exists (e0, e1, e2, e3, e4, e5, e6: 10e6 <= 10 + 10e0 - 10e1 + 9e5 and e6 <= -l__1 + e4 + e5 and e4 <= -1 + t__1 and e5 >= 1 and e6 <= -1 + e0 - e1 + e5 and e6 >= e5 and 50e4 >= 51l__1 - t__1 + x__1 + 50e0 - 50e1 + 50e2 - 50e3 and e5 <= l__1 and 10e6 >= -9l__1 - 10e2 + 10e3 + 10e4 + 9e5 and e6 >= 1 - l__1 - e2 + e3 + e4 + e5)); N[0, t__1, t__1] : t__1 >= 0; N[l__1, t__1, -l__1 + t__1] : l__1 >= 1 and l__1 <= 10 and t__1 >= l__1 } (0.03s), failed.