Как преобразовать требования безопасности системы в линейные временные свойства..?
Я изменил свою проблему более ясно здесь. Существует две разные модели: модель отправителя и модель получателя. Я хочу проверить, что передаваемое сообщение не совпадает с получателем.
MODULE main()
VAR
state : { informationsource, getinformation, transmitter, receiver, destination, ACK };
messageReceived : boolean;
messageTransmitted : boolean;
ASSIGN
init(state) := informationsource;
init(messageReceived) := FALSE;
next(state) := case
state = informationsource : getinformation;
state = getinformation : transmitter;
state = transmitter : receiver;
state = receiver & messageReceived = TRUE : destination;
TRUE : {destination, ACK} ;
esac;
LTLSPEC (G (состояние = получатель -> messageTransmited!= MessageReceived))