NuSMV 模型检查中的错误？

Question

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

显然，从这样的模型中，我们有 X r 在 s0（初始状态）中得到满足，因为 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 returns 说明 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

NuSMV 模型检查中的错误？

Bug in NuSMV Model Checking?

logic

model-checking

nusmv