From 532b0cf3ad0cdea6e5e6c3deb3ace99cc2b6becb Mon Sep 17 00:00:00 2001 From: masawei Date: Thu, 14 Aug 2014 12:45:58 +0200 Subject: [PATCH] Added function to test if a formula is a probability bounded reachability formula, i.e. conforms to the pattern P[<,<=,>,>=]p ([phi U, E] psi) where phi, psi are propositional formulas (consisting only of And, Or, Not and AP). - For that implemented function that checks if a formula is a propositional logic formula to all three logics. - Added tests for the function. - Added documentation for the function. Former-commit-id: 3fcb84b990ae8ef13cdea7231691f8eae7f7a6bf --- src/formula/AbstractFormula.h | 10 ++ src/formula/PrctlFormulaChecker.h | 2 +- src/formula/csl/AbstractCslFormula.h | 43 +++++++++ src/formula/csl/And.h | 9 ++ src/formula/csl/Ap.h | 9 ++ src/formula/csl/Not.h | 9 ++ src/formula/csl/Or.h | 9 ++ src/formula/ltl/And.h | 9 ++ src/formula/ltl/Ap.h | 10 ++ src/formula/ltl/Not.h | 10 ++ src/formula/ltl/Or.h | 10 ++ src/formula/prctl/AbstractPrctlFormula.h | 42 ++++++++ src/formula/prctl/And.h | 10 ++ src/formula/prctl/Ap.h | 10 ++ src/formula/prctl/Not.h | 11 +++ src/formula/prctl/Or.h | 10 ++ test/functional/parser/CslParserTest.cpp | 45 ++++++++- test/functional/parser/LtlParserTest.cpp | 106 ++++++++++++--------- test/functional/parser/PrctlParserTest.cpp | 64 ++++++++++--- 19 files changed, 363 insertions(+), 65 deletions(-) diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h index b1e7f262d..c790d8eae 100644 --- a/src/formula/AbstractFormula.h +++ b/src/formula/AbstractFormula.h @@ -79,6 +79,16 @@ public: * @return true iff all subtrees are valid. */ virtual bool validate(AbstractFormulaChecker const & checker) const = 0; + + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const { + return false; + } }; } // namespace property diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h index 08b40f895..5ed817e09 100644 --- a/src/formula/PrctlFormulaChecker.h +++ b/src/formula/PrctlFormulaChecker.h @@ -23,7 +23,7 @@ class PrctlFormulaChecker : public AbstractFormulaChecker { * Implementation of AbstractFormulaChecker::validate() using code * looking exactly like the sample code given there. */ - virtual bool validate(std::shared_ptr> const & formula) const { + virtual bool validate(std::shared_ptr> const & formula) const { // What to support: Principles of Model Checking Def. 10.76 + syntactic sugar if ( dynamic_pointer_cast>(formula) || diff --git a/src/formula/csl/AbstractCslFormula.h b/src/formula/csl/AbstractCslFormula.h index 7de783d96..6631a753f 100644 --- a/src/formula/csl/AbstractCslFormula.h +++ b/src/formula/csl/AbstractCslFormula.h @@ -14,6 +14,18 @@ namespace storm { namespace property { namespace csl { +template class ProbabilisticBoundOperator; +template class Eventually; +template class Until; + +} +} +} + +namespace storm { +namespace property { +namespace csl { + /*! * Abstract base class for all CSL root formulas. */ @@ -23,6 +35,37 @@ public: virtual ~AbstractCslFormula() { // Intentionally left empty } + + /*! + * Checks whether the formula is a probabilistic bound reachability formula. + * Returns true iff the formula conforms to the following pattern. + * Pattern: P[<,<=,>,>=]p ([psi U, E] phi) whith psi, phi propositional logic formulas (consisiting only of And, Or, Not and AP). + * That is, a probabilistic bound operator as root with a single until or eventually formula directly below it, whose subformulas are propositional + * (denoting some set of atomic propositions). + * + * @return True iff this is a probabilistic bound reachability formula. + */ + bool isProbEventuallyAP() const { + + if(dynamic_cast const *>(this) == nullptr) { + return false; + } + + auto probFormula = dynamic_cast const *>(this); + + if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + + auto eventuallyFormula = std::dynamic_pointer_cast>(probFormula->getChild()); + return eventuallyFormula->getChild()->isPropositional(); + } + else if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + + auto untilFormula = std::dynamic_pointer_cast>(probFormula->getChild()); + return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional(); + } + + return false; + } }; } /* namespace csl */ diff --git a/src/formula/csl/And.h b/src/formula/csl/And.h index 0d10fbef6..0218edecb 100644 --- a/src/formula/csl/And.h +++ b/src/formula/csl/And.h @@ -139,6 +139,15 @@ public: return checker.validate(this->left) && checker.validate(this->right); } + /*! Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return left->isPropositional() && right->isPropositional(); + } + /*! * Sets the left child node. * diff --git a/src/formula/csl/Ap.h b/src/formula/csl/Ap.h index 6b7f8ec56..284f94eeb 100644 --- a/src/formula/csl/Ap.h +++ b/src/formula/csl/Ap.h @@ -106,6 +106,15 @@ public: return true; } + /*! Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return true; + } + /*! * @returns the name of the atomic proposition */ diff --git a/src/formula/csl/Not.h b/src/formula/csl/Not.h index 002adb5bf..698b92b89 100644 --- a/src/formula/csl/Not.h +++ b/src/formula/csl/Not.h @@ -125,6 +125,15 @@ public: return checker.validate(this->child); } + /*! Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return child->isPropositional(); + } + /*! * @returns The child node */ diff --git a/src/formula/csl/Or.h b/src/formula/csl/Or.h index fa9649f61..2ecc7fab9 100644 --- a/src/formula/csl/Or.h +++ b/src/formula/csl/Or.h @@ -137,6 +137,15 @@ public: return checker.validate(this->left) && checker.validate(this->right); } + /*! Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return left->isPropositional() && right->isPropositional(); + } + /*! * Sets the left child node. * diff --git a/src/formula/ltl/And.h b/src/formula/ltl/And.h index ffc5848de..48c4350cb 100644 --- a/src/formula/ltl/And.h +++ b/src/formula/ltl/And.h @@ -138,6 +138,15 @@ public: return checker.validate(this->left) && checker.validate(this->right); } + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return left->isPropositional() && right->isPropositional(); + } /*! * Sets the left child node. diff --git a/src/formula/ltl/Ap.h b/src/formula/ltl/Ap.h index b84aff340..c7845604f 100644 --- a/src/formula/ltl/Ap.h +++ b/src/formula/ltl/Ap.h @@ -118,6 +118,16 @@ public: return true; } + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return true; + } + /*! * @returns the name of the atomic proposition */ diff --git a/src/formula/ltl/Not.h b/src/formula/ltl/Not.h index ebc742800..99a90736c 100644 --- a/src/formula/ltl/Not.h +++ b/src/formula/ltl/Not.h @@ -123,6 +123,16 @@ public: return checker.validate(this->child); } + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return child->isPropositional(); + } + /*! * @returns The child node */ diff --git a/src/formula/ltl/Or.h b/src/formula/ltl/Or.h index d2ee4a4f5..336da397b 100644 --- a/src/formula/ltl/Or.h +++ b/src/formula/ltl/Or.h @@ -135,6 +135,16 @@ public: return checker.validate(this->left) && checker.validate(this->right); } + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return left->isPropositional() && right->isPropositional(); + } + /*! * Sets the left child node. * diff --git a/src/formula/prctl/AbstractPrctlFormula.h b/src/formula/prctl/AbstractPrctlFormula.h index 3beddb206..044996b9c 100644 --- a/src/formula/prctl/AbstractPrctlFormula.h +++ b/src/formula/prctl/AbstractPrctlFormula.h @@ -14,6 +14,18 @@ namespace storm { namespace property { namespace prctl { +template class ProbabilisticBoundOperator; +template class Eventually; +template class Until; + +} +} +} + +namespace storm { +namespace property { +namespace prctl { + /*! * Interface class for all PRCTL root formulas. */ @@ -23,6 +35,36 @@ public: virtual ~AbstractPrctlFormula() { // Intentionally left empty } + + /*! Returns whether the formula is a probabilistic bound reachability formula. + * Returns true iff the formula conforms to the following pattern. + * Pattern: P[<,<=,>,>=]p ([psi U, E] phi) whith psi, phi propositional logic formulas (consisiting only of And, Or, Not and AP). + * That is, a probabilistic bound operator as root with a single until or eventually formula directly below it, whose subformulas are propositional + * (denoting some set of atomic propositions). + * + * @return True iff this is a probabilistic bound reachability formula. + */ + bool isProbEventuallyAP() const { + + if(dynamic_cast const *>(this) == nullptr) { + return false; + } + + auto probFormula = dynamic_cast const *>(this); + + if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + + auto eventuallyFormula = std::dynamic_pointer_cast>(probFormula->getChild()); + return eventuallyFormula->getChild()->isPropositional(); + } + else if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + + auto untilFormula = std::dynamic_pointer_cast>(probFormula->getChild()); + return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional(); + } + + return false; + } }; } /* namespace prctl */ diff --git a/src/formula/prctl/And.h b/src/formula/prctl/And.h index f821f08d4..80a9cffd3 100644 --- a/src/formula/prctl/And.h +++ b/src/formula/prctl/And.h @@ -139,6 +139,16 @@ public: return checker.validate(this->left) && checker.validate(this->right); } + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return left->isPropositional() && right->isPropositional(); + } + /*! * Sets the left child node. * diff --git a/src/formula/prctl/Ap.h b/src/formula/prctl/Ap.h index 906158ac9..ef6d77b12 100644 --- a/src/formula/prctl/Ap.h +++ b/src/formula/prctl/Ap.h @@ -106,6 +106,16 @@ public: return true; } + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return true; + } + /*! * @returns the name of the atomic proposition */ diff --git a/src/formula/prctl/Not.h b/src/formula/prctl/Not.h index 49660f1af..7531989f6 100644 --- a/src/formula/prctl/Not.h +++ b/src/formula/prctl/Not.h @@ -124,6 +124,17 @@ public: return checker.validate(this->child); } + + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return child->isPropositional(); + } + /*! * @returns The child node */ diff --git a/src/formula/prctl/Or.h b/src/formula/prctl/Or.h index 004b633c7..7bbc0e045 100644 --- a/src/formula/prctl/Or.h +++ b/src/formula/prctl/Or.h @@ -136,6 +136,16 @@ public: return checker.validate(this->left) && checker.validate(this->right); } + /*! + * Returns whether the formula is a propositional logic formula. + * That is, this formula and all its subformulas consist only of And, Or, Not and AP. + * + * @return True iff this is a propositional logic formula. + */ + virtual bool isPropositional() const override { + return left->isPropositional() && right->isPropositional(); + } + /*! * Sets the left child node. * diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index e4289a2b4..ecff80e4d 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -27,6 +27,9 @@ TEST(CslParserTest, parseApOnlyTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula.get(), nullptr); + ASSERT_TRUE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + // The input was parsed correctly. ASSERT_EQ(input, formula->toString()); } @@ -41,6 +44,9 @@ TEST(CslParserTest, parsePropositionalFormulaTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula.get(), nullptr); + ASSERT_TRUE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + // The input was parsed correctly. ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); } @@ -58,16 +64,25 @@ TEST(CslParserTest, parsePathFormulaTest) { // The input was parsed correctly. ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); auto nextFormula = std::dynamic_pointer_cast>(formula->getChild()); + ASSERT_FALSE(nextFormula->isPropositional()); + ASSERT_FALSE(nextFormula->isProbEventuallyAP()); + ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); auto probBoundFormula = std::dynamic_pointer_cast>(nextFormula->getChild()); + ASSERT_EQ(0.9, probBoundFormula->getBound()); + ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator()); + ASSERT_FALSE(probBoundFormula->isPropositional()); + ASSERT_TRUE(probBoundFormula->isProbEventuallyAP()); + ASSERT_NE(std::dynamic_pointer_cast>(probBoundFormula->getChild()).get(), nullptr); auto untilFormula = std::dynamic_pointer_cast>(probBoundFormula->getChild()); + ASSERT_FALSE(untilFormula->isPropositional()); + ASSERT_FALSE(untilFormula->isProbEventuallyAP()); + ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getLeft()).get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getRight()).get(), nullptr); ASSERT_EQ("a", std::dynamic_pointer_cast>(untilFormula->getLeft())->getAp()); ASSERT_EQ("b", std::dynamic_pointer_cast>(untilFormula->getRight())->getAp()); - ASSERT_EQ(0.9, probBoundFormula->getBound()); - ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator()); // The string representation is also correct. @@ -88,6 +103,8 @@ TEST(CslParserTest, parseProbabilisticFormulaTest) { ASSERT_NE(op.get(), nullptr); ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); + ASSERT_FALSE(op->isPropositional()); + ASSERT_TRUE(op->isProbEventuallyAP()); // Test the string representation for the parsed formula. ASSERT_EQ("P > 0.500000 (F a)", formula->toString()); @@ -107,6 +124,8 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) { ASSERT_NE(op.get(), nullptr); ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); + ASSERT_FALSE(op->isPropositional()); + ASSERT_FALSE(op->isProbEventuallyAP()); // Test the string representation for the parsed formula. ASSERT_EQ("S >= 15.000000 (P < 0.200000 (a U[0.000000,3.000000] b))", formula->toString()); @@ -122,6 +141,9 @@ TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula.get(), nullptr); + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + // The input was parsed correctly. ASSERT_EQ("S = ? (P <= 0.500000 (F[0.000000,3.000000] a))", formula->toString()); } @@ -136,6 +158,9 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula.get(), nullptr); + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + // The input was parsed correctly. ASSERT_EQ("P = ? (a U[3.000000,4.000000] (b & !c))", formula->toString()); } @@ -151,6 +176,9 @@ TEST(CslParserTest, parseComplexFormulaTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula.get(), nullptr); + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + // The input was parsed correctly. ASSERT_EQ("S <= 0.500000 ((P <= 0.500000 (a U c) & (P > 0.500000 (G b) | !P < 0.400000 (G P > 0.900000 (F>=7.000000 (a & b))))))", formula->toString()); } @@ -174,12 +202,15 @@ TEST(CslParserTest, parseCslFilterTest) { ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + // The input was parsed correctly. ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); } TEST(CslParserTest, commentTest) { - std::string input = "// This is a comment. And this is a commented out formula: P = ? [ F a ]"; + std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ X a ]"; std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( formula = storm::parser::CslParser::parseCslFormula(input) @@ -189,11 +220,15 @@ TEST(CslParserTest, commentTest) { ASSERT_NE(nullptr, formula.get()); // Test if the parser recognizes the comment at the end of a line. - input = "P = ? [ F a ] // This is a comment."; + input = "P<=0.5 [ X a ] // This is a comment."; ASSERT_NO_THROW( formula = storm::parser::CslParser::parseCslFormula(input) ); - ASSERT_EQ("P = ? (F a)", formula->toString()); + + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + + ASSERT_EQ("P <= 0.500000 (X a)", formula->toString()); } TEST(CslParserTest, wrongProbabilisticFormulaTest) { diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp index 5c55ab54a..e44f84f0e 100644 --- a/test/functional/parser/LtlParserTest.cpp +++ b/test/functional/parser/LtlParserTest.cpp @@ -17,25 +17,29 @@ namespace ltl = storm::property::ltl; TEST(LtlParserTest, parseApOnlyTest) { - std::string formula = "ap"; - std::shared_ptr> ltlFormula(nullptr); + std::string input = "ap"; + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( - ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula); + formula = storm::parser::LtlParser::parseLtlFormula(input); ); - ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ(formula, ltlFormula->toString()); + ASSERT_TRUE(formula->getChild()->isPropositional()); + + ASSERT_NE(formula.get(), nullptr); + ASSERT_EQ(input, formula->toString()); } TEST(LtlParserTest, parsePropositionalFormulaTest) { - std::string formula = "!(a & b) | a & ! c"; - std::shared_ptr> ltlFormula(nullptr); + std::string input = "!(a & b) | a & ! c"; + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( - ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula); + formula = storm::parser::LtlParser::parseLtlFormula(input); ); - ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ("(!(a & b) | (a & !c))", ltlFormula->toString()); + ASSERT_TRUE(formula->getChild()->isPropositional()); + + ASSERT_NE(formula.get(), nullptr); + ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); } /*! @@ -43,14 +47,16 @@ TEST(LtlParserTest, parsePropositionalFormulaTest) { * "Eventually" operator. */ TEST(LtlParserTest, parseAmbiguousFormulaTest) { - std::string formula = "F & b"; - std::shared_ptr> ltlFormula(nullptr); + std::string input = "F & b"; + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( - ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula); + formula = storm::parser::LtlParser::parseLtlFormula(input); ); - ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ("(F & b)", ltlFormula->toString()); + ASSERT_TRUE(formula->getChild()->isPropositional()); + + ASSERT_NE(formula.get(), nullptr); + ASSERT_EQ("(F & b)", formula->toString()); } /*! @@ -58,48 +64,54 @@ TEST(LtlParserTest, parseAmbiguousFormulaTest) { * depending where it occurs. */ TEST(LtlParserTest, parseAmbiguousFormulaTest2) { - std::string formula = "F F"; - std::shared_ptr> ltlFormula(nullptr); + std::string input = "F F"; + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( - ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula); + formula = storm::parser::LtlParser::parseLtlFormula(input); ); - ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ("F F", ltlFormula->toString()); + ASSERT_FALSE(formula->getChild()->isPropositional()); + + ASSERT_NE(formula.get(), nullptr); + ASSERT_EQ("F F", formula->toString()); } TEST(LtlParserTest, parseBoundedEventuallyFormulaTest) { - std::string formula = "F<=5 a"; - std::shared_ptr> ltlFormula(nullptr); + std::string input = "F<=5 a"; + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( - ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula); + formula = storm::parser::LtlParser::parseLtlFormula(input); ); - ASSERT_NE(ltlFormula.get(), nullptr); + ASSERT_NE(formula.get(), nullptr); - std::shared_ptr> op = std::dynamic_pointer_cast>(ltlFormula->getChild()); + ASSERT_FALSE(formula->getChild()->isPropositional()); + + std::shared_ptr> op = std::dynamic_pointer_cast>(formula->getChild()); ASSERT_NE(op.get(), nullptr); ASSERT_EQ(static_cast(5), op->getBound()); - ASSERT_EQ("F<=5 a", ltlFormula->toString()); + ASSERT_EQ("F<=5 a", formula->toString()); } TEST(LtlParserTest, parseBoundedUntilFormulaTest) { - std::string formula = "a U<=3 b"; - std::shared_ptr> ltlFormula(nullptr); + std::string input = "a U<=3 b"; + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( - ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula); + formula = storm::parser::LtlParser::parseLtlFormula(input); ); - ASSERT_NE(ltlFormula.get(), nullptr); + ASSERT_NE(formula.get(), nullptr); - std::shared_ptr> op = std::dynamic_pointer_cast>(ltlFormula->getChild()); + ASSERT_FALSE(formula->getChild()->isPropositional()); + + std::shared_ptr> op = std::dynamic_pointer_cast>(formula->getChild()); ASSERT_NE(op.get(), nullptr); ASSERT_EQ(static_cast(3), op->getBound()); - ASSERT_EQ("(a U<=3 b)", ltlFormula->toString()); + ASSERT_EQ("(a U<=3 b)", formula->toString()); } TEST(LtlParserTest, parseLtlFilterTest) { @@ -112,6 +124,8 @@ TEST(LtlParserTest, parseLtlFilterTest) { // The parser did not falsely recognize the input as a comment. ASSERT_NE(formula, nullptr); + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator()); ASSERT_EQ(4, formula->getActionCount()); @@ -133,41 +147,45 @@ TEST(LtlParserTest, commentTest) { // The parser recognized the input as a comment. ASSERT_NE(nullptr, formula.get()); + ASSERT_EQ(nullptr, formula->getChild().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_FALSE(formula->getChild()->isPropositional()); + ASSERT_EQ("F X a", formula->toString()); } TEST(LtlParserTest, parseComplexUntilTest) { - std::string formula = "a U b U<=3 c"; - std::shared_ptr> ltlFormula(nullptr); + std::string input = "a U b U<=3 c"; + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( - ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula); + formula = storm::parser::LtlParser::parseLtlFormula(input); ); - ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ("((a U b) U<=3 c)", ltlFormula->toString()); + ASSERT_NE(formula.get(), nullptr); + ASSERT_EQ("((a U b) U<=3 c)", formula->toString()); } TEST(LtlParserTest, parseComplexFormulaTest) { - std::string formula = "a U F b | G a & F<=3 a U<=7 b // and a comment"; - std::shared_ptr> ltlFormula(nullptr); + std::string input = "a U F b | G a & F<=3 a U<=7 b // and a comment"; + std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( - ltlFormula = storm::parser::LtlParser::parseLtlFormula(formula); + formula = storm::parser::LtlParser::parseLtlFormula(input); ); - ASSERT_NE(ltlFormula.get(), nullptr); - ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", ltlFormula->toString()); + ASSERT_NE(formula.get(), nullptr); + ASSERT_EQ("(a U F (b | G (a & F<=3 (a U<=7 b))))", formula->toString()); } TEST(LtlParserTest, wrongFormulaTest) { - std::string formula = "(a | c) & +"; + std::string input = "(a | c) & +"; ASSERT_THROW( - storm::parser::LtlParser::parseLtlFormula(formula), + storm::parser::LtlParser::parseLtlFormula(input), storm::exceptions::WrongFormatException ); } diff --git a/test/functional/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp index bed83948c..1a63495d0 100644 --- a/test/functional/parser/PrctlParserTest.cpp +++ b/test/functional/parser/PrctlParserTest.cpp @@ -26,7 +26,10 @@ TEST(PrctlParserTest, parseApOnlyTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); + + ASSERT_TRUE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); // The input was parsed correctly. ASSERT_EQ(input, formula->toString()); @@ -40,7 +43,10 @@ TEST(PrctlParserTest, parsePropositionalFormulaTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); + + ASSERT_TRUE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); // The input was parsed correctly. ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString()); @@ -54,22 +60,30 @@ TEST(PrctlParserTest, parsePathFormulaTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); // The input was parsed correctly. ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); auto nextFormula = std::dynamic_pointer_cast>(formula->getChild()); + ASSERT_FALSE(nextFormula->isPropositional()); + ASSERT_FALSE(nextFormula->isProbEventuallyAP()); + ASSERT_NE(std::dynamic_pointer_cast>(nextFormula->getChild()).get(), nullptr); auto probBoundFormula = std::dynamic_pointer_cast>(nextFormula->getChild()); + ASSERT_EQ(0.9, probBoundFormula->getBound()); + ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator()); + ASSERT_FALSE(probBoundFormula->isPropositional()); + ASSERT_TRUE(probBoundFormula->isProbEventuallyAP()); + ASSERT_NE(std::dynamic_pointer_cast>(probBoundFormula->getChild()).get(), nullptr); auto untilFormula = std::dynamic_pointer_cast>(probBoundFormula->getChild()); + ASSERT_FALSE(untilFormula->isPropositional()); + ASSERT_FALSE(untilFormula->isProbEventuallyAP()); + ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getLeft()).get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast>(untilFormula->getRight()).get(), nullptr); ASSERT_EQ("a", std::dynamic_pointer_cast>(untilFormula->getLeft())->getAp()); ASSERT_EQ("b", std::dynamic_pointer_cast>(untilFormula->getRight())->getAp()); - ASSERT_EQ(0.9, probBoundFormula->getBound()); - ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator()); - // The string representation is also correct. ASSERT_EQ("P = ? (X P < 0.900000 (a U b))", formula->toString()); @@ -83,7 +97,7 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); @@ -91,6 +105,8 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) { ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); + ASSERT_FALSE(op->isPropositional()); + ASSERT_TRUE(op->isProbEventuallyAP()); // Test the string representation for the parsed formula. ASSERT_EQ("P > 0.500000 (F a)", formula->toString()); @@ -104,13 +120,15 @@ TEST(PrctlParserTest, parseRewardFormulaTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast>(formula->getChild()).get(), nullptr); std::shared_ptr> op = std::static_pointer_cast>(formula->getChild()); ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); + ASSERT_FALSE(op->isPropositional()); + ASSERT_FALSE(op->isProbEventuallyAP()); // Test the string representation for the parsed formula. ASSERT_EQ("R >= 15.000000 (I=5)", formula->toString()); @@ -124,7 +142,10 @@ TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); + + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); // The input was parsed correctly. ASSERT_EQ("R = ? (F a)", formula->toString()); @@ -138,7 +159,10 @@ TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); + + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); // The input was parsed correctly. ASSERT_EQ("P = ? (a U<=4 (b & !c))", formula->toString()); @@ -152,7 +176,10 @@ TEST(PrctlParserTest, parseComplexFormulaTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); + + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); // The input was parsed correctly. ASSERT_EQ("(R <= 0.500000 (S) & (R > 15.000000 (C <= 0.500000) | !P < 0.400000 (G P > 0.900000 (F<=7 (a & b)))))", formula->toString()); @@ -166,7 +193,7 @@ TEST(PrctlParserTest, parsePrctlFilterTest) { ); // The parser did not falsely recognize the input as a comment. - ASSERT_NE(formula, nullptr); + ASSERT_NE(formula.get(), nullptr); ASSERT_EQ(storm::property::MAXIMIZE, formula->getOptimizingOperator()); @@ -177,12 +204,15 @@ TEST(PrctlParserTest, parsePrctlFilterTest) { ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(3)).get(), nullptr); ASSERT_NE(std::dynamic_pointer_cast>(formula->getAction(4)).get(), nullptr); + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + // The input was parsed correctly. ASSERT_EQ("filter[max; formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString()); } TEST(PrctlParserTest, commentTest) { - std::string input = "// This is a comment. And this is a commented out formula: R = ? [ F a ]"; + std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ X a ]"; std::shared_ptr> formula(nullptr); ASSERT_NO_THROW( formula = storm::parser::PrctlParser::parsePrctlFormula(input) @@ -192,11 +222,15 @@ TEST(PrctlParserTest, commentTest) { ASSERT_NE(nullptr, formula.get()); // Test if the parser recognizes the comment at the end of a line. - input = "R = ? [ F a ] // This is a comment."; + input = "P<=0.5 [ X a ] // This is a comment."; ASSERT_NO_THROW( formula = storm::parser::PrctlParser::parsePrctlFormula(input) ); - ASSERT_EQ("R = ? (F a)", formula->toString()); + + ASSERT_FALSE(formula->getChild()->isPropositional()); + ASSERT_FALSE(formula->getChild()->isProbEventuallyAP()); + + ASSERT_EQ("P <= 0.500000 (X a)", formula->toString()); }