Figure¶

Source code¶

model main {

  var da, db, r, temp;

  states start, lbl_12_1, lbl_8_2, stop;

  transition t_39 := {
    from   := start;
    to     := lbl_12_1;
    guard  := 0 <= r;
    action := da' = 2 * r - 1, db' = 2 * r - 1, temp' = 2 * r;
  };

  transition t_38 := {
    from   := start;
    to     := lbl_8_2;
    guard  := 0 <= r;
    action := da' = 2 * r - 1, db' = 2 * r;
  };

  transition t_28 := {
    from   := start;
    to     := stop;
    guard  := r + 1 <= 0;
    action := ;
  };

  transition t_35 := {
    from   := lbl_12_1;
    to     := lbl_8_2;
    guard  := r <= da;
    action := da' = da - 1;
  };

  transition t_34 := {
    from   := lbl_12_1;
    to     := stop;
    guard  := da + 1 <= r;
    action := ;
  };

  transition t_36 := {
    from   := lbl_12_1;
    to     := lbl_12_1;
    guard  := r <= da;
    action := da' = db - 1, db' = db - 1, temp' = da;
  };

  transition t_33 := {
    from   := lbl_8_2;
    to     := lbl_12_1;
    guard  := r <= da;
    action := da' = db - 1, db' = db - 1, temp' = da;
  };

  transition t_31 := {
    from   := lbl_8_2;
    to     := stop;
    guard  := da + 1 <= r;
    action := ;
  };

  transition t_32 := {
    from   := lbl_8_2;
    to     := lbl_8_2;
    guard  := r <= da;
    action := da' = da - 1;
  };

}

strategy main_s {

  Region init := {state = start};

}

Expected invariant¶

{ lbl_12_1[v1, v1, v3, v4] : 2v3 >= 1 + v1 and v4 <= 1 + v1 and v4 >= v3; lbl_8_2[v1, v2, v3, v4] : 2v3 >= v2 and v2 >= 1 + v1 and v3 <= 1 + v1 }

Results¶

• With Aspic: { lbl_12_1[da, da, r, temp] : temp >= r and 2r >= 1 + da and temp <= 1 + da; start[da, db, r, temp]; lbl_8_2[da, db, r, temp] : 2r >= db and db >= 1 + da and r <= 1 + da; stop[da, db, r, temp] } (0.09s), OK.
• With ISL: { stop[da__1, db__1, r__1, temp__1] : r__1 <= -1; stop[da__1, db__1, 1 + da__1, temp__1] : (da__1 >= 0 and db__1 >= 1 + da__1 and db__1 <= 2da__1 and temp__1 >= 1 + da__1) or (da__1 >= 0 and db__1 >= 1 + da__1 and temp__1 >= 1 + da__1 and db__1 <= 2da__1); stop[-1, 0, 0, temp__1]; stop[da__1, da__1, r__1, temp__1] : (r__1 >= 1 and 2r__1 >= 2 + da__1 and temp__1 >= r__1 and r__1 >= 1 + da__1) or (r__1 >= 1 and 2r__1 >= 2 + da__1 and temp__1 >= r__1 and r__1 >= 1 + da__1); stop[-1, -1, 0, 0]; stop[da__1, 2 + 2da__1, 1 + da__1, temp__1] : da__1 >= 0; stop[da__1, 1 + 2da__1, 1 + da__1, temp__1] : da__1 >= 0 and temp__1 <= 1 + 2da__1 and temp__1 >= 1 + da__1; stop[da__1, 1 + 2da__1, 1 + da__1, 2 + 2da__1] : da__1 >= 0; lbl_12_1[da__1, da__1, r__1, temp__1] : (2r__1 = 1 + da__1 and da__1 >= -1 and temp__1 <= da__1 and 2temp__1 >= 1 + da__1) or (r__1 >= 1 and 2r__1 >= 2 + da__1 and temp__1 >= r__1) or (r__1 >= 1 and 2r__1 >= 2 + da__1 and temp__1 >= r__1); lbl_12_1[da__1, da__1, r__1, 1 + da__1] : 2r__1 = 1 + da__1 and da__1 >= -1; start[da, db, r, temp]; lbl_8_2[da__1, db__1, r__1, temp__1] : (2r__1 = db__1 and db__1 >= 0 and db__1 >= 2 + da__1 and db__1 <= 2 + 2da__1) or (2r__1 = 1 + db__1 and db__1 >= -1 and temp__1 <= db__1 and 2temp__1 >= 1 + db__1 and db__1 <= 1 + 2da__1 and db__1 >= 1 + da__1) or (r__1 >= 1 and db__1 >= 1 + da__1 and 2r__1 >= 2 + db__1 and r__1 <= 1 + da__1 and temp__1 >= r__1) or (r__1 >= 1 and db__1 >= 1 + da__1 and temp__1 >= r__1 and 2r__1 >= 2 + db__1 and r__1 <= 1 + da__1); lbl_8_2[da__1, db__1, r__1, 1 + db__1] : 2r__1 = 1 + db__1 and db__1 >= -1 and db__1 <= 1 + 2da__1 and db__1 >= 1 + da__1; lbl_8_2[da__1, 1 + da__1, r__1, temp__1] : 2r__1 = 1 + da__1 and da__1 >= -1 } (0.03s), failed.