/* This is a simple traffic light system that transitions between red and green.
   The purpose is to show how to model state transitions.
*/

module traffic_light
{
    type light_state_t = enum { RED, GREEN };
    var current_state : light_state_t;

    init {
        current_state = RED;
    }

    next {
        current_state' = if (current_state == RED) then GREEN else RED;
    }

    invariant "no_concurrent_states" : (current_state == RED) -> (current_state != GREEN);

    control {
        simulate 10;
        check;
        print_results;
    }
}
