Спецификация NuSMV CTL
Я начал изучать 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
Прежде всего, позвольте мне переименовать state в my_var в вашей модели. Это позволяет не путать фактическое состояние автомата с введенной вами переменной state.
AG (my_var = a -> AX my_var = b)
In every state of every possible execution, if
my_varis equal toathen it must be necessarily the case that in the next statemy_varis equal tob.
Это свойство является, которое вы хотите проверить.
AF (my_var=a -> AX my_var=b)
Sooner or later, if
my_varis equal toathen it must be necessarily the case that in the next statemy_varis equal tob.
Обратите внимание, что значение является истинный в двух случаях:
- когда посылка верна и вывод верен, или
- когда предпосылка ложна
Таким образом, импликация тривиально становится истинной для любого состояния, для которого посылка my_var=a не проверена, то есть для любого состояния, отличного от начального. Поскольку вы используете AF, вам требуется, чтобы импликация проверялась только (по крайней мере) в одном состоянии для каждого возможного пути выполнения.
В некотором смысле это "слишком слабый" по отношению к тому, что вы хотите проверить.
AF (my_var=a -> AF my_var=b)
Sooner or later, if
my_varis equal toathen it must be necessarily the case at some point in the future (wrt. the state in whichmy_varis equal toa)my_varbecomes equal tob.
Подобно предыдущему, это еще слабее, потому что даже не указано, в какой момент 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 или эти слайды, чтобы узнать больше об инструменте и языке.
Что такое
Stages?