menshovsergey / verification Goto Github PK

Мы использовали ltl2ba (http://www.lsv.fr/~gastin/ltl2ba/). LTL to Buchi

• make в ltl2ba
• mvn clean package в корневой

Операторы !, &, |, ->, <->, X, G, F, R, U

Доступны скобки и значения true и false

Переменные записываются в кавычках

В файлах ./data/example* содержится автомат и корректные/некорректные формулы

java -jar ./target/verifier.jar -m ./data/example.xstd -f ./data/example_correct.ltl - запускает верификатор на модели example и проверяет все LTL формулы из файла data/example_correct.ltl;