module traffic_light {
    // Define the states of the traffic light
    type state_t = enum { RED, GREEN };

    // Variable to hold the current state of the traffic light
    var current_state : state_t;

    // Initialize the traffic light to start at RED
    init {
        current_state = RED;
    }

    // Define the state transitions
    next {
        if (current_state == RED) {
            current_state' = GREEN;
        } else {
            current_state' = RED;
        }
    }
}

module main {
    // Instance of the traffic light
    instance tl : traffic_light;

    // Main control block to simulate and check the model
    control {
        // Unroll the model transitions to observe behavior over multiple cycles
        v = unroll(10);
        check;
        print_results;
    }
}
