Figure¶

Source code¶

model gcd {

  var x, y;

  states start, lbl_11_1, lbl_10_1, cut, stop, lbl_6;

  transition t_32 := {
    from   := start;
    to     := lbl_11_1;
    guard  := y + 1 <= x && 1 <= y;
    action := x' = x - y;
  };

  transition t_31 := {
    from   := start;
    to     := lbl_10_1;
    guard  := x + 1 <= y && 1 <= x;
    action := y' = y - x;
  };

  transition t_30 := {
    from   := start;
    to     := cut;
    guard  := y = x && 1 <= y;
    action := ;
  };

  transition t_20 := {
    from   := start;
    to     := lbl_6;
    guard  := 1 <= x && y <= 0;
    action := ;
  };

  transition t_18 := {
    from   := start;
    to     := stop;
    guard  := x <= 0;
    action := ;
  };

  transition t_28 := {
    from   := lbl_11_1;
    to     := lbl_10_1;
    guard  := x + 1 <= y;
    action := y' = y - x;
  };

  transition t_27 := {
    from   := lbl_11_1;
    to     := cut;
    guard  := y = x;
    action := ;
  };

  transition t_29 := {
    from   := lbl_11_1;
    to     := lbl_11_1;
    guard  := y + 1 <= x;
    action := x' = x - y;
  };

  transition t_26 := {
    from   := lbl_10_1;
    to     := lbl_11_1;
    guard  := y + 1 <= x;
    action := x' = x - y;
  };

  transition t_24 := {
    from   := lbl_10_1;
    to     := cut;
    guard  := y = x;
    action := ;
  };

  transition t_25 := {
    from   := lbl_10_1;
    to     := lbl_10_1;
    guard  := x + 1 <= y;
    action := y' = y - x;
  };

  transition fromCut := {
    from   := cut;
    to     := stop;
    guard  := true;
    action := ;
  };

  transition t_2 := {
    from   := lbl_6;
    to     := stop;
    guard  := true;
    action := ;
  };

}

strategy gcd_s {

  Region init := {state = start};

}

Expected invariant¶

{ lbl_11_1[v1, v2] : v1 >= 1 and v2 >= 1; cut[v1, v1] : v1 >= 1; lbl_6[v1, v2] : v1 >= 1 and v2 <= 0; lbl_10_1[v1, v2] : v1 >= 1 and v2 >= 1 }

Results¶

