案例条件是不是详尽无遗？答案

【问题标题】：Case conditions are not exhaustive?案例条件是不是详尽无遗？
【发布时间】：2017-03-11 22:21:53
【问题描述】：

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

代码如下：

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;

【问题讨论】：

标签： model-checking nusmv

【解决方案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 时，它不知道在下一个状态下应该为 nearE 分配什么值。

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

如果您不希望nearE 的值发生变化，一种常见的设计做法是添加一个catch all case 条件，如下所示：

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

【讨论】：