0

次の構造 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 による Logic in Computer Science の教科書に記載されている表記法を使用しています。

明らかに、このようなモデルから、s1 と s2 で r が満たされているため、s0 (初期状態) で X r が満たされていることがわかります。Kripke 構造の NuSMV コードは次のとおりです (ここで説明)。

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 が false であることを返し、反例を生成します。

4

1 に答える 1

2

あなたのモデルは正しくありません。最初は、stateiss0とrisFALSEです。

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
于 2015-12-01T17:46:08.743 に答える