Модель NuSMV - AND

Question

Я пытаюсь написать следующую модель в NuSMV

Другими словами, z становится плохим только тогда, когда x и y также находятся в плохом состоянии. Это код, который я написал

MODULE singleton
    VAR state: {good, bad};
    INIT state = good
    TRANS (state = good) -> next(state) = bad
    TRANS (state = bad) -> next(state) = bad

MODULE effect(cond)
    VAR state: {good, bad};
    ASSIGN
    init(state) := good;
    next(state) := case
        (state = bad) : bad;
        (state = good & cond) : bad;
        (!cond) : good;
        TRUE : state;
        esac;

MODULE main 
    VAR x : singleton;
    VAR y : singleton;
    VAR z : effect((x.state = bad) & (y.state = bad));

Но я получил только эти достижимые состояния

NuSMV > print_reachable_states -v
######################################################################
system diameter: 3
reachable states: 3 (2^1.58496) out of 8 (2^3)
  ------- State    1 ------
  x.state = good
  y.state = good
  z.state = good
  ------- State    2 ------
  x.state = bad
  y.state = bad
  z.state = bad
  ------- State    3 ------
  x.state = bad
  y.state = bad
  z.state = good
  -------------------------
######################################################################

Как я могу изменить свой код, чтобы получить также

x.state = good
y.state = bad
z.state = good

x.state = bad
y.state = good
z.state = good

в достижимых штатах?

Кроме того, я не уверен, должен ли я добавить или нет ту красную стрелку, напечатанную на рисунке модели: если x и y находятся в плохом состоянии, я хочу, чтобы наверняка рано или поздно z тоже стало плохим.

Большое спасибо за помощь!

Answer 1

Штаты

x.state = good
y.state = bad
z.state = good

x.state = bad
y.state = good
z.state = good

недоступны, потому что каждый подмодуль main выполняет переход одновременно с другими, и потому что вы инициируете детерминированный переход для ваших переменных состояния; то есть в вашей модели оба x а также y изменить состояние с good в bad в то же время. Более того, в отличие от вашей красивой картинки, ваш smv В коде не допускается какой-либо цикл за исключением цикла в конечном состоянии.

---

Чтобы исправить вашу модель, вам нужно только указать, что - в случае x (Соотв. y) является good-- ты хочешь next(x) (Соотв. next(y)) быть либо good или же bad, но не насильственное решение. например

MODULE singleton
VAR
  state: { good, bad };

ASSIGN
  init(state) := good;
  next(state) := case
      state = good : { good, bad };
      TRUE         : bad;
    esac;


MODULE effect(cond)
VAR
  state: { good, bad };

ASSIGN
  init(state) := good;
  next(state) := case
      (state = bad | cond) : bad;
      TRUE                 : state;
    esac;


MODULE main
VAR
    x : singleton;
    y : singleton;
    z : effect((x.state = bad) & (y.state = bad));

примечание: я также упростил правила для модуляeffectхотя это было ненужным.

Вы можете проверить модель следующим образом:

nuXmv > reset; read_model -i test.smv ; go; print_reachable_states -v
######################################################################
system diameter: 3
reachable states: 5 (2^2.32193) out of 8 (2^3)
  ------- State    1 ------
  x.state = good
  y.state = bad
  z.state = good
  ------- State    2 ------
  x.state = good
  y.state = good
  z.state = good
  ------- State    3 ------
  x.state = bad
  y.state = good
  z.state = good
  ------- State    4 ------
  x.state = bad
  y.state = bad
  z.state = bad
  ------- State    5 ------
  x.state = bad
  y.state = bad
  z.state = good
  -------------------------
######################################################################

---

Что касается вашего второго вопроса, пример кода, который я вам предоставил, гарантирует собственность, которую вы хотите проверить:

nuXmv > check_ltlspec -p "G ((x.state = bad & y.state = bad) -> F z.state = bad)"
-- specification  G ((x.state = bad & y.state = bad) ->  F z.state = bad)  is true

Это, очевидно, так, потому что самоконтроль, обведенный красным краем на вашей картинке, отсутствует. Если вы подумаете об этом, этот переход позволил бы по крайней мере одно выполнение, в котором текущее состояние остается равным

x.state = bad
y.state = bad
z.state = good

на неопределенный срок, и это будет контрпример к вашей спецификации.

---

РЕДАКТИРОВАТЬ:

Вы также можете исправить код, просто написав это:

MODULE singleton
    VAR state: {good, bad};
    INIT state = good
    TRANS (state = bad) -> next(state) = bad

Удаление линии TRANS (state = good) -> next(state) = bad позволяет x а также y изменить произвольно, когда state = goodЭто означает, что они могут оставаться недетерминированными good или стать bad, Это полностью эквивалентно предоставленному мною коду, хотя на первый взгляд менее понятно, поскольку скрывает недетерминизм под капотом, а не делает его явным.