From 3833c8af4123b038b847b6a4727a1f845d4565e4 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 6 Feb 2013 12:08:22 +0100 Subject: [PATCH] Some more test cases for PRCTL formula parsing --- src/formula/ProbabilisticNoBoundOperator.h | 2 +- src/formula/RewardNoBoundOperator.h | 2 +- src/parser/PrctlParser.cpp | 38 +++++------ test/parser/PrctlParserTest.cpp | 65 +++++++++++++++++-- test/parser/prctl_files/complexFormula.prctl | 1 + .../probabilisticNoBoundFormula.prctl | 1 + .../prctl_files/rewardNoBoundFormula.prctl | 1 + 7 files changed, 84 insertions(+), 26 deletions(-) create mode 100644 test/parser/prctl_files/complexFormula.prctl create mode 100644 test/parser/prctl_files/probabilisticNoBoundFormula.prctl create mode 100644 test/parser/prctl_files/rewardNoBoundFormula.prctl diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h index ad4ab4851..dd79d64d5 100644 --- a/src/formula/ProbabilisticNoBoundOperator.h +++ b/src/formula/ProbabilisticNoBoundOperator.h @@ -69,7 +69,7 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = " P=? ["; + std::string result = "P = ? ["; result += this->getPathFormula().toString(); result += "]"; return result; diff --git a/src/formula/RewardNoBoundOperator.h b/src/formula/RewardNoBoundOperator.h index 3362ff136..91e0c89f0 100644 --- a/src/formula/RewardNoBoundOperator.h +++ b/src/formula/RewardNoBoundOperator.h @@ -69,7 +69,7 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = " R=? ["; + std::string result = "R = ? ["; result += this->getPathFormula().toString(); result += "]"; return result; diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index eda309eaf..b4af33b0b 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -34,58 +34,58 @@ struct PrctlParser::PrctlGrammar : qi::grammar> stateFormula >> qi::lit("&") >> stateFormula >> qi::lit(")"))[ qi::_val = phoenix::new_>(qi::_1, qi::_2)]; - orFormula = (qi::lit("(") >> stateFormula >> '|' >> stateFormula >> ')')[qi::_val = + orFormula = (qi::lit("(") >> stateFormula >> qi::lit("|") >> stateFormula >> qi::lit(")"))[qi::_val = phoenix::new_>(qi::_1, qi::_2)]; - notFormula = ('!' >> stateFormula)[qi::_val = + notFormula = (qi::lit("!") >> stateFormula)[qi::_val = phoenix::new_>(qi::_1)]; atomicProposition = (freeIdentifierName)[qi::_val = phoenix::new_>(qi::_1)]; probabilisticBoundOperator = ( (qi::lit("P") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit(">=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("P") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("P") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS, qi::_1, qi::_2)] | - (qi::lit("P") >> qi::lit("<=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("P") >> qi::lit("<=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); rewardBoundOperator = ( - (qi::lit("R") >> qi::lit(">") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER, qi::_1, qi::_2)] | - (qi::lit("R") >> qi::lit(">=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | - (qi::lit("R") >> qi::lit("<") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS, qi::_1, qi::_2)] | - (qi::lit("R") >> qi::lit("<=")>> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); //This block defines rules for parsing formulas with noBoundOperators - noBoundOperator %= (probabilisticNoBoundOperator | rewardNoBoundOperator); - probabilisticNoBoundOperator = ("P=?[" >> pathFormula >> ']')[qi::_val = + noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); + probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1)]; - rewardNoBoundOperator = ("R=?[" >> pathFormula >> ']')[qi::_val = + rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1)]; //This block defines rules for parsing path formulas - pathFormula %= (eventually | boundedEventually | globally | boundedUntil | until); - eventually = ('F' >> stateFormula)[qi::_val = + pathFormula = (eventually | boundedEventually | globally | boundedUntil | until); + eventually = (qi::lit("F") >> stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - boundedEventually = ("F<=" >> qi::int_ >> stateFormula)[qi::_val = + boundedEventually = (qi::lit("F") >> qi::lit("<=") >> qi::int_ >> stateFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; - globally = ('G' >> stateFormula)[qi::_val = + globally = (qi::lit("G") >> stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; until = (stateFormula >> qi::lit("U") >> stateFormula)[qi::_val = phoenix::new_>(qi::_1, qi::_2)]; - boundedUntil = (stateFormula >> "U<=" >> qi::int_ >> stateFormula)[qi::_val = + boundedUntil = (stateFormula >> qi::lit("U") >> qi::lit("<=") >> qi::int_ >> stateFormula)[qi::_val = phoenix::new_>(qi::_1, qi::_3, qi::_2)]; - start %= (stateFormula | noBoundOperator); + start = (noBoundOperator | stateFormula); } qi::rule*(), Skipper> start; diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp index 4fd579d67..9b61af858 100644 --- a/test/parser/PrctlParserTest.cpp +++ b/test/parser/PrctlParserTest.cpp @@ -9,9 +9,8 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/PrctlParser.h" -#include -TEST(PrctlParserTest, apOnly) { +TEST(PrctlParserTest, parseApOnlyTest) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_NO_THROW( prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/apOnly.prctl") @@ -22,11 +21,12 @@ TEST(PrctlParserTest, apOnly) { ASSERT_EQ(prctlParser->getFormula()->toString(), "P"); + delete prctlParser->getFormula(); delete prctlParser; } -TEST(PrctlParserTest, propositionalFormula) { +TEST(PrctlParserTest, parsePropositionalFormulaTest) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_NO_THROW( prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl") @@ -37,11 +37,12 @@ TEST(PrctlParserTest, propositionalFormula) { ASSERT_EQ(prctlParser->getFormula()->toString(), "!(a && b)"); + delete prctlParser->getFormula(); delete prctlParser; } -TEST(PrctlParserTest, probabilisticFormula) { +TEST(PrctlParserTest, parseProbabilisticFormulaTest) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_NO_THROW( prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl") @@ -49,14 +50,19 @@ TEST(PrctlParserTest, probabilisticFormula) { ASSERT_NE(prctlParser->getFormula(), nullptr); + storm::formula::ProbabilisticBoundOperator* op = static_cast*>(prctlParser->getFormula()); + + ASSERT_EQ(storm::formula::BoundOperator::GREATER, op->getComparisonOperator()); + ASSERT_EQ(0.5, op->getBound()); ASSERT_EQ(prctlParser->getFormula()->toString(), "P > 0.500000 [F a]"); + delete prctlParser->getFormula(); delete prctlParser; } -TEST(PrctlParserTest, rewardFormula) { +TEST(PrctlParserTest, parseRewardFormulaTest) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_NO_THROW( prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl") @@ -65,10 +71,59 @@ TEST(PrctlParserTest, rewardFormula) { ASSERT_NE(prctlParser->getFormula(), nullptr); storm::formula::RewardBoundOperator* op = static_cast*>(prctlParser->getFormula()); + ASSERT_EQ(storm::formula::BoundOperator::GREATER_EQUAL, op->getComparisonOperator()); + ASSERT_EQ(15.0, op->getBound()); ASSERT_EQ(prctlParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]"); + delete prctlParser->getFormula(); + delete prctlParser; +} + +TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_NO_THROW( + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardNoBoundFormula.prctl") + ); + + ASSERT_NE(prctlParser->getFormula(), nullptr); + + + ASSERT_EQ(prctlParser->getFormula()->toString(), "R = ? [(a U<=4 (b && !c))]"); + + delete prctlParser->getFormula(); + delete prctlParser; + +} + +TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_NO_THROW( + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticNoBoundFormula.prctl") + ); + + ASSERT_NE(prctlParser->getFormula(), nullptr); + + + ASSERT_EQ(prctlParser->getFormula()->toString(), "P = ? [F<=42 !a]"); + + delete prctlParser->getFormula(); + delete prctlParser; + +} + +TEST(PrctlParserTest, parseComplexFormulaTest) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_NO_THROW( + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/complexFormula.prctl") + ); + + ASSERT_NE(prctlParser->getFormula(), nullptr); + + + ASSERT_EQ(prctlParser->getFormula()->toString(), "(P <= 0.500000 [F a] && (R > 15.000000 [G !b] || P > 0.900000 [F<=7 (a && b)]))"); + delete prctlParser->getFormula(); delete prctlParser; } diff --git a/test/parser/prctl_files/complexFormula.prctl b/test/parser/prctl_files/complexFormula.prctl new file mode 100644 index 000000000..c9c8d9f3f --- /dev/null +++ b/test/parser/prctl_files/complexFormula.prctl @@ -0,0 +1 @@ +(P<=0.5 [ F a ] & (R > 15 [ G !b ] | P>0.9 [F<=7 (a & b)])) \ No newline at end of file diff --git a/test/parser/prctl_files/probabilisticNoBoundFormula.prctl b/test/parser/prctl_files/probabilisticNoBoundFormula.prctl new file mode 100644 index 000000000..9d3c68b30 --- /dev/null +++ b/test/parser/prctl_files/probabilisticNoBoundFormula.prctl @@ -0,0 +1 @@ +P = ? [ F <= 42 !a ] \ No newline at end of file diff --git a/test/parser/prctl_files/rewardNoBoundFormula.prctl b/test/parser/prctl_files/rewardNoBoundFormula.prctl new file mode 100644 index 000000000..c3415980c --- /dev/null +++ b/test/parser/prctl_files/rewardNoBoundFormula.prctl @@ -0,0 +1 @@ +R = ? [ a U <= 4 (b & !c) ] \ No newline at end of file