NuSMV模型检查中的错误? [英] Bug in NuSMV Model Checking?

问题描述

假设我具有以下结构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在计算机科学中的逻辑"教科书中描述的符号.

Suppose I have following structure M = (S, R, L) where S = {s0, s1, s2} is the set of possible states, R is a transition relation such that: s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, and L is the labeling function for each state defined by: L(s0) = {p, q}, L(s1) = {q, r}, and L(s2) = {r}. I am using notations describe in Logic in Computer Science textbook by Huth and Ryan.

很显然，根据这种模型，由于r在s1和s2中满足，因此我们在s0(初始状态)中满足了X r.我对Kripke结构的NuSMV代码如下(此处所述).

Clearly, from such model, we have X r is satisfied in s0 (the initial state), since r is satisfied in s1 and s2. My NuSMV code for the Kripke structure is as follows (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为假，并产生了反例.

But NuSMV returns that specification X r is false and yields a counterexample.

推荐答案

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

Your model is not correct. Initially, state is s0 and r is FALSE.

计算next(r)时，state仍为s0.因此，只有最后一种情况为真，其中r保留为FALSE.结果，X r不成立.

When next(r) is calculated, the state is still s0. Therefore, only the last case is true, where r remains FALSE. As a result, X r does not hold.

您可以按以下方式修改模型，其中DEFINE用于定义标签功能:

You can modify your model as follows, where DEFINE is used for defining the labeling function:

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模型检查中的错误?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！