案例条件不详尽？

Question

我正在 NuSMV 中编写两个模块，但收到错误，"Case conditions are not exhaustive"此错误指向我在代码中的最后一个 case 语句。我不确定如何解决这个问题，因为我目前拥有的案例是变量需要的唯一案例。第一个模块 "train" 被实例化两次，以便两列火车可以在一条轨道上。模块 "controller" 充当控制器，接收来自两列火车的输入并防止它们同时在桥上。

代码如下：

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

你实际上在所有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

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

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

现在，outE 是连接到 trainE.out 的输入。在模块 Train 内，out 被声明为一个变量，可以有 3 个可能的值 : {None, arrive, leave}。但是，在您的代码中，您仅针对 outE 的两个可能当前值指定了 nearE 的 未来值 。因此，NuSMV 有理由抱怨，因为它不知道在当前状态 outE 等于 None。

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

在不希望nearE的值发生变化的情况下，常见的设计做法是添加一个catch all case condition如下:

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

案例条件不详尽？

Case conditions are not exhaustive?

model-checking

nusmv