diff --git a/src/formula/Actions/Action.h b/src/formula/Actions/AbstractAction.h similarity index 77% rename from src/formula/Actions/Action.h rename to src/formula/Actions/AbstractAction.h index dd7bd3502..d5a548046 100644 --- a/src/formula/Actions/Action.h +++ b/src/formula/Actions/AbstractAction.h @@ -1,12 +1,12 @@ /* - * Action.h + * AbstractAction.h * * Created on: Apr 26, 2014 * Author: Manuel Sascha Weiand */ -#ifndef STORM_FORMULA_ACTION_ACTION_H_ -#define STORM_FORMULA_ACTION_ACTION_H_ +#ifndef STORM_FORMULA_ACTION_ABSTRACTACTION_H_ +#define STORM_FORMULA_ACTION_ABSTRACTACTION_H_ #include #include "src/storage/BitVector.h" @@ -16,7 +16,7 @@ namespace property { namespace action { template -class Action { +class AbstractAction { public: @@ -24,7 +24,7 @@ public: * Virtual destructor * To ensure that the right destructor is called */ - virtual ~Action() { + virtual ~AbstractAction() { //Intentionally left empty } @@ -58,4 +58,4 @@ public: } //namespace storm -#endif /* STORM_FORMULA_ACTION_ACTION_H_ */ +#endif /* STORM_FORMULA_ACTION_ABSTRACTACTION_H_ */ diff --git a/src/formula/Actions/MinMaxAction.h b/src/formula/Actions/MinMaxAction.h index 2c32bd964..f23dd3195 100644 --- a/src/formula/Actions/MinMaxAction.h +++ b/src/formula/Actions/MinMaxAction.h @@ -8,14 +8,14 @@ #ifndef STORM_FORMULA_ACTION_MINMAXACTION_H_ #define STORM_FORMULA_ACTION_MINMAXACTION_H_ -#include "src/formula/Actions/Action.h" +#include "src/formula/Actions/AbstractAction.h" namespace storm { namespace property { namespace action { template -class MinMaxAction : Action { +class MinMaxAction : AbstractAction { public: @@ -27,6 +27,14 @@ public: //Intentionally left empty. } + /*! + * Virtual destructor + * To ensure that the right destructor is called + */ + virtual ~MinMaxAction() { + //Intentionally left empty + } + /*! * */ diff --git a/src/formula/Actions/RangeAction.h b/src/formula/Actions/RangeAction.h index 58a44aa0e..5ea2bd6ee 100644 --- a/src/formula/Actions/RangeAction.h +++ b/src/formula/Actions/RangeAction.h @@ -8,14 +8,14 @@ #ifndef STORM_FORMULA_ACTION_RANGEACTION_H_ #define STORM_FORMULA_ACTION_RANGEACTION_H_ -#include "src/formula/Actions/Action.h" +#include "src/formula/Actions/AbstractAction.h" namespace storm { namespace property { namespace action { template -class RangeAction : Action { +class RangeAction : AbstractAction { public: diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index fb58d7ee9..e5d6d47fa 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -2,6 +2,11 @@ #include "src/utility/OsDetection.h" #include "src/utility/constants.h" +// The action class header. +#include "src/formula/Actions/AbstractAction.h" +#include "src/formula/Actions/MinMaxAction.h" +#include "src/formula/Actions/RangeAction.h" + // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" @@ -33,7 +38,7 @@ namespace storm { namespace parser { template -struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper > { +struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper > { PrctlGrammar() : PrctlGrammar::base_type(start) { //This block contains helper rules that may be used several times freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; @@ -85,30 +90,6 @@ struct PrctlParser::PrctlGrammar : qi::grammar> 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"); - //This block defines rules for parsing probabilistic path formulas pathFormula = (boundedEventually | eventually | next | globally | boundedUntil | until); pathFormula.name("path formula"); @@ -145,16 +126,33 @@ struct PrctlParser::PrctlGrammar : qi::grammar>()]; - formula = (noBoundOperator | stateFormula); + formula = (pathFormula | stateFormula); formula.name("PRCTL formula"); - start = (((formula) > (comment | qi::eps))[qi::_val = qi::_1] | - comment - ) > qi::eoi; - start.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)]); + 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.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.name("PRCTL formula filter"); + + start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment) > qi::eoi; + start.name("PRCTL formula filter"); } - qi::rule*(), Skipper> start; + qi::rule*(), Skipper> start; + qi::rule*(), Skipper> filter; + + qi::rule*(), Skipper> abstractAction; + qi::rule*(), Skipper> rangeAction; + qi::rule*(), Skipper> minMaxAction; + qi::rule*(), Skipper> formula; qi::rule*(), Skipper> comment; @@ -168,10 +166,6 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> probabilisticBoundOperator; qi::rule*(), Skipper> rewardBoundOperator; - qi::rule*(), Skipper> noBoundOperator; - qi::rule*(), Skipper> probabilisticNoBoundOperator; - qi::rule*(), Skipper> rewardNoBoundOperator; - qi::rule*(), Skipper> pathFormula; qi::rule*(), Skipper> boundedEventually; qi::rule*(), Skipper> eventually;