Traffic light in NuSMV

Question

I'm trying to create a traffic light system implementation in NuSMV. Right now I have 6 booleans for NS/EW red, yellow, green. However when I specify that they are each always true in a future state, it comes back false. If anyone sees any errors in my code I would appreciate the help. Thanks.

MODULE main
VAR
    nsRed : boolean;
    nsYellow : boolean;
    nsGreen : boolean;

    time : 0..60;

    ewRed : boolean;
    ewYellow : boolean;
    ewGreen : boolean;
ASSIGN
    init(nsRed) := TRUE;
    init(nsYellow) := FALSE;
    init(nsGreen) := FALSE;
    init(ewRed) := FALSE;
    init(ewYellow) := FALSE;
    init(ewGreen) := TRUE;
    init(time) := 60;
next(nsRed) :=
    case
        (nsYellow = TRUE & (ewGreen = TRUE | ewYellow = TRUE) & time = 0) : TRUE;
        (nsRed = TRUE & time = 0) : FALSE;
        TRUE : nsRed;
    esac;
next(nsYellow) :=
    case
        (nsGreen = TRUE & ewRed = TRUE & time = 0) : TRUE;
        (nsYellow = TRUE & time = 0) : FALSE;
        TRUE : nsYellow;
    esac;
next(nsGreen) :=
    case
        (nsRed = TRUE & ewRed = TRUE & time = 0) : TRUE;
        (nsGreen = TRUE & time = 0) : FALSE;
        TRUE : nsGreen;
    esac;

next(ewRed) :=
    case
        (ewYellow = TRUE & (nsGreen = TRUE | nsYellow = TRUE) & time = 0) : TRUE;
        (ewRed = TRUE & time = 0) : FALSE;
        TRUE : ewRed;
    esac;
next(ewYellow) :=
    case
        (ewGreen = TRUE & nsRed = TRUE & time = 0) : TRUE;
        (ewYellow = TRUE & time = 0) : FALSE;
        TRUE : ewYellow;
    esac;
next(ewGreen) :=
    case
        (ewRed = TRUE & nsRed = TRUE & time = 0) : TRUE;
        (ewGreen = TRUE & time = 0) : FALSE;
        TRUE : ewGreen;
    esac;

next(time) :=
    case
        (time > 0) : time - 1;
        (time = 0 & nsRed = TRUE) : 60;
        (time = 0 & nsYellow = TRUE) : 60;
        (time = 0 & nsGreen = TRUE) : 3;
        (time = 0 & ewRed = TRUE) : 60;
        (time = 0 & ewYellow = TRUE) : 60;
        (time = 0 & ewGreen = TRUE) : 3;
        --(time = 0 & nsRed = TRUE & ewRed = TRUE) : 3
        TRUE : time;
    esac;

-- specification 
SPEC AG !(nsRed = TRUE & nsYellow = TRUE)
SPEC AG !(nsGreen = TRUE & nsRed = TRUE)
SPEC AG !(nsGreen = TRUE & ewGreen = TRUE)
SPEC AG !(nsYellow = TRUE & ewYellow = TRUE)
SPEC AG !(nsRed = TRUE & ewRed = TRUE)
SPEC AG (nsRed = TRUE | nsYellow = TRUE | nsGreen = TRUE | ewRed = TRUE | ewYellow = TRUE | ewGreen = TRUE)
--LTLSPEC F nsGreen = TRUE
LTLSPEC F ewGreen = TRUE

Answer 1

How about defining two different states indicating the trafic lights for NS and EW sides of the street? I have written a sample code, hope you find it useful...

MODULE main
VAR
    nsLight : {RED, YELLOW, GREEN};
    ewLight : {RED, YELLOW, GREEN};

    timeMove    : 0..10;
    timeYellow  : 0..5;

ASSIGN
init(nsLight)   := RED;
init(ewLight)   := GREEN;
init(timeMove)  := 10;
init(timeYellow):= 5;

--  NS:                                 |   EW:

--  R (10 sec) -> R ->   G (10 sec)     |   G (10 sec) -> Y (5 sec) ->   R (10 sec)
-- / \                   |              |   |                            |
--  |                   \ /             |   |                           \ /
--  |------------------- Y (5 sec)      |   |--------------------------- R


next(nsLight) := case
                    (nsLight = RED & ewLight = GREEN & timeMove = 0)        : RED;
                    (nsLight = RED & ewLight = YELLOW & timeYellow = 0)     : GREEN;
                    (nsLight = GREEN & ewLight = RED & timeMove = 0)        : YELLOW;
                    (nsLight = YELLOW & ewLight = RED & timeYellow = 0)     : RED;
                    TRUE                                                    : nsLight;
                esac;

next(ewLight) := case
                    (ewLight = GREEN & nsLight = RED & timeMove = 0)        : YELLOW;
                    (ewLight = YELLOW & nsLight = RED & timeYellow = 0)     : RED;
                    (ewLight = RED & nsLight = GREEN & timeMove = 0)        : RED;
                    (ewLight = RED & nsLight = YELLOW & timeYellow = 0)     : GREEN;
                    TRUE                                                    : ewLight;
                esac;

next(timeMove) := case
                    timeMove > 0 & ewLight != YELLOW & nsLight != YELLOW        : timeMove - 1;
                    timeMove = 0                                                : 10;
                    TRUE                                                        : timeMove;
                    esac;

next(timeYellow) := case
                    timeYellow > 0  & (ewLight = YELLOW | nsLight = YELLOW)     : timeYellow - 1;
                    timeYellow = 0                                              : 5;
                    TRUE                                                        : timeYellow;
                    esac;

The idea is to have a moving counter from 10 -> 0 while we're in the states of GREEN or RED and another counter 5 -> 0, I called it timeYellow, to make sure the transition from GREEN to YELLOW is smooth and less dangerous!

Answer 2

The reason that the property F nsGreen = TRUE is false is that there exists an infinite execution where nsGreen is never true. This is the counter-example that NuSMV generates (I cut out the counting down of the timer). Note that only updates of variables are printed.

-- specification  F nsGreen = TRUE  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  nsRed = TRUE
  nsYellow = FALSE
  nsGreen = FALSE
  time = 60
  ewRed = FALSE
  ewYellow = FALSE
  ewGreen = TRUE
-> State: 1.2 <-
  time = 59
  ...
-> State: 1.61 <-
  time = 0
-> State: 1.62 <-
  nsRed = FALSE
  time = 60
  ewYellow = TRUE
  ewGreen = FALSE
-> State: 1.63 <-
  time = 59
  ...
-> State: 1.122 <-
  time = 0
-> State: 1.123 <-
  time = 60
  ewYellow = FALSE
-> State: 1.124 <-
  time = 59
  ...
-> State: 1.182 <-
  time = 1
-- Loop starts here
-> State: 1.183 <-
  time = 0
-> State: 1.184 <-

The trace shows that nsRed is already set to false when the timer reaches 0 for the first time. Also, ewYellow becomes false, but ewRed is not set to true.

I would suggested you use an enum variable for the traffic lights instead of three booleans, like this:

MODULE main
VAR
    ns : {RED, YELLOW, GREEN};
    ew : {RED, YELLOW, GREEN};