Какова интерпретация <> P -> (! PUR) - PullRequest
Новая
       38

Какова интерпретация <> P -> (! PUR)

1 голос
/ 19 апреля 2019

Что такое интерпретация <> P -> (! P U R)? Это кажется противоречием, так как в будущем ожидается P и проверка отсутствия P до R. Инструмент проверки моделей передает это как через BDD, так и через методы BMC.

1 Ответ

2 голосов
/ 24 апреля 2019

Я не вижу никакого противоречия.

Свойство реализуется любым автоматом Бучи st

  • P всегда ложно [потому что предпосылка импликации ложна], или
  • В какой-то момент в будущем P становится истинным, но в течение некоторого времени P может быть ложным, пока не станет истинным R.

т.е.

enter image description here

На естественном языке это свойство можно выразить следующим образом: "Если по какой-либо случайности рано или поздно P станет истинным, то оно должноможет быть случай, когда 'событие' R сработало первым '.

Например, вы можете представить, что P будет "отправляющим ответное сообщение" и R be "полученным входным сигналомсообщение " и все свойство равно " не отправлено ни одного нежелательного ответного сообщения ".

...