Спецификация NuSMV CTL - PullRequest
Новая
       98

Спецификация NuSMV CTL

1 голос
/ 29 мая 2019

Я начал изучать NuSMV в эти дни. У меня есть этот код: 

 MODULE main

 VAR

 state: {a,b,c,d,e};   
 ASSIGN

 init(state) := a; 

 next(state) := case

            (state = a)  : b;

            (state = b)  : c;

            (state = c)  : d;

            (state = d)  : e;                   

            TRUE:Stages;

       esac;

Я хочу убедиться, что каждый раз, когда мы находимся в состоянии «а», следующим состоянием будет состояние «б». какой из них правильный (даже если я попробовал оба из них, и они дали мне оба из них правда): 

check_ctlspec -p "AG (state=a -> AX state=b)"

check_ctlspec -p "AF (state=a -> AX state=b)"

check_ctlspec -p "AF (state=a -> AF state=b)"  

check_ctlspec -p "AF (state=a -> state=b)"

Мой второй вопрос: в приведенной выше модели нет перехода из состояния «d» в состояние «a», но когда я проверяю это, используя 

check_ctlspec -p "AF (state=d -> AX state=a)"

результат был верным. Почему это так?

1 Ответ

0 голосов
/ 30 мая 2019

Прежде всего, позвольте мне переименовать state с my_var в вашей модели.Это позволяет избежать путаницы с действительным состоянием автомата с введенной вами переменной state.

  • AG (my_var = a -> AX my_var = b)

В каждом состояниипри каждом возможном выполнении, если my_var равно a, то в следующем состоянии my_var обязательно должно быть b.

Это свойство, которое вы хотите проверить.

  • AF (my_var=a -> AX my_var=b)

Рано или поздно, если my_var равно a тогда обязательно должен быть случай, когда в следующем состоянии my_var равно b.

Обратите внимание, что значение равно true в двух случаях:

  • , когда предпосылка верна, а вывод верен, или
  • , когда предпосылка ложна

Таким образом, утверждение тривиальновыполняется любым состоянием, для которого предпосылка my_var=a не проверена, то есть любым состоянием, отличным от исходного состояния.Поскольку вы используете AF, вы требуете проверки импликации только (хотя бы) в одном состоянии для каждого возможного пути выполнения.

В некотором смысле это "слишком слабый" относительно того, что вы хотите проверить.

  • AF (my_var=a -> AF my_var=b)

Рано или поздно, если my_var равно aтогда это должно быть обязательно в какой-то момент в будущем (в отношении состояния, в котором my_var равно a) my_var становится равным b.

как и предыдущий, он еще слабее, поскольку даже не указывает, в какой момент my_var становится равным b.

  • AF (my_var=a -> my_var=b)

Обратите внимание, что значение (my_var=a -> my_var=b) истинно только тогда, когда my_var=a ложно, потому что my_var нельзя одновременно назначать как a, так и b.Тем не менее, это условие проверяется любым состоянием, отличным от исходного состояния, поэтому снова свойство проверяется тривиально.

  • AF (my_var=d -> AX my_var=a)

Опять же, этоусловие слишком слабое, потому что вы используете AF, а не AG.Это подразумевается любым состоянием, для которого my_var != d, поэтому достаточно для проверки всего свойства.

Я бы пригласил вас взглянуть на этот стек-переполнение Q / A или этих слайдов для получения дополнительной информации об инструменте и языке.

...