module Automobile {
  var buckled: boolean;
  var ignition: boolean;
  var nowarn: boolean;
  var time: integer;
  var warn: boolean;
  var beep: boolean;
  var redLight: boolean;

  init {
    beep = false;
    redLight = false;
    warn = false;
    nowarn = true;
    time = 0;
    ignition = false;
    buckled = false;

  }
  procedure step()
    modifies beep;
    modifies warn;
    modifies redLight;
    modifies time;
  {
    if (ignition) {
      if ((warn || !buckled) && (time < 30)) {
        beep = true;
        redLight = true;
        time = (time + 1);
        if (buckled) {
          warn = false;
          redLight = false;
          beep = false;
        }
      } else {
        warn = false;
        beep = false;
        redLight = false;
      }
    }
  }

  next {
    call step();
  }
}
