From b190fe6e8fc2f92ce5adf4e961ef8f21085ca707 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 10 Jul 2019 12:55:30 +0200 Subject: [PATCH] Various bugfixes for deterministic scheds. --- .../DeterministicSchedsLpChecker.cpp | 58 ++++++++----------- .../DeterministicSchedsLpChecker.h | 2 +- .../DeterministicSchedsObjectiveHelper.cpp | 29 +--------- .../DeterministicSchedsParetoExplorer.cpp | 8 ++- 4 files changed, 34 insertions(+), 63 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp index 6d261a829..ae788a31f 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.cpp @@ -30,31 +30,31 @@ namespace storm { return res; } - bool isMinNegativeEncoding() { + bool isMinNegativeEncoding() { // + 1 return encodingSettings().get(63); } - bool isMaxDiffEncoding() { + bool isMaxDiffEncoding() { // + 2 bool result = encodingSettings().get(62); STORM_LOG_ERROR_COND(!result || !isMinNegativeEncoding(), "maxDiffEncoding only works without minnegative encoding."); return result; } - bool choiceVarReduction() { + bool choiceVarReduction() { // + 4 return encodingSettings().get(61); } - bool inOutEncoding() { + bool inOutEncoding() { // + 8 return encodingSettings().get(60); } - bool assertBottomStateSum() { + bool assertBottomStateSum() { // + 16 bool result = encodingSettings().get(59); STORM_LOG_ERROR_COND(!result || inOutEncoding(), "Asserting bottom state sum is only relevant for in-out encoding."); return result; } - bool useNonOptimalSolutions() { + bool useNonOptimalSolutions() { // + 32 bool result = encodingSettings().get(58); return result; } @@ -215,7 +215,7 @@ namespace storm { for (auto const& stateChoices : ec) { auto state = stateChoices.first; ValueType minProb = storm::utility::one(); - for (uint64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++state) { + for (uint64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++choice) { if (stateChoices.second.count(choice) == 0) { // The choice leaves the EC, so we take the sum over the exiting probabilities ValueType exitProbabilitySum = storm::utility::zero(); @@ -294,12 +294,13 @@ namespace storm { } template - std::vector> DeterministicSchedsLpChecker::createEcVariables() { - std::vector> result(objectiveHelper.size(), std::vector(model.getNumberOfStates())); + bool DeterministicSchedsLpChecker::processEndComponents(std::vector>& ecVars) { + bool hasEndComponents = false; uint64_t ecCounter = 0; auto backwardTransitions = model.getBackwardTransitions(); - // Get the choices that do not induce a value (i.e. reward) for all objectives + // Get the choices that do not induce a value (i.e. reward) for all objectives. + // Only MECS consisting of these choices are relevant storm::storage::BitVector choicesWithValueZero(model.getNumberOfChoices(), true); for (auto const& objHelper : objectiveHelper) { for (auto const& value : objHelper.getChoiceValueOffsets()) { @@ -308,7 +309,6 @@ namespace storm { } } storm::storage::MaximalEndComponentDecomposition mecs(model.getTransitionMatrix(), backwardTransitions, storm::storage::BitVector(model.getNumberOfStates(), true), choicesWithValueZero); - for (auto const& mec : mecs) { // For each objective we might need to split this mec into several subECs, if the objective yields a non-zero scheduler-independent state value for some states of this ec. std::map, std::vector> excludedStatesToObjIndex; @@ -330,11 +330,11 @@ namespace storm { if (mecContainsSchedulerDependentValue) { for (auto const& exclStates : excludedStatesToObjIndex) { if (exclStates.first.empty()) { - auto ecVars = processEc(mec, model.getTransitionMatrix(), "", choiceVariables, *lpModel); + auto varsForMec = processEc(mec, model.getTransitionMatrix(), "", choiceVariables, *lpModel); ++ecCounter; - for (auto const& stateVar : ecVars) { + for (auto const& stateVar : varsForMec) { for (auto const& objIndex : exclStates.second) { - result[objIndex][stateVar.first] = stateVar.second; + ecVars[objIndex][stateVar.first] = stateVar.second; } } } else { @@ -350,11 +350,11 @@ namespace storm { } storm::storage::MaximalEndComponentDecomposition subEcs(model.getTransitionMatrix(), backwardTransitions, subEcStates, subEcChoices); for (auto const& subEc : subEcs) { - auto ecVars = processEc(subEc, model.getTransitionMatrix(), "o" + std::to_string(*exclStates.second.begin()), choiceVariables, *lpModel); + auto varsForSubEc = processEc(subEc, model.getTransitionMatrix(), "o" + std::to_string(*exclStates.second.begin()), choiceVariables, *lpModel); ++ecCounter; - for (auto const& stateVar : ecVars) { + for (auto const& stateVar : varsForSubEc) { for (auto const& objIndex : exclStates.second) { - result[objIndex][stateVar.first] = stateVar.second; + ecVars[objIndex][stateVar.first] = stateVar.second; } } } @@ -362,8 +362,9 @@ namespace storm { } } } - STORM_LOG_WARN_COND(ecCounter == 0, "Processed " << ecCounter << " End components."); - return result; + hasEndComponents = ecCounter > 0 || storm::utility::graph::checkIfECWithChoiceExists(model.getTransitionMatrix(), backwardTransitions, storm::storage::BitVector(model.getNumberOfStates(), true), ~choicesWithValueZero); + STORM_LOG_WARN_COND(!hasEndComponents, "Processed " << ecCounter << " End components."); + return hasEndComponents; } template @@ -406,19 +407,8 @@ namespace storm { } } // Create ec Variables for each state/objective - auto ecVars = createEcVariables(); - bool hasEndComponents = false; - for (auto const& objEcVars : ecVars) { - for (auto const& ecVar : objEcVars) { - if (ecVar.isInitialized()) { - hasEndComponents = true; - break; - } - } - if (hasEndComponents) { - break; - } - } + std::vector> ecVars(objectiveHelper.size(), std::vector(model.getNumberOfStates())); + bool hasEndComponents = processEndComponents(ecVars); // ECs are not supported with choiceVarReduction. STORM_LOG_THROW(!hasEndComponents || !choiceVarReduction(), storm::exceptions::InvalidOperationException, "Choice var reduction is not supported with end components."); @@ -438,7 +428,7 @@ namespace storm { // Compute upper bounds for each state std::vector visitingTimesUpperBounds = DeterministicSchedsObjectiveHelper::computeUpperBoundOnExpectedVisitingTimes(model.getTransitionMatrix(), bottomStates, nonBottomStates, hasEndComponents); - + std::cout << "maximal visiting times upper bound is " << *std::max_element(visitingTimesUpperBounds.begin(), visitingTimesUpperBounds.end()) << std::endl; // create choiceValue variables and assert deterministic ones. std::vector choiceValVars(model.getNumberOfChoices()); for (auto const& state : nonBottomStates) { @@ -784,8 +774,6 @@ namespace storm { STORM_PRINT_AND_LOG("Validating Lp solution for objective " << objIndex << ": LP" << storm::utility::convertNumber(expectedValue) << " InducedScheduler=" << storm::utility::convertNumber(actualValue) << " (difference is " << diff << ")" << std::endl); STORM_LOG_WARN_COND(diff <= 1e-4 * std::abs(storm::utility::convertNumber(actualValue)), "Invalid value for objective " << objIndex << ": expected " << expectedValue << " but got " << actualValue << " (difference is " << diff << ")"); } - std::cout << std::endl; - } template class DeterministicSchedsLpChecker, storm::RationalNumber>; diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h index 4416bb307..e97a99efc 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsLpChecker.h @@ -46,7 +46,7 @@ namespace storm { std::pair, std::vector> check(storm::Environment const& env, storm::storage::geometry::PolytopeTree& polytopeTree, Point const& eps); private: - std::vector> createEcVariables(); + bool processEndComponents(std::vector>& ecVars); void initializeLpModel(Environment const& env); // Builds the induced markov chain of the current model and checks whether the resulting value coincide with the result of the lp solver. diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp index deeb71b68..698ef3c9e 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.cpp @@ -401,40 +401,17 @@ namespace storm { std::cout << "Checking a mec with " << mecStates.getNumberOfSetBits() << " states " << numChoices << " choices and " << numTransitions << " transitions." << std::endl; lpath = storm::utility::one() / getExpVisitsUpperBoundForMec(mecStates, modelTransitions); }*/ - // Multiply the smallest probability occurring at each state. - for (auto const& stateChoices : mec) { - auto state = stateChoices.first; - ValueType minProb = storm::utility::one(); - for (uint64_t choice = modelTransitions.getRowGroupIndices()[state]; choice < modelTransitions.getRowGroupIndices()[state + 1]; ++state) { - if (stateChoices.second.count(choice) > 0) { - for (auto const& transition : modelTransitions.getRow(choice)) { - if (!storm::utility::isZero(transition.getValue())) { - minProb = std::min(minProb, transition.getValue()); - } - } - } else { - ValueType sum = storm::utility::zero(); - for (auto const& transition : modelTransitions.getRow(choice)) { - if (!mec.containsState(transition.getColumn())) { - sum += transition.getValue(); - } - } - minProb = std::min(minProb, sum); - } - } - lpath *= minProb; - } // We multiply the smallest transition probabilities occurring at each state and MEC-Choice // as well as the smallest 'exit' probability ValueType minExitProbability = storm::utility::one(); for (auto const& stateChoices : mec) { auto state = stateChoices.first; ValueType minProb = storm::utility::one(); - for (uint64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++state) { + for (uint64_t choice = modelTransitions.getRowGroupIndices()[state]; choice < modelTransitions.getRowGroupIndices()[state + 1]; ++choice) { if (stateChoices.second.count(choice) == 0) { // The choice leaves the EC, so we take the sum over the exiting probabilities ValueType exitProbabilitySum = storm::utility::zero(); - for (auto const& transition : transitions.getRow(choice)) { + for (auto const& transition : modelTransitions.getRow(choice)) { if (!mec.containsState(transition.getColumn())) { exitProbabilitySum += transition.getValue(); } @@ -442,7 +419,7 @@ namespace storm { minExitProbability = std::min(minExitProbability, exitProbabilitySum); } else { // Get the minimum over all transition probabilities - for (auto const& transition : transitions.getRow(choice)) { + for (auto const& transition : modelTransitions.getRow(choice)) { if (!storm::utility::isZero(transition.getValue())) { minProb = std::min(minProb, transition.getValue()); } diff --git a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp index 21bc8fe7a..349b68ce1 100644 --- a/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp +++ b/src/storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.cpp @@ -306,7 +306,13 @@ namespace storm { GeometryValueType epsScalingFactor = storm::utility::convertNumber(env.modelchecker().multi().getPrecision()); epsScalingFactor += epsScalingFactor; epsScalingFactor = epsScalingFactor / storm::utility::convertNumber(pointset.size()); - storm::utility::vector::scaleVectorInPlace(eps, epsScalingFactor); + for (auto& ei : eps) { + if (storm::utility::isZero(ei)) { + // This is for the special case where the objective value was zero for all considered schedulers in the initialization phase. + ei = storm::utility::convertNumber(1e-8); + } + ei *=epsScalingFactor; + } std::cout << "scaled precision is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(eps)) << std::endl; while (!unprocessedFacets.empty()) {