module main {
    // State variables
    var door_open : boolean; // Indicates if any door is open
    var light_on : boolean;  // Indicates if the dome light is on
    var time : int;          // Timer to count the time after doors are closed

    // Constants
    const TIME_LIMIT : int = 30; // Time limit for the light to stay on after doors are closed

    // Initialization of the state
    init {
        door_open = false;
        light_on = false;
        time = 0;
    }

    // Transition relation
    next {
        if (door_open') {
            // If any door is opened
            light_on' = true;
            time' = 0;
        } else {
            // If all doors are closed
            if (time < TIME_LIMIT) {
                // Continue counting time until the TIME_LIMIT is reached
                light_on' = true;
                time' = time + 1;
            } else {
                // Turn off the light after the TIME_LIMIT
                light_on' = false;
                time' = 0;
            }
        }
    }

    // Specification: The light should be on when any door is open
    invariant light_on_when_door_open : door_open => light_on;

    // Specification: The light should stay on for 30 seconds after all doors are closed
    invariant light_on_after_doors_closed : (!door_open && time < TIME_LIMIT) => light_on;

    // Control block to drive the simulation or verification
    control {
        // Simulate for 40 steps to observe the behavior longer than the TIME_LIMIT
        v = simulate(40);
        print_trace;
    }
}
