// Two traffic lights at an intersection
module traffic_lights
{
    type state_t = enum { RED, GREEN };
    var traffic_light1 : state_t;
    var traffic_light2 : state_t;

    init {
        traffic_light1 = RED;
        traffic_light2 = GREEN;
    }

    next {
        case
        traffic_light1' = GREEN;
        traffic_light2' = RED;
        traffic_light1' = RED;
        traffic_light2' = GREEN;
        esac
    }

    input action_A : boolean;
    input action_B : boolean;

    invariant no_deadlock : !(traffic_light1 == RED && traffic_light2 == RED) && !(traffic_light1 == GREEN && traffic_light2 == GREEN);

    control {
        check;
        print_results;
    }
}
