我们可以在 NuSMV 中有终端状态吗？

Question

是否有可能在 NuSMV 中有一个状态没有到任何其他状态的转换？例如，在我的代码 l3 中没有任何转换是否有效？当我运行这个 NuSMV 给我的错误是 "case conditions are not exhaustive"。谢谢！

MODULE main

VAR

location: {l1,l2,l3};


ASSIGN

init(location):=l1;

next(location):= case
             (location = l1): l2;
             (location = l2): l1;
             (location = l2): l3;
             esac;

Answer 1

通过构造，在所谓的赋值样式中[在您的模型中使用]：

总是至少有一个初始状态
所有状态至少有一个下一个状态
不确定性很明显

或者，可以使用所谓的约束样式，它允许：

不一致的INIT约束，导致没有初始状态
不一致的 TRANS 约束，导致死锁状态 （即没有任何外向转换到下一个状态的状态）
隐藏了非确定性

有关详细信息，请参阅 the second part of this course，其中大部分内容也适用于 NuSMV。

FSM 的一个示例，其中某些状态没有未来状态：

MODULE main
VAR b : boolean;
TRANS b -> FALSE;

b处于true的状态没有未来状态。反之，b为false的状态可以自己循环，也可以进入b = true.

的状态

您可以使用命令 check_fsm 来检测死锁状态。

请注意，在某些情况下，死锁状态的存在会影响模型检查的正确性。例如：

FAQ #007: CTL specification with top level existential path quantifier is wrongly reported as being violated. For example, for the model below both specifications are reported to be false though one is just the negation of the other! I know such problems can arise with deadlock states, but running it with -ctt says that everything is fine.
MODULE main
VAR b : boolean;
TRANS next(b) = b;
CTLSPEC EF b
CTLSPEC !(EF b)

对于转换关系中死锁状态的其他关键后果，请参阅this page。

通常，当 NuSMV 表示 "the case conditions are not exhaustive" 时，会添加一个 默认操作 和 TRUE 条件在 case 构造的末尾，当前面条件的 none 应用时触发。 默认操作最常见的选择是自循环，其编码如下：

MODULE main
VAR
  location: {l1,l2,l3};
ASSIGN
  init(location):= l1;
  next(location):=
    case
      (location = l1): l2;
      (location = l2): {l1, l3};
      TRUE           : location;
    esac;

注意：请注意，如果有多个条件具有相同的 guard，则只会使用这些条件中的第一个。因此，当在您的模型中 location = l2 时，location 的下一个值只能是 l1 而永远不会是 l3。要解决此问题，并在 l1 和 l3 之间做出一些不确定的选择，必须在与 set 值相同的条件下列出所有可能的未来值（即 {l1, l3}）。

我们可以在 NuSMV 中有终端状态吗？

Can we have terminal states in NuSMV?

verification

nusmv