node cdrom(probe speed: int) returns (plus, minus, error: bool)
var ps, count: int;
  _a, _b, _la, _lb: bool;
let
  ps = 0 -> pre speed;

  assume h1 : speed - ps <= 4 and speed - ps >= -4;
  assume h2 : if (false -> pre plus) then (speed - ps > 0)
              else if (false -> pre minus) then (speed - ps < 0)
              else true;

  plus = (ps <= 9);
  minus = (ps >= 11);

  _a = speed < 8;
  _b = speed > 12;
  _la = true -> pre _a;
  _lb = false -> pre _b;

  count = if speed < 8 or speed > 12
            then (0 -> pre count) + 1 else 0;

  error = (count >= 15);
  guarantee g: not error;
tel