NuSMV: разница между IVAR и VAR - PullRequest
Новая
       24

NuSMV: разница между IVAR и VAR

0 голосов
/ 11 мая 2018

Я знаю разницу между IVAR (входные переменные) и VAR (переменные состояния) в NuSMV. Тем не менее, я могу понять контрпример, когда используется VAR, но я не в другом случае.

Позвольте мне показать это на примере. 

MODULE main

VAR

  v1: 0..20;

  v2: 0..20;

  v3: 0..100;


INIT

v3 = 0;

TRANS

    ((v2+v1 = 0)  -> (next(v3) = 10)) &

    (!(v2+v1 = 0) -> (next(v3) = v1 + v2))

LTLSPEC
  G(v3 = 10);

Контрпример (достаточно ясный), приведенный NuSMV: 

Trace Type: Counterexample 

  -> State: 1.1 <-

    v1 = 0

    v2 = 0

    v3 = 0

  -- Loop starts here

  -> State: 1.2 <-

    v3 = 10

  -> State: 1.3 <-

    v1 = 7

    v2 = 6

  -> State: 1.4 <-
    v1 = 0

    v2 = 0

    v3 = 13
  -> State: 1.5 <-

    v3 = 10

Теперь измените v1 и v2 на IVAR. 

MODULE main

IVAR

  v1: 0..20;

  v2: 0..20;

VAR

  v3: 0..100;

INIT

    v3 = 0;

TRANS

    ((v2+v1 = 0)  -> (next(v3) = 10)) &

    (!(v2+v1 = 0) -> (next(v3) = v1 + v2))

LTLSPEC
  G(v3 = 10);

Контрпример: 

Trace Type: Counterexample 

  -> State: 1.1 <-

    v3 = 0

  -> Input: 1.2 <-

    v1 = 7

    v2 = 3

  -- Loop starts here

  -> State: 1.2 <-

    v3 = 10

  -> Input: 1.3 <-

  -- Loop starts here

  -> State: 1.3 <-

  -> Input: 1.4 <-

  -- Loop starts here

  -> State: 1.4 <-

  -> Input: 1.5 <-

  -- Loop starts here

  -> State: 1.5 <-

  -> Input: 1.6 <-

  -- Loop starts here

  -> State: 1.6 <-

  -> Input: 1.7 <-

  -> State: 1.7 <-

Может ли кто-нибудь объяснить, почему этот контрпример такой странный? Имеет несколько вложенных циклов. Что означает вывод?

1 Ответ

0 голосов
/ 11 мая 2018

Оба контрпримеры фальсифицируют свойство в самом первом состоянии трассировки выполнения, так что то, что происходит дальше, не очень важно.

Из документов nuXmv:

4,7 Следы

Трассировка состоит из начального состояния, за которым может следовать последовательность пар состояний-входов, соответствующая возможному выполнению модели. Помимо начального состояния каждая пара содержит входы, которые вызвали переход в новое состояние, и новое состояние сам. Исходное состояние не имеет таких входных значений, определенных как не зависит от значений любого из входов. [...]

Таким образом, трасса обычно имеет следующую структуру: 

S_0 | I_0 -> S_1 | I_1 -> S_2 | ... | I_{N-1} -> S_N

Идея состоит в том, что состояние S_{k+1} получается путем применения входных данных I_k к состоянию S_k.

Можно попробовать использовать команды goto_state и print_current_state, чтобы перейти к контрпримеру и напечатать содержимое каждого состояния. В качестве альтернативы можно вспомнить, что NuSMV и nuXmv выводят только изменяемые переменные из одного состояния в другое, поэтому трассировка выполнения должна выглядеть следующим образом: 

  -> State: 1.1 <-
    v3 = 0
  -> Input: 1.2 <-
    v1 = 7
    v2 = 3

  -- Loop starts here
  -> State: 1.2 <-
    v3 = 10
  -> Input: 1.3 <-
    v1 = 7
    v2 = 3

  -- Loop starts here
  -> State: 1.3 <-
    v3 = 10
  -> Input: 1.4 <-
    v1 = 7
    v2 = 3

  -- Loop starts here
  -> State: 1.4 <-
    v3 = 10
  -> Input: 1.5 <-
    v1 = 7
    v2 = 3

  -> State: 1.5 <-
    v3 = 10

Так что, в основном, после первого перехода мы навсегда останемся в одном и том же состоянии с неизменными входами и выходами.

Возможно, вы захотите связаться со списком рассылки NuSMV или nuXmv и сообщить об этой проблеме в программе вывода.

...