
Fix the following UCLID5 code using the compiler feedback provided below.

```

module main {
    type time_t = int;
    
    // State variables
    var time : time_t;       // Timestamp in seconds since the engine started
    var ignition : boolean;  // Engine state; true if on, false if off
    var buckled : boolean;   // Seat belt status; true if buckled, false if not
    var warn : boolean;      // Sensor warning state
    var noWarn : boolean;    // Sensor no warning state
    var beeper_active : boolean; // Beeper status
    var warning_light : boolean; // Red warning light status
    
    // Constants
    const MAX_BEEPER_TIME : time_t = 30; // Maximum time for the beeper to be active
    
    // Initialization
    init {
        time := 0;
        ignition := false;
        buckled := true;
        warn := false;
        noWarn := true;
        beeper_active := false;
        warning_light := false;
    }

    // Transitions
    next(time) = (ignition ? time + 1 : 0);
    next(warn) = (ignition && !buckled);
    next(noWarn) = (!ignition || buckled);
    next(buckled) = (noWarn ? true : buckled);
    next(ignition) = ignition; // Assume external control of ignition
    next(beeper_active) = (time <= MAX_BEEPER_TIME && warn ? true : false);
    next(warning_light) = (!buckled && ignition);

    // Procedures for events
    procedure engine_on() {
        ignition := true;
        if (!buckled) {
            warn := true;
            noWarn := false;
        }
        beeper_active := warn;
        warning_light := !buckled;
    }

    procedure engine_off() {
        ignition := false;
        warn := false;
        noWarn := true;
        beeper_active := false;
        warning_light := false;
    }

    procedure seat_belt_toggle() {
        buckled := !buckled;
        warn := !buckled && ignition;
        noWarn := buckled;
        beeper_active := (time <= MAX_BEEPER_TIME && !buckled && ignition);
        warning_light := (!buckled && ignition);
    }

    // Safety properties
    // Beeper should not sound longer than 30 seconds
    invariant "beeper_time_limit" (beeper_active => time <= MAX_BEEPER_TIME);

    // Warning light is on iff a seatbelt is unbuckled while ignition is on
    invariant "warning_light_correctness" (warning_light <=> (!buckled && ignition));
}
```

Compiler feedback:

```
Syntax error on line 19: Syntax Error in Expression.
        time := 0;

```
Reply with your UCLID5 code inside one unique code block.

I can definitely do that! Here is the UCLID5 code:
```
