
// Define states for the traffic lights
type state_t = enum { RED, GREEN, YELLOW }
type main_light_t = enum { GREEN_PHASE, YELLOW_PHASE, RED_PHASE }
type secondary_light_t = enum { RED_WAIT, GREEN_PHASE, YELLOW_PHASE }

// Variables representing the state of each of the lights on both roads
var ml : main_light_t
var sl : secondary_light_t
var timer : int
var vehicle_detected : boolean

// Constants for timing
const lengthMainGreen : int = 180    // Main green phase: 3 minutes (180 seconds)
const lengthMainYellow : int = 5     // Main yellow phase: 5 seconds
const lengthMainRed : int = 55       // Main red phase: 55 seconds
const lengthSecGreen : int = 50      // Secondary green phase: 50 seconds
const lengthSecYellow : int = 5      // Secondary yellow phase: 5 seconds

init {
    ml = GREEN_PHASE
    sl = RED_WAIT
    timer = 0
    vehicle_detected = false
}

// Update timer
next (timer) := 
    if (timer < lengthMainGreen + lengthMainYellow + lengthMainRed) {
        timer + 1
    } else {
        0
    }

// Update vehicle detection input
input (vehicle_detected_signal: boolean)
next (vehicle_detected) := vehicle_detected_signal

// Update main light state
next (ml) := 
    switch (ml) {
        case GREEN_PHASE:
            if (timer >= lengthMainGreen) {
                YELLOW_PHASE
            } else {
                GREEN_PHASE
            }
        case YELLOW_PHASE:
            if (timer >= lengthMainGreen + lengthMainYellow) {
                RED_PHASE
            } else {
                YELLOW_PHASE
            }
        case RED_PHASE:
            if (timer >= lengthMainGreen + lengthMainYellow + lengthMainRed) {
                GREEN_PHASE
            } else {
                RED_PHASE
            }
        default:
            ml
    }

// Update secondary light state
next (sl) := 
    switch (sl) {
        case RED_WAIT:
            if (timer >= lengthMainGreen + lengthMainYellow) {
                GREEN_PHASE
            } else {
                RED_WAIT
            }
        case GREEN_PHASE:
            if (timer >= lengthMainGreen + lengthMainYellow + lengthSecGreen) {
                YELLOW_PHASE
            } else {
                GREEN_PHASE
            }
        case YELLOW_PHASE:
            if (timer >= lengthMainGreen + lengthMainYellow + lengthSecGreen + lengthSecYellow) {
                RED_WAIT
            } else {
                YELLOW_PHASE
            }
        default:
            sl
    }

// Output functions for light signaling
define mG : bool = (ml == GREEN_PHASE)
define mY : bool = (ml == YELLOW_PHASE)
define mR : bool = (ml == RED_PHASE)
define sG : bool = (sl == GREEN_PHASE)
define sY : bool = (sl == YELLOW_PHASE)
define sR : bool = (sl == RED_WAIT)