
module main
{
  type event_t = enum { warn, noWarn };

  var warn_event : event_t;
  var nowarn_event : event_t;
  var time : int;
  var ignition : boolean;
  var buckled : boolean;

  init {
    warn_event = noWarn;
    nowarn_event = noWarn;
    time = 0;
    ignition = false;
    buckled = true; // Assume all passengers start with seat belts buckled
  }

  transition {
    if (warn_event == warn && !buckled) {
      warn_event' = noWarn;
      nowarn_event' = warn;
      time' = 1;
    } else if (nowarn_event == warn && !buckled) {
      nowarn_event' = warn;
      time' = time + 1;
    } else if (nowarn_event == warn && buckled) {
      nowarn_event' = noWarn;
      time' = 0;
    } else if (warn_event == warn && buckled) {
      warn_event' = noWarn;
      time' = 0;
    } else {
      warn_event' = noWarn;
      nowarn_event' = noWarn;
      time' = 0;
    }

    if (ignition) {
      if (time < 30) {
        time' = time + 1;
      } else {
        warn_event' = noWarn;
        nowarn_event' = noWarn;
        time' = 0;
      }
    }

    if (ignition) {
      if (!buckled) {
        warn_event' = warn;
      }
    }
  }

}
