Figure¶

Source code¶

model main {

  var x, y1, y2, z;

  states start, lbl_11_1, lbl_22_1, lbl_16_1, stop;

  transition t_53 := {
    from   := start;
    to     := lbl_11_1;
    guard  := x <= 100;
    action := y1' = x + 11, y2' = 2;
  };

  transition t_49 := {
    from   := start;
    to     := stop;
    guard  := 101 <= x;
    action := y1' = x, y2' = 1, z' = x - 10;
  };

  transition t_65 := {
    from   := lbl_11_1;
    to     := lbl_22_1;
    guard  := 111 <= y1 && 3 <= y2;
    action := y1' = y1 - 9, y2' = y2 - 1;
  };

  transition t_64 := {
    from   := lbl_11_1;
    to     := lbl_22_1;
    guard  := y1 <= 110 && 101 <= y1 && 3 <= y2 || y1 <= 110 && 101 <= y1 && 2 <= y2;
    action := y1' = y1 + 1, y2' = y2;
  };

  transition t_63 := {
    from   := lbl_11_1;
    to     := lbl_16_1;
    guard  := 111 <= y1 && 2 = y2;
    action := y1' = y1 - 10, y2' = y2 - 1, z' = y1 - 20;
  };

  transition t_62 := {
    from   := lbl_11_1;
    to     := stop;
    guard  := 101 <= y1 && y2 <= 1;
    action := ;
  };

  transition t_51 := {
    from   := lbl_11_1;
    to     := lbl_11_1;
    guard  := y1 <= 100;
    action := y1' = y1 + 11, y2' = y2 + 1;
  };

  transition t_59 := {
    from   := lbl_22_1;
    to     := lbl_16_1;
    guard  := 111 <= y1 && 2 = y2;
    action := y1' = y1 - 10, y2' = y2 - 1, z' = y1 - 20;
  };

  transition t_58 := {
    from   := lbl_22_1;
    to     := stop;
    guard  := y2 <= 1;
    action := ;
  };

  transition t_61 := {
    from   := lbl_22_1;
    to     := lbl_22_1;
    guard  := 111 <= y1 && 3 <= y2;
    action := y1' = y1 - 9, y2' = y2 - 1;
  };

  transition t_60 := {
    from   := lbl_22_1;
    to     := lbl_22_1;
    guard  := y1 <= 110 && 3 <= y2 || y1 <= 110 && 2 <= y2;
    action := y1' = y1 + 1, y2' = y2;
  };

  transition t_57 := {
    from   := lbl_16_1;
    to     := lbl_22_1;
    guard  := 111 <= y1 && 3 <= y2;
    action := y1' = y1 - 9, y2' = y2 - 1;
  };

  transition t_56 := {
    from   := lbl_16_1;
    to     := lbl_22_1;
    guard  := y1 <= 110 && 3 <= y2 || y1 <= 110 && 2 <= y2;
    action := y1' = y1 + 1, y2' = y2;
  };

  transition t_54 := {
    from   := lbl_16_1;
    to     := stop;
    guard  := y2 <= 1;
    action := ;
  };

  transition t_55 := {
    from   := lbl_16_1;
    to     := lbl_16_1;
    guard  := 111 <= y1 && 2 = y2;
    action := y1' = y1 - 10, y2' = y2 - 1, z' = y1 - 20;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

{ lbl_22_1[v1, v2, v3, v4] : v3 >= 2 and v2 >= 102 and v2 <= 111 and 11v3 <= 10 - v1 + v2; stop[v1, v2, 1, -10 + v2] : v2 >= v1 and v2 >= 101; lbl_11_1[v1, v2, v3, v4] : 11v3 = 11 - v1 + v2 and v2 <= 111 and v2 >= 11 + v1; lbl_16_1[v1, 101, 1, 91] : v1 <= 100 }

Results¶

• With Aspic: { start[x, y1, y2, z]; lbl_22_1[x, y1, y2, z] : y2 >= 2 and y1 >= 102 and y1 <= 111 and 11y2 <= 10 - x + y1; lbl_11_1[x, y1, y2, z] : 11y2 = 11 - x + y1 and y1 <= 111 and y1 >= 11 + x; stop[x, y1, 1, -10 + y1] : y1 >= x and y1 >= 101; lbl_16_1[x, 101, 1, 91] : x <= 100 } (0.06s), OK.
• With ISL: { lbl_22_1[x__1, y1__1, y2__1, z__1] : (11y2__1 = 10 - x__1 + y1__1 and x__1 <= 89 and y1__1 >= 23 + x__1 and y1__1 <= 111 and y1__1 >= 102) or (exists (e0 = [(x__1)/11]: 11e0 = x__1 and x__1 <= 88 and 99y2__1 <= -132 - 9x__1 + 11y1__1 and y2__1 >= 2 and 11y2__1 <= 121 - x__1 and 110y2__1 <= -22 - 10x__1 + 11y1__1)) or (exists (e0 = [(122 - x__1)/11]: x__1 <= 89 and 11y2__1 <= 122 - x__1 and 11e0 <= 120 - x__1 and 11e0 >= 112 - x__1 and 110y2__1 <= -13 - 10x__1 + 11y1__1 and 2e0 <= 10 - x__1 + y1__1 - 9y2__1 and y2__1 >= 2)) or (exists (e0 = [(-1 + x__1)/11]: 11e0 = -1 + x__1 and x__1 <= 89 and 99y2__1 <= -123 - 9x__1 + 11y1__1 and 110y2__1 <= -23 - 10x__1 + 11y1__1 and y2__1 >= 2 and 11y2__1 <= 111 - x__1)); lbl_22_1[x__1, 102, y2__1, z__1] : 11y2__1 = 111 - x__1 and x__1 <= 89; lbl_22_1[x__1, y1__1, 2, z__1] : x__1 <= 98 and x__1 >= 90 and y1__1 >= 13 + x__1; lbl_22_1[x__1, 12 + x__1, 2, z__1] : x__1 <= 99 and x__1 >= 90; stop[x__1, y1__1, 1, -10 + y1__1] : (exists (e0 = [(x__1)/11]: 11e0 = x__1 and x__1 <= 88 and 11y1__1 >= 220 + 9x__1 and 11y1__1 >= 132 + 10x__1 and y1__1 >= 101)) or (exists (e0 = [(-1 + x__1)/11]: 11e0 = -1 + x__1 and x__1 <= 89 and 11y1__1 >= 211 + 9x__1 and 11y1__1 >= 133 + 10x__1 and y1__1 >= 101)); stop[100, 101, 1, 91]; stop[x__1, y1__1, 1, -10 + y1__1] : (x__1 <= 98 and x__1 >= 90 and y1__1 >= 3 + x__1 and y1__1 >= 101) or (exists (e0 = [(122 - x__1)/11]: x__1 <= 89 and y1__1 >= 101 and 11e0 <= 120 - x__1 and 11e0 >= 112 - x__1 and 11y1__1 >= 123 + 10x__1 and 2e0 <= 2 - x__1 + y1__1)); stop[99, 101, 1, 91]; stop[x__1, x__1, 1, -10 + x__1] : x__1 >= 101; lbl_11_1[x__1, y1__1, y2__1, z__1] : 11y2__1 = 11 - x__1 + y1__1 and x__1 <= 89 and y1__1 >= 22 + x__1 and y1__1 <= 111; lbl_11_1[x__1, 11 + x__1, 2, z__1] : x__1 <= 100; lbl_16_1[x__1, y1__1, 1, -10 + y1__1] : (exists (e0 = [(x__1)/11]: 11e0 = x__1 and x__1 <= 88 and 11y1__1 >= 220 + 9x__1 and 11y1__1 >= 132 + 10x__1 and y1__1 >= 101)) or (exists (e0 = [(-1 + x__1)/11]: 11e0 = -1 + x__1 and x__1 <= 89 and 11y1__1 >= 211 + 9x__1 and 11y1__1 >= 133 + 10x__1 and y1__1 >= 101)); lbl_16_1[100, 101, 1, 91]; lbl_16_1[x__1, y1__1, 1, -10 + y1__1] : (x__1 <= 98 and x__1 >= 90 and y1__1 >= 3 + x__1 and y1__1 >= 101) or (exists (e0 = [(122 - x__1)/11]: x__1 <= 89 and y1__1 >= 101 and 11e0 <= 120 - x__1 and 11e0 >= 112 - x__1 and 11y1__1 >= 123 + 10x__1 and 2e0 <= 2 - x__1 + y1__1)); lbl_16_1[99, 101, 1, 91]; start[x, y1, y2, z] } (0.08s), failed.