From 01b1efc12d96a153ac271e48616cde1751752bca Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 23 Apr 2013 11:27:55 +0200 Subject: [PATCH] Some improvements/corrections to the LTL parser and some test cases for it --- src/formula/Ltl/BoundedUntil.h | 12 +++ src/formula/Ltl/Until.h | 12 +++ src/formula/abstract/AbstractFormula.h | 2 +- src/parser/LtlParser.cpp | 18 ++--- test/parser/CslParserTest.cpp | 1 - test/parser/LtlParserTest.cpp | 107 +++++++++++++++++++++++++ 6 files changed, 140 insertions(+), 12 deletions(-) create mode 100644 test/parser/LtlParserTest.cpp diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h index d42b92109..fb4ce5e43 100644 --- a/src/formula/Ltl/BoundedUntil.h +++ b/src/formula/Ltl/BoundedUntil.h @@ -88,6 +88,18 @@ public: //intentionally left empty } + /*! + * @brief Return string representation of this formula. + * + * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the + * root of a path formula); hence this function is overwritten in this class. + * + * @return A string representation of the formula. + */ + virtual std::string toString() const { + return "(" + storm::formula::abstract::BoundedUntil>::toString() + ")"; + } + /*! * Clones the called object. * diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h index 1689f7d00..d885ca6eb 100644 --- a/src/formula/Ltl/Until.h +++ b/src/formula/Ltl/Until.h @@ -84,6 +84,18 @@ public: // Intentionally left empty } + /*! + * @brief Return string representation of this formula. + * + * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the + * root of a path formula); hence this function is overwritten in this class. + * + * @return A string representation of the formula. + */ + virtual std::string toString() const { + return "(" + storm::formula::abstract::Until>::toString() + ")"; + } + /*! * Clones the called object. * diff --git a/src/formula/abstract/AbstractFormula.h b/src/formula/abstract/AbstractFormula.h index 99fa7f78c..83f3f8f43 100644 --- a/src/formula/abstract/AbstractFormula.h +++ b/src/formula/abstract/AbstractFormula.h @@ -62,7 +62,7 @@ public: /*! * @brief Return string representation of this formula. * - * @note very subclass must implement this method. + * @note every subclass must implement this method. * * @returns a string representation of the formula */ diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index 2ee16bf40..bd75a73b2 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -51,9 +51,12 @@ struct LtlParser::LtlGrammar : qi::grammar *(qi::lit("|") > andFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_1)]; orFormula.name("state formula"); - andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = + andFormula = untilFormula[qi::_val = qi::_1] > *(qi::lit("&") > untilFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_1)]; andFormula.name("state formula"); + untilFormula = notFormula[qi::_val = qi::_1] > + *((qi::lit("U") >> qi::lit("<=") > qi::int_ > notFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_2, qi::_1)] | + (qi::lit("U") > notFormula)[qi::_val = phoenix::new_>(qi::_val, qi::_1)]); notFormula = atomicLtlFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicLtlFormula)[qi::_val = phoenix::new_>(qi::_1)]; notFormula.name("state formula"); @@ -85,7 +88,7 @@ struct LtlParser::LtlGrammar : qi::grammar> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; @@ -96,12 +99,6 @@ struct LtlParser::LtlGrammar : qi::grammar ltlFormula)[qi::_val = phoenix::new_ >(qi::_1)]; globally.name("ltl formula"); - boundedUntil = (ltlFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > ltlFormula) - [qi::_val = phoenix::new_>(phoenix::bind(&storm::formula::ltl::AbstractLtlFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_3, qi::_2)]; - boundedUntil.name("ltl formula"); - until = (ltlFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") > ltlFormula)[qi::_val = - phoenix::new_>(phoenix::bind(&storm::formula::ltl::AbstractLtlFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_2)]; - until.name("ltl formula"); start = ltlFormula; start.name("LTL formula"); @@ -113,6 +110,7 @@ struct LtlParser::LtlGrammar : qi::grammar*(), Skipper> atomicLtlFormula; qi::rule*(), Skipper> andFormula; + qi::rule*(), Skipper> untilFormula; qi::rule*(), Skipper> atomicProposition; qi::rule*(), Skipper> orFormula; qi::rule*(), Skipper> notFormula; @@ -125,8 +123,8 @@ struct LtlParser::LtlGrammar : qi::grammar*(), Skipper> boundedEventually; qi::rule*(), Skipper> eventually; qi::rule*(), Skipper> globally; - qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; - qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> until; + qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; + qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> until; qi::rule freeIdentifierName; diff --git a/test/parser/CslParserTest.cpp b/test/parser/CslParserTest.cpp index 313142a14..f7637ceb1 100644 --- a/test/parser/CslParserTest.cpp +++ b/test/parser/CslParserTest.cpp @@ -94,7 +94,6 @@ TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) { delete cslParser->getFormula(); delete cslParser; - } TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { diff --git a/test/parser/LtlParserTest.cpp b/test/parser/LtlParserTest.cpp new file mode 100644 index 000000000..cd2a842d6 --- /dev/null +++ b/test/parser/LtlParserTest.cpp @@ -0,0 +1,107 @@ +/* + * LtlParserTest.cpp + * + * Created on: 22.04.2013 + * Author: thomas + */ + +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/LtlParser.h" + +TEST(LtlParserTest, parseApOnlyTest) { + std::string ap = "ap"; + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_NO_THROW( + ltlParser = new storm::parser::LtlParser(ap); + ); + + ASSERT_NE(ltlParser->getFormula(), nullptr); + + + ASSERT_EQ(ltlParser->getFormula()->toString(), ap); + + delete ltlParser->getFormula(); + delete ltlParser; +} + +TEST(LtlParserTest, parsePropositionalFormulaTest) { + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_NO_THROW( + ltlParser = new storm::parser::LtlParser("!(a & b) | a & ! c") + ); + + ASSERT_NE(ltlParser->getFormula(), nullptr); + + + ASSERT_EQ(ltlParser->getFormula()->toString(), "(!(a & b) | (a & !c))"); + + delete ltlParser->getFormula(); + delete ltlParser; +} + +TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_NO_THROW( + ltlParser = new storm::parser::LtlParser("F<=5 a") + ); + + ASSERT_NE(ltlParser->getFormula(), nullptr); + + storm::formula::ltl::BoundedEventually* op = static_cast*>(ltlParser->getFormula()); + + ASSERT_EQ(static_cast(5), op->getBound()); + + ASSERT_EQ(ltlParser->getFormula()->toString(), "F<=5 a"); + + delete ltlParser->getFormula(); + delete ltlParser; +} + +TEST(LtlParserTest, parseBoundedUntilFormulaTest) { + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_NO_THROW( + ltlParser = new storm::parser::LtlParser("a U<=3 b") + ); + + ASSERT_NE(ltlParser->getFormula(), nullptr); + + storm::formula::ltl::BoundedUntil* op = static_cast*>(ltlParser->getFormula()); + + ASSERT_EQ(static_cast(3), op->getBound()); + + ASSERT_EQ("(a U<=3 b)", ltlParser->getFormula()->toString()); + + delete ltlParser->getFormula(); + delete ltlParser; +} + +TEST(LtlParserTest, parseComplexUntilTest) { + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_NO_THROW( + ltlParser = new storm::parser::LtlParser("a U b U<=3 c") + ); + + ASSERT_NE(ltlParser->getFormula(), nullptr); + + + ASSERT_EQ(ltlParser->getFormula()->toString(), "((a U b) U<=3 c)"); + + delete ltlParser->getFormula(); + delete ltlParser; +} + +TEST(LtlParserTest, parseComplexFormulaTest) { + storm::parser::LtlParser* ltlParser = nullptr; + ASSERT_NO_THROW( + ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b") + ); + + ASSERT_NE(ltlParser->getFormula(), nullptr); + + ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlParser->getFormula()->toString()); + delete ltlParser->getFormula(); + delete ltlParser; + +} +