From aa3a1f5ff7cfbe42bf54df11a48acb612c51a4d5 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 14 Mar 2019 13:42:23 +0100 Subject: [PATCH] Quantiles: Improved performance by excluding already analyzed epochs from the created epochSequences --- .../MultiDimensionalRewardUnfolding.cpp | 37 +++--------- .../MultiDimensionalRewardUnfolding.h | 11 ++-- .../helper/rewardbounded/QuantileHelper.cpp | 60 +++++++++---------- .../helper/rewardbounded/QuantileHelper.h | 1 + 4 files changed, 44 insertions(+), 65 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp index fad4feda2..5a1001b3d 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -64,8 +64,6 @@ namespace storm { template void MultiDimensionalRewardUnfolding::initialize(std::set const& infinityBoundVariables) { - maxSolutionsStored = 0; - STORM_LOG_ASSERT(!SingleObjectiveMode || (this->objectives.size() == 1), "Enabled single objective mode but there are multiple objectives."); std::vector epochSteps; initializeObjectives(epochSteps, infinityBoundVariables); @@ -333,41 +331,27 @@ namespace storm { } template - std::vector::Epoch> MultiDimensionalRewardUnfolding::getEpochComputationOrder(Epoch const& startEpoch) { + std::vector::Epoch> MultiDimensionalRewardUnfolding::getEpochComputationOrder(Epoch const& startEpoch, bool stopAtComputedEpochs) { // Perform a DFS to find all the reachable epochs std::vector dfsStack; std::set> collectedEpochs(std::bind(&EpochManager::epochClassZigZagOrder, &epochManager, std::placeholders::_1, std::placeholders::_2)); - collectedEpochs.insert(startEpoch); - dfsStack.push_back(startEpoch); + if (!stopAtComputedEpochs || epochSolutions.count(startEpoch) == 0) { + collectedEpochs.insert(startEpoch); + dfsStack.push_back(startEpoch); + } while (!dfsStack.empty()) { Epoch currentEpoch = dfsStack.back(); dfsStack.pop_back(); for (auto const& step : possibleEpochSteps) { Epoch successorEpoch = epochManager.getSuccessorEpoch(currentEpoch, step); - /* - for (auto const& e : collectedEpochs) { - std::cout << "Comparing " << epochManager.toString(e) << " and " << epochManager.toString(successorEpoch) << std::endl; - if (epochManager.epochClassZigZagOrder(e, successorEpoch)) { - std::cout << " " << epochManager.toString(e) << " < " << epochManager.toString(successorEpoch) << std::endl; - } - if (epochManager.epochClassZigZagOrder(successorEpoch, e)) { - std::cout << " " << epochManager.toString(e) << " > " << epochManager.toString(successorEpoch) << std::endl; + if (!stopAtComputedEpochs || epochSolutions.count(successorEpoch) == 0) { + if (collectedEpochs.insert(successorEpoch).second) { + dfsStack.push_back(std::move(successorEpoch)); } } - */ - if (collectedEpochs.insert(successorEpoch).second) { - dfsStack.push_back(std::move(successorEpoch)); - } } } - /* - std::cout << "Resulting order: "; - for (auto const& e : collectedEpochs) { - std::cout << epochManager.toString(e) << ", "; - } - std::cout << std::endl; - */ return std::vector(collectedEpochs.begin(), collectedEpochs.end()); } @@ -629,8 +613,6 @@ namespace storm { epochModel.objectiveRewardFilter.push_back(storm::utility::vector::filterZero(objRewards)); epochModel.objectiveRewardFilter.back().complement(); } - - epochModelSizes.push_back(epochModel.epochMatrix.getRowGroupCount()); } @@ -846,9 +828,6 @@ namespace storm { solution.productStateToSolutionVectorMap = productStateToEpochModelInStateMap; solution.solutions = std::move(inStateSolutions); epochSolutions[currentEpoch.get()] = std::move(solution); - - maxSolutionsStored = std::max((uint64_t) epochSolutions.size(), maxSolutionsStored); - } template diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h index 3844c1af7..db4eb2e6d 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -54,7 +54,11 @@ namespace storm { */ Epoch getStartEpoch(bool setUnknownDimsToBottom = false); - std::vector getEpochComputationOrder(Epoch const& startEpoch); + /*! + * Computes a sequence of epochs that need to be analyzed to get a result at the start epoch. + * @param stopAtComputedEpochs if set, the search for epochs that need to be computed is stopped at epochs that already have been computed earlier. + */ + std::vector getEpochComputationOrder(Epoch const& startEpoch, bool stopAtComputedEpochs = false); EpochModel& setCurrentEpoch(Epoch const& epoch); @@ -138,11 +142,6 @@ namespace storm { std::vector> dimensions; std::vector objectiveDimensions; - - - storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4; - std::vector epochModelSizes; - uint64_t maxSolutionsStored; }; } } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index c6bdda24e..ea7d5ad06 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -186,6 +186,7 @@ namespace storm { numCheckedEpochs = 0; numPrecisionRefinements = 0; swEpochAnalysis.reset(); + swExploration.reset(); cachedSubQueryResults.clear(); std::vector> result; @@ -217,7 +218,8 @@ namespace storm { if (storm::settings::getModule().isShowStatisticsSet()) { std::cout << "Number of checked epochs: " << numCheckedEpochs << std::endl; std::cout << "Number of required precision refinements: " << numPrecisionRefinements << std::endl; - std::cout << "Time for epoch model analysis: " << swEpochAnalysis << " seconds." << std::endl; + std::cout << "Time for epoch exploration: " << swExploration << " seconds." << std::endl; + std::cout << "\tTime for epoch model analysis: " << swEpochAnalysis << " seconds." << std::endl; } return result; } @@ -359,8 +361,7 @@ namespace storm { auto upperBound = rewardUnfolding.getUpperObjectiveBound(); std::vector x, b; std::unique_ptr> minMaxSolver; - std::set checkedEpochs; - + swExploration.start(); bool progress = true; for (CostLimit candidateCostLimitSum(0); progress; ++candidateCostLimitSum.get()) { CostLimits currentCandidate(satCostLimits.dimension(), CostLimit(0)); @@ -389,42 +390,41 @@ namespace storm { ++costLimitIt; } STORM_LOG_DEBUG("Checking start epoch " << rewardUnfolding.getEpochManager().toString(startEpoch) << "."); - auto epochSequence = rewardUnfolding.getEpochComputationOrder(startEpoch); + auto epochSequence = rewardUnfolding.getEpochComputationOrder(startEpoch, true); for (auto const& epoch : epochSequence) { - if (checkedEpochs.count(epoch) == 0) { - ++numCheckedEpochs; - swEpochAnalysis.start(); - checkedEpochs.insert(epoch); - auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); - rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env,boundedUntilOperator.getOptimalityType(), x, b, minMaxSolver, lowerBound, upperBound)); - swEpochAnalysis.stop(); + ++numCheckedEpochs; + swEpochAnalysis.start(); + auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); + rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env,boundedUntilOperator.getOptimalityType(), x, b, minMaxSolver, lowerBound, upperBound)); + swEpochAnalysis.stop(); - CostLimits epochAsCostLimits; - if (translateEpochToCostLimits(epoch, startEpoch, consideredDimensions, lowerBoundedDimensions, rewardUnfolding.getEpochManager(), epochAsCostLimits)) { - ValueType currValue = rewardUnfolding.getInitialStateResult(epoch); - bool propertySatisfied; - if (env.solver().isForceSoundness()) { - ValueType sumOfEpochDimensions = storm::utility::convertNumber(rewardUnfolding.getEpochManager().getSumOfDimensions(epoch) + 1); - auto lowerUpperValue = getLowerUpperBound(env, sumOfEpochDimensions, currValue); - propertySatisfied = boundedUntilOperator.getBound().isSatisfied(lowerUpperValue.first); - if (propertySatisfied != boundedUntilOperator.getBound().isSatisfied(lowerUpperValue.second)) { - // unclear result due to insufficient precision. - return false; - } - } else { - propertySatisfied = boundedUntilOperator.getBound().isSatisfied(currValue); - } - if (propertySatisfied) { - satCostLimits.insert(epochAsCostLimits); - } else { - unsatCostLimits.insert(epochAsCostLimits); + CostLimits epochAsCostLimits; + if (translateEpochToCostLimits(epoch, startEpoch, consideredDimensions, lowerBoundedDimensions, rewardUnfolding.getEpochManager(), epochAsCostLimits)) { + ValueType currValue = rewardUnfolding.getInitialStateResult(epoch); + bool propertySatisfied; + if (env.solver().isForceSoundness()) { + ValueType sumOfEpochDimensions = storm::utility::convertNumber(rewardUnfolding.getEpochManager().getSumOfDimensions(epoch) + 1); + auto lowerUpperValue = getLowerUpperBound(env, sumOfEpochDimensions, currValue); + propertySatisfied = boundedUntilOperator.getBound().isSatisfied(lowerUpperValue.first); + if (propertySatisfied != boundedUntilOperator.getBound().isSatisfied(lowerUpperValue.second)) { + // unclear result due to insufficient precision. + swExploration.stop(); + return false; } + } else { + propertySatisfied = boundedUntilOperator.getBound().isSatisfied(currValue); + } + if (propertySatisfied) { + satCostLimits.insert(epochAsCostLimits); + } else { + unsatCostLimits.insert(epochAsCostLimits); } } } } } while (getNextCandidateCostLimit(candidateCostLimitSum, currentCandidate)); } + swExploration.stop(); return true; } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h index 63a06e34e..e4377616d 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h @@ -53,6 +53,7 @@ namespace storm { mutable uint64_t numCheckedEpochs; mutable uint64_t numPrecisionRefinements; mutable storm::utility::Stopwatch swEpochAnalysis; + mutable storm::utility::Stopwatch swExploration; }; } }