Применение на практике mcheck

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

<>p -> (!p U (s & !p & X(!p U t))) 

Эта формула описывает требование, что событию p предшествуют события s,t.

На первый взгляд, кажется, что подформулу !p & X(!p U t) можно заменить на более короткую формулу !p U t. Эквивалентность этих двух формул можно легко проверить с помощью mcheck. Для этого необходимо создать файл eq.txt, содержащий пару формул с префиксом '?' и разделителем ':':

? !p & X(!p U t)
: !p U t

После запуска верификатора выясняется, что формулы не эквивалентные, и имеется контр-пример:

$ java -jar mch.jar eq.txt 
Comparing: LTL : !p & X (!p U t)

     with: LTL : !p U t


Not equivalent.

second allows: T t {T T T T}*

Анализируя контр-пример, становится понятно, что вторая формула допускает состояние с меткой t в следующем (втором) состоянии после начального, тогда как первая - не допускает!