module DomeLightModule {
  var light_on: boolean;
  var time: integer;

  input door_open: boolean;

  output dome_light_status: boolean;

  init {
    light_on = false;
    time = 0;

  }
  next {
    if (door_open) {
      light_on' = true;
      time' = 30;
    } else {
      if (time > 0) {
        time' = (time - 1);
        light_on' = true;
      } else {
        light_on' = false;
      }
    }

  }
  invariant spec: ((door_open || (time > 0)) == light_on);

}
