diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp new file mode 100644 index 000000000..28d53f20f --- /dev/null +++ b/src/parser/PrctlFileParser.cpp @@ -0,0 +1,32 @@ +/* + * PrctlFileParser.cpp + * + * Created on: 06.02.2013 + * Author: Thomas Heinemann + */ + +#include "PrctlFileParser.h" + +namespace storm { +namespace parser { + +PrctlFileParser::PrctlFileParser(std::string filename) { + // Open file and initialize result. + std::ifstream inputFileStream(filename, std::ios::in); + + // Prepare iterators to input. + // TODO: Right now, this parses the whole contents of the file into a string first. + // While this is usually not necessary, because there exist adapters that make an input stream + // iterable in both directions without storing it into a string, using the corresponding + // Boost classes gives an awful output under valgrind and is thus disabled for the time being. + std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); + parse(fileContent); +} + +PrctlFileParser::~PrctlFileParser() { + //intentionally left empty + //formulas are not deleted with the parser! +} + +} /* namespace parser */ +} /* namespace storm */ diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h new file mode 100644 index 000000000..3520d8949 --- /dev/null +++ b/src/parser/PrctlFileParser.h @@ -0,0 +1,24 @@ +/* + * PrctlFileParser.h + * + * Created on: 06.02.2013 + * Author: Thomas Heinemann + */ + +#ifndef STORM_PARSER_PRCTLFILEPARSER_H_ +#define STORM_PARSER_PRCTLFILEPARSER_H_ + +#include "PrctlParser.h" + +namespace storm { +namespace parser { + +class PrctlFileParser: public storm::parser::PrctlParser { +public: + PrctlFileParser(std::string filename); + virtual ~PrctlFileParser(); +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_PRCTLFILEPARSER_H_ */ diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 6e0132ff8..6f84aa89c 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -124,19 +124,10 @@ struct PrctlParser::PrctlGrammar : qi::grammar(inputFileStream)), (std::istreambuf_iterator())); - BaseIteratorType stringIteratorBegin = fileContent.begin(); - BaseIteratorType stringIteratorEnd = fileContent.end(); - PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename); +void storm::parser::PrctlParser::parse(std::string formulaString) { + BaseIteratorType stringIteratorBegin = formulaString.begin(); + BaseIteratorType stringIteratorEnd = formulaString.end(); + PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString); PositionIteratorType positionIteratorEnd; @@ -148,5 +139,8 @@ storm::parser::PrctlParser::PrctlParser(std::string filename) { qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); formula = result_pointer; +} +storm::parser::PrctlParser::PrctlParser(std::string formula) { + parse(formula); } diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index f9f34cb63..f0c95923b 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -15,7 +15,8 @@ namespace parser { class PrctlParser : Parser { public: - PrctlParser(std::string filename); + PrctlParser() { } + PrctlParser(std::string formulaString); /*! * @brief return formula object parsed from file. @@ -25,6 +26,13 @@ class PrctlParser : Parser return this->formula; } + protected: + /*! + * Parses a formula and stores the result in the field "formula" + * @param formula The string representation of the formula to parse + */ + void parse(std::string formula); + private: storm::formula::AbstractFormula* formula; diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp index 6d795819c..5a2dd3cf2 100644 --- a/test/parser/PrctlParserTest.cpp +++ b/test/parser/PrctlParserTest.cpp @@ -9,11 +9,12 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/PrctlParser.h" +#include "src/parser/PrctlFileParser.h" 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") + prctlParser = new storm::parser::PrctlParser("P"); ); ASSERT_NE(prctlParser->getFormula(), nullptr); @@ -27,103 +28,103 @@ TEST(PrctlParserTest, parseApOnlyTest) { } TEST(PrctlParserTest, parsePropositionalFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::parser::PrctlFileParser* prctlFileParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl") + prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/propositionalFormula.prctl") ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + ASSERT_NE(prctlFileParser->getFormula(), nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "(!(a && b) || (a && !c))"); + ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(!(a && b) || (a && !c))"); - delete prctlParser->getFormula(); - delete prctlParser; + delete prctlFileParser->getFormula(); + delete prctlFileParser; } TEST(PrctlParserTest, parseProbabilisticFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::parser::PrctlFileParser* prctlFileParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl") + prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticFormula.prctl") ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + ASSERT_NE(prctlFileParser->getFormula(), nullptr); - storm::formula::ProbabilisticBoundOperator* op = static_cast*>(prctlParser->getFormula()); + storm::formula::ProbabilisticBoundOperator* op = static_cast*>(prctlFileParser->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]"); + ASSERT_EQ(prctlFileParser->getFormula()->toString(), "P > 0.500000 [F a]"); - delete prctlParser->getFormula(); - delete prctlParser; + delete prctlFileParser->getFormula(); + delete prctlFileParser; } TEST(PrctlParserTest, parseRewardFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::parser::PrctlFileParser* prctlFileParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl") + prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardFormula.prctl") ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + ASSERT_NE(prctlFileParser->getFormula(), nullptr); - storm::formula::RewardBoundOperator* op = static_cast*>(prctlParser->getFormula()); + storm::formula::RewardBoundOperator* op = static_cast*>(prctlFileParser->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)]"); + ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]"); - delete prctlParser->getFormula(); - delete prctlParser; + delete prctlFileParser->getFormula(); + delete prctlFileParser; } TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::parser::PrctlFileParser* prctlFileParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardNoBoundFormula.prctl") + prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/rewardNoBoundFormula.prctl") ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + ASSERT_NE(prctlFileParser->getFormula(), nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "R = ? [(a U<=4 (b && !c))]"); + ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R = ? [(a U<=4 (b && !c))]"); - delete prctlParser->getFormula(); - delete prctlParser; + delete prctlFileParser->getFormula(); + delete prctlFileParser; } TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::parser::PrctlFileParser* prctlFileParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticNoBoundFormula.prctl") + prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/probabilisticNoBoundFormula.prctl") ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + ASSERT_NE(prctlFileParser->getFormula(), nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "P = ? [F<=42 !a]"); + ASSERT_EQ(prctlFileParser->getFormula()->toString(), "P = ? [F<=42 !a]"); - delete prctlParser->getFormula(); - delete prctlParser; + delete prctlFileParser->getFormula(); + delete prctlFileParser; } TEST(PrctlParserTest, parseComplexFormulaTest) { - storm::parser::PrctlParser* prctlParser = nullptr; + storm::parser::PrctlFileParser* prctlFileParser = nullptr; ASSERT_NO_THROW( - prctlParser = new storm::parser::PrctlParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/complexFormula.prctl") + prctlFileParser = new storm::parser::PrctlFileParser(STORM_CPP_TESTS_BASE_PATH "/parser/prctl_files/complexFormula.prctl") ); - ASSERT_NE(prctlParser->getFormula(), nullptr); + ASSERT_NE(prctlFileParser->getFormula(), nullptr); - ASSERT_EQ(prctlParser->getFormula()->toString(), "(P <= 0.500000 [F a] && (R > 15.000000 [G P > 0.900000 [F<=7 (a && b)]] || !P < 0.400000 [G !b]))"); - delete prctlParser->getFormula(); - delete prctlParser; + ASSERT_EQ(prctlFileParser->getFormula()->toString(), "(P <= 0.500000 [F a] && (R > 15.000000 [G P > 0.900000 [F<=7 (a && b)]] || !P < 0.400000 [G !b]))"); + delete prctlFileParser->getFormula(); + delete prctlFileParser; }