Traffic Light Controller Examples in SMVHimanshu JainBug catching (Fall 2007)2Plan for todayModeling Traffic Light Controller in SMVProperties to CheckFour different SMV models for traffic light controller3NSWScenario4NSWNo turning5NSWBinary traffic lights6NSWSafetyPropertyThis should nothappen7NSWSafetyPropertyThis should nothappen8NSWLivenessPropertyWhen will the stupid light become green again9NSWLivenessPropertyThank God!Traffic in each direction must be served10Let’s see how to model all this in SMV11NSWSMV variablesN-go=0S-go=0W-go=1Three Boolean variables track the status of lights12NSWSMV variables Three Boolean variables sensethe traffic in each directionN-sense =1S-sense =1W-sense =0These variables are called N, Sy, W in thecode I will show you13Properties we would like to checkMutual exclusion SPEC AG !(W-Go & (N-Go | S-Go))Liveness in North directionSPEC AG(N-sense & !N-Go -> AF N-Go)Similar liveness properties for south and west14Properties we would like to checkNo strict sequencingWe don’t want the traffic lights to give turns to each other (if there is no need for it)For example, if there is no traffic on west lane, we do not want W-go becoming 1 periodicallyWe can specify such properties atleast partiallyAG(W-Go -> A[W-Go U (!W-Go & A[!W-Go U (N-Go | S-Go)])])See code other such propertiesWe want these properties to FAIL15NSWSMV modulesNorth modulewill control South modulewill control West modulewill control Main module will-Initialize variables-Start north, south, west modules16NSWWhat if north light is always green and there is always traffic in north direction17Fairness ConstraintsWhat if north light is always green and there is always traffic in north directionWe will avoid such scenarios by means of fairness constraintsFAIRNESS running & !(N-Go & N-sense)On an infinite execution, there are infinite number of states where either north light is not green or there is no traffic in north directionSimilar, fairness constraints for south and west directions18Now we look at some concrete implementations19Some more variablesTo ensure mutual exclusion We will have two Boolean variablesNS-Lock: denotes locking of north/south laneEW-Lock: denotes locking of west laneTo remember that there is traffic on a laneBoolean variables: N-Req, S-Req, W-ReqIf N-sense becomes 1, then N-Req is set to trueSimilarly, for others….20Traffic1.smvMODULE mainVAR N : boolean; --senses traffic going along north Sy : boolean; --senses traffic going along south W : boolean; --senses traffic going westward N-Req : boolean; --rememebers that there is traffic along north that needs to go S-Req : boolean; --rememebers that there is traffic along south that needs to go W-Req : boolean; --rememebers that there is traffic along west that needs to go N-Go : boolean; --north direction green light on S-Go : boolean; --south direction green light on W-Go : boolean; --west direction green light on NS-Lock : boolean; --north/south lane locked EW-Lock : boolean; --east/west lane locked north : process north1(NS-Lock, EW-Lock, N-Req, N-Go,N,S-Go); south : process south1(NS-Lock,EW-Lock,S-Req,S-Go,Sy,N-Go); west : process west1(NS-Lock,EW-Lock,W-Req,W-Go,W);ASSIGN init(NS-Lock) := 0; init(Sy) := 0; init(W) := 0; init(W-Req) := 0; …………………..OTHER INITIALIZATIONS21MODULE north(NS-Lock, EW-Lock, N-Req, N-Go,N,S-Go)VAR state : {idle, entering , critical , exiting};ASSIGN init(state) := idle; next(state) := case state = idle : case N-Req = 1 : entering; 1 : state; esac; state = entering & !EW-Lock : critical; state = critical & !N : exiting; state = exiting : idle; 1 : state; esac; next(NS-Lock) := case state = entering & !EW-Lock : 1 ; state = exiting & !S-Go : 0; 1 : NS-Lock; esac; next(N-Req) := case !N-Req & N : 1; state = exiting : 0; 1 : N-Req; esac; next(N-Go) := case state = critical : 1; state = exiting : 0; 1 : N-Go; esac;-- non-deterministically chose N next(N) := {0,1};FAIRNESS running & !(N-Go & N)22Module south is similarModule west1 is a little differentEverything seems ok!Let us run a model checker23Mutual exclusion fails (Counterexample)1. All variables zero2. N-sense=1 (North module executed)3. S-sense=1 (South module executed)4. S-Req=15. south.state=entering6. S-sense=0, NS-Lock=1, south.state=critical7. S-sense=1,S-go=1,south.state=exiting8. N-Req=19. north.state=entering10. north.state=critical11. S-Req=0, S-Go=0, NS-Lock=0, south.state=idle12. W=113. W-Req=114. west.state=entering15. EW-lock=1, west.state=critical16. W-Go=117. N-Go=1One module is executing at each step24Mutual exclusion fails (Counterexample)1. All variables zero2. N-sense=1 (North module executed)3. S-sense=1 (South module executed)4. S-Req=15. south.state=entering6. S-sense=0, NS-Lock=1, south.state=critical7. S-sense=1,S-go=1,south.state=exiting8. N-Req=19. north.state=entering10. north.state=critical11. S-Req=0, S-Go=0, NS-Lock=0, south.state=idle12. W=113. W-Req=114. west.state=entering15. EW-lock=1, west.state=critical16. W-Go=117. N-Go=1One module is executing at each stepEven though north.state is critical the NS-lock is released25Mutual exclusion fails (Counterexample)1. All variables zero2. N-sense=1 (North module executed)3. S-sense=1 (South module executed)4. S-Req=15. south.state=entering6. S-sense=0, NS-Lock=1, south.state=critical7. S-sense=1,S-go=1,south.state=exiting8. N-Req=19. north.state=entering10. north.state=critical11. S-Req=0, S-Go=0, NS-Lock=0, south.state=idle12. W=113. W-Req=114. west.state=entering15. EW-lock=1, west.state=critical16. W-Go=117. N-Go=1One module is executing at each stepOne problem is the one-step difference Between North.state=critical and N-Go=126MODULE north(NS-Lock, EW-Lock, N-Req, N-Go,N,S-Go)VAR state : {idle, entering , critical , exiting};ASSIGN init(state) := idle; next(state) := case state = idle : case N-Req = 1 : entering; 1 : state; esac; state = entering & !EW-Lock : critical; state = critical & !N : exiting; state = exiting : idle; 1 : state; esac; next(NS-Lock) := case state = entering & !EW-Lock : 1 ; state = exiting & !S-Go : 0; 1 : NS-Lock; esac; next(N-Req) := case !N-Req & N : 1;