diff --git a/src/formula/StateBoundOperator.h b/src/formula/StateBoundOperator.h index 323994c76..441c91f1d 100644 --- a/src/formula/StateBoundOperator.h +++ b/src/formula/StateBoundOperator.h @@ -129,7 +129,7 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = ""; + std::string result = " "; switch (comparisonOperator) { case LESS: result += "< "; break; case LESS_EQUAL: result += "<= "; break; diff --git a/src/formula/SteadyStateBoundOperator.h b/src/formula/SteadyStateBoundOperator.h index 2f5baaab3..3296c0452 100644 --- a/src/formula/SteadyStateBoundOperator.h +++ b/src/formula/SteadyStateBoundOperator.h @@ -78,11 +78,7 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = "("; - result += " S "; - result += StateBoundOperator::toString(); - result += ")"; - return result; + return "S" + StateBoundOperator::toString(); } /*! diff --git a/src/formula/SteadyStateNoBoundOperator.h b/src/formula/SteadyStateNoBoundOperator.h index 7344e2a5a..4c47bbf99 100644 --- a/src/formula/SteadyStateNoBoundOperator.h +++ b/src/formula/SteadyStateNoBoundOperator.h @@ -57,11 +57,7 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = "("; - result += " S "; - result += StateNoBoundOperator::toString(); - result += ")"; - return result; + return "S" + StateNoBoundOperator::toString(); } /*! diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index 02edb2743..1f451e433 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -77,13 +77,13 @@ struct CslParser::CslGrammar : qi::grammar> qi::lit(">") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::PathBoundOperator::GREATER, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::StateBoundOperator::GREATER, qi::_1, qi::_2)] | (qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::PathBoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::StateBoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | (qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::PathBoundOperator::LESS, qi::_1, qi::_2)] | + phoenix::new_ >(storm::formula::StateBoundOperator::LESS, qi::_1, qi::_2)] | (qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(storm::formula::PathBoundOperator::LESS_EQUAL, qi::_1, qi::_2)] + phoenix::new_ >(storm::formula::StateBoundOperator::LESS_EQUAL, qi::_1, qi::_2)] ); steadyStateBoundOperator.name("state formula"); @@ -102,19 +102,19 @@ struct CslParser::CslGrammar : qi::grammar> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; - boundedEventually.name("path formula (for probablistic operator)"); + boundedEventually.name("path formula (for probabilistic operator)"); eventually = (qi::lit("F") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - eventually.name("path formula (for probablistic operator)"); + eventually.name("path formula (for probabilistic operator)"); globally = (qi::lit("G") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - globally.name("path formula (for probablistic operator)"); + globally.name("path formula (for probabilistic operator)"); boundedUntil = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula) [qi::_val = phoenix::new_>(phoenix::bind(&storm::formula::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_3, qi::_2)]; - boundedUntil.name("path formula (for probablistic operator)"); + boundedUntil.name("path formula (for probabilistic operator)"); until = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val = phoenix::new_>(phoenix::bind(&storm::formula::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_2)]; - until.name("path formula (for probablistic operator)"); + until.name("path formula (for probabilistic operator)"); start = (noBoundOperator | stateFormula); start.name("CSL formula"); @@ -156,12 +156,61 @@ struct CslParser::CslGrammar : qi::grammar* result_pointer = nullptr; + + CslGrammar grammar; + + // Now, parse the formula from the given string + try { + qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); + } catch(const qi::expectation_failure& e) { + // If the parser expected content different than the one provided, display information + // about the location of the error. + const boost::spirit::classic::file_position_base& pos = e.first.get_position(); + + // Construct the error message including a caret display of the position in the + // erroneous line. + std::stringstream msg; + msg << pos.file << ", line " << pos.line << ", column " << pos.column + << ": parse error: expected " << e.what_ << std::endl << "\t" + << e.first.get_currentline() << std::endl << "\t"; + int i = 0; + for (i = 0; i < pos.column; ++i) { + msg << "-"; + } + msg << "^"; + for (; i < 80; ++i) { + msg << "-"; + } + msg << std::endl; + + std::cerr << msg.str(); + + // Now propagate exception. + throw storm::exceptions::WrongFormatException() << msg.str(); + } + + // The syntax can be so wrong that no rule can be matched at all + // In that case, no expectation failure is thrown, but the parser just returns nullptr + // Then, of course the result is not usable, hence we throw a WrongFormatException, too. + if (result_pointer == nullptr) { + throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; + } + formula = result_pointer; } CslParser::~CslParser() { - // TODO Auto-generated destructor stub + // Intentionally left empty + // Parsed formula is not deleted with the parser! } } /* namespace parser */ diff --git a/test/parser/CslParserTest.cpp b/test/parser/CslParserTest.cpp new file mode 100644 index 000000000..6ec438519 --- /dev/null +++ b/test/parser/CslParserTest.cpp @@ -0,0 +1,158 @@ +/* + * CslParserTest.cpp + * + * Created on: 09.04.2013 + * Author: Thomas Heinemann + */ + +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/CslParser.h" + +TEST(CslParserTest, parseApOnlyTest) { + std::string ap = "ap"; + storm::parser::CslParser* cslParser = nullptr; + ASSERT_NO_THROW( + cslParser = new storm::parser::CslParser(ap); + ); + + ASSERT_NE(cslParser->getFormula(), nullptr); + + + ASSERT_EQ(ap, cslParser->getFormula()->toString()); + + delete cslParser->getFormula(); + delete cslParser; + +} + +TEST(CslParserTest, parsePropositionalFormulaTest) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_NO_THROW( + cslParser = new storm::parser::CslParser("!(a & b) | a & ! c") + ); + + ASSERT_NE(cslParser->getFormula(), nullptr); + + + ASSERT_EQ(cslParser->getFormula()->toString(), "(!(a & b) | (a & !c))"); + + delete cslParser->getFormula(); + delete cslParser; + +} + +TEST(CslParserTest, parseProbabilisticFormulaTest) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_NO_THROW( + cslParser = new storm::parser::CslParser("P > 0.5 [ F a ]") + ); + + ASSERT_NE(cslParser->getFormula(), nullptr); + + storm::formula::ProbabilisticBoundOperator* op = static_cast*>(cslParser->getFormula()); + + ASSERT_EQ(storm::formula::PathBoundOperator::GREATER, op->getComparisonOperator()); + ASSERT_EQ(0.5, op->getBound()); + + ASSERT_EQ(cslParser->getFormula()->toString(), "P > 0.500000 [F a]"); + + delete cslParser->getFormula(); + delete cslParser; + +} + +TEST(CslParserTest, parseSteadyStateBoundFormulaTest) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_NO_THROW( + cslParser = new storm::parser::CslParser("S >= 15 [ a & b ]") + ); + + ASSERT_NE(cslParser->getFormula(), nullptr); + + storm::formula::SteadyStateBoundOperator* op = static_cast*>(cslParser->getFormula()); + + ASSERT_EQ(storm::formula::StateBoundOperator::GREATER_EQUAL, op->getComparisonOperator()); + ASSERT_EQ(15.0, op->getBound()); + + ASSERT_EQ("S >= 15.000000 [(a & b)]", cslParser->getFormula()->toString()); + + delete cslParser->getFormula(); + delete cslParser; +} + +TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_NO_THROW( + cslParser = new storm::parser::CslParser("S = ? [ P <= 0.5 [ F a ] ]") + ); + + ASSERT_NE(cslParser->getFormula(), nullptr); + + + ASSERT_EQ(cslParser->getFormula()->toString(), "S = ? [P <= 0.500000 [F a]]"); + + delete cslParser->getFormula(); + delete cslParser; + +} + +TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_NO_THROW( + cslParser = new storm::parser::CslParser("P = ? [ a U <= 4 b & (!c) ]") + ); + + ASSERT_NE(cslParser->getFormula(), nullptr); + + + ASSERT_EQ(cslParser->getFormula()->toString(), "P = ? [a U<=4 (b & !c)]"); + + delete cslParser->getFormula(); + delete cslParser; + +} + +TEST(CslParserTest, parseComplexFormulaTest) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_NO_THROW( + cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])") + ); + + ASSERT_NE(cslParser->getFormula(), nullptr); + + + 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 (a & b)]]))", cslParser->getFormula()->toString()); + delete cslParser->getFormula(); + delete cslParser; + +} + + +TEST(CslParserTest, wrongProbabilisticFormulaTest) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_THROW( + cslParser = new storm::parser::CslParser("P > 0.5 [ a ]"), + storm::exceptions::WrongFormatException + ); + + delete cslParser; +} + +TEST(CslParserTest, wrongFormulaTest) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_THROW( + cslParser = new storm::parser::CslParser("(a | b) & +"), + storm::exceptions::WrongFormatException + ); + delete cslParser; +} + +TEST(CslParserTest, wrongFormulaTest2) { + storm::parser::CslParser* cslParser = nullptr; + ASSERT_THROW( + cslParser = new storm::parser::CslParser("P>0 [ F & a ]"), + storm::exceptions::WrongFormatException + ); + delete cslParser; +}