NuSMV 模型检查中的错误？

Question

假设我有以下结构 M = (S, R, L) 其中 S = {s0, s1, s2} 是可能状态的集合，R 是一个转换关系，这样：s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, L是每个状态的标记函数，定义为： L(s0) = {p, q}, L(s1) = {q, r }，并且 L(s2) = {r}。我正在使用 Huth 和 Ryan 在计算机科学教科书中的逻辑中描述的符号。

显然，从这样的模型中，我们在 s0（初始状态）中满足 X r，因为 r 在 s1 和 s2 中满足。我的 Kripke 结构的 NuSMV 代码如下 (as described here)。

MODULE main
VAR
    p : boolean;
    q : boolean;
    r : boolean;
    state : {s0, s1, s2};

ASSIGN
    init(state) := s0;
    next(state) := 
    case
        state = s0          : {s1, s2};
        state = s1          : {s2};
        state = s2          : {s2};
        TRUE                : state;
    esac;

   init(p) := TRUE; 
   init(q) := TRUE;
   init(r) := FALSE;

   next(p) :=
    case
        state = s1 | state = s2     : FALSE;
    esac;
    next(q) :=
    case
        state = s1                  : TRUE;
        state = s2                  : FALSE;
        TRUE                        : q;
    esac;
   next(r) :=
    case
        state = s1                  : FALSE;
        state = s2                  : TRUE;
        TRUE                        : r;
    esac;

LTLSPEC
    X r

但 NuSMV 返回规范 X r 为假并产生反例。

Answer 1

您的模型不正确。最初，state 是 s0，r 是 FALSE。

当计算next(r) 时，state 仍然是s0。因此，只有最后一种情况为真，r 仍然是FALSE。结果，X r 不成立。

您可以如下修改您的模型，其中DEFINE 用于定义标注功能：

MODULE main
VAR
  state : {s0, s1, s2};

ASSIGN
  init(state) := s0;
  next(state) :=
  case
    state = s0          : {s1, s2};
    state = s1          : {s0, s2};
    state = s2          : {s2};
  esac;

DEFINE
  p := state = s0;
  q := state = s0 | state = s1;
  r := state = s1 | state = s2;

LTLSPEC
  X r