diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h index a0e4c423a..ec5873160 100644 --- a/src/formula/BoundOperator.h +++ b/src/formula/BoundOperator.h @@ -116,10 +116,10 @@ public: virtual std::string toString() const { std::string result = ""; switch (comparisonOperator) { - case LESS: result += "<"; break; - case LESS_EQUAL: result += "<="; break; - case GREATER: result += ">"; break; - case GREATER_EQUAL: result += ">="; break; + case LESS: result += "< "; break; + case LESS_EQUAL: result += "<= "; break; + case GREATER: result += "> "; break; + case GREATER_EQUAL: result += ">= "; break; } result += std::to_string(bound); result += " ["; diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h index ac1bf2709..be4ddfd4e 100644 --- a/src/formula/ProbabilisticBoundOperator.h +++ b/src/formula/ProbabilisticBoundOperator.h @@ -59,7 +59,7 @@ public: */ ProbabilisticBoundOperator( typename BoundOperator::ComparisonType comparisonRelation, T bound, PctlPathFormula* pathFormula) : - BoundOperator(BoundOperator::LESS, bound, pathFormula) { + BoundOperator(comparisonRelation, bound, pathFormula) { // Intentionally left empty } @@ -67,7 +67,7 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = "P"; + std::string result = "P "; result += BoundOperator::toString(); return result; } diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h index 1f0a21cd6..34b4d1084 100644 --- a/src/formula/RewardBoundOperator.h +++ b/src/formula/RewardBoundOperator.h @@ -57,7 +57,7 @@ public: */ RewardBoundOperator( typename BoundOperator::ComparisonType comparisonRelation, T bound, PctlPathFormula* pathFormula) : - BoundOperator(BoundOperator::LESS, bound, pathFormula) { + BoundOperator(comparisonRelation, bound, pathFormula) { // Intentionally left empty } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 298520092..eda309eaf 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -47,17 +47,21 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER, qi::_1, qi::_2)] | - ("P>=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("P") >> qi::lit(">=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | - ("P<" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("P") >> qi::lit("<") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS, qi::_1, qi::_2)] | - ("P<=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("P") >> qi::lit("<=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); rewardBoundOperator = ( - ("R>=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = - phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | - ("R<=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + (qi::lit("R") >> qi::lit(">") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + phoenix::new_ >(storm::formula::BoundOperator::GREATER, qi::_1, qi::_2)] | + (qi::lit("R") >> qi::lit(">=") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | + (qi::lit("R") >> qi::lit("<") >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + phoenix::new_ >(storm::formula::BoundOperator::LESS, qi::_1, qi::_2)] | + (qi::lit("R") >> qi::lit("<=")>> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); @@ -76,7 +80,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar>(qi::_2, qi::_1)]; globally = ('G' >> stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - until = (stateFormula >> 'U' >> stateFormula)[qi::_val = + until = (stateFormula >> qi::lit("U") >> stateFormula)[qi::_val = phoenix::new_>(qi::_1, qi::_2)]; boundedUntil = (stateFormula >> "U<=" >> qi::int_ >> stateFormula)[qi::_val = phoenix::new_>(qi::_1, qi::_3, qi::_2)]; diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp index 5def77bf7..4fd579d67 100644 --- a/test/parser/PrctlParserTest.cpp +++ b/test/parser/PrctlParserTest.cpp @@ -26,10 +26,10 @@ TEST(PrctlParserTest, apOnly) { } -TEST(PrctlParserTest, formulaTest1) { +TEST(PrctlParserTest, propositionalFormula) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula1.prctl") + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl") ); ASSERT_NE(prctlParser->getFormula(), nullptr); @@ -41,16 +41,33 @@ TEST(PrctlParserTest, formulaTest1) { } -TEST(PrctlParserTest, formulaTest2) { +TEST(PrctlParserTest, probabilisticFormula) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula2.prctl") + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl") ); ASSERT_NE(prctlParser->getFormula(), nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "P<0.500000 [F a]"); + ASSERT_EQ(prctlParser->getFormula()->toString(), "P > 0.500000 [F a]"); + + delete prctlParser; + +} + +TEST(PrctlParserTest, rewardFormula) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_NO_THROW( + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl") + ); + + ASSERT_NE(prctlParser->getFormula(), nullptr); + + storm::formula::RewardBoundOperator* op = static_cast*>(prctlParser->getFormula()); + ASSERT_EQ(storm::formula::BoundOperator::GREATER_EQUAL, op->getComparisonOperator()); + + ASSERT_EQ(prctlParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]"); delete prctlParser; diff --git a/test/parser/prctl_files/testFormula2.prctl b/test/parser/prctl_files/probabilisticFormula.prctl similarity index 100% rename from test/parser/prctl_files/testFormula2.prctl rename to test/parser/prctl_files/probabilisticFormula.prctl diff --git a/test/parser/prctl_files/testFormula1.prctl b/test/parser/prctl_files/propositionalFormula.prctl similarity index 100% rename from test/parser/prctl_files/testFormula1.prctl rename to test/parser/prctl_files/propositionalFormula.prctl diff --git a/test/parser/prctl_files/rewardFormula.prctl b/test/parser/prctl_files/rewardFormula.prctl new file mode 100644 index 000000000..9ef3ab203 --- /dev/null +++ b/test/parser/prctl_files/rewardFormula.prctl @@ -0,0 +1 @@ +R >= 15 [ a U !b ] \ No newline at end of file