Ошибка в проверке модели 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}. Я использую обозначения, описанные в логике в учебнике информатики Хутом и Райаном.

Понятно, что из такой модели X r удовлетворяется в s0 (начальное состояние), поскольку r выполняется в s1 и s2. Мой код 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 является ложной и дает контрпример.

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