1

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;
4

1 回答 1

2

您实际上在所有case情况下都有相同的错误：

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

让我们考虑 line 处的错误56。您写了以下案例：

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

现在，outE是一个连接到 的输入trainE.out。在模块内部Train，out被声明为一个可以有3 个可能值的变量：{None, arrive, leave}. 但是，在您的代码中，您仅为 的两个可能的当前值指定未来值。因此，NuSMV理所当然地抱怨，因为当当前状态等于时，它不知道在下一个状态应该分配什么值。nearEoutEnearEoutENone

因此，为了修复此错误，您应该考虑您希望在何时发生什么outE = None并将该规范添加到您的模型中。

在您不希望nearE更改的值的情况下，常见的设计实践是添加一个catch all case 条件，如下所示：

next(nearE) := case
    outE = arrive : TRUE;
    outE = leave  : FALSE;
    TRUE          : nearE;
esac;
于 2017-03-12T12:39:42.053 回答