Case conditions are not exhaustive?

Question

I am writing two modules in NuSMV but I am receiving the error, "Case conditions are not exhaustive" This error points to the last case statement I have in the code. I am not sure how to fix this because the cases that I currently have there are the only cases that the variable requires. The first module "train" is instantiated twice so that two trains can be on one track. The module "controller" acts as a controller which receives input from the two trains and prevents them both from being on a bridge at the same time.

Here is the code:

MODULE main
VAR
  trainE : Train(controller1.signalE);
  trainW : Train(controller1.signalW);
  controller1 : controller(trainE.out, trainW.out);

  INVARSPEC(!(trainE.mode = bridge & trainW.mode = bridge))
MODULE Train(signal)
    VAR 
    mode: {away, wait, bridge};
    out: {None, arrive, leave};
    ASSIGN
        init(mode) := away;
        init(out) := None;

        --Task A1
        next(out)  := case
                    mode = away: arrive;
                    mode = bridge: leave;
                    TRUE: None;
        esac;

        --Task A2
        next(mode) := case
                    mode = away & next(out) = arrive: wait;
                    mode = bridge & next(out) = leave: away;
                    mode = wait & signal = green: bridge;
                    TRUE: mode;

        esac;

MODULE controller(outE, outW)
    VAR
        signalE: {green, red};
        signalW: {green, red};
        west: {green, red};
        east: {green, red};
        nearE: boolean;
        nearW: boolean;
    ASSIGN
        init(west):= red;
        init(east):= red;
        init(nearW):= FALSE;
        init(nearE):= FALSE;

        --Task A1
        next(signalW):= west;

        --Task A2
        next(signalE):= east;

        --Task A3
        next(nearE):= case
                        outE = arrive: TRUE;
                        outE = leave: FALSE;
                        esac;
        next(nearW):= case
                        outW = arrive: TRUE;
                        outW = leave: FALSE;
                        esac;
        next(east):= case
                        next(nearE) = FALSE: red;
                        west = red: green;
                        esac;
        next(west):= case
                        next(nearW) = FALSE: red;
                        east = red: green;
                        esac;

Answer 1

You actually have the same error in all case conditions:

file test.smv: line 68: case conditions are not exhaustive
file test.smv: line 64: case conditions are not exhaustive
file test.smv: line 60: case conditions are not exhaustive
file test.smv: line 56: case conditions are not exhaustive

Let's consider the error at line 56. You wrote the following cases:

next(nearE) := case
    outE = arrive : TRUE;
    outE = leave  : FALSE;
esac;

Now, outE is an input connected to trainE.out. Inside module Train, out is declared as a variable that can have 3 possible values: {None, arrive, leave}. However, in your code, you specify the future value of nearE only for two possible current values of outE. Therefore, NuSMV rightfully complains because it doesn't know what value should be assigned to nearE in the next state when in the current state outE is equal to None.

Thus, in order to fix this error, you should think what you would like to happen when outE = None and add that specification to your model.

In the case in which you don't want the value of nearE to change, a common design practice is to add a catch all case condition as follows:

next(nearE) := case
    outE = arrive : TRUE;
    outE = leave  : FALSE;
    TRUE          : nearE;
esac;