From 8e71081f1e55567f6bd14eb621c7a04fe75a7479 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 7 Jan 2015 19:55:13 +0100 Subject: [PATCH] Functional tests now work again. Former-commit-id: 46d964ad2212b9932fe272fa0328cd7f0196b19c --- src/parser/PrismParser.cpp | 24 ++--- src/solver/GlpkLpSolver.cpp | 18 ++-- src/solver/LpSolver.h | 2 +- src/storage/dd/CuddDdForwardIterator.cpp | 8 +- src/storage/dd/CuddDdManager.cpp | 8 +- src/storage/expressions/Expression.cpp | 2 +- src/storage/expressions/ExpressionManager.cpp | 22 ++++- src/storage/expressions/ExpressionManager.h | 87 +++++++++++++------ .../expressions/LinearCoefficientVisitor.cpp | 6 +- src/storage/expressions/SimpleValuation.cpp | 19 +++- src/storage/expressions/SimpleValuation.h | 3 + src/storage/expressions/Type.cpp | 37 +++++--- src/storage/expressions/Valuation.h | 20 ++++- src/storage/prism/Program.cpp | 26 +++--- test/functional/parser/PrismParserTest.cpp | 4 +- test/functional/solver/GlpkLpSolverTest.cpp | 4 +- test/functional/solver/GurobiLpSolverTest.cpp | 4 +- 17 files changed, 197 insertions(+), 97 deletions(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 4a34af248..df247824f 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -225,7 +225,7 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { if (!this->secondRun) { try { - storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType()); + storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant); this->identifiers_.add(newConstant, newVariable.getExpression()); } catch (storm::exceptions::InvalidArgumentException const& e) { if (manager->hasVariable(newConstant)) { @@ -241,7 +241,7 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const { if (!this->secondRun) { try { - storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant); this->identifiers_.add(newConstant, newVariable.getExpression()); } catch (storm::exceptions::InvalidArgumentException const& e) { if (manager->hasVariable(newConstant)) { @@ -257,7 +257,7 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const { if (!this->secondRun) { try { - storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getRationalType()); + storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant); this->identifiers_.add(newConstant, newVariable.getExpression()); } catch (storm::exceptions::InvalidArgumentException const& e) { if (manager->hasVariable(newConstant)) { @@ -273,7 +273,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { try { - storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType()); + storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant); this->identifiers_.add(newConstant, newVariable.getExpression()); } catch (storm::exceptions::InvalidArgumentException const& e) { if (manager->hasVariable(newConstant)) { @@ -289,7 +289,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { try { - storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant); this->identifiers_.add(newConstant, newVariable.getExpression()); } catch (storm::exceptions::InvalidArgumentException const& e) { if (manager->hasVariable(newConstant)) { @@ -305,7 +305,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { try { - storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant); this->identifiers_.add(newConstant, newVariable.getExpression()); } catch (storm::exceptions::InvalidArgumentException const& e) { if (manager->hasVariable(newConstant)) { @@ -361,7 +361,7 @@ namespace storm { storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const { if (!this->secondRun) { try { - storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getBooleanType()); + storm::expressions::Variable newVariable = manager->declareBooleanVariable(variableName); this->identifiers_.add(variableName, newVariable.getExpression()); } catch (storm::exceptions::InvalidArgumentException const& e) { if (manager->hasVariable(variableName)) { @@ -377,7 +377,7 @@ namespace storm { 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) { try { - storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareIntegerVariable(variableName); this->identifiers_.add(variableName, newVariable.getExpression()); } catch (storm::exceptions::InvalidArgumentException const& e) { if (manager->hasVariable(variableName)) { @@ -406,14 +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."); - storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType()); - this->identifiers_.add(renamingPair->first, renamedVariable.getExpression()); + storm::expressions::Variable renamedVariable = manager->declareBooleanVariable(renamingPair->second); + this->identifiers_.add(renamingPair->second, 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."); - storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType()); - this->identifiers_.add(renamingPair->first, renamedVariable.getExpression()); + storm::expressions::Variable renamedVariable = manager->declareIntegerVariable(renamingPair->second); + this->identifiers_.add(renamingPair->second, renamedVariable.getExpression()); } // Return a dummy module in the first pass. diff --git a/src/solver/GlpkLpSolver.cpp b/src/solver/GlpkLpSolver.cpp index dabb5bbdf..d88fdb407 100644 --- a/src/solver/GlpkLpSolver.cpp +++ b/src/solver/GlpkLpSolver.cpp @@ -48,59 +48,59 @@ namespace storm { } storm::expressions::Variable GlpkLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + storm::expressions::Variable newVariable = manager->declareRationalVariable(name); this->addVariable(newVariable, GLP_CV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient); return newVariable; } storm::expressions::Variable GlpkLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + storm::expressions::Variable newVariable = manager->declareRationalVariable(name); this->addVariable(newVariable, GLP_CV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient); return newVariable; } storm::expressions::Variable GlpkLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + storm::expressions::Variable newVariable = manager->declareRationalVariable(name); this->addVariable(newVariable, GLP_CV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient); return newVariable; } storm::expressions::Variable GlpkLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + storm::expressions::Variable newVariable = manager->declareRationalVariable(name); this->addVariable(newVariable, GLP_CV, GLP_FR, 0, 0, objectiveFunctionCoefficient); return newVariable; } storm::expressions::Variable GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_IV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } storm::expressions::Variable GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_IV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } storm::expressions::Variable GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_IV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } storm::expressions::Variable GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_IV, GLP_FR, 0, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } storm::expressions::Variable GlpkLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_BV, GLP_FR, 0, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; diff --git a/src/solver/LpSolver.h b/src/solver/LpSolver.h index 46fd327fe..50a1be39e 100644 --- a/src/solver/LpSolver.h +++ b/src/solver/LpSolver.h @@ -34,7 +34,7 @@ namespace storm { * @param modelSense A value indicating whether the objective function of this model is to be minimized or * maximized. */ - LpSolver(ModelSense const& modelSense) : currentModelHasBeenOptimized(false), modelSense(modelSense) { + LpSolver(ModelSense const& modelSense) : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), modelSense(modelSense) { // Intentionally left empty. } diff --git a/src/storage/dd/CuddDdForwardIterator.cpp b/src/storage/dd/CuddDdForwardIterator.cpp index c1d0f7392..6a8f0fa85 100644 --- a/src/storage/dd/CuddDdForwardIterator.cpp +++ b/src/storage/dd/CuddDdForwardIterator.cpp @@ -5,7 +5,7 @@ namespace storm { namespace dd { - DdForwardIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { + DdForwardIterator::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() { // Intentionally left empty. } @@ -90,9 +90,9 @@ namespace storm { } else { storm::expressions::Variable const& metaVariable = std::get<1>(this->relevantDontCareDdVariables[index]); if ((this->cubeCounter & (1ull << index)) != 0) { - currentValuation.setIntegerValue(metaVariable, ((currentValuation.getIntegerValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); + currentValuation.setBoundedIntegerValue(metaVariable, ((currentValuation.getBoundedIntegerValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); } else { - currentValuation.setIntegerValue(metaVariable, ((currentValuation.getIntegerValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); + currentValuation.setBoundedIntegerValue(metaVariable, ((currentValuation.getBoundedIntegerValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow()); } } } @@ -134,7 +134,7 @@ namespace storm { } } if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) { - currentValuation.setIntegerValue(metaVariable, intValue + ddMetaVariable.getLow()); + currentValuation.setBoundedIntegerValue(metaVariable, intValue + ddMetaVariable.getLow()); } } diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 896e39fcc..884da639b 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -110,8 +110,8 @@ namespace storm { std::size_t numberOfBits = static_cast(std::ceil(std::log2(high - low + 1))); - storm::expressions::Variable unprimed = manager->declareVariable(name, manager->getBoundedIntegerType(numberOfBits)); - storm::expressions::Variable primed = manager->declareVariable(name + "'", manager->getBoundedIntegerType(numberOfBits)); + storm::expressions::Variable unprimed = manager->declareBoundedIntegerVariable(name, numberOfBits); + storm::expressions::Variable primed = manager->declareBoundedIntegerVariable(name + "'", numberOfBits); std::vector> variables; std::vector> variablesPrime; @@ -138,8 +138,8 @@ namespace storm { // Check whether a meta variable already exists. STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists."); - storm::expressions::Variable unprimed = manager->declareVariable(name, manager->getBooleanType()); - storm::expressions::Variable primed = manager->declareVariable(name + "'", manager->getBooleanType()); + storm::expressions::Variable unprimed = manager->declareBooleanVariable(name); + storm::expressions::Variable primed = manager->declareBooleanVariable(name + "'"); std::vector> variables; std::vector> variablesPrime; diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index b11a80457..4be75c347 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -166,7 +166,7 @@ namespace storm { } Expression operator-(Expression const& first) { - return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Minus))); + return Expression(std::shared_ptr(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minus(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Minus))); } Expression operator*(Expression const& first, Expression const& second) { diff --git a/src/storage/expressions/ExpressionManager.cpp b/src/storage/expressions/ExpressionManager.cpp index fbe608a5c..b624af766 100644 --- a/src/storage/expressions/ExpressionManager.cpp +++ b/src/storage/expressions/ExpressionManager.cpp @@ -51,7 +51,7 @@ namespace storm { } } - ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), variableTypeToCountMapping(), numberOfVariables(0), auxiliaryVariableTypeToCountMapping(), numberOfAuxiliaryVariables(0), freshVariableCounter(0), booleanType(nullptr), integerType(nullptr), rationalType(nullptr) { + ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), numberOfVariables(0), variableTypeToCountMapping(), auxiliaryVariableTypeToCountMapping(), numberOfAuxiliaryVariables(0), freshVariableCounter(0), booleanType(nullptr), integerType(nullptr), rationalType(nullptr) { // Intentionally left empty. } @@ -126,6 +126,10 @@ namespace storm { return this->declareVariable(name, this->getIntegerType()); } + Variable ExpressionManager::declareBoundedIntegerVariable(std::string const& name, std::size_t width) { + return this->declareVariable(name, this->getBoundedIntegerType(width)); + } + Variable ExpressionManager::declareRationalVariable(std::string const& name) { return this->declareVariable(name, this->getRationalType()); } @@ -218,6 +222,12 @@ namespace storm { return getNumberOfVariables(getIntegerType()); } + uint_fast64_t ExpressionManager::getNumberOfBoundedIntegerVariables() const { + // The bit width of the type is not of importance here, since bit vector types are considered the same when + // it comes to counting. + return getNumberOfVariables(getBoundedIntegerType(0)); + } + uint_fast64_t ExpressionManager::getNumberOfRationalVariables() const { return getNumberOfVariables(getRationalType()); } @@ -243,6 +253,12 @@ namespace storm { return getNumberOfAuxiliaryVariables(getIntegerType()); } + uint_fast64_t ExpressionManager::getNumberOfAuxiliaryBoundedIntegerVariables() const { + // The bit width of the type is not of importance here, since bit vector types are considered the same when + // it comes to counting. + return getNumberOfAuxiliaryVariables(getBoundedIntegerType(0)); + } + uint_fast64_t ExpressionManager::getNumberOfAuxiliaryRationalVariables() const { return getNumberOfAuxiliaryVariables(getRationalType()); } @@ -279,5 +295,9 @@ namespace storm { return this->shared_from_this(); } + bool ExpressionManager::ManagerTypeEquality::operator()(Type const& a, Type const& b) const { + return a.getMask() == b.getMask(); + } + } // namespace expressions } // namespace storm \ No newline at end of file diff --git a/src/storage/expressions/ExpressionManager.h b/src/storage/expressions/ExpressionManager.h index 5106beb5a..9661cf696 100644 --- a/src/storage/expressions/ExpressionManager.h +++ b/src/storage/expressions/ExpressionManager.h @@ -166,6 +166,17 @@ namespace storm { */ Variable declareIntegerVariable(std::string const& name); + /*! + * Declares a new bounded integer variable with a name that must not yet exist and the bounded type of the + * given bit width. Note that the name must not start with two underscores since these variables are + * reserved for internal use only. + * + * @param name The name of the variable. + * @param width The bit width of the bounded type. + * @return The newly declared variable. + */ + Variable declareBoundedIntegerVariable(std::string const& name, std::size_t width); + /*! * Declares a new rational variable with a name that must not yet exist and its corresponding type. Note that * the name must not start with two underscores since these variables are reserved for internal use only. @@ -240,13 +251,6 @@ namespace storm { * @return The variable. */ Variable declareFreshAuxiliaryVariable(storm::expressions::Type const& variableType); - - /*! - * Retrieves the number of variables with the given type. - * - * @return The number of variables with the given type. - */ - uint_fast64_t getNumberOfVariables(storm::expressions::Type const& variableType) const; /*! * Retrieves the number of variables. @@ -268,6 +272,13 @@ namespace storm { * @return The number of integer variables. */ uint_fast64_t getNumberOfIntegerVariables() const; + + /*! + * Retrieves the number of bounded integer variables. + * + * @return The number of bounded integer variables. + */ + uint_fast64_t getNumberOfBoundedIntegerVariables() const; /*! * Retrieves the number of rational variables. @@ -275,13 +286,6 @@ namespace storm { * @return The number of rational variables. */ uint_fast64_t getNumberOfRationalVariables() const; - - /*! - * Retrieves the number of auxiliary variables with the given type. - * - * @return The number of auxiliary variables with the given type. - */ - uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::Type const& variableType) const; /*! * Retrieves the number of auxiliary variables. @@ -291,23 +295,30 @@ namespace storm { uint_fast64_t getNumberOfAuxiliaryVariables() const; /*! - * Retrieves the number of boolean variables. + * Retrieves the number of auxiliary boolean variables. * - * @return The number of boolean variables. + * @return The number of auxiliary boolean variables. */ uint_fast64_t getNumberOfAuxiliaryBooleanVariables() const; /*! - * Retrieves the number of integer variables. + * Retrieves the number of auxiliary integer variables. * - * @return The number of integer variables. + * @return The number of auxiliary integer variables. */ uint_fast64_t getNumberOfAuxiliaryIntegerVariables() const; /*! - * Retrieves the number of rational variables. + * Retrieves the number of auxiliary bounded integer variables. * - * @return The number of rational variables. + * @return The number of auxiliary bounded integer variables. + */ + uint_fast64_t getNumberOfAuxiliaryBoundedIntegerVariables() const; + + /*! + * Retrieves the number of auxiliary rational variables. + * + * @return The number of auxiliary rational variables. */ uint_fast64_t getNumberOfAuxiliaryRationalVariables() const; @@ -364,6 +375,12 @@ namespace storm { std::shared_ptr getSharedPointer() const; private: + // A functor used for treating bit vector types of different bit widths equally when it comes to the variable + // count. + struct ManagerTypeEquality { + bool operator()(Type const& a, Type const& b) const; + }; + /*! * Checks whether the given variable name is valid. * @@ -392,23 +409,39 @@ namespace storm { */ Variable declareOrGetVariable(std::string const& name, storm::expressions::Type const& variableType, bool auxiliary, bool checkName); + /*! + * Retrieves the number of variables with the given type. Note that this considers bounded integer variables + * to be of the same type, no matter which bit width they have. + * + * @param variableType The type for which to query the number of variables. + */ + uint_fast64_t getNumberOfVariables(storm::expressions::Type const& variableType) const; + + /*! + * Retrieves the number of auxiliary variables with the given type. Note that this considers bounded integer + * variables to be of the same type, no matter which bit width they have. + * + * @param variableType The type for which to query the number of auxiliary variables. + */ + uint_fast64_t getNumberOfAuxiliaryVariables(storm::expressions::Type const& variableType) const; + // A mapping from all variable names (auxiliary + normal) to their indices. std::unordered_map nameToIndexMapping; // A mapping from all variable indices to their names. - std::unordered_map indexToNameMapping; + std::unordered_map indexToNameMapping; // A mapping from all variable indices to their types. - std::unordered_map indexToTypeMapping; + std::unordered_map indexToTypeMapping; - // Store counts for variables. - std::unordered_map variableTypeToCountMapping; - // The number of declared variables. uint_fast64_t numberOfVariables; - + + // Store counts for variables. + std::unordered_map, ManagerTypeEquality> variableTypeToCountMapping; + // Store counts for auxiliary variables. - std::unordered_map auxiliaryVariableTypeToCountMapping; + std::unordered_map, ManagerTypeEquality> auxiliaryVariableTypeToCountMapping; // The number of declared auxiliary variables. uint_fast64_t numberOfAuxiliaryVariables; diff --git a/src/storage/expressions/LinearCoefficientVisitor.cpp b/src/storage/expressions/LinearCoefficientVisitor.cpp index 1c5cd72bf..ee7d397ae 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.cpp +++ b/src/storage/expressions/LinearCoefficientVisitor.cpp @@ -32,8 +32,8 @@ namespace storm { variableToCoefficientMapping = std::move(other.variableToCoefficientMapping); std::swap(constantPart, other.constantPart); } - for (auto const& otherVariableCoefficientPair : other.variableToCoefficientMapping) { - this->variableToCoefficientMapping[otherVariableCoefficientPair.first] *= other.constantPart; + for (auto& variableCoefficientPair : this->variableToCoefficientMapping) { + variableCoefficientPair.second *= other.constantPart; } constantPart *= other.constantPart; return *this; @@ -110,7 +110,7 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression is non-linear."); } - return rightResult; + return leftResult; } boost::any LinearCoefficientVisitor::visit(BinaryRelationExpression const& expression) { diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index b49a717c9..bc9454815 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -11,13 +11,16 @@ namespace storm { // Intentionally left empty. } - SimpleValuation::SimpleValuation(std::shared_ptr const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), rationalValues(nullptr) { + SimpleValuation::SimpleValuation(std::shared_ptr const& manager) : Valuation(manager), booleanValues(nullptr), integerValues(nullptr), boundedIntegerValues(nullptr), rationalValues(nullptr) { if (this->getManager().getNumberOfBooleanVariables() > 0) { booleanValues = std::unique_ptr>(new std::vector(this->getManager().getNumberOfBooleanVariables())); } if (this->getManager().getNumberOfIntegerVariables() > 0) { integerValues = std::unique_ptr>(new std::vector(this->getManager().getNumberOfIntegerVariables())); } + if (this->getManager().getNumberOfBoundedIntegerVariables() > 0) { + boundedIntegerValues = std::unique_ptr>(new std::vector(this->getManager().getNumberOfBoundedIntegerVariables())); + } if (this->getManager().getNumberOfRationalVariables() > 0) { rationalValues = std::unique_ptr>(new std::vector(this->getManager().getNumberOfRationalVariables())); } @@ -30,6 +33,9 @@ namespace storm { if (other.integerValues != nullptr) { integerValues = std::unique_ptr>(new std::vector(*other.integerValues)); } + if (other.boundedIntegerValues != nullptr) { + boundedIntegerValues = std::unique_ptr>(new std::vector(*other.boundedIntegerValues)); + } if (other.rationalValues != nullptr) { rationalValues = std::unique_ptr>(new std::vector(*other.rationalValues)); } @@ -44,6 +50,9 @@ namespace storm { if (other.integerValues != nullptr) { integerValues = std::unique_ptr>(new std::vector(*other.integerValues)); } + if (other.boundedIntegerValues != nullptr) { + boundedIntegerValues = std::unique_ptr>(new std::vector(*other.boundedIntegerValues)); + } if (other.booleanValues != nullptr) { rationalValues = std::unique_ptr>(new std::vector(*other.rationalValues)); } @@ -80,6 +89,10 @@ namespace storm { int_fast64_t SimpleValuation::getIntegerValue(Variable const& integerVariable) const { return (*integerValues)[integerVariable.getOffset()]; } + + int_fast64_t SimpleValuation::getBoundedIntegerValue(Variable const& integerVariable) const { + return (*boundedIntegerValues)[integerVariable.getOffset()]; + } double SimpleValuation::getRationalValue(Variable const& rationalVariable) const { return (*rationalValues)[rationalVariable.getOffset()]; @@ -93,6 +106,10 @@ namespace storm { (*integerValues)[integerVariable.getOffset()] = value; } + void SimpleValuation::setBoundedIntegerValue(Variable const& integerVariable, int_fast64_t value) { + (*boundedIntegerValues)[integerVariable.getOffset()] = value; + } + void SimpleValuation::setRationalValue(Variable const& rationalVariable, double value) { (*rationalValues)[rationalVariable.getOffset()] = value; } diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 3e19fea8d..d4418641b 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -47,7 +47,9 @@ namespace storm { virtual bool getBooleanValue(Variable const& booleanVariable) const override; virtual void setBooleanValue(Variable const& booleanVariable, bool value) override; virtual int_fast64_t getIntegerValue(Variable const& integerVariable) const override; + virtual int_fast64_t getBoundedIntegerValue(Variable const& integerVariable) const override; virtual void setIntegerValue(Variable const& integerVariable, int_fast64_t value) override; + virtual void setBoundedIntegerValue(Variable const& integerVariable, int_fast64_t value) override; virtual double getRationalValue(Variable const& rationalVariable) const override; virtual void setRationalValue(Variable const& rationalVariable, double value) override; @@ -55,6 +57,7 @@ namespace storm { // Containers that store the values of the variables of the appropriate type. std::unique_ptr> booleanValues; std::unique_ptr> integerValues; + std::unique_ptr> boundedIntegerValues; std::unique_ptr> rationalValues; }; diff --git a/src/storage/expressions/Type.cpp b/src/storage/expressions/Type.cpp index d3516b662..9efa6cf65 100644 --- a/src/storage/expressions/Type.cpp +++ b/src/storage/expressions/Type.cpp @@ -4,6 +4,7 @@ #include "src/storage/expressions/ExpressionManager.h" #include "src/utility/macros.h" +#include "src/exceptions/InvalidTypeException.h" namespace storm { namespace expressions { @@ -145,7 +146,7 @@ namespace storm { } Type Type::plusMinusTimes(Type const& other) const { - STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); + STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands."); if (this->isRationalType() || other.isRationalType()) { return this->getManager().getRationalType(); } @@ -153,17 +154,20 @@ namespace storm { } Type Type::minus() const { - STORM_LOG_ASSERT(this->isNumericalType(), "Operator requires numerical operand."); + STORM_LOG_THROW(this->isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operand."); return *this; } Type Type::divide(Type const& other) const { - STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); - return this->getManager().getRationalType(); + STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands."); + if (this->isRationalType() || other.isRationalType()) { + return this->getManager().getRationalType(); + } + return this->getManager().getIntegerType(); } Type Type::power(Type const& other) const { - STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); + STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands."); if (this->isRationalType() || other.isRationalType()) { return getManager().getRationalType(); } @@ -171,33 +175,42 @@ namespace storm { } Type Type::logicalConnective(Type const& other) const { - STORM_LOG_ASSERT(this->isBooleanType() && other.isBooleanType(), "Operator requires boolean operands."); + STORM_LOG_THROW(this->isBooleanType() && other.isBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean operands."); return *this; } Type Type::logicalConnective() const { - STORM_LOG_ASSERT(this->isBooleanType(), "Operator requires boolean operand."); + STORM_LOG_THROW(this->isBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean operand."); return *this; } Type Type::numericalComparison(Type const& other) const { - STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); + STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands."); return this->getManager().getBooleanType(); } Type Type::ite(Type const& thenType, Type const& elseType) const { - STORM_LOG_ASSERT(this->isBooleanType(), "Operator requires boolean condition."); - STORM_LOG_ASSERT(thenType == elseType, "Operator requires equal types."); + STORM_LOG_THROW(this->isBooleanType(), storm::exceptions::InvalidTypeException, "Operator requires boolean condition."); + if (thenType == elseType) { + return thenType; + } else { + STORM_LOG_THROW(thenType.isNumericalType() == elseType.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator 'ite' requires proper types."); + if (thenType.isRationalType() || elseType.isRationalType()) { + return this->getManager().getRationalType(); + } else { + return this->getManager().getIntegerType(); + } + } return thenType; } Type Type::floorCeil() const { - STORM_LOG_ASSERT(this->isRationalType(), "Operator requires rational operand."); + STORM_LOG_THROW(this->isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires rational operand."); return this->getManager().getIntegerType(); } Type Type::minimumMaximum(Type const& other) const { - STORM_LOG_ASSERT(this->isNumericalType() && other.isNumericalType(), "Operator requires numerical operands."); + STORM_LOG_THROW(this->isNumericalType() && other.isNumericalType(), storm::exceptions::InvalidTypeException, "Operator requires numerical operands."); if (this->isRationalType() || other.isRationalType()) { return this->getManager().getRationalType(); } diff --git a/src/storage/expressions/Valuation.h b/src/storage/expressions/Valuation.h index 1dd08751a..8b420a3ec 100644 --- a/src/storage/expressions/Valuation.h +++ b/src/storage/expressions/Valuation.h @@ -48,13 +48,29 @@ namespace storm { virtual int_fast64_t getIntegerValue(Variable const& integerVariable) const = 0; /*! - * Sets the value of the given boolean variable to the provided value. + * Retrieves the value of the given bounded integer variable. + * + * @param integerVariable The bounded integer variable whose value to retrieve. + * @return The value of the bounded integer variable. + */ + virtual int_fast64_t getBoundedIntegerValue(Variable const& integerVariable) const = 0; + + /*! + * Sets the value of the given integer variable to the provided value. * * @param integerVariable The variable whose value to set. * @param value The new value of the variable. */ virtual void setIntegerValue(Variable const& integerVariable, int_fast64_t value) = 0; - + + /*! + * Sets the value of the given bounded integer variable to the provided value. + * + * @param integerVariable The variable whose value to set. + * @param value The new value of the variable. + */ + virtual void setBoundedIntegerValue(Variable const& integerVariable, int_fast64_t value) = 0; + /*! * Retrieves the value of the given rational variable. * diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index ea7fcc3a1..6a79834a6 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -16,25 +16,23 @@ namespace storm { // Create a new initial construct if the corresponding flag was set. if (fixInitialConstruct) { - if (this->getInitialConstruct().getInitialStatesExpression().isFalse()) { - storm::expressions::Expression newInitialExpression = manager->boolean(true); - - for (auto const& booleanVariable : this->getGlobalBooleanVariables()) { + storm::expressions::Expression newInitialExpression = manager->boolean(true); + + for (auto const& booleanVariable : this->getGlobalBooleanVariables()) { + newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); + } + for (auto const& integerVariable : this->getGlobalIntegerVariables()) { + newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); + } + for (auto const& module : this->getModules()) { + for (auto const& booleanVariable : module.getBooleanVariables()) { newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); } - for (auto const& integerVariable : this->getGlobalIntegerVariables()) { + for (auto const& integerVariable : module.getIntegerVariables()) { newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); } - for (auto const& module : this->getModules()) { - for (auto const& booleanVariable : module.getBooleanVariables()) { - newInitialExpression = newInitialExpression && storm::expressions::iff(booleanVariable.getExpression(), booleanVariable.getInitialValueExpression()); - } - for (auto const& integerVariable : module.getIntegerVariables()) { - newInitialExpression = newInitialExpression && integerVariable.getExpression() == integerVariable.getInitialValueExpression(); - } - } - this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber()); } + this->initialConstruct = storm::prism::InitialConstruct(newInitialExpression, this->getInitialConstruct().getFilename(), this->getInitialConstruct().getLineNumber()); } if (checkValidity) { diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index dbbf5b4a4..c4850c42d 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -58,7 +58,7 @@ TEST(PrismParser, ComplexTest) { formula test = a >= 10 & (max(a,b) > floor(e)); formula test2 = a+b; - formula test3 = (a + b > 10 ? floor(a) : h) + a; + formula test3 = (a + b > 10 ? floor(e) : h) + a; global g : bool init false; global h : [0 .. b]; @@ -68,7 +68,7 @@ TEST(PrismParser, ComplexTest) { j : bool init c; k : [125..a] init a; - [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(a) + max(k, b) - 1 + k); + [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(e) + max(k, b) - 1 + k); endmodule module mod2 diff --git a/test/functional/solver/GlpkLpSolverTest.cpp b/test/functional/solver/GlpkLpSolverTest.cpp index ab3511d83..fe2014471 100644 --- a/test/functional/solver/GlpkLpSolverTest.cpp +++ b/test/functional/solver/GlpkLpSolverTest.cpp @@ -51,7 +51,7 @@ TEST(GlpkLpSolver, LPOptimizeMin) { ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); - ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5))); ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); @@ -117,7 +117,7 @@ TEST(GlpkLpSolver, MILPOptimizeMin) { ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); - ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5))); ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); diff --git a/test/functional/solver/GurobiLpSolverTest.cpp b/test/functional/solver/GurobiLpSolverTest.cpp index 083ed19bc..6c07a1f19 100644 --- a/test/functional/solver/GurobiLpSolverTest.cpp +++ b/test/functional/solver/GurobiLpSolverTest.cpp @@ -51,7 +51,7 @@ TEST(GurobiLpSolver, LPOptimizeMin) { ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); - ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5))); ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update()); @@ -117,7 +117,7 @@ TEST(GurobiLpSolver, MILPOptimizeMin) { ASSERT_NO_THROW(solver.update()); ASSERT_NO_THROW(solver.addConstraint("", x + y + z <= solver.getConstant(12))); - ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x == solver.getConstant(5))); + ASSERT_NO_THROW(solver.addConstraint("", solver.getConstant(0.5) * y + z - x <= solver.getConstant(5))); ASSERT_NO_THROW(solver.addConstraint("", y - x <= solver.getConstant(5.5))); ASSERT_NO_THROW(solver.update());