From 7ec3e8b21463180b056ff2755f179bb617d920f1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 5 Jan 2015 23:44:26 +0100 Subject: [PATCH] Further fixes for new variable handling. libstorm now compiles again, yay. Former-commit-id: a9ac5c03560418646958457cd9ee7488c03368d8 --- src/parser/ExpressionParser.cpp | 34 +++---- src/parser/ExpressionParser.h | 14 ++- src/parser/PrismParser.cpp | 134 ++++++++++++++++++++------- src/parser/PrismParser.h | 6 +- src/solver/Z3SmtSolver.cpp | 6 +- src/storage/dd/CuddDd.cpp | 8 +- src/storage/expressions/Variable.cpp | 4 + src/storage/expressions/Variable.h | 16 ++-- src/storage/prism/Module.cpp | 2 +- src/storage/prism/Module.h | 4 +- src/storage/prism/Program.cpp | 27 +----- src/storage/prism/RewardModel.cpp | 2 +- src/storage/prism/RewardModel.h | 4 +- 13 files changed, 159 insertions(+), 102 deletions(-) diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 052f4470c..19ff25040 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -5,7 +5,7 @@ namespace storm { namespace parser { - ExpressionParser::ExpressionParser(qi::symbols const& invalidIdentifiers_) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { + ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols const& invalidIdentifiers_) : 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_) { 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"); @@ -98,7 +98,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + 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 { @@ -113,7 +113,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + 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 { @@ -127,7 +127,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + 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 { @@ -144,7 +144,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + 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 { @@ -159,7 +159,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + 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 { @@ -174,7 +174,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + 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 { @@ -189,7 +189,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + 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 { @@ -203,7 +203,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + return manager.boolean(false); } storm::expressions::Expression ExpressionParser::createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1) const { @@ -222,7 +222,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + return manager.boolean(false); } storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const { @@ -232,17 +232,17 @@ namespace storm { } if (this->createExpressions) { - return storm::expressions::Expression::createDoubleLiteral(value); + return manager.rational(value); } else { - return storm::expressions::Expression::createFalse(); + return manager.boolean(false); } } storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value) const { if (this->createExpressions) { - return storm::expressions::Expression::createIntegerLiteral(static_cast(value)); + return manager.integer(value); } else { - return storm::expressions::Expression::createFalse(); + return manager.boolean(false); } } @@ -258,7 +258,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + return manager.boolean(false); } storm::expressions::Expression ExpressionParser::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1) const { @@ -273,7 +273,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); } } - return storm::expressions::Expression::createFalse(); + return manager.boolean(false); } storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const { @@ -283,7 +283,7 @@ namespace storm { STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'."); return *expression; } else { - return storm::expressions::Expression::createFalse(); + return manager.boolean(false); } } diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 80721dfb2..bff79fc14 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -19,16 +19,17 @@ namespace storm { * generate the actual expressions, a mapping of valid identifiers to their expressions need to be provided * later. * + * @param manager The manager responsible for the expressions. * @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected. */ - ExpressionParser(qi::symbols const& invalidIdentifiers_); + ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols const& invalidIdentifiers_); /*! * 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 * this, the parser will generate expressions. * - * @param identifiers A pointer to a mapping from identifiers to expressions. + * @param identifiers_ A pointer to a mapping from identifiers to expressions. */ void setIdentifierMapping(qi::symbols const* identifiers_); @@ -157,16 +158,19 @@ namespace storm { minMaxOperatorStruct minMaxOperator_; struct trueFalseOperatorStruct : qi::symbols { - trueFalseOperatorStruct() { + trueFalseOperatorStruct(storm::expressions::ExpressionManager& manager) { add - ("true", storm::expressions::Expression::createTrue()) - ("false", storm::expressions::Expression::createFalse()); + ("true", manager.boolean(true)) + ("false", manager.boolean(false)); } }; // A parser used for recognizing the literals true and false. trueFalseOperatorStruct trueFalse_; + // The manager responsible for the expressions. + storm::expressions::ExpressionManager& manager; + // A flag that indicates whether expressions should actually be generated or just a syntax check shall be // performed. bool createExpressions; diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index b327b0984..4a34af248 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -61,7 +61,7 @@ namespace storm { return result; } - PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), expressionParser(keywords_) { + PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(*manager, keywords_) { // Parse simple identifier. identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); @@ -96,7 +96,7 @@ namespace storm { formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)]; formulaDefinition.name("formula definition"); - booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)]; + booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)]; booleanVariableDefinition.name("boolean variable definition"); integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser[qi::_a = qi::_1] > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; @@ -133,7 +133,7 @@ namespace storm { assignmentDefinitionList %= +assignmentDefinition % "&"; assignmentDefinitionList.name("assignment list"); - updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; + updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; updateDefinition.name("update"); updateListDefinition %= +updateDefinition(qi::_r1) % "+"; @@ -224,50 +224,98 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { if (!this->secondRun) { - STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant)); + try { + storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType()); + this->identifiers_.add(newConstant, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(newConstant)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'."); + } + } } - return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename()); + return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); } storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const { if (!this->secondRun) { - STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant)); + try { + storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType()); + this->identifiers_.add(newConstant, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(newConstant)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'."); + } + } } - return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename()); + return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); } storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const { if (!this->secondRun) { - STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant)); + try { + storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getRationalType()); + this->identifiers_.add(newConstant, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(newConstant)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'."); + } + } } - return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename()); + return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); } storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { - STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant)); + try { + storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType()); + this->identifiers_.add(newConstant, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(newConstant)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'."); + } + } } - return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename()); + return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { - STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant)); + try { + storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType()); + this->identifiers_.add(newConstant, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(newConstant)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'."); + } + } } - return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename()); + return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { - STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); - this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant)); + try { + storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType()); + this->identifiers_.add(newConstant, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(newConstant)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'."); + } + } } - return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename()); + return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); } storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) { @@ -312,18 +360,34 @@ namespace storm { storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const { if (!this->secondRun) { - STORM_LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'."); - this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName)); + try { + storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getBooleanType()); + this->identifiers_.add(variableName, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(variableName)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'."); + } + } } - return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename()); + return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, this->getFilename()); } storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const { if (!this->secondRun) { - STORM_LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'."); - this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName)); + try { + storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getIntegerType()); + this->identifiers_.add(variableName, newVariable.getExpression()); + } catch (storm::exceptions::InvalidArgumentException const& e) { + if (manager->hasVariable(variableName)) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'."); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'."); + } + } } - return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename()); + return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename()); } storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const { @@ -342,12 +406,14 @@ namespace storm { for (auto const& variable : moduleToRename.getBooleanVariables()) { auto const& renamingPair = renaming.find(variable.getName()); STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed."); - this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second)); + storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType()); + this->identifiers_.add(renamingPair->first, renamedVariable.getExpression()); } for (auto const& variable : moduleToRename.getIntegerVariables()) { auto const& renamingPair = renaming.find(variable.getName()); STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed."); - this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second)); + storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType()); + this->identifiers_.add(renamingPair->first, renamedVariable.getExpression()); } // Return a dummy module in the first pass. @@ -357,12 +423,12 @@ namespace storm { globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size(); // Create a mapping from identifiers to the expressions they need to be replaced with. - std::map expressionRenaming; + std::map expressionRenaming; for (auto const& namePair : renaming) { storm::expressions::Expression const* substitutedExpression = this->identifiers_.find(namePair.second); // If the mapped-to-value is an expression, we need to replace it. if (substitutedExpression != nullptr) { - expressionRenaming.emplace(namePair.first, *substitutedExpression); + expressionRenaming.emplace(manager->getVariable(namePair.first), *substitutedExpression); } } @@ -372,7 +438,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed."); - booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); } // Rename the integer variables. @@ -381,7 +447,7 @@ namespace storm { auto const& renamingPair = renaming.find(variable.getName()); STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed."); - integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); } // Rename commands. @@ -417,7 +483,7 @@ namespace storm { } storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const { - return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun); + return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun); } } // namespace parser } // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 2f6b13251..38e31a568 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -9,6 +9,7 @@ #include "src/parser/SpiritParserDefinitions.h" #include "src/parser/ExpressionParser.h" #include "src/storage/prism/Program.h" +#include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expressions.h" #include "src/utility/macros.h" @@ -20,7 +21,7 @@ namespace storm { class GlobalProgramInformation { public: // Default construct the header information. - GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(),hasInitialConstruct(false), initialConstruct(storm::expressions::Expression::createFalse()), currentCommandIndex(0), currentUpdateIndex(0) { + GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), currentCommandIndex(0), currentUpdateIndex(0) { // Intentionally left empty. } @@ -212,7 +213,8 @@ namespace storm { storm::parser::PrismParser::modelTypeStruct modelType_; qi::symbols identifiers_; - // Parser used for recognizing expressions. + // Parser and manager used for recognizing expressions. + std::shared_ptr manager; storm::parser::ExpressionParser expressionParser; // Helper methods used in the grammar. diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 6527ed348..0ee80e469 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -201,7 +201,7 @@ namespace storm { #ifdef STORM_HAVE_Z3 storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) { - storm::expressions::SimpleValuation stormModel(this->getManager()); + storm::expressions::SimpleValuation stormModel(this->getManager().getSharedPointer()); for (unsigned i = 0; i < model.num_consts(); ++i) { z3::func_decl variableI = model.get_const_decl(i); @@ -252,7 +252,7 @@ namespace storm { z3::model model = this->solver->get_model(); z3::expr modelExpr = this->context->bool_val(true); - storm::expressions::SimpleValuation valuation(this->getManager()); + storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer()); for (storm::expressions::Variable const& importantAtom : important) { z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression()); @@ -294,7 +294,7 @@ namespace storm { z3::model model = this->solver->get_model(); z3::expr modelExpr = this->context->bool_val(true); - storm::expressions::SimpleValuation valuation(this->getManager()); + storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer()); for (storm::expressions::Variable const& importantAtom : important) { z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression()); diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index bbd886f9f..6e474bebf 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -303,10 +303,10 @@ namespace storm { } } - std::set unionOfMetaVariableNames; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin())); - std::set containedMetaVariableNames; - std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin())); + std::set unionOfMetaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); + std::set containedMetaVariables; + std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); return Dd(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables); } diff --git a/src/storage/expressions/Variable.cpp b/src/storage/expressions/Variable.cpp index 492a6ae32..1608c8b56 100644 --- a/src/storage/expressions/Variable.cpp +++ b/src/storage/expressions/Variable.cpp @@ -11,6 +11,10 @@ namespace storm { return manager == other.manager && index == other.index; } + bool Variable::operator<(Variable const& other) const { + return this->getIndex() < other.getIndex(); + } + storm::expressions::Expression Variable::getExpression() const { return storm::expressions::Expression(*this); } diff --git a/src/storage/expressions/Variable.h b/src/storage/expressions/Variable.h index 8bb7e0ce8..fd9796658 100644 --- a/src/storage/expressions/Variable.h +++ b/src/storage/expressions/Variable.h @@ -40,6 +40,14 @@ namespace storm { * @return True iff the two variables are the same. */ bool operator==(Variable const& other) const; + + /*! + * Checks whether the variable appears earlier in the total ordering of variables. + * + * @param other The variable to compare with. + * @return True iff the first variable appears earlier than the given one. + */ + bool operator<(Variable const& other) const; /*! * Retrieves the name of the variable. @@ -129,14 +137,6 @@ namespace std { return std::hash()(variable.getIndex()); } }; - - // Provide a less operator, so we can put variables in ordered collections. - template <> - struct less { - std::size_t operator()(storm::expressions::Variable const& variable1, storm::expressions::Variable const& variable2) const { - return variable1.getIndex() < variable2.getIndex(); - } - }; } #endif /* STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ */ \ No newline at end of file diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 327ffbcc3..2233ababa 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -146,7 +146,7 @@ namespace storm { return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands); } - Module Module::substitute(std::map const& substitution) const { + Module Module::substitute(std::map const& substitution) const { std::vector newBooleanVariables; newBooleanVariables.reserve(this->getNumberOfBooleanVariables()); for (auto const& booleanVariable : this->getBooleanVariables()) { diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index 1031cbf27..9fe981340 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -189,12 +189,12 @@ namespace storm { Module restrictCommands(boost::container::flat_set const& indexSet) const; /*! - * Substitutes all identifiers in the module according to the given map. + * Substitutes all variables in the module according to the given map. * * @param substitution The substitution to perform. * @return The resulting module. */ - Module substitute(std::map const& substitution) const; + Module substitute(std::map const& substitution) const; friend std::ostream& operator<<(std::ostream& stream, Module const& module); diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 203e25e75..a405d601b 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -255,7 +255,7 @@ namespace storm { STORM_LOG_THROW(constantDefinitions.find(constant.getExpressionVariable()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'."); // Now replace the occurrences of undefined constants in its defining expression. - newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber()); + newConstants.emplace_back(constant.getExpressionVariable(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber()); } else { auto const& variableExpressionPair = constantDefinitions.find(constant.getExpressionVariable()); @@ -344,9 +344,6 @@ namespace storm { } void Program::checkValidity() const { - // We need to construct a mapping from identifiers to their types, so we can type-check the expressions later. - std::map identifierToTypeMap; - // Start by checking the constant declarations. std::set allIdentifiers; std::set globalIdentifiers; @@ -362,9 +359,6 @@ namespace storm { STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers."); } - // Finally, register the type of the constant for later type checks. - identifierToTypeMap.emplace(constant.getName(), constant.getType()); - // Record the new identifier for future checks. constantNames.insert(constant.getName()); allIdentifiers.insert(constant.getName()); @@ -382,9 +376,6 @@ namespace storm { bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); - // Register the type of the constant for later type checks. - identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool); - // Record the new identifier for future checks. variableNames.insert(variable.getName()); allIdentifiers.insert(variable.getName()); @@ -408,9 +399,6 @@ namespace storm { isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); - // Register the type of the constant for later type checks. - identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int); - // Record the new identifier for future checks. variableNames.insert(variable.getName()); allIdentifiers.insert(variable.getName()); @@ -428,9 +416,6 @@ namespace storm { bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants."); - // Register the type of the constant for later type checks. - identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool); - // Record the new identifier for future checks. variableNames.insert(variable.getName()); allIdentifiers.insert(variable.getName()); @@ -439,9 +424,6 @@ namespace storm { // Check for duplicate identifiers. STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'."); - // Register the type of the constant for later type checks. - identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int); - // Check that bound expressions of the range. std::set containedIdentifiers = variable.getLowerBoundExpression().getVariables(); bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end()); @@ -500,8 +482,7 @@ namespace storm { } } STORM_LOG_THROW(alreadyAssignedIdentifiers.find(assignment.getVariableName()) == alreadyAssignedIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'."); - auto variableTypePair = identifierToTypeMap.find(assignment.getVariableName()); - STORM_LOG_THROW(variableTypePair->second == assignment.getExpression().getReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getReturnType() << "' to variable '" << variableTypePair->first << "' of type '" << variableTypePair->second << "'."); + STORM_LOG_THROW(manager->getVariable(assignment.getVariableName()).getType() == assignment.getExpression().getType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << manager->getVariable(assignment.getVariableName()).getType() << "'."); containedIdentifiers = assignment.getExpression().getVariables(); isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end()); @@ -572,11 +553,11 @@ namespace storm { } storm::expressions::ExpressionManager const& Program::getManager() const { - return this->manager; + return *this->manager; } storm::expressions::ExpressionManager& Program::getManager() { - return this->manager; + return *this->manager; } std::ostream& operator<<(std::ostream& stream, Program const& program) { diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp index 7f9b8107a..2c1b49ae7 100644 --- a/src/storage/prism/RewardModel.cpp +++ b/src/storage/prism/RewardModel.cpp @@ -30,7 +30,7 @@ namespace storm { return this->transitionRewards; } - RewardModel RewardModel::substitute(std::map const& substitution) const { + RewardModel RewardModel::substitute(std::map const& substitution) const { std::vector newStateRewards; newStateRewards.reserve(this->getStateRewards().size()); for (auto const& stateReward : this->getStateRewards()) { diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h index 62841ef5e..2a2b0ab97 100644 --- a/src/storage/prism/RewardModel.h +++ b/src/storage/prism/RewardModel.h @@ -76,12 +76,12 @@ namespace storm { std::vector const& getTransitionRewards() const; /*! - * Substitutes all identifiers in the reward model according to the given map. + * Substitutes all variables in the reward model according to the given map. * * @param substitution The substitution to perform. * @return The resulting reward model. */ - RewardModel substitute(std::map const& substitution) const; + RewardModel substitute(std::map const& substitution) const; friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);