From 5467043807393cdb3f10dcabeafa96a79454b783 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 31 May 2019 11:49:27 +0200
Subject: [PATCH] DeterministicSchedsLpChecker: Only consider end components
with value zero for all objectives.
---
.../DeterministicSchedsLpChecker.cpp | 90 ++++++++-----------
.../IterativeMinMaxLinearEquationSolver.cpp | 16 ++--
2 files changed, 45 insertions(+), 61 deletions(-)
diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
index fee459534..ed60c0921 100644
--- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp
@@ -204,11 +204,21 @@ namespace storm {
template <typename ModelType, typename GeometryValueType>
std::vector<std::vector<storm::expressions::Variable>> DeterministicSchedsLpChecker<ModelType, GeometryValueType>::createEcVariables(std::vector<storm::expressions::Expression> const& choiceVars) {
+
+ // Get the choices that do not induce a value (i.e. reward) for all objectives
+ storm::storage::BitVector choicesWithValueZero(model.getNumberOfChoices(), true);
+ for (auto const& objHelper : objectiveHelper) {
+ for (auto const& value : objHelper.getChoiceValueOffsets()) {
+ STORM_LOG_ASSERT(!storm::utility::isZero(value.second), "Expected non-zero choice-value offset.");
+ choicesWithValueZero.set(value.first, false);
+ }
+ }
+ storm::storage::MaximalEndComponentDecomposition<ValueType> mecs(model.getTransitionMatrix(), model.getBackwardTransitions(), storm::storage::BitVector(model.getNumberOfStates(), true), choicesWithValueZero);
+
+
auto one = lpModel->getConstant(storm::utility::one<ValueType>());
- std::vector<std::vector<storm::expressions::Variable>> result(model.getNumberOfStates());
- storm::storage::MaximalEndComponentDecomposition<ValueType> mecs(model);
uint64_t ecCounter = 0;
-
+ std::vector<std::vector<storm::expressions::Variable>> result(model.getNumberOfStates());
for (auto const& mec : mecs) {
// Create a submatrix for the current mec as well as a mapping to map back to the original states.
storm::storage::BitVector mecStatesAsBitVector(model.getNumberOfStates(), false);
@@ -228,64 +238,38 @@ namespace storm {
// Also assert that not every state takes an ec choice.
auto subEcs = getSubEndComponents(mecTransitions);
for (auto const& subEc : subEcs) {
- // get the choices of the current EC with some non-zero value (i.e. reward).
- // std::cout << "sub ec choices of ec" << ecCounter << ": " << subEc.second << std::endl;
- storm::storage::BitVector subEcChoicesWithValueZero = subEc.second;
+ // Create a variable that is one iff upon entering this subEC no more choice value is collected.
+ auto ecVar = lpModel->addBoundedIntegerVariable("ec" + std::to_string(ecCounter++), storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
+ // assign this variable to every state in the ec
+ for (auto const& localSubEcStateIndex : subEc.first) {
+ uint64_t subEcState = toGlobalStateIndexMapping[localSubEcStateIndex];
+ result[subEcState].push_back(ecVar);
+ }
+ // Create the sum over all choice vars that induce zero choice value
+ std::vector<storm::expressions::Expression> ecChoiceVars;
+ uint64_t numSubEcStatesWithMultipleChoices = subEc.first.getNumberOfSetBits();
for (auto const& localSubEcChoiceIndex : subEc.second) {
uint64_t subEcChoice = toGlobalChoiceIndexMapping[localSubEcChoiceIndex];
- for (auto const& objHelper : objectiveHelper) {
- if (objHelper.getChoiceValueOffsets().count(subEcChoice) > 0) {
- STORM_LOG_ASSERT(!storm::utility::isZero(objHelper.getChoiceValueOffsets().at(subEcChoice)), "Expected non-zero choice-value offset.");
- subEcChoicesWithValueZero.set(localSubEcChoiceIndex, false);
- break;
- }
+ if (choiceVars[subEcChoice].isInitialized()) {
+ ecChoiceVars.push_back(choiceVars[subEcChoice]);
+ } else {
+ // If there is no choiceVariable, it means that this corresponds to a state with just one choice.
+ assert(numSubEcStatesWithMultipleChoices > 0);
+ --numSubEcStatesWithMultipleChoices;
}
}
-
- // Check whether each state has at least one zero-valued choice
- bool zeroValueSubEc = true;
- for (auto const& state : subEc.first) {
- if (subEcChoicesWithValueZero.getNextSetIndex(mecTransitions.getRowGroupIndices()[state]) >= mecTransitions.getRowGroupIndices()[state + 1]) {
- zeroValueSubEc = false;
- break;
- }
+ // Assert that the ecVar is one iff the sum over the zero-value-choice variables equals the number of states in this ec
+ storm::expressions::Expression ecVarBound = one - lpModel->getConstant(storm::utility::convertNumber<ValueType>(numSubEcStatesWithMultipleChoices)).simplify();
+ if (!ecChoiceVars.empty()) {
+ ecVarBound = ecVarBound + storm::expressions::sum(ecChoiceVars);
}
-
- if (zeroValueSubEc) {
- // Create a variable that is one iff upon entering this subEC no more choice value is collected.
- auto ecVar = lpModel->addBoundedIntegerVariable("ec" + std::to_string(ecCounter++), storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
- // assign this variable to every state in the ec
- for (auto const& localSubEcStateIndex : subEc.first) {
- uint64_t subEcState = toGlobalStateIndexMapping[localSubEcStateIndex];
- result[subEcState].push_back(ecVar);
- }
- // Create the sum over all choice vars that induce zero choice value
- std::vector<storm::expressions::Expression> ecChoiceVars;
- uint64_t numSubEcStatesWithMultipleChoices = subEc.first.getNumberOfSetBits();
- for (auto const& localSubEcChoiceIndex : subEcChoicesWithValueZero) {
- uint64_t subEcChoice = toGlobalChoiceIndexMapping[localSubEcChoiceIndex];
- if (choiceVars[subEcChoice].isInitialized()) {
- ecChoiceVars.push_back(choiceVars[subEcChoice]);
- } else {
- // If there is no choiceVariable, it means that this corresponds to a state with just one choice.
- assert(numSubEcStatesWithMultipleChoices > 0);
- --numSubEcStatesWithMultipleChoices;
- }
- }
- // Assert that the ecVar is one iff the sum over the zero-value-choice variables equals the number of states in this ec
- storm::expressions::Expression ecVarBound = one - lpModel->getConstant(storm::utility::convertNumber<ValueType>(numSubEcStatesWithMultipleChoices)).simplify();
- if (!ecChoiceVars.empty()) {
- ecVarBound = ecVarBound + storm::expressions::sum(ecChoiceVars);
- }
- if (inOutEncoding()) {
- lpModel->addConstraint("", ecVar <= ecVarBound);
- } else {
- lpModel->addConstraint("", ecVar >= ecVarBound);
- }
+ if (inOutEncoding()) {
+ lpModel->addConstraint("", ecVar <= ecVarBound);
+ } else {
+ lpModel->addConstraint("", ecVar >= ecVarBound);
}
}
}
-
STORM_LOG_TRACE("Found " << ecCounter << " end components.");
return result;
}
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index becaa1d17..37f9c1ab5 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -241,7 +241,7 @@ namespace storm {
if (!this->hasUniqueSolution()) { // Traditional value iteration has no requirements if the solution is unique.
// Computing a scheduler is only possible if the solution is unique
if (this->isTrackSchedulerSet()) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
} else {
// As we want the smallest (largest) solution for maximizing (minimizing) equation systems, we have to approach the solution from below (above).
if (!direction || direction.get() == OptimizationDirection::Maximize) {
@@ -255,7 +255,7 @@ namespace storm {
} else if (method == MinMaxMethod::IntervalIteration) {
// Interval iteration requires a unique solution and lower+upper bounds
if (!this->hasUniqueSolution()) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
requirements.requireBounds();
} else if (method == MinMaxMethod::RationalSearch) {
@@ -263,22 +263,22 @@ namespace storm {
requirements.requireLowerBounds();
// The solution needs to be unique in case of minimizing or in cases where we want a scheduler.
if (!this->hasUniqueSolution() && (!direction || direction.get() == OptimizationDirection::Minimize || this->isTrackSchedulerSet())) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
} else if (method == MinMaxMethod::PolicyIteration) {
- if (!this->hasUniqueSolution()) {
+ // The initial scheduler shall not select an end component
+ if (!this->hasNoEndComponents()) {
requirements.requireValidInitialScheduler();
}
} else if (method == MinMaxMethod::SoundValueIteration) {
if (!this->hasUniqueSolution()) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
requirements.requireBounds(false);
} else if (method == MinMaxMethod::ViToPi) {
- // Since we want to use value iteration to extract an initial scheduler, it helps to eliminate all end components first.
- // TODO: We might get around this, as the initial value iteration scheduler is only a heuristic.
+ // Since we want to use value iteration to extract an initial scheduler, the solution has to be unique.
if (!this->hasUniqueSolution()) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "Unsupported technique for iterative MinMax linear equation solver.");