From d23b3dbee5cdf6e15fec3c5b5970f6bcc167d642 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Fri, 25 Jan 2013 17:27:33 +0100 Subject: [PATCH] First compiling version of PRCTL parser --- src/formula/BoundOperator.h | 19 ++++-- src/formula/Formulas.h | 2 - src/formula/PctlPathFormula.h | 1 + src/formula/PctlStateFormula.h | 1 + src/formula/ProbabilisticBoundOperator.h | 25 ++++---- src/formula/RewardBoundOperator.h | 24 ++++--- src/models/GraphTransitions.h | 4 +- src/parser/PrctlParser.cpp | 80 +++++++++++------------- 8 files changed, 80 insertions(+), 76 deletions(-) diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h index 0d0abedbd..a0e4c423a 100644 --- a/src/formula/BoundOperator.h +++ b/src/formula/BoundOperator.h @@ -46,8 +46,8 @@ public: /*! * Constructor * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability + * @param comparisonOperator The relation for the bound. + * @param bound The bound for the probability * @param pathFormula The child node */ BoundOperator(ComparisonType comparisonOperator, T bound, PctlPathFormula* pathFormula) @@ -83,6 +83,17 @@ public: this->pathFormula = pathFormula; } + /*! + * @returns the comparison relation + */ + const ComparisonType getComparisonOperator() const { + return comparisonOperator; + } + + void setComparisonOperator(ComparisonType comparisonOperator) { + this->comparisonOperator = comparisonOperator; + } + /*! * @returns the bound for the measure */ @@ -103,7 +114,7 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = "P "; + std::string result = ""; switch (comparisonOperator) { case LESS: result += "<"; break; case LESS_EQUAL: result += "<="; break; @@ -117,7 +128,7 @@ public: return result; } - bool meetsBound(T value) { + bool meetsBound(T value) const { switch (comparisonOperator) { case LESS: return value < bound; break; case LESS_EQUAL: return value <= bound; break; diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 38c607771..6fb771ca5 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -8,8 +8,6 @@ #ifndef STORM_FORMULA_FORMULAS_H_ #define STORM_FORMULA_FORMULAS_H_ -#include "modelChecker/ForwardDeclarations.h" - #include "And.h" #include "Ap.h" #include "BoundedUntil.h" diff --git a/src/formula/PctlPathFormula.h b/src/formula/PctlPathFormula.h index eaebd087e..01889b56e 100644 --- a/src/formula/PctlPathFormula.h +++ b/src/formula/PctlPathFormula.h @@ -8,6 +8,7 @@ #ifndef STORM_FORMULA_PCTLPATHFORMULA_H_ #define STORM_FORMULA_PCTLPATHFORMULA_H_ +#include "modelChecker/ForwardDeclarations.h" #include "PctlFormula.h" #include diff --git a/src/formula/PctlStateFormula.h b/src/formula/PctlStateFormula.h index eb7424d3f..b27b0087e 100644 --- a/src/formula/PctlStateFormula.h +++ b/src/formula/PctlStateFormula.h @@ -8,6 +8,7 @@ #ifndef STORM_FORMULA_PCTLSTATEFORMULA_H_ #define STORM_FORMULA_PCTLSTATEFORMULA_H_ +#include "modelChecker/ForwardDeclarations.h" #include "PctlFormula.h" #include "storage/BitVector.h" diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h index e541619c1..ac1bf2709 100644 --- a/src/formula/ProbabilisticBoundOperator.h +++ b/src/formula/ProbabilisticBoundOperator.h @@ -45,18 +45,21 @@ public: /*! * Empty constructor */ - ProbabilisticBoundOperator() : BoundOperator(storm::utility::constGetZero(), storm::utility::constGetZero(), nullptr) { + ProbabilisticBoundOperator() : BoundOperator + (BoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { // Intentionally left empty } /*! * Constructor * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability + * @param comparisonRelation The relation to compare the actual value and the bound + * @param bound The bound for the probability * @param pathFormula The child node */ - ProbabilisticBoundOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) : BoundOperator(lowerBound, upperBound, pathFormula) { + ProbabilisticBoundOperator( + typename BoundOperator::ComparisonType comparisonRelation, T bound, PctlPathFormula* pathFormula) : + BoundOperator(BoundOperator::LESS, bound, pathFormula) { // Intentionally left empty } @@ -64,13 +67,8 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = "P ["; - result += std::to_string(this->getLowerBound()); - result += ","; - result += std::to_string(this->getUpperBound()); - result += "] ("; - result += this->getPathFormula()->toString(); - result += ")"; + std::string result = "P"; + result += BoundOperator::toString(); return result; } @@ -83,8 +81,9 @@ public: */ virtual PctlStateFormula* clone() const { ProbabilisticBoundOperator* result = new ProbabilisticBoundOperator(); - result->setInterval(this->getLowerBound(), this->getUpperBound()); - result->setPathFormula(this->getPathFormula()->clone()); + result->setComparisonOperator(this->getComparisonOperator()); + result->setBound(this->getBound()); + result->setPathFormula(this->getPathFormula().clone()); return result; } }; diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h index 8118fdbe2..1f0a21cd6 100644 --- a/src/formula/RewardBoundOperator.h +++ b/src/formula/RewardBoundOperator.h @@ -44,18 +44,20 @@ public: /*! * Empty constructor */ - RewardBoundOperator() : BoundOperator(storm::utility::constGetZero(), storm::utility::constGetZero(), nullptr) { + RewardBoundOperator() : BoundOperator(BoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { // Intentionally left empty } /*! * Constructor * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability + * @param comparisonRelation The relation to compare the actual value and the bound + * @param bound The bound for the probability * @param pathFormula The child node */ - RewardBoundOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) : BoundOperator(lowerBound, upperBound, pathFormula) { + RewardBoundOperator( + typename BoundOperator::ComparisonType comparisonRelation, T bound, PctlPathFormula* pathFormula) : + BoundOperator(BoundOperator::LESS, bound, pathFormula) { // Intentionally left empty } @@ -63,13 +65,8 @@ public: * @returns a string representation of the formula */ virtual std::string toString() const { - std::string result = "R ["; - result += std::to_string(this->getLowerBound()); - result += ", "; - result += std::to_string(this->getUpperBound()); - result += "] ["; - result += this->getPathFormula()->toString(); - result += "]"; + std::string result = "R "; + result += BoundOperator::toString(); return result; } @@ -82,8 +79,9 @@ public: */ virtual PctlStateFormula* clone() const { RewardBoundOperator* result = new RewardBoundOperator(); - result->setBound(this->getLowerBound(), this->getUpperBound()); - result->setPathFormula(this->getPathFormula()->clone()); + result->setComparisonOperator(this->getComparisonOperator()); + result->setBound(this->getBound()); + result->setPathFormula(this->getPathFormula().clone()); return result; } }; diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 576d99f8c..6605f1983 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -110,8 +110,8 @@ private: * matrix. */ void initializeBackward(std::shared_ptr> transitionMatrix) { - this->successorList = new uint_fast64_t[numberOfNonZeroTransitions](); - this->stateIndications = new uint_fast64_t[numberOfStates + 1](); + this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]; + this->stateIndications = new uint_fast64_t[numberOfStates + 1]; // First, we need to count how many backward transitions each state has. // NOTE: We disregard the diagonal here, as we only consider "true" diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index b3bd6d06f..f3f80289a 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -20,9 +20,8 @@ #include // Some typedefs and namespace definitions to reduce code size. -typedef std::istreambuf_iterator base_iterator_type; -typedef boost::spirit::multi_pass forward_iterator_type; -typedef boost::spirit::classic::position_iterator2 pos_iterator_type; +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; @@ -36,54 +35,47 @@ struct PrctlParser::PrctlGrammar : qi::grammar>(qi::_1, qi::_2)]; - orFormula = ('(' << stateFormula << '|' << stateFormula << ')')[qi::_val = + stateFormula %= (andFormula | atomicProposition | orFormula | notFormula | probabilisticBoundOperator | rewardBoundOperator); + + andFormula = (qi::lit("(") >> stateFormula >> qi::lit("&") >> stateFormula >> qi::lit(")"))[ + qi::_val = phoenix::new_>(qi::_1, qi::_2)]; + orFormula = (qi::lit("(") >> stateFormula >> '|' >> stateFormula >> ')')[qi::_val = phoenix::new_>(qi::_1, qi::_2)]; - notFormula = ('!' << stateFormula)[qi::_val = + notFormula = ('!' >> stateFormula)[qi::_val = phoenix::new_>(qi::_1)]; atomicProposition = (freeIdentifierName)[qi::_val = phoenix::new_>(qi::_1)]; probabilisticBoundOperator = ( - ("P=" << qi::double_ << '[' << pathFormula << ']') [qi::_val = - phoenix::new_>(qi::_1, qi::_1, qi::_2)] | - ("P[" << qi::double_ << qi::double_ << ']' << '[' << pathFormula << ']')[qi::_val = - phoenix::new_ >(qi::_1, qi::_2, qi::_3)] | - ("P>=" << qi::double_ << '[' << pathFormula << ']')[qi::_val = - phoenix::new_ >(qi::_1, 1, qi::_2)] | - ("P<=" << qi::double_ << '[' << pathFormula << ']')[qi::_val = - phoenix::new_ >(0, qi::_1, qi::_2)] + ("P>=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | + ("P<=" >> 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_ >(qi::_1, qi::_1, qi::_2)] | - ("R[" << qi::double_ << qi::double_ << ']' << '[' << pathFormula << ']')[qi::_val = - phoenix::new_ >(qi::_1, qi::_2, qi::_3)] | - ("R>=" << qi::double_ << '[' << pathFormula << ']')[qi::_val = - phoenix::new_ >(qi::_1, storm::utility::constGetInfinity(), qi::_2)] | - ("R<=" << qi::double_ << '[' << pathFormula << ']')[qi::_val = - phoenix::new_ >(0, qi::_1, qi::_2)] + ("R>=" >> qi::double_ >> '[' >> pathFormula >> ']')[qi::_val = + phoenix::new_ >(storm::formula::BoundOperator::GREATER_EQUAL, qi::_1, qi::_2)] | + ("R<=" >> qi::double_ >> '[' >> pathFormula >> ']')[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 = + probabilisticNoBoundOperator = ("P=?[" >> pathFormula >> ']')[qi::_val = phoenix::new_ >(qi::_1)]; - rewardNoBoundOperator = ("R=?[" << pathFormula << ']')[qi::_val = + rewardNoBoundOperator = ("R=?[" >> pathFormula >> ']')[qi::_val = phoenix::new_ >(qi::_1)]; //This block defines rules for parsing path formulas pathFormula %= (eventually | boundedEventually | globally | boundedUntil | until); - eventually = ('F' << pathFormula)[qi::_val = + eventually = ('F' >> stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - boundedEventually = ("F<=" << qi::double_ << pathFormula)[qi::_val = + boundedEventually = ("F<=" >> qi::int_ >> stateFormula)[qi::_val = phoenix::new_>(qi::_2, qi::_1)]; - globally = ('G' << pathFormula)[qi::_val = + globally = ('G' >> stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - until = (stateFormula << 'U' << stateFormula)[qi::_val = + until = (stateFormula >> 'U' >> stateFormula)[qi::_val = phoenix::new_>(qi::_1, qi::_2)]; - boundedUntil = (stateFormula << "U<=" << qi::double_ << stateFormula)[qi::_val = + boundedUntil = (stateFormula >> "U<=" >> qi::int_ >> stateFormula)[qi::_val = phoenix::new_>(qi::_1, qi::_3, qi::_2)]; start %= (stateFormula | noBoundOperator); @@ -93,7 +85,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> stateFormula; qi::rule*(), Skipper> andFormula; - qi::rule*(), Skipper> atomicProposition; + qi::rule*(), Skipper> atomicProposition; qi::rule*(), Skipper> orFormula; qi::rule*(), Skipper> notFormula; qi::rule*(), Skipper> probabilisticBoundOperator; @@ -117,24 +109,28 @@ struct PrctlParser::PrctlGrammar : qi::grammar(inputFileStream)), (std::istreambuf_iterator())); + BaseIteratorType stringIteratorBegin = fileContent.begin(); + BaseIteratorType stringIteratorEnd = fileContent.end(); + PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename); + PositionIteratorType positionIteratorEnd; + // Prepare resulting intermediate representation of input. - storm::formula::PctlFormula* result_pointer; + storm::formula::PctlFormula* result_pointer = nullptr; - PrctlGrammar grammar; + PrctlGrammar grammar; - qi::phrase_parse(position_begin, position_end, grammar, boost::spirit::ascii::space, result_pointer); + qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); }