title: Case conditions are not exhaustive?
body: <p>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.</p>
  
  <p>Here is the code:</p>
  
  <pre><code>MODULE main
  VAR
    trainE : Train(controller1.signalE);
    trainW : Train(controller1.signalW);
    controller1 : controller(trainE.out, trainW.out);
  
    INVARSPEC(!(trainE.mode = bridge &amp; 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 &amp; next(out) = arrive: wait;
                      mode = bridge &amp; next(out) = leave: away;
                      mode = wait &amp; 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;
  </code></pre>