diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 1c9c85180..298520092 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -34,7 +34,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar> stateFormula >> qi::lit("&") >> stateFormula >> qi::lit(")"))[ qi::_val = phoenix::new_>(qi::_1, qi::_2)]; @@ -45,7 +45,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar>(qi::_1)]; probabilisticBoundOperator = ( - ("P>" >> 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, qi::_1, qi::_2)] | ("P>=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp index bb18aaaad..5def77bf7 100644 --- a/test/parser/PrctlParserTest.cpp +++ b/test/parser/PrctlParserTest.cpp @@ -11,16 +11,46 @@ #include "src/parser/PrctlParser.h" #include -TEST(PrctlParserTest, parseAndOutput) { +TEST(PrctlParserTest, apOnly) { storm::parser::PrctlParser* prctlParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula.prctl") + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/apOnly.prctl") ); ASSERT_NE(prctlParser->getFormula(), nullptr); - std::cout << prctlParser->getFormula()->toString(); + ASSERT_EQ(prctlParser->getFormula()->toString(), "P"); + + delete prctlParser; + +} + +TEST(PrctlParserTest, formulaTest1) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_NO_THROW( + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula1.prctl") + ); + + ASSERT_NE(prctlParser->getFormula(), nullptr); + + + ASSERT_EQ(prctlParser->getFormula()->toString(), "!(a && b)"); + + delete prctlParser; + +} + +TEST(PrctlParserTest, formulaTest2) { + storm::parser::PrctlParser* prctlParser = nullptr; + ASSERT_NO_THROW( + prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/testFormula2.prctl") + ); + + ASSERT_NE(prctlParser->getFormula(), nullptr); + + + ASSERT_EQ(prctlParser->getFormula()->toString(), "P<0.500000 [F a]"); delete prctlParser; diff --git a/test/parser/prctl_files/apOnly.prctl b/test/parser/prctl_files/apOnly.prctl new file mode 100644 index 000000000..675f43ab4 --- /dev/null +++ b/test/parser/prctl_files/apOnly.prctl @@ -0,0 +1 @@ +P \ No newline at end of file diff --git a/test/parser/prctl_files/testFormula.prctl b/test/parser/prctl_files/testFormula.prctl deleted file mode 100644 index fd395528e..000000000 --- a/test/parser/prctl_files/testFormula.prctl +++ /dev/null @@ -1 +0,0 @@ -((P>=0 [ F a ]) & P<0.5 [ G !(b) ]) \ No newline at end of file diff --git a/test/parser/prctl_files/testFormula1.prctl b/test/parser/prctl_files/testFormula1.prctl new file mode 100644 index 000000000..62ed48627 --- /dev/null +++ b/test/parser/prctl_files/testFormula1.prctl @@ -0,0 +1 @@ +!(a & b) \ No newline at end of file diff --git a/test/parser/prctl_files/testFormula2.prctl b/test/parser/prctl_files/testFormula2.prctl new file mode 100644 index 000000000..947aa8543 --- /dev/null +++ b/test/parser/prctl_files/testFormula2.prctl @@ -0,0 +1 @@ +P > 0.5 [ F a ] \ No newline at end of file