diff --git a/src/formula/csl/CslFilter.h b/src/formula/csl/CslFilter.h index d09902760..d77d38592 100644 --- a/src/formula/csl/CslFilter.h +++ b/src/formula/csl/CslFilter.h @@ -52,7 +52,7 @@ public: } virtual ~CslFilter() { - this->actions.clear(); + // Intentionally left empty. } void check(storm::modelchecker::csl::AbstractModelChecker const & modelchecker) const { diff --git a/src/formula/ltl/LtlFilter.h b/src/formula/ltl/LtlFilter.h index d35b9fd46..2dd9c9a7f 100644 --- a/src/formula/ltl/LtlFilter.h +++ b/src/formula/ltl/LtlFilter.h @@ -42,7 +42,7 @@ public: } LtlFilter(std::shared_ptr> const & child, std::shared_ptr> const & action, OptimizingOperator opt = UNDEFINED) : AbstractFilter(action, opt), child(child) { - this->actions.push_back(action); + // Intentionally left empty. } LtlFilter(std::shared_ptr> const & child, std::vector>> const & actions, OptimizingOperator opt = UNDEFINED) : AbstractFilter(actions, opt), child(child) { @@ -50,7 +50,7 @@ public: } virtual ~LtlFilter() { - this->actions.clear(); + // Intentionally left empty. } @@ -83,6 +83,35 @@ public: } + Result evaluate(storm::modelchecker::ltl::AbstractModelChecker const & modelchecker) const { + // First, get the model checking result. + Result result; + + if(this->opt != UNDEFINED) { + // If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker. + LOG4CPLUS_ERROR(logger, "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented."); + throw storm::exceptions::NotImplementedException() << "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented."; + } else { + result.pathResult = child->check(modelchecker); + } + + // Now apply all filter actions and return the result. + + // Init the state selection and state map vectors. + result.selection = storm::storage::BitVector(result.stateResult.size(), true); + result.stateMap = std::vector(result.selection.size()); + for(uint_fast64_t i = 0; i < result.selection.size(); i++) { + result.stateMap[i] = i; + } + + // Now apply all filter actions and return the result. + for(auto action : this->actions) { + result = action->evaluate(result, modelchecker); + } + + return result; + } + std::string toString() const override { std::string desc = ""; @@ -142,35 +171,6 @@ public: private: - Result evaluate(storm::modelchecker::ltl::AbstractModelChecker const & modelchecker) const { - // First, get the model checking result. - Result result; - - if(this->opt != UNDEFINED) { - // If it is specified that min/max probabilities/rewards should be computed, call the appropriate method of the model checker. - LOG4CPLUS_ERROR(logger, "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented."); - throw storm::exceptions::NotImplementedException() << "Calculation of minimizing and maximizing schedulers for LTL-formula model checking is not yet implemented."; - } else { - result.stateResult = child->check(modelchecker); - } - - // Now apply all filter actions and return the result. - - // Init the state selection and state map vectors. - result.selection = storm::storage::BitVector(result.stateResult.size(), true); - result.stateMap = std::vector(result.selection.size()); - for(uint_fast64_t i = 0; i < result.selection.size(); i++) { - result.stateMap[i] = i; - } - - // Now apply all filter actions and return the result. - for(auto action : this->actions) { - result = action->evaluate(result, modelchecker); - } - - return result; - } - void writeOut(Result const & result, storm::modelchecker::ltl::AbstractModelChecker const & modelchecker) const { // Test for the kind of result. Values or states. diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp index 25d62d241..74cb89944 100644 --- a/src/parser/LtlParser.cpp +++ b/src/parser/LtlParser.cpp @@ -62,13 +62,13 @@ struct LtlParser::LtlGrammar : qi::grammar::INDEX] | (qi::lit("value"))[qi::_val = storm::property::action::SortAction::VALUE] ); - //Comment: Empty line or line starting with "//" + // Comment: Empty line or line starting with "//" comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; - //This block defines rules for parsing state formulas - formula %= orFormula; + // This block defines rules for parsing state formulas + formula %= orFormula | qi::lit("(") >> formula >> qi::lit(")")| qi::lit("[") >> formula >> qi::lit("]"); formula.name("LTL formula"); orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = MAKE(ltl::Or, qi::_val, qi::_1)]; @@ -85,7 +85,7 @@ struct LtlParser::LtlGrammar : qi::grammar> formula >> qi::lit(")"); + atomicLtlFormula %= pathFormula | atomicProposition; atomicLtlFormula.name("LTL formula"); atomicProposition = (freeIdentifierName)[qi::_val = MAKE(ltl::Ap, qi::_1)]; @@ -133,7 +133,7 @@ struct LtlParser::LtlGrammar : qi::grammar> (qi::lit(";") | qi::eps); + abstractAction = (qi::lit(";") | qi::eps) >> (boundAction | invertAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps); abstractAction.name("filter action"); filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index 4d13479e1..e4289a2b4 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -156,7 +156,7 @@ TEST(CslParserTest, parseComplexFormulaTest) { } TEST(CslParserTest, parseCslFilterTest) { - std::string input = "filter[formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)"; + std::string input = "filter[max; formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)"; std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( formula = storm::parser::CslParser::parseCslFormula(input) @@ -165,6 +165,8 @@ TEST(CslParserTest, parseCslFilterTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula, nullptr); + ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator()); + ASSERT_EQ(5, formula->getActionCount()); ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); @@ -173,7 +175,7 @@ TEST(CslParserTest, parseCslFilterTest) { ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); // The input was parsed correctly. - ASSERT_EQ("filter[formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); + ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); } TEST(CslParserTest, commentTest) { diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp index 0ccda625a..8086bbf88 100644 --- a/test/functional/parser/LtlParserTest.cpp +++ b/test/functional/parser/LtlParserTest.cpp @@ -9,6 +9,10 @@ #include "storm-config.h" #include "src/parser/LtlParser.h" #include "src/exceptions/WrongFormatException.h" +#include "src/formula/actions/InvertAction.h" +#include "src/formula/actions/SortAction.h" +#include "src/formula/actions/RangeAction.h" +#include "src/formula/actions/BoundAction.h" namespace ltl = storm::property::ltl; @@ -20,7 +24,7 @@ TEST(LtlParserTest, parseApOnlyTest) { ); ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ(ltlFormula->toString(), formula); + ASSERT_EQ(formula, ltlFormula->toString()); } TEST(LtlParserTest, parsePropositionalFormulaTest) { @@ -31,7 +35,7 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) { ); ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ(ltlFormula->toString(), "(!(a & b) | (a & !c))"); + ASSERT_EQ("(!(a & b) | (a & !c))", ltlFormula->toString()); } /*! @@ -46,7 +50,7 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest) { ); ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ(ltlFormula->toString(), "(F & b)"); + ASSERT_EQ("(F & b)", ltlFormula->toString()); } /*! @@ -61,7 +65,7 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest2) { ); ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ(ltlFormula->toString(), "F F"); + ASSERT_EQ("F F", ltlFormula->toString()); } TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { @@ -78,7 +82,7 @@ TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { ASSERT_EQ(static_cast(5), op->getBound()); - ASSERT_EQ(ltlFormula->toString(), "F<=5 a"); + ASSERT_EQ("F<=5 a", ltlFormula->toString()); } TEST(LtlParserTest, parseBoundedUntilFormulaTest) { @@ -95,7 +99,47 @@ TEST(LtlParserTest, parseBoundedUntilFormulaTest) { ASSERT_EQ(static_cast(3), op->getBound()); - ASSERT_EQ(ltlFormula->toString(), "(a U<=3 b)"); + ASSERT_EQ("(a U<=3 b)", ltlFormula->toString()); +} + +TEST(LtlParserTest, parseLtlFilterTest) { + std::string input = "filter[max; invert; bound(<, 0.5); sort(value); range(0,3)](X a)"; + std::shared_ptr> formula(nullptr); + ASSERT_NO_THROW( + formula = storm::parser::LtlParser::parseLtlFormula(input) + ); + + // The parser did not falsely recognize the input as a comment. + ASSERT_NE(formula, nullptr); + + ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator()); + + ASSERT_EQ(4, formula->getActionCount()); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(2)).get(), nullptr); + ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); + + // The input was parsed correctly. + ASSERT_EQ("filter[max; invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](X a)", formula->toString()); +} + +TEST(PrctlParserTest, 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( + formula = storm::parser::LtlParser::parseLtlFormula(input) + ); + + // The parser recognized the input as a comment. + ASSERT_NE(nullptr, formula.get()); + + // Test if the parser recognizes the comment at the end of a line. + input = "F X a // This is a comment."; + ASSERT_NO_THROW( + formula = storm::parser::LtlParser::parseLtlFormula(input) + ); + ASSERT_EQ("F X a", formula->toString()); } TEST(LtlParserTest, parseComplexUntilTest) { @@ -106,7 +150,7 @@ TEST(LtlParserTest, parseComplexUntilTest) { ); ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ(ltlFormula->toString(), "((a U b) U<=3 c)"); + ASSERT_EQ("((a U b) U<=3 c)", ltlFormula->toString()); } TEST(LtlParserTest, parseComplexFormulaTest) { @@ -117,7 +161,7 @@ TEST(LtlParserTest, parseComplexFormulaTest) { ); ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ(ltlFormula->toString(), "(a U F (b | G (a & F<=3 (a U<=7 b))))"); + ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlFormula->toString()); } TEST(LtlParserTest, wrongFormulaTest) { diff --git a/test/functional/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp index ee86d92e8..dbdb508b7 100644 --- a/test/functional/parser/PrctlParserTest.cpp +++ b/test/functional/parser/PrctlParserTest.cpp @@ -159,7 +159,7 @@ TEST(PrctlParserTest, parseComplexFormulaTest) { } TEST(PrctlParserTest, parsePrctlFilterTest) { - std::string input = "filter[formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)"; + std::string input = "filter[max; formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)"; std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( formula = storm::parser::PrctlParser::parsePrctlFormula(input) @@ -168,6 +168,8 @@ TEST(PrctlParserTest, parsePrctlFilterTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula, nullptr); + ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator()); + ASSERT_EQ(5, formula->getActionCount()); ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(0)).get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(1)).get(), nullptr); @@ -176,10 +178,10 @@ TEST(PrctlParserTest, parsePrctlFilterTest) { ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); // The input was parsed correctly. - ASSERT_EQ("filter[formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); + ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); } -TEST(PrctlParserTest, commentTest) { +TEST(LtlParserTest, 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(