From 4322d00034f9579eef946aaed7982adad24cbc3b Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 07:24:09 +0200 Subject: [PATCH 1/5] FilteredRewardModel: added create method that works without a checkout. --- src/storm/utility/FilteredRewardModel.h | 26 ++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/src/storm/utility/FilteredRewardModel.h b/src/storm/utility/FilteredRewardModel.h index 32dc13521..5280cfd98 100644 --- a/src/storm/utility/FilteredRewardModel.h +++ b/src/storm/utility/FilteredRewardModel.h @@ -8,9 +8,8 @@ namespace storm { namespace utility { - /* - * This class wraps around a + * This class wraps around a Reward model where certain reward types are disabled. */ template class FilteredRewardModel { @@ -45,20 +44,25 @@ namespace storm { RewardModelType const* rewardModel; }; - template - FilteredRewardModel createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) { - auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel(); - if (checkTask.getFormula().hasRewardAccumulation()) { - auto const& acc = checkTask.getFormula().getRewardAccumulation(); - STORM_LOG_THROW(model.isDiscreteTimeModel() || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported."); + template + FilteredRewardModel createFilteredRewardModel(RewardModelType const& baseRewardModel, bool isDiscreteTimeModel, FormulaType const& formula) { + if (formula.hasRewardAccumulation()) { + auto const& acc = formula.getRewardAccumulation(); + STORM_LOG_THROW(isDiscreteTimeModel || !acc.isExitSet() || !baseRewardModel.hasStateRewards(), storm::exceptions::NotSupportedException, "Exit rewards for continuous time models are not supported."); // Check which of the available reward types are allowed. - bool hasStateRewards = model.isDiscreteTimeModel() ? acc.isExitSet() : acc.isTimeSet(); + bool hasStateRewards = isDiscreteTimeModel ? acc.isExitSet() : acc.isTimeSet(); bool hasStateActionRewards = acc.isStepsSet(); bool hasTransitionRewards = acc.isStepsSet(); - return FilteredRewardModel(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards); + return FilteredRewardModel(baseRewardModel, hasStateRewards, hasStateActionRewards, hasTransitionRewards); } else { - return FilteredRewardModel(baseRewardModel, true, true, true); + return FilteredRewardModel(baseRewardModel, true, true, true); } } + + template + FilteredRewardModel createFilteredRewardModel(ModelType const& model, CheckTaskType const& checkTask) { + auto const& baseRewardModel = checkTask.isRewardModelSet() ? model.getRewardModel(checkTask.getRewardModel()) : model.getUniqueRewardModel(); + return createFilteredRewardModel(baseRewardModel, model.isDiscreteTimeModel(), checkTask.getFormula()); + } } } \ No newline at end of file From 160c6a67f4be4fb688f218ba8578cd6f28441003 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 07:24:30 +0200 Subject: [PATCH 2/5] Added missing method in case z3 lp solver is not available. --- src/storm/solver/Z3LpSolver.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index c152a9d20..16c04bd57 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -393,6 +393,11 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } + template + void Z3LpSolver::writeModelToFile(std::string const& filename) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } + template void Z3LpSolver::push() { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; From adaba036485e9b1ca93849700a3da6ea3be2f1af Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 09:25:50 +0200 Subject: [PATCH 3/5] ExpressionManager: Asserted that when getting a variable with declareOrGetVariable, the returned type is as expected. --- src/storm/storage/expressions/ExpressionManager.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index 5cc3ffcd5..ce10152e4 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -167,6 +167,7 @@ namespace storm { STORM_LOG_THROW(!checkName || isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); auto nameIndexPair = nameToIndexMapping.find(name); if (nameIndexPair != nameToIndexMapping.end()) { + STORM_LOG_ASSERT(indexToTypeMapping.at(nameIndexPair->second) == variableType, "Tried to declareOrGet variable '" << name << "' of type '" << variableType << "' but there is a variable with that name and different type '" << indexToTypeMapping.at(nameIndexPair->second)"'."); return Variable(this->getSharedPointer(), nameIndexPair->second); } else { uint_fast64_t offset = 0; From 91951f6714f99e2ff13a3fe4cd8a2fbdb3663380 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 09:29:29 +0200 Subject: [PATCH 4/5] GurobiLpSolver: Fixed an issue when popping and pushing variables with the same name. --- src/storm/solver/GurobiLpSolver.cpp | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp index 3fef398f0..3e0db5333 100644 --- a/src/storm/solver/GurobiLpSolver.cpp +++ b/src/storm/solver/GurobiLpSolver.cpp @@ -93,69 +93,72 @@ namespace storm { template storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType()); this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, upperBound, objectiveFunctionCoefficient); return newVariable; } template storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType()); this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient); return newVariable; } template storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType()); this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient); return newVariable; } template storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getRationalType()); this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient); return newVariable; } template storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_INTEGER, lowerBound, upperBound, objectiveFunctionCoefficient); return newVariable; } template storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_INTEGER, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient); return newVariable; } template storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient); return newVariable; } template storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient); return newVariable; } template storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); + storm::expressions::Variable newVariable = this->manager->declareOrGetVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_BINARY, 0, 1, objectiveFunctionCoefficient); return newVariable; } template void GurobiLpSolver::addVariable(storm::expressions::Variable const& variable, char variableType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + // Assert whether the variable does not exist yet. + // Due to incremental usage (push(), pop()), a variable might be declared in the manager but not in the lp model. + STORM_LOG_ASSERT(variableToIndexMap.count(variable) == 0, "Variable " << variable.getName() << " exists already in the model."); // Check for valid variable type. STORM_LOG_ASSERT(variableType == GRB_CONTINUOUS || variableType == GRB_INTEGER || variableType == GRB_BINARY, "Illegal type '" << variableType << "' for Gurobi variable."); From ca9102616bfd5d873c4b0f1b5cd616ef278872aa Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 29 Apr 2019 09:43:31 +0200 Subject: [PATCH 5/5] ExpressionManager: Asserted that when getting a variable with declareOrGetVariable, the returned type is as expected (part 2...). --- src/storm/storage/expressions/ExpressionManager.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index ce10152e4..219e5a521 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -167,7 +167,7 @@ namespace storm { STORM_LOG_THROW(!checkName || isValidVariableName(name), storm::exceptions::InvalidArgumentException, "Invalid variable name '" << name << "'."); auto nameIndexPair = nameToIndexMapping.find(name); if (nameIndexPair != nameToIndexMapping.end()) { - STORM_LOG_ASSERT(indexToTypeMapping.at(nameIndexPair->second) == variableType, "Tried to declareOrGet variable '" << name << "' of type '" << variableType << "' but there is a variable with that name and different type '" << indexToTypeMapping.at(nameIndexPair->second)"'."); + STORM_LOG_ASSERT(indexToTypeMapping.at(nameIndexPair->second) == variableType, "Tried to declareOrGet variable '" << name << "' of type '" << variableType << "' but there is a variable with that name and different type '" << indexToTypeMapping.at(nameIndexPair->second) << "'."); return Variable(this->getSharedPointer(), nameIndexPair->second); } else { uint_fast64_t offset = 0;