From 27df78c2b0b1514551c7b41cac6202eb6f601a44 Mon Sep 17 00:00:00 2001 From: masawei Date: Wed, 13 Aug 2014 00:40:24 +0200 Subject: [PATCH] Finished testing Ltl. - Regrettably, the LtlFilterTest could not be done, since an Ltl modechecker would be needed for that. Which, we don't have. |- So that is a TODO until such a modelchecker is implemented. - This concludes the testing for the refactured formulas. Next up: Documentation. Former-commit-id: 2d731edcd9a7a492a9792a1c82cac57c29c5c176 --- src/formula/csl/CslFilter.h | 4 +-- src/formula/ltl/LtlFilter.h | 4 +-- src/formula/ltl/Next.h | 4 +-- src/formula/prctl/PrctlFilter.h | 4 +-- src/parser/LtlParser.cpp | 30 ++++++++++----------- test/functional/modelchecker/FilterTest.cpp | 2 ++ test/functional/parser/LtlParserTest.cpp | 2 +- test/functional/parser/PrctlParserTest.cpp | 2 +- 8 files changed, 26 insertions(+), 26 deletions(-) diff --git a/src/formula/csl/CslFilter.h b/src/formula/csl/CslFilter.h index d77d38592..ef1ec5044 100644 --- a/src/formula/csl/CslFilter.h +++ b/src/formula/csl/CslFilter.h @@ -111,10 +111,10 @@ public: switch(this->opt) { case MINIMIZE: - desc += "min, "; + desc += "min; "; break; case MAXIMIZE: - desc += "max, "; + desc += "max; "; break; default: break; diff --git a/src/formula/ltl/LtlFilter.h b/src/formula/ltl/LtlFilter.h index 2dd9c9a7f..9f876bd8c 100644 --- a/src/formula/ltl/LtlFilter.h +++ b/src/formula/ltl/LtlFilter.h @@ -124,10 +124,10 @@ public: switch(this->opt) { case MINIMIZE: - desc += " min, "; + desc += "min; "; break; case MAXIMIZE: - desc += " max, "; + desc += "max; "; break; default: break; diff --git a/src/formula/ltl/Next.h b/src/formula/ltl/Next.h index ebf8edc96..0fd069135 100644 --- a/src/formula/ltl/Next.h +++ b/src/formula/ltl/Next.h @@ -112,10 +112,8 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const override { - std::string result = "("; - result += " X "; + std::string result = "X "; result += child->toString(); - result += ")"; return result; } diff --git a/src/formula/prctl/PrctlFilter.h b/src/formula/prctl/PrctlFilter.h index 48967486e..6341764f9 100644 --- a/src/formula/prctl/PrctlFilter.h +++ b/src/formula/prctl/PrctlFilter.h @@ -125,10 +125,10 @@ public: switch(this->opt) { case MINIMIZE: - desc += " min, "; + desc += "min; "; break; case MAXIMIZE: - desc += " max, "; + desc += "max; "; break; default: break; diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index 74cb89944..bb87ab79c 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -68,44 +68,45 @@ struct LtlParser::LtlGrammar : qi::grammar> formula >> qi::lit(")")| qi::lit("[") >> formula >> qi::lit("]"); + formula %= orFormula; formula.name("LTL formula"); orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = MAKE(ltl::Or, qi::_val, qi::_1)]; - orFormula.name("LTL formula"); + orFormula.name("Or"); andFormula = untilFormula[qi::_val = qi::_1] > *(qi::lit("&") > untilFormula)[qi::_val = MAKE(ltl::And, qi::_val, qi::_1)]; - andFormula.name("LTL formula"); + andFormula.name("And"); untilFormula = notFormula[qi::_val = qi::_1] > *((qi::lit("U") >> qi::lit("<=") > qi::int_ > notFormula)[qi::_val = MAKE(ltl::BoundedUntil, qi::_val, qi::_2, qi::_1)] | (qi::lit("U") > notFormula)[qi::_val = MAKE(ltl::Until, qi::_val, qi::_1)]); + until.name("Until"); notFormula = atomicLtlFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicLtlFormula)[qi::_val = MAKE(ltl::Not, qi::_1)]; - notFormula.name("LTL formula"); + notFormula.name("Not"); //This block defines rules for "atomic" state formulas //(Propositions, probabilistic/reward formulas, and state formulas in brackets) - atomicLtlFormula %= pathFormula | atomicProposition; - atomicLtlFormula.name("LTL formula"); + atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> formula >> qi::lit(")")| qi::lit("[") >> formula >> qi::lit("]"); + atomicLtlFormula.name("Atomic LTL formula"); atomicProposition = (freeIdentifierName)[qi::_val = MAKE(ltl::Ap, qi::_1)]; - atomicProposition.name("LTL formula"); + atomicProposition.name("Atomic Proposition"); //This block defines rules for parsing probabilistic path formulas pathFormula = (boundedEventually | eventually | globally | next); - pathFormula.name("LTL formula"); + pathFormula.name("Path Formula"); boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > formula)[qi::_val = MAKE(ltl::BoundedEventually, qi::_2, qi::_1)]; - boundedEventually.name("LTL formula"); + boundedEventually.name("Bounded Eventually"); eventually = (qi::lit("F") >> formula)[qi::_val = MAKE(ltl::Eventually, qi::_1)]; - eventually.name("LTL formula"); + eventually.name("Eventually"); globally = (qi::lit("G") >> formula)[qi::_val = MAKE(ltl::Globally, qi::_1)]; - globally.name("LTL formula"); + globally.name("Globally"); next = (qi::lit("X") >> formula)[qi::_val = MAKE(ltl::Next, qi::_1)]; - next.name("LTL formula"); + next.name("Next"); // This block defines rules for parsing filter actions. boundAction = (qi::lit("bound") > qi::lit("(") >> comparisonType >> qi::lit(",") >> qi::double_ >> qi::lit(")"))[qi::_val = @@ -144,10 +145,10 @@ struct LtlParser::LtlGrammar : qi::grammar, qi::_2, qi::_1, storm::property::MINIMIZE)] | (formula)[qi::_val = MAKE(ltl::LtlFilter, qi::_1)]; - filter.name("PRCTL formula filter"); + filter.name("LTL formula filter"); start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(ltl::LtlFilter, nullptr)] ) > qi::eoi; - start.name("LTL formula"); + start.name("start"); } qi::rule>(), Skipper> start; @@ -180,7 +181,6 @@ struct LtlParser::LtlGrammar : qi::grammar freeIdentifierName; qi::rule comparisonType; qi::rule::SortingCategory(), Skipper> sortingCategory; - }; std::shared_ptr> LtlParser::parseLtlFormula(std::string formulaString) { diff --git a/test/functional/modelchecker/FilterTest.cpp b/test/functional/modelchecker/FilterTest.cpp index a9f3cfbe8..ffbd11978 100644 --- a/test/functional/modelchecker/FilterTest.cpp +++ b/test/functional/modelchecker/FilterTest.cpp @@ -356,3 +356,5 @@ TEST(CslFilterTest, Safety) { ASSERT_EQ(0, result.selection.size()); ASSERT_EQ(0, result.stateMap.size()); } + +// TODO Set up the LtlFilterTest once an Ltl modelchecker has been implemented. diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp index 8086bbf88..5c55ab54a 100644 --- a/test/functional/parser/LtlParserTest.cpp +++ b/test/functional/parser/LtlParserTest.cpp @@ -124,7 +124,7 @@ TEST(LtlParserTest, parseLtlFilterTest) { ASSERT_EQ("filter[max; invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](X a)", formula->toString()); } -TEST(PrctlParserTest, commentTest) { +TEST(LtlParserTest, commentTest) { std::string input = "// This is a comment. And this is a commented out formula: F X a"; std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( diff --git a/test/functional/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp index dbdb508b7..bed83948c 100644 --- a/test/functional/parser/PrctlParserTest.cpp +++ b/test/functional/parser/PrctlParserTest.cpp @@ -181,7 +181,7 @@ TEST(PrctlParserTest, parsePrctlFilterTest) { ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); } -TEST(LtlParserTest, commentTest) { +TEST(PrctlParserTest, commentTest) { std::string input = "// This is a comment. And this is a commented out formula: R = ? [ F a ]"; std::shared_ptr> formula(nullptr); ASSERT_NO_THROW(