TrafficController.smv

MODULE main
VAR
    senseFromNorth : boolean;
    senseFromEast : boolean;
    senseFromWest : boolean;
    senseFromSouth : boolean;

    requireNorthLight : boolean;
    requireEastLight : boolean;
    requireWestLight : boolean;
    requireSouthLight : boolean;

    northLight : { off, oneThird, twoThird, full};
    eastLight : { off, oneThird, twoThird, full};
    westLight : { off, oneThird, twoThird, full};
    southLight : { off, oneThird, twoThird, full};

    lock : boolean;

    queue : array 0..3 of {1,2,3,4};
    pushIndex : {0,1,2,3};
    popIndex : {0,1,2,3};

    light1 : process TrafficLight(senseFromNorth,requireNorthLight,northLight,lock,requireEastLight,requireWestLight,requireSouthLight,queue,pushIndex,popIndex,1);
    light2 : process TrafficLight(senseFromEast,requireEastLight,eastLight,lock,requireWestLight,requireSouthLight,requireNorthLight,queue,pushIndex,popIndex,2);
    light3 : process TrafficLight(senseFromWest,requireWestLight,westLight,lock,requireSouthLight,requireNorthLight,requireEastLight,queue,pushIndex,popIndex,3);
    light4 : process TrafficLight(senseFromSouth,requireSouthLight,southLight,lock,requireNorthLight,requireEastLight,requireWestLight,queue,pushIndex,popIndex,4);

    -- Safety : No two lights are on together.
    LTLSPEC G ! (northLight!=off & eastLight!=off)
    LTLSPEC G ! (northLight!=off & westLight!=off)
    LTLSPEC G ! (northLight!=off & southLight!=off)
    LTLSPEC G ! (eastLight!=off & westLight!=off)
    LTLSPEC G ! (eastLight!=off & southLight!=off)
    LTLSPEC G ! (westLight!=off & southLight!=off)

    -- Liveness
    LTLSPEC G (senseFromNorth -> F(northLight!=off))
    LTLSPEC G (senseFromEast -> F(eastLight!=off))
    LTLSPEC G (senseFromWest -> F(westLight!=off))
    LTLSPEC G (senseFromSouth -> F(southLight!=off))

    -- no strict sequencing
    LTLSPEC  G ((northLight!=off) -> (F(southLight!=off) -> ( ((eastLight=off)&(westLight=off)) U (southLight!=off))) )
    LTLSPEC G ((northLight!=off) -> (F(eastLight!=off) -> ( ((southLight=off)&(westLight=off)) U (eastLight!=off))) )
    LTLSPEC G ((northLight!=off) -> (F(westLight!=off) -> ( ((eastLight=off)&(southLight=off)) U (westLight!=off))) )


ASSIGN
    init(senseFromNorth) := FALSE;
    init(senseFromEast) := FALSE;
    init(senseFromWest) := FALSE;
    init(senseFromSouth) := FALSE;

    init(requireNorthLight) := FALSE;
    init(requireEastLight) := FALSE;
    init(requireWestLight) := FALSE;
    init(requireSouthLight) := FALSE;

    init(northLight) := off;
    init(eastLight) := off;
    init(westLight) := off;
    init(southLight) := off;

    init(lock) := FALSE;

    init(pushIndex) := 0;
    init(popIndex) := 0;

MODULE TrafficLight(mySenseCar, myReqLight, myLight, lock, otherReq1, otherReq2, otherReq3, queue, pushI, popI,myID)
VAR 
    selfLock : boolean;
ASSIGN
    next(mySenseCar) := {TRUE, FALSE};

    next(myReqLight) := case
                            mySenseCar & !myReqLight & (myLight=off) : TRUE;
                            myLight!=off : FALSE;
                            TRUE : myReqLight;
                        esac;
    
    next(myLight) := case
                    myReqLight & selfLock & (myLight=off) : oneThird;
                    myLight=oneThird : twoThird;
                    myLight=twoThird : full;
                    (myLight=full) & (otherReq1 | otherReq2 | otherReq3) : off;
                    TRUE : myLight;
                esac;

    next(queue[0]) := case
                            (pushI=0) & mySenseCar & !myReqLight & (myLight=off) : myID ;
                            TRUE : queue[0];
                        esac;
    next(queue[1]) := case
                        (pushI=1) & mySenseCar & !myReqLight & (myLight=off) : myID ;
                        TRUE : queue[1];
                    esac;
    next(queue[2]) := case
                        (pushI=2) & mySenseCar & !myReqLight & (myLight=off) : myID ;
                        TRUE : queue[2];
                    esac;
    next(queue[3]) := case
                        (pushI=3) & mySenseCar & !myReqLight & (myLight=off) : myID ;
                        TRUE : queue[3];
                    esac;
    
    next(pushI) := case
                       ! (mySenseCar & !myReqLight & (myLight=off)) : pushI;
                       pushI = 0 : 1;
                       pushI = 1 : 2; 
                       pushI = 2 : 3; 
                       pushI = 3 : 0;
                       TRUE : pushI;
                    esac; 


    next(lock) := case
                    (queue[popI] = myID) & myReqLight & !lock : TRUE;
                    selfLock & (myLight=off & !myReqLight) : FALSE;
                    TRUE : lock;
                  esac;
    
    next(popI) := case
                    ! (selfLock & (myLight=off & !myReqLight)) : popI;
                    popI = 0 : 1;
                    popI = 1 : 2; 
                    popI = 2 : 3; 
                    popI = 3 : 0;
                    TRUE : popI;
                esac;

    init(selfLock) := FALSE;              
    next(selfLock) := case
                    (queue[popI] = myID) & myReqLight & !lock : TRUE;
                    selfLock & (myLight=off & !myReqLight) : FALSE;
                    TRUE : selfLock;
                  esac;
    
FAIRNESS running