
module main
{
  var light_on : boolean; // indicates if the dome light is on
  var door_open : boolean; // indicates if any door is open
  var time : int; // time elapsed since last door closure

  init {
    light_on = false;
    door_open = false;
    time = 0;
  }

  transition {
    if (door_open) {
      light_on' = true;
      time' = 0;
    } else {
      if (time < 30) {
        light_on' = true;
        time' = time + 1;
      } else {
        light_on' = false;
        time' = 0;
      }
    }
  }

  system {
    door_open = nondet();
  }
}