• With Aspic: { lbl_10_1[x, y] : x >= 1 and y >= 1; lbl_6[x, y] : x >= 1 and y <= 0; stop[x, y]; lbl_11_1[x, y] : x >= 1 and y >= 1; start[x, y]; cut[x, x] : x >= 1 } (0.06s), OK.
• With ISL: { lbl_11_1[x__1, y__1] : (x__1 >= 1 and y__1 >= 1) or (y__1 >= 1 and y__1 >= 1 - x__1 and x__1 >= 1) or (y__1 >= 1 and y__1 >= 1 - x__1 and x__1 >= 1) or x__1 >= 1 or x__1 >= 1 or (y__1 >= 1 and x__1 >= 1) or (exists (e0, e1: e1 >= 1 + e0 and e0 >= 1 and e1 >= 2 + y__1 + e0 and 2e1 >= 1 + 3e0 and 3e1 <= -1 + 5e0 and x__1 >= 1)) or x__1 >= 1 or (y__1 >= 3 and x__1 >= 1) or x__1 >= 1 or (y__1 <= -2 + x__1 and x__1 >= 1) or (y__1 >= 5 and x__1 >= 1) or x__1 >= 1 or (x__1 >= 1 and y__1 <= -2 + x__1) or (x__1 >= 1 and y__1 >= 1) or x__1 >= 1 or x__1 >= 1 or (x__1 >= 1 and y__1 >= 3) or x__1 >= 1 or x__1 >= 1 or (y__1 >= 5 and x__1 >= 1) or x__1 >= 1 or (y__1 <= -3 + x__1 and x__1 >= 1) or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or (y__1 <= -2 + x__1 and x__1 >= 1) or x__1 >= 1 or (x__1 >= 1 and y__1 <= -2 + x__1) or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or (x__1 >= 1 and y__1 <= -2 + x__1) or (y__1 <= -2 + x__1 and x__1 >= 1) or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or (y__1 <= -3 + x__1 and x__1 >= 1) or x__1 >= 1 or (y__1 <= -2 + x__1 and x__1 >= 1) or (x__1 >= 1 and y__1 <= -2 + x__1) or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or (y__1 <= -2 + x__1 and x__1 >= 1) or (x__1 >= 1 and y__1 >= 1) or x__1 >= 1 or x__1 >= 1 or (x__1 >= 1 and y__1 >= 3) or x__1 >= 1 or x__1 >= 1 or (y__1 >= 5 and x__1 >= 1); cut[x__1, x__1] : x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or (exists (e0, e1: e1 >= 1 + e0 and e0 >= 1 and e1 >= 2 + x__1 + e0 and 2e1 >= 1 + 3e0 and 3e1 <= -1 + 5e0 and x__1 >= 1)) or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 5 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 1 or x__1 >= 5 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 1 or x__1 >= 5 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 1 or x__1 >= 2 or (exists (e0, e1: e1 >= 1 + e0 and e0 >= 1 and e1 >= 1 + 2x__1 + e0 and 2e1 >= 1 + 3e0 and 3e1 <= -1 + 5e0 and x__1 >= 1)) or x__1 >= 1 or x__1 >= 2 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 2; lbl_6[x__1, y__1] : x__1 >= 1 and y__1 <= 0; stop[x__1, y__1] : (x__1 >= 1 and y__1 <= 0) or x__1 <= 0; stop[x__1, x__1] : x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or (exists (e0, e1: e1 >= 1 + e0 and e0 >= 1 and e1 >= 2 + x__1 + e0 and 2e1 >= 1 + 3e0 and 3e1 <= -1 + 5e0 and x__1 >= 1)) or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 5 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 1 or x__1 >= 5 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 1 or x__1 >= 5 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 1 or x__1 >= 2 or (exists (e0, e1: e1 >= 1 + e0 and e0 >= 1 and e1 >= 1 + 2x__1 + e0 and 2e1 >= 1 + 3e0 and 3e1 <= -1 + 5e0 and x__1 >= 1)) or x__1 >= 1 or x__1 >= 2 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 1 or x__1 >= 3 or x__1 >= 1 or x__1 >= 2; start[x, y]; lbl_10_1[x__1, y__1] : (y__1 >= 1 and x__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (y__1 >= 1 - x__1 and y__1 >= 1 - 2x__1 and x__1 >= 1 and y__1 >= 1) or (x__1 >= 1 and y__1 >= 1) or (y__1 >= 1 and y__1 >= 1 - 2x__1 and x__1 >= 1) or (x__1 >= 1 and y__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (y__1 >= 5 - x__1 and x__1 >= 1 and y__1 >= 1) or (x__1 >= 1 and y__1 >= 1) or (y__1 >= 1 - x__1 and x__1 >= 1 and y__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (y__1 >= 1 and y__1 >= 5 - x__1 and x__1 >= 1) or (x__1 >= 1 and y__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (y__1 >= 3 - x__1 and x__1 >= 1 and y__1 >= 1) or (exists (e0, e1: e1 >= 1 + e0 and e0 >= 1 and e1 >= 1 + 2x__1 + e0 and 2e1 >= 1 + 3e0 and 3e1 <= -1 + 5e0 and x__1 >= 1 and y__1 >= 1)) or (x__1 >= 1 and y__1 >= 1) or (y__1 >= 1 and y__1 >= 3 - x__1 and x__1 >= 1) or (x__1 >= 1 and y__1 >= 1) or (x__1 >= 1 and y__1 >= 1 - x__1 and y__1 >= 1) or (x__1 >= 1 and y__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (x__1 >= 1 and y__1 >= 1) or (x__1 >= 1 and y__1 >= 1 - x__1 and y__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (x__1 >= 1 and y__1 >= 5 - x__1 and y__1 >= 1) or (y__1 >= 1 and x__1 >= 1) or (y__1 >= 1 and y__1 >= 3 - x__1 and x__1 >= 1) } (0.67s), failed.