From cf6623c68ce8c29e28071e608198ee7c3deef148 Mon Sep 17 00:00:00 2001 From: masawei Date: Thu, 15 May 2014 22:54:57 +0200 Subject: [PATCH] Intruduced legacy support. - Every PRCTL formula that worked before works now and behaves in the same way. One exception: |- Formulas of the type Pmin<0.5[Phi] and Rmin<0.5[Psi] result in a parsing error, as the comparison operator already implies the scheduler to be used. | Also, the modelchecker now actually uses the comparison operator in order to choose the correct scheduler for MDPs. Former-commit-id: d942d18e7e472dcbdfe5c1bc83d7802d1af26cd8 --- src/formula/AbstractFilter.h | 12 +-- src/formula/Actions/AbstractAction.h | 2 +- src/formula/Actions/MinMaxAction.h | 2 +- src/formula/Actions/RangeAction.h | 31 ++++++-- src/formula/Prctl/PrctlFilter.h | 56 +++++++------ src/modelchecker/prctl/AbstractModelChecker.h | 4 +- .../prctl/SparseMdpPrctlModelChecker.h | 74 +++++++++++++++++ src/parser/PrctlFileParser.cpp | 4 +- src/parser/PrctlFileParser.h | 3 +- src/parser/PrctlParser.cpp | 79 +++++++++++++------ src/parser/PrctlParser.h | 6 +- 11 files changed, 201 insertions(+), 72 deletions(-) diff --git a/src/formula/AbstractFilter.h b/src/formula/AbstractFilter.h index 6e73913c8..4031125d5 100644 --- a/src/formula/AbstractFilter.h +++ b/src/formula/AbstractFilter.h @@ -10,7 +10,7 @@ #include #include "src/formula/AbstractFormula.h" -#include "src/formula/Actions/Action.h" +#include "src/formula/Actions/AbstractAction.h" namespace storm { namespace property { @@ -24,11 +24,11 @@ public: // Intentionally left empty. } - AbstractFilter(action::Action* action) { + AbstractFilter(action::AbstractAction* action) { actions.push_back(action); } - AbstractFilter(std::vector*> actions) : actions(actions) { + AbstractFilter(std::vector*> actions) : actions(actions) { // Intentionally left empty. } @@ -50,7 +50,7 @@ public: return desc; } - void addAction(action::Action* action) { + void addAction(action::AbstractAction* action) { actions.push_back(action); } @@ -58,7 +58,7 @@ public: actions.pop_back(); } - action::Action* getAction(uint_fast64_t pos) const { + action::AbstractAction* getAction(uint_fast64_t pos) const { return actions[pos]; } @@ -68,7 +68,7 @@ public: protected: - std::vector*> actions; + std::vector*> actions; }; } //namespace property diff --git a/src/formula/Actions/AbstractAction.h b/src/formula/Actions/AbstractAction.h index d5a548046..c58ad6be0 100644 --- a/src/formula/Actions/AbstractAction.h +++ b/src/formula/Actions/AbstractAction.h @@ -38,7 +38,7 @@ public: /*! * */ - virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const { + virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const { return input; } diff --git a/src/formula/Actions/MinMaxAction.h b/src/formula/Actions/MinMaxAction.h index f23dd3195..c775700e7 100644 --- a/src/formula/Actions/MinMaxAction.h +++ b/src/formula/Actions/MinMaxAction.h @@ -15,7 +15,7 @@ namespace property { namespace action { template -class MinMaxAction : AbstractAction { +class MinMaxAction : public AbstractAction { public: diff --git a/src/formula/Actions/RangeAction.h b/src/formula/Actions/RangeAction.h index 5ea2bd6ee..3952419ae 100644 --- a/src/formula/Actions/RangeAction.h +++ b/src/formula/Actions/RangeAction.h @@ -10,12 +10,14 @@ #include "src/formula/Actions/AbstractAction.h" +#include + namespace storm { namespace property { namespace action { template -class RangeAction : AbstractAction { +class RangeAction : public AbstractAction { public: @@ -49,8 +51,19 @@ public: /*! * */ - virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const override { - storm::storage::BitVector out(to - from + 1, input.begin() + from, input.begin() + to); + virtual storm::storage::BitVector evaluate(storm::storage::BitVector input) const override { + //Initialize the output vector. + storm::storage::BitVector out(to - from + 1); + + storm::storage::BitVector::const_iterator it = input.begin(); + + //Proceed the set index iterator to the first set bit within the range. + for(; *it < from; ++it); + + //Fill the output vector. + for(; *it <= to; ++it) { + out.set(*it-from); + } return out; } @@ -58,14 +71,22 @@ public: * */ virtual std::string toString() const override { - return "range, " + from + ", " + to; + std::string out = "range, "; + out += std::to_string(from); + out += ", "; + out += std::to_string(to); + return out; } /*! * */ virtual std::string toFormulaString() const override { - return "\"range\", " + from + ", " + to; + std::string out = "\"range\", "; + out += std::to_string(from); + out += ", "; + out += std::to_string(to); + return out; } private: diff --git a/src/formula/Prctl/PrctlFilter.h b/src/formula/Prctl/PrctlFilter.h index 9af9dc39a..f766a5942 100644 --- a/src/formula/Prctl/PrctlFilter.h +++ b/src/formula/Prctl/PrctlFilter.h @@ -12,13 +12,15 @@ #include "src/formula/Prctl/AbstractPrctlFormula.h" #include "src/formula/Prctl/AbstractPathFormula.h" #include "src/formula/Prctl/AbstractStateFormula.h" +#include "src/modelchecker/prctl/AbstractModelChecker.h" +#include "src/formula/Actions/MinMaxAction.h" namespace storm { namespace property { namespace prctl { template -class PrctlFilter : storm::property::AbstractFilter { +class PrctlFilter : public storm::property::AbstractFilter { public: @@ -26,24 +28,28 @@ public: // Intentionally left empty. } - PrctlFilter(AbstractPrctlFormula* child) : child(child) { + PrctlFilter(AbstractPrctlFormula* child) : child(child) { // Intentionally left empty. } - PrctlFilter(AbstractPrctlFormula* child, action::Action* action) : child(child) { - actions.push_back(action); + PrctlFilter(AbstractPrctlFormula* child, bool minimize) : child(child) { + this->actions.push_back(new storm::property::action::MinMaxAction(minimize)); } - PrctlFilter(AbstractPrctlFormula* child, std::vector*> actions) : child(child), actions(actions) { + PrctlFilter(AbstractPrctlFormula* child, action::AbstractAction* action) : child(child) { + this->actions.push_back(action); + } + + PrctlFilter(AbstractPrctlFormula* child, std::vector*> actions) : AbstractFilter(actions), child(child) { // Intentionally left empty. } virtual ~PrctlFilter() { - actions.clear(); + this->actions.clear(); delete child; } - void check(AbstractModelChecker const & modelchecker) const { + void check(storm::modelchecker::prctl::AbstractModelChecker const & modelchecker) const { // Write out the formula to be checked. std::cout << std::endl; @@ -68,13 +74,13 @@ public: // Now write out the result. - if(actions.empty()) { + if(this->actions.empty()) { // There is no filter action given. So provide legacy support: // Return the results for all states labeled with "init". LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : modelchecker.getModel>().getInitialStates()) { + for (auto initialState : modelchecker.getModel().getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied")); std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl; } @@ -100,13 +106,13 @@ public: // Now write out the result. - if(actions.empty()) { + if(this->actions.empty()) { // There is no filter action given. So provide legacy support: // Return the results for all states labeled with "init". LOG4CPLUS_INFO(logger, "Result for initial states:"); std::cout << "Result for initial states:" << std::endl; - for (auto initialState : modelchecker.getModel>().getInitialStates()) { + for (auto initialState : modelchecker.getModel().getInitialStates()) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]); std::cout << "\t" << initialState << ": " << result[initialState] << std::endl; } @@ -147,61 +153,61 @@ public: std::string toString() const { std::string desc = "Filter: "; desc += "\nActions:"; - for(auto action : actions) { - desc += "\n\t" + action.toString(); + for(auto action : this->actions) { + desc += "\n\t" + action->toString(); } desc += "\nFormula:\n\t" + child->toString(); return desc; } - void setChild(AbstractPrctlFormula* child) { + void setChild(AbstractPrctlFormula* child) { this->child = child; } - AbstractFormula* getChild() const { + AbstractPrctlFormula* getChild() const { return child; } private: - BitVector evaluate(AbstractModelChecker const & modelchecker, AbstractStateFormula* formula) const { + storm::storage::BitVector evaluate(storm::modelchecker::prctl::AbstractModelChecker const & modelchecker, AbstractStateFormula* formula) const { // First, get the model checking result. - BitVector result = modelchecker.checkMinMaxOperator(formula); + storm::storage::BitVector result; - if(getActionCount() != 0 && dynamic_cast*>(getAction(0)) != nullptr) { + if(this->getActionCount() != 0 && dynamic_cast*>(this->getAction(0)) != nullptr) { // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. - result = modelchecker.checkMinMaxOperator(formula, static_cast*>(getAction(0))->getMinimize()); + result = modelchecker.checkMinMaxOperator(formula, static_cast*>(this->getAction(0))->getMinimize()); } else { result = formula->check(modelchecker); } // Now apply all filter actions and return the result. - for(auto action : actions) { + for(auto action : this->actions) { result = action->evaluate(result); } return result; } - std::vector evaluate(AbstractModelChecker const & modelchecker, AbstractPathFormula* formula) const { + std::vector evaluate(storm::modelchecker::prctl::AbstractModelChecker const & modelchecker, AbstractPathFormula* formula) const { // First, get the model checking result. std::vector result; - if(getActionCount() != 0 && dynamic_cast*>(getAction(0)) != nullptr) { + if(this->getActionCount() != 0 && dynamic_cast*>(this->getAction(0)) != nullptr) { // If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker. - result = modelchecker.checkMinMaxOperator(formula, static_cast*>(getAction(0))->getMinimize()); + result = modelchecker.checkMinMaxOperator(formula, static_cast*>(this->getAction(0))->getMinimize()); } else { result = formula->check(modelchecker, false); } // Now apply all filter actions and return the result. - for(auto action : actions) { + for(auto action : this->actions) { result = action->evaluate(result); } return result; } - AbstractPrctlFormula* child; + AbstractPrctlFormula* child; }; } //namespace prctl diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 5eaa14f80..ed79fdace 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -187,7 +187,7 @@ public: * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator const& formula) const { + virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator const& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector quantitativeResult = formula.getPathFormula().check(*this, false); @@ -211,7 +211,7 @@ public: * @param formula The formula to check. * @return The set of states satisfying the formula represented by a bit vector. */ - storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator& formula) const { + virtual storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector quantitativeResult = formula.getPathFormula().check(*this, false); diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 7a9c7c29c..c68c1057f 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -69,6 +69,80 @@ namespace storm { return AbstractModelChecker::template getModel>(); } + /*! + * Checks the given formula that is a P operator over a path formula featuring a value bound. + * + * @param formula The formula to check. + * @return The set of states satisfying the formula represented by a bit vector. + */ + virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator const& formula) const override { + + // For P< and P<= the MDP satisfies the formula iff the probability maximizing scheduler is used. + // For P> and P>= " iff the probability minimizing " . + if(formula.getComparisonOperator() == storm::property::LESS || formula.getComparisonOperator() == storm::property::LESS_EQUAL) { + this->minimumOperatorStack.push(false); + } + else { + this->minimumOperatorStack.push(true); + } + + // First, we need to compute the probability for satisfying the path formula for each state. + std::vector quantitativeResult = formula.getPathFormula().check(*this, false); + + //Remove the minimizing operator entry from the stack. + this->minimumOperatorStack.pop(); + + // Create resulting bit vector that will hold the yes/no-answer for every state. + storm::storage::BitVector result(quantitativeResult.size()); + + // Now, we can compute which states meet the bound specified in this operator and set the + // corresponding bits to true in the resulting vector. + for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) { + if (formula.meetsBound(quantitativeResult[i])) { + result.set(i, true); + } + } + + return result; + } + + /*! + * Checks the given formula that is an R operator over a reward formula featuring a value bound. + * + * @param formula The formula to check. + * @return The set of states satisfying the formula represented by a bit vector. + */ + virtual storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator& formula) const override { + + // For R< and R<= the MDP satisfies the formula iff the reward maximizing scheduler is used. + // For R> and R>= " iff the reward minimizing " . + if(formula.getComparisonOperator() == storm::property::LESS || formula.getComparisonOperator() == storm::property::LESS_EQUAL) { + this->minimumOperatorStack.push(false); + } + else { + this->minimumOperatorStack.push(true); + } + + // First, we need to compute the probability for satisfying the path formula for each state. + std::vector quantitativeResult = formula.getPathFormula().check(*this, false); + + //Remove the minimizing operator entry from the stack. + this->minimumOperatorStack.pop(); + + // Create resulting bit vector that will hold the yes/no-answer for every state. + storm::storage::BitVector result(quantitativeResult.size()); + + // Now, we can compute which states meet the bound specified in this operator and set the + // corresponding bits to true in the resulting vector. + for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) { + if (formula.meetsBound(quantitativeResult[i])) { + result.set(i, true); + } + } + + return result; + } + /*! * Computes the probability to satisfy phi until psi within a limited number of steps for each state. * diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index b4f2b3f2e..9fadfbf2f 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -14,7 +14,7 @@ namespace storm { namespace parser { -std::list*> PrctlFileParser(std::string filename) { +std::list*> PrctlFileParser(std::string filename) { // Open file std::ifstream inputFileStream; inputFileStream.open(filename, std::ios::in); @@ -24,7 +24,7 @@ std::list*> PrctlFileParser throw storm::exceptions::FileIoException() << message << filename; } - std::list*> result; + std::list*> result; std::string line; //The while loop reads the input file line by line diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h index b2a4335a2..15fc6b382 100644 --- a/src/parser/PrctlFileParser.h +++ b/src/parser/PrctlFileParser.h @@ -9,6 +9,7 @@ #define STORM_PARSER_PRCTLFILEPARSER_H_ #include "formula/Prctl.h" +#include "src/formula/Prctl/PrctlFilter.h" #include @@ -21,7 +22,7 @@ namespace parser { * @param filename * @return The list of parsed formulas */ -std::list*> PrctlFileParser(std::string filename); +std::list*> PrctlFileParser(std::string filename); } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index e5d6d47fa..4be6ad1a3 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -2,7 +2,7 @@ #include "src/utility/OsDetection.h" #include "src/utility/constants.h" -// The action class header. +// The action class headers. #include "src/formula/Actions/AbstractAction.h" #include "src/formula/Actions/MinMaxAction.h" #include "src/formula/Actions/RangeAction.h" @@ -70,24 +70,12 @@ struct PrctlParser::PrctlGrammar : qi::grammar>(qi::_1)]; atomicProposition.name("state formula"); - probabilisticBoundOperator = ( - (qi::lit("P") >> qi::lit("min") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1, qi::_2, qi::_3, true)] | - (qi::lit("P") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1, qi::_2, qi::_3, false)] | - (qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1, qi::_2, qi::_3)] - ); + probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3)]); probabilisticBoundOperator.name("state formula"); - rewardBoundOperator = ( - (qi::lit("R") >> qi::lit("min") > comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1, qi::_2, qi::_3, true)] | - (qi::lit("R") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1, qi::_2, qi::_3, false)] | - (qi::lit("R") >> comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = - phoenix::new_ >(qi::_1, qi::_2, qi::_3)] - ); + rewardBoundOperator = ((qi::lit("R") >> comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, qi::_2, qi::_3)]); rewardBoundOperator.name("state formula"); //This block defines rules for parsing probabilistic path formulas @@ -115,31 +103,66 @@ struct PrctlParser::PrctlGrammar : qi::grammar qi::lit("<=") > qi::double_) - [qi::_val = phoenix::new_>(qi::_1)]; + cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_)[qi::_val = + phoenix::new_>(qi::_1)]; cumulativeReward.name("path formula (for reward operator)"); reachabilityReward = (qi::lit("F") > stateFormula)[qi::_val = phoenix::new_>(qi::_1)]; reachabilityReward.name("path formula (for reward operator)"); - instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_) - [qi::_val = phoenix::new_>(qi::_1)]; + instantaneousReward = (qi::lit("I") > qi::lit("=") > qi::double_)[qi::_val = + phoenix::new_>(qi::_1)]; instantaneousReward.name("path formula (for reward operator)"); steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_>()]; formula = (pathFormula | stateFormula); formula.name("PRCTL formula"); - minMaxAction = qi::lit("minmax") >> qi::lit(",") >> (qi::lit("min")[qi::_val = phoenix::new_>(true)] | qi::lit("min")[qi::_val = storm::property::action::MinMaxAction(false)]); + //This block defines rules for parsing formulas with noBoundOperators + //Note that this is purely for legacy support. + //NoBoundOperators are no longer part of the formula tree and are therefore deprecated. + noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); + noBoundOperator.name("no bound operator"); + probabilisticNoBoundOperator = ( + (qi::lit("P") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, true)] | + (qi::lit("P") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, false)] | + (qi::lit("P") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)] + ); + probabilisticNoBoundOperator.name("no bound operator"); + + rewardNoBoundOperator = ( + (qi::lit("R") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, true)] | + (qi::lit("R") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, false)] | + (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)] + + ); + rewardNoBoundOperator.name("no bound operator"); + + minMaxAction = qi::lit("minmax") >> qi::lit(",") >> ( + qi::lit("min")[qi::_val = + phoenix::new_>(true)] | + qi::lit("min")[qi::_val = + phoenix::new_>(false)]); minMaxAction.name("minmax action for the formula filter"); - rangeAction = (qi::lit("range") >> qi::lit(",") >> qi::uint_ >> qi::lit(",") >> qi::uint_)[qi::_val = phoenix::new_>(qi::_1, qi::_2)]; + rangeAction = (qi::lit("range") >> qi::lit(",") >> qi::uint_ >> qi::lit(",") >> qi::uint_)[qi::_val = + phoenix::new_>(qi::_1, qi::_2)]; rangeAction.name("range action for the formula filter"); abstractAction = (rangeAction | minMaxAction) >> (qi::eps | qi::lit(",")); abstractAction.name("filter action"); - filter = ((qi::eps | qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]")) >> (formula | (qi::lit("(") >> formula >> qi::lit(")")))) - [qi::_val = phoenix::new_>(qi::_2, qi::_1)]; + filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") >> qi::lit("(") >> formula >> qi::lit(")"))[qi::_val = + phoenix::new_>(qi::_2, qi::_1)] | + (formula)[qi::_val = + phoenix::new_>(qi::_1)] | + (noBoundOperator)[qi::_val = + qi::_1]; filter.name("PRCTL formula filter"); start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment) > qi::eoi; @@ -149,6 +172,10 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> start; qi::rule*(), Skipper> filter; + qi::rule*(), Skipper> noBoundOperator; + qi::rule*(), Skipper> probabilisticNoBoundOperator; + qi::rule*(), Skipper> rewardNoBoundOperator; + qi::rule*(), Skipper> abstractAction; qi::rule*(), Skipper> rangeAction; qi::rule*(), Skipper> minMaxAction; @@ -198,7 +225,7 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) { // Prepare resulting intermediate representation of input. - storm::property::prctl::AbstractPrctlFormula* result_pointer = nullptr; + storm::property::prctl::PrctlFilter* result_pointer = nullptr; PrctlGrammar grammar; diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 3ba8f1998..52a403afd 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -2,7 +2,7 @@ #define STORM_PARSER_PRCTLPARSER_H_ #include "src/formula/Prctl.h" -//#include +#include "src/formula/Prctl/PrctlFilter.h" namespace storm { namespace parser { @@ -32,7 +32,7 @@ class PrctlParser { /*! * @return a pointer to the parsed formula object */ - storm::property::prctl::AbstractPrctlFormula* getFormula() { + storm::property::prctl::PrctlFilter* getFormula() { return this->formula; } @@ -47,7 +47,7 @@ class PrctlParser { } private: - storm::property::prctl::AbstractPrctlFormula* formula; + storm::property::prctl::PrctlFilter* formula; /*! * Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas.