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 std::vector> DeterministicSchedsLpChecker::createEcVariables(std::vector 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 mecs(model.getTransitionMatrix(), model.getBackwardTransitions(), storm::storage::BitVector(model.getNumberOfStates(), true), choicesWithValueZero); + + auto one = lpModel->getConstant(storm::utility::one()); - std::vector> result(model.getNumberOfStates()); - storm::storage::MaximalEndComponentDecomposition mecs(model); uint64_t ecCounter = 0; - + std::vector> 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(), storm::utility::one()); + // 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 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(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(), storm::utility::one()); - // 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 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(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.");