时间戳

首页 > 解决方案 > 我们可以在 NuSMV 中有终端状态吗？

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

问题描述

是否有可能在 NuSMV 中有一个没有转换到任何其他状态的状态？例如，在我的代码中 l3 没有任何转换是否有效？当我运行这个 NuSMV 时，我给出了“案例条件并不详尽”的错误。谢谢！

MODULE main

VAR

location: {l1,l2,l3};


ASSIGN

init(location):=l1;

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

标签： verificationnusmv

解决方案

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

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

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

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

有关更多信息，请参阅本课程的第二部分，这也适用NuSMV于大部分内容。

某个状态没有未来状态的 FSM 的示例是：

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

bis的状态true没有未来状态。相反，bis的状态false可以自行循环或转到 的状态b = true。

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

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

常见问题解答 #007：具有顶级存在路径量词的 CTL 规范被错误地报告为违反。例如，对于下面的模型，两种规格都被报告为错误的，尽管其中一个只是对另一个的否定！我知道死锁状态可能会出现此类问题，但是使用 -ctt 运行它表示一切都很好。

MODULE main
VAR b : boolean;
TRANS next(b) = b;
CTLSPEC EF b
CTLSPEC !(EF b)

有关转换关系中死锁状态的其他严重后果，请参阅此页面。

通常，当NuSMV说“案例条件并非详尽无遗”时，会在构造末尾添加一个带有条件的默认操作，当前面的条件都不适用时会触发该操作。默认动作最常见的选择是自循环，其编码如下：TRUEcase

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

注意：请注意，如果有多个条件具有相同的保护，则只会使用这些条件中的第一个。出于这个原因，当在您的模型中时，location = l2下一个值location只能是l1并且从不l3。为了解决这个问题，并在 和 中进行一些不确定的选择l1，必须列出与一组l3值相同的条件下所有可能的未来值（即）。{l1, l3}

推荐阅读