From ffc9eda1c270e8847b14302041e2de9e1dec8c2c Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 26 Aug 2015 18:24:22 +0200 Subject: [PATCH] enabled terminal states for explicit model builder Former-commit-id: f0304e64d2eed0ea5a9108a01bdd13bfe317235d --- src/builder/ExplicitPrismModelBuilder.cpp | 64 +++- src/builder/ExplicitPrismModelBuilder.h | 17 +- src/cli/cli.cpp | 2 +- src/parser/ExpressionParser.cpp | 36 +-- src/parser/ExpressionParser.h | 5 +- src/parser/FormulaParser.cpp | 354 ++++++++++++++++------ src/parser/FormulaParser.h | 164 ++-------- 7 files changed, 381 insertions(+), 261 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index f4efe7195..fcffe1344 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -106,17 +106,17 @@ namespace storm { } template - ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() { + ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()) { + ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates() { this->preserveFormula(formula); } template - ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() { + ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; @@ -124,6 +124,33 @@ namespace storm { for (auto const& formula : formulas) { this->preserveFormula(*formula); } + if (formulas.size() == 1) { + this->setTerminalStatesFromFormula(*formulas.front()); + } + } + } + + template + void ExplicitPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + if (formula.isAtomicExpressionFormula()) { + terminalStates = formula.asAtomicExpressionFormula().getExpression(); + } else if (formula.isAtomicLabelFormula()) { + terminalStates = formula.asAtomicLabelFormula().getLabel(); + } else if (formula.isEventuallyFormula()) { + storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); + if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } else if (formula.isUntilFormula()) { + storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(right); + } + } else if (formula.isProbabilityOperatorFormula()) { + storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula() || sub.isUntilFormula()) { + this->setTerminalStatesFromFormula(sub); + } } } @@ -152,6 +179,9 @@ namespace storm { // Extract all the expressions used in the formula. std::vector> atomicExpressionFormulas = formula.getAtomicExpressionFormulas(); for (auto const& formula : atomicExpressionFormulas) { + if (!expressionLabels) { + expressionLabels = std::vector(); + } expressionLabels.get().push_back(formula.get()->getExpression()); } } @@ -528,7 +558,7 @@ namespace storm { } template - boost::optional>> ExplicitPrismModelBuilder::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders) { + boost::optional>> ExplicitPrismModelBuilder::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression) { // Create choice labels, if requested, boost::optional>> choiceLabels; if (commandLabels) { @@ -579,9 +609,16 @@ namespace storm { STORM_LOG_TRACE("Exploring state with id " << stateIndex << "."); unpackStateIntoEvaluator(currentState, variableInformation, evaluator); - // Retrieve all choices for the current state. - std::vector> allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator); - std::vector> allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator); + // If a terminal expression was given, we check whether the current state needs to be explored further. + std::vector> allUnlabeledChoices; + std::vector> allLabeledChoices; + if (terminalExpression && evaluator.asBool(terminalExpression.get())) { + // Nothing to do in this case. + } else { + // Retrieve all choices for the current state. + allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator); + allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator); + } uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size(); @@ -890,7 +927,18 @@ namespace storm { rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards()); } - modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders); + // If we were asked to treat some states as terminal states, we cut away their transitions now. + boost::optional terminalExpression; + if (options.terminalStates) { + if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { + terminalExpression = boost::get(options.terminalStates.get()); + } else { + std::string const& labelName = boost::get(options.terminalStates.get()); + terminalExpression = program.getLabelExpression(labelName); + } + } + + modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression); modelComponents.transitionMatrix = transitionMatrixBuilder.build(); diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index 5fa7e363c..313b1652c 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -162,6 +162,16 @@ namespace storm { */ void preserveFormula(storm::logic::Formula const& formula); + /*! + * Analyzes the given formula and sets an expression for the states states of the model that can be + * treated as terminal states. Note that this may interfere with checking properties different than the + * one provided. + * + * @param formula The formula used to (possibly) derive an expression for the terminal states of the + * model. + */ + void setTerminalStatesFromFormula(storm::logic::Formula const& formula); + // A flag that indicates whether or not command labels are to be built. bool buildCommandLabels; @@ -182,6 +192,10 @@ namespace storm { // An optional set of expressions for which labels need to be built. boost::optional> expressionLabels; + + // An optional expression or label that characterizes the terminal states of the model. If this is set, + // the outgoing transitions of these states are replaced with a self-loop. + boost::optional> terminalStates; }; /*! @@ -267,10 +281,11 @@ namespace storm { * function. * @param rewardModelBuilders A vector of reward model builders that is used to build the vector of selected * reward models. + * @param terminalExpression If given, terminal states are not explored further. * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin * and a vector containing the labels associated with each choice. */ - static boost::optional>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders); + static boost::optional>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); /*! * Explores the state space of the given program and returns the components of the model as a result. diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 7a9ea6f3c..cfc88468b 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -224,7 +224,7 @@ namespace storm { if (settings.isPropertySet()) { storm::parser::FormulaParser formulaParser; if (program) { - storm::parser::FormulaParser formulaParser = storm::parser::FormulaParser(program.get().getManager().getSharedPointer()); + formulaParser = storm::parser::FormulaParser(program.get().getManager().getSharedPointer()); } // If the given property looks like a file (containing a dot and there exists a file with that name), diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 5a933a998..c67f808e0 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -5,7 +5,7 @@ namespace storm { namespace parser { - ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { + ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); @@ -144,7 +144,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const { @@ -159,7 +159,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const { @@ -173,7 +173,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const { @@ -190,7 +190,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const { @@ -205,7 +205,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const { @@ -220,7 +220,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const { @@ -235,7 +235,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const { @@ -249,7 +249,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1) const { @@ -268,7 +268,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const { @@ -278,17 +278,17 @@ namespace storm { } if (this->createExpressions) { - return manager.rational(value); + return manager->rational(value); } else { - return manager.boolean(false); + return manager->boolean(false); } } storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value) const { if (this->createExpressions) { - return manager.integer(value); + return manager->integer(value); } else { - return manager.boolean(false); + return manager->boolean(false); } } @@ -304,7 +304,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1) const { @@ -319,7 +319,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return manager.boolean(false); + return manager->boolean(false); } storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const { @@ -329,14 +329,14 @@ namespace storm { if (expression == nullptr) { if (allowBacktracking) { pass = false; - return manager.boolean(false); + return manager->boolean(false); } else { STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'."); } } return *expression; } else { - return manager.boolean(false); + return manager->boolean(false); } } diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 55df73e2a..19c129b4a 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -27,6 +27,9 @@ namespace storm { */ ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking = false); + ExpressionParser(ExpressionParser const& other) = default; + ExpressionParser& operator=(ExpressionParser const& other) = default; + /*! * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to * expressions will be substituted wherever the key value appears in the parsed expression. After setting @@ -172,7 +175,7 @@ namespace storm { trueFalseOperatorStruct trueFalse_; // The manager responsible for the expressions. - storm::expressions::ExpressionManager const& manager; + std::shared_ptr manager; // A flag that indicates whether expressions should actually be generated or just a syntax check shall be // performed. diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 5acbba56c..3aa9820d1 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -8,7 +8,238 @@ namespace storm { namespace parser { - FormulaParser::FormulaParser(std::shared_ptr const& manager) : FormulaParser::base_type(start), expressionParser(*manager, keywords_, true) { + class FormulaParserGrammar : public qi::grammar>(), Skipper> { + public: + FormulaParserGrammar(std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); + + FormulaParserGrammar(FormulaParserGrammar const& other) = default; + FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = default; + + /*! + * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used + * to substitute special identifiers in the formula by expressions. + * + * @param identifier The identifier that is supposed to be substituted. + * @param expression The expression it is to be substituted with. + */ + void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression); + + private: + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("true", 1) + ("false", 2) + ("min", 3) + ("max", 4) + ("F", 5) + ("G", 6) + ("X", 7); + } + }; + + // A parser used for recognizing the keywords. + keywordsStruct keywords_; + + struct relationalOperatorStruct : qi::symbols { + relationalOperatorStruct() { + add + (">=", storm::logic::ComparisonType::GreaterEqual) + (">", storm::logic::ComparisonType::Greater) + ("<=", storm::logic::ComparisonType::LessEqual) + ("<", storm::logic::ComparisonType::Less); + } + }; + + // A parser used for recognizing the operators at the "relational" precedence level. + relationalOperatorStruct relationalOperator_; + + struct binaryBooleanOperatorStruct : qi::symbols { + binaryBooleanOperatorStruct() { + add + ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And) + ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or); + } + }; + + // A parser used for recognizing the operators at the "binary" precedence level. + binaryBooleanOperatorStruct binaryBooleanOperator_; + + struct unaryBooleanOperatorStruct : qi::symbols { + unaryBooleanOperatorStruct() { + add + ("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not); + } + }; + + // A parser used for recognizing the operators at the "unary" precedence level. + unaryBooleanOperatorStruct unaryBooleanOperator_; + + struct optimalityOperatorStruct : qi::symbols { + optimalityOperatorStruct() { + add + ("min", storm::logic::OptimalityType::Minimize) + ("max", storm::logic::OptimalityType::Maximize); + } + }; + + // A parser used for recognizing the optimality operators. + optimalityOperatorStruct optimalityOperator_; + + // Parser and manager used for recognizing expressions. + storm::parser::ExpressionParser expressionParser; + + // Functor used for displaying error information. + struct ErrorHandler { + typedef qi::error_handler_result result_type; + + template + qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { + std::stringstream whatAsString; + whatAsString << what; + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << whatAsString.str() << "."); + return qi::fail; + } + }; + + // An error handler function. + phoenix::function handler; + + // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions + // they are to be replaced with. + qi::symbols identifiers_; + + qi::rule>(), Skipper> start; + + qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule(), Skipper> probabilityOperator; + qi::rule(), Skipper> rewardOperator; + qi::rule(), Skipper> expectedTimeOperator; + qi::rule(), Skipper> steadyStateOperator; + + qi::rule(), Skipper> simpleFormula; + qi::rule(), Skipper> stateFormula; + qi::rule(), Skipper> pathFormula; + qi::rule(), Skipper> pathFormulaWithoutUntil; + qi::rule(), Skipper> simplePathFormula; + qi::rule(), Skipper> atomicStateFormula; + qi::rule(), Skipper> operatorFormula; + qi::rule label; + qi::rule rewardModelName; + + qi::rule(), Skipper> andStateFormula; + qi::rule(), Skipper> orStateFormula; + qi::rule(), Skipper> notStateFormula; + qi::rule(), Skipper> labelFormula; + qi::rule(), Skipper> expressionFormula; + qi::rule(), qi::locals, Skipper> booleanLiteralFormula; + + qi::rule(), Skipper> conditionalFormula; + qi::rule(), Skipper> eventuallyFormula; + qi::rule(), Skipper> nextFormula; + qi::rule(), Skipper> globallyFormula; + qi::rule(), Skipper> untilFormula; + qi::rule, uint_fast64_t>(), Skipper> timeBound; + + qi::rule(), Skipper> rewardPathFormula; + qi::rule(), Skipper> cumulativeRewardFormula; + qi::rule(), Skipper> reachabilityRewardFormula; + qi::rule(), Skipper> instantaneousRewardFormula; + + // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). + boost::spirit::qi::real_parser> strict_double; + + // Methods that actually create the expression objects. + std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; + std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; + std::shared_ptr createBooleanLiteralFormula(bool literal) const; + std::shared_ptr createAtomicLabelFormula(std::string const& label) const; + std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const; + std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; + std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); + std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); + std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); + }; + + FormulaParser::FormulaParser(std::shared_ptr const& manager) : manager(manager->getSharedPointer()), grammar(new FormulaParserGrammar(manager)) { + // Intentionally left empty. + } + + FormulaParser::FormulaParser(FormulaParser const& other) : FormulaParser(other.manager) { + other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); }); + } + + FormulaParser& FormulaParser::operator=(FormulaParser const& other) { + this->manager = other.manager; + this->grammar = std::shared_ptr(new FormulaParserGrammar(this->manager)); + other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); }); + return *this; + } + + std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) { + std::vector> formulas = parseFromString(formulaString); + STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead."); + return formulas.front(); + } + + std::vector> FormulaParser::parseFromFile(std::string const& filename) { + // Open file and initialize result. + std::ifstream inputFileStream(filename, std::ios::in); + STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); + + std::vector> formulas; + + // Now try to parse the contents of the file. + try { + std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); + formulas = parseFromString(fileContent); + } catch(std::exception& e) { + // In case of an exception properly close the file before passing exception. + inputFileStream.close(); + throw e; + } + + // Close the stream in case everything went smoothly and return result. + inputFileStream.close(); + return formulas; + } + + std::vector> FormulaParser::parseFromString(std::string const& formulaString) { + PositionIteratorType first(formulaString.begin()); + PositionIteratorType iter = first; + PositionIteratorType last(formulaString.end()); + + // Create empty result; + std::vector> result; + + // Create grammar. + try { + // Start parsing. + bool succeeded = qi::phrase_parse(iter, last, *grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); + STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse formula."); + STORM_LOG_DEBUG("Parsed formula successfully."); + } catch (qi::expectation_failure const& e) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); + } + + return result; + } + + void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { + // Record the mapping and hand it over to the grammar. + this->identifiers_.add(identifier, expression); + grammar->addIdentifierExpression(identifier, expression); + } + + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), expressionParser(*manager, keywords_, true) { // Register all variables so we can parse them in the expressions. for (auto variableTypePair : *manager) { identifiers_.add(variableTypePair.first.getName(), variableTypePair.first); @@ -16,28 +247,28 @@ namespace storm { // Set the identifier mapping to actually generate expressions. expressionParser.setIdentifierMapping(&identifiers_); - instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; + instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; instantaneousRewardFormula.name("instantaneous reward formula"); - cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParser::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; + cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; cumulativeRewardFormula.name("cumulative reward formula"); - reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParser::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)]; + reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)]; reachabilityRewardFormula.name("reachability reward formula"); rewardPathFormula = reachabilityRewardFormula | cumulativeRewardFormula | instantaneousRewardFormula; rewardPathFormula.name("reward path formula"); - expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParser::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; + expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; expressionFormula.name("expression formula"); label = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]]; label.name("label"); - labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParser::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)]; + labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)]; labelFormula.name("label formula"); - booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParser::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; + booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; booleanLiteralFormula.name("boolean literal formula"); operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator; @@ -46,25 +277,25 @@ namespace storm { atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; atomicStateFormula.name("atomic state formula"); - notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; + notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; notStateFormula.name("negation formula"); - eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_2)]; eventuallyFormula.name("eventually formula"); - globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createGloballyFormula, phoenix::ref(*this), qi::_1)]; + globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; globallyFormula.name("globally formula"); - nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createNextFormula, phoenix::ref(*this), qi::_1)]; + nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; nextFormula.name("next formula"); pathFormulaWithoutUntil = eventuallyFormula | globallyFormula | nextFormula | stateFormula; pathFormulaWithoutUntil.name("path formula"); - untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; + untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; untilFormula.name("until formula"); - conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParser::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1)]; + conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1)]; conditionalFormula.name("conditional formula"); timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1]; @@ -76,25 +307,25 @@ namespace storm { operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct, boost::optional, boost::optional>>(qi::_a, qi::_b, qi::_c)]; operatorInformation.name("operator information"); - steadyStateOperator = (qi::lit("LRA") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + steadyStateOperator = (qi::lit("LRA") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; steadyStateOperator.name("long-run average operator"); rewardModelName = qi::lit("{\"") > label > qi::lit("\"}"); rewardModelName.name("reward model name"); - rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; + rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; rewardOperator.name("reward operator"); - expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; expectedTimeOperator.name("expected time operator"); - probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; probabilityOperator.name("probability operator"); - andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; + andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; andStateFormula.name("and state formula"); - orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; + orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; orStateFormula.name("or state formula"); stateFormula = (orStateFormula); @@ -154,60 +385,11 @@ namespace storm { qi::on_error(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } - void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { + void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { this->identifiers_.add(identifier, expression); } - std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) { - std::vector> formulas = parseFromString(formulaString); - STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead."); - return formulas.front(); - } - - std::vector> FormulaParser::parseFromFile(std::string const& filename) { - // Open file and initialize result. - std::ifstream inputFileStream(filename, std::ios::in); - STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); - - std::vector> formulas; - - // Now try to parse the contents of the file. - try { - std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); - formulas = parseFromString(fileContent); - } catch(std::exception& e) { - // In case of an exception properly close the file before passing exception. - inputFileStream.close(); - throw e; - } - - // Close the stream in case everything went smoothly and return result. - inputFileStream.close(); - return formulas; - } - - std::vector> FormulaParser::parseFromString(std::string const& formulaString) { - PositionIteratorType first(formulaString.begin()); - PositionIteratorType iter = first; - PositionIteratorType last(formulaString.end()); - - // Create empty result; - std::vector> result; - - // Create grammar. - try { - // Start parsing. - bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); - STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse formula."); - STORM_LOG_DEBUG("Parsed formula successfully."); - } catch (qi::expectation_failure const& e) { - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); - } - - return result; - } - - std::shared_ptr FormulaParser::createInstantaneousRewardFormula(boost::variant const& timeBound) const { + std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { if (timeBound.which() == 0) { return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); } else { @@ -217,7 +399,7 @@ namespace storm { } } - std::shared_ptr FormulaParser::createCumulativeRewardFormula(boost::variant const& timeBound) const { + std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(boost::variant const& timeBound) const { if (timeBound.which() == 0) { return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); } else { @@ -227,24 +409,24 @@ namespace storm { } } - std::shared_ptr FormulaParser::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { + std::shared_ptr FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { return std::shared_ptr(new storm::logic::ReachabilityRewardFormula(stateFormula)); } - std::shared_ptr FormulaParser::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { + std::shared_ptr FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type."); return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); } - std::shared_ptr FormulaParser::createBooleanLiteralFormula(bool literal) const { + std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); } - std::shared_ptr FormulaParser::createAtomicLabelFormula(std::string const& label) const { + std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParser::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const { if (timeBound) { if (timeBound.get().which() == 0) { std::pair const& bounds = boost::get>(timeBound.get()); @@ -257,15 +439,15 @@ namespace storm { } } - std::shared_ptr FormulaParser::createGloballyFormula(std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); } - std::shared_ptr FormulaParser::createNextFormula(std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParser::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { if (timeBound.get().which() == 0) { std::pair const& bounds = boost::get>(timeBound.get()); @@ -278,31 +460,31 @@ namespace storm { } } - std::shared_ptr FormulaParser::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const { + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const { return std::shared_ptr(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParser::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParser::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParser::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParser::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) { return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula)); } - std::shared_ptr FormulaParser::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { + std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); } - std::shared_ptr FormulaParser::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { + std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { if (operatorType) { return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); } else { diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index ad8ea8459..895d84cd5 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -1,5 +1,5 @@ -#ifndef STORM_PARSER_PRCTLPARSER_H_ -#define STORM_PARSER_PRCTLPARSER_H_ +#ifndef STORM_PARSER_FORMULAPARSER_H_ +#define STORM_PARSER_FORMULAPARSER_H_ #include @@ -12,9 +12,15 @@ namespace storm { namespace parser { - class FormulaParser : public qi::grammar>(), Skipper> { + // Forward-declare grammar. + class FormulaParserGrammar; + + class FormulaParser { public: FormulaParser(std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); + + FormulaParser(FormulaParser const& other); + FormulaParser& operator=(FormulaParser const& other); /*! * Parses the formula given by the provided string. @@ -23,7 +29,7 @@ namespace storm { * @return The resulting formula. */ std::shared_ptr parseSingleFormulaFromString(std::string const& formulaString); - + /*! * Parses the formula given by the provided string. * @@ -31,7 +37,7 @@ namespace storm { * @return The contained formulas. */ std::vector> parseFromString(std::string const& formulaString); - + /*! * Parses the formulas in the given file. * @@ -50,151 +56,17 @@ namespace storm { void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression); private: - struct keywordsStruct : qi::symbols { - keywordsStruct() { - add - ("true", 1) - ("false", 2) - ("min", 3) - ("max", 4) - ("F", 5) - ("G", 6) - ("X", 7); - } - }; - - // A parser used for recognizing the keywords. - keywordsStruct keywords_; - - struct relationalOperatorStruct : qi::symbols { - relationalOperatorStruct() { - add - (">=", storm::logic::ComparisonType::GreaterEqual) - (">", storm::logic::ComparisonType::Greater) - ("<=", storm::logic::ComparisonType::LessEqual) - ("<", storm::logic::ComparisonType::Less); - } - }; - - // A parser used for recognizing the operators at the "relational" precedence level. - relationalOperatorStruct relationalOperator_; - - struct binaryBooleanOperatorStruct : qi::symbols { - binaryBooleanOperatorStruct() { - add - ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And) - ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or); - } - }; - - // A parser used for recognizing the operators at the "binary" precedence level. - binaryBooleanOperatorStruct binaryBooleanOperator_; - - struct unaryBooleanOperatorStruct : qi::symbols { - unaryBooleanOperatorStruct() { - add - ("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not); - } - }; - - // A parser used for recognizing the operators at the "unary" precedence level. - unaryBooleanOperatorStruct unaryBooleanOperator_; - - struct optimalityOperatorStruct : qi::symbols { - optimalityOperatorStruct() { - add - ("min", storm::logic::OptimalityType::Minimize) - ("max", storm::logic::OptimalityType::Maximize); - } - }; + // The manager used to parse expressions. + std::shared_ptr manager; - // A parser used for recognizing the optimality operators. - optimalityOperatorStruct optimalityOperator_; - - // Parser and manager used for recognizing expressions. - storm::parser::ExpressionParser expressionParser; - - // Functor used for displaying error information. - struct ErrorHandler { - typedef qi::error_handler_result result_type; - - template - qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { - std::stringstream whatAsString; - whatAsString << what; - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << whatAsString.str() << "."); - return qi::fail; - } - }; - - // An error handler function. - phoenix::function handler; - - // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions - // they are to be replaced with. + // Keep track of added identifier expressions. qi::symbols identifiers_; - qi::rule>(), Skipper> start; - - qi::rule, boost::optional, boost::optional>(), qi::locals, boost::optional, boost::optional>, Skipper> operatorInformation; - qi::rule(), Skipper> probabilityOperator; - qi::rule(), Skipper> rewardOperator; - qi::rule(), Skipper> expectedTimeOperator; - qi::rule(), Skipper> steadyStateOperator; - - qi::rule(), Skipper> simpleFormula; - qi::rule(), Skipper> stateFormula; - qi::rule(), Skipper> pathFormula; - qi::rule(), Skipper> pathFormulaWithoutUntil; - qi::rule(), Skipper> simplePathFormula; - qi::rule(), Skipper> atomicStateFormula; - qi::rule(), Skipper> operatorFormula; - qi::rule label; - qi::rule rewardModelName; - - qi::rule(), Skipper> andStateFormula; - qi::rule(), Skipper> orStateFormula; - qi::rule(), Skipper> notStateFormula; - qi::rule(), Skipper> labelFormula; - qi::rule(), Skipper> expressionFormula; - qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - - qi::rule(), Skipper> conditionalFormula; - qi::rule(), Skipper> eventuallyFormula; - qi::rule(), Skipper> nextFormula; - qi::rule(), Skipper> globallyFormula; - qi::rule(), Skipper> untilFormula; - qi::rule, uint_fast64_t>(), Skipper> timeBound; - - qi::rule(), Skipper> rewardPathFormula; - qi::rule(), Skipper> cumulativeRewardFormula; - qi::rule(), Skipper> reachabilityRewardFormula; - qi::rule(), Skipper> instantaneousRewardFormula; - - // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). - boost::spirit::qi::real_parser> strict_double; - - // Methods that actually create the expression objects. - std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; - std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; - std::shared_ptr createBooleanLiteralFormula(bool literal) const; - std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& subformula) const; - std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); - std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula) const; - std::shared_ptr createLongRunAverageOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createExpectedTimeOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> const& operatorInformation, std::shared_ptr const& subformula); - std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); - std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); + // The grammar used to parse the input. + std::shared_ptr grammar; }; - + } // namespace parser } // namespace storm -#endif /* STORM_PARSER_PRCTLPARSER_H_ */ +#endif /* STORM_PARSER_FORMULAPARSER_H_ */