From b788c1b403d6645bc2ecb9ea382223c4e8acd362 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 4 Oct 2017 16:34:44 +0200
Subject: [PATCH] reuse scheduler from previous epoch as initial hint
---
.../pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp | 7 +++++--
.../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 4 ++++
2 files changed, 9 insertions(+), 2 deletions(-)
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
index 3bad88500..f2ce81b87 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
@@ -97,6 +97,8 @@ namespace storm {
// Check whether the linear equation solver needs to be updated
auto const& choices = cachedData.minMaxSolver->getSchedulerChoices();
if (cachedData.schedulerChoices != choices) {
+ std::vector<uint64_t> choicesTmp = choices;
+ cachedData.minMaxSolver->setInitialScheduler(std::move(choicesTmp));
swAux2.start();
++numSchedChanges;
cachedData.schedulerChoices = choices;
@@ -204,8 +206,9 @@ namespace storm {
cachedData.minMaxSolver->setRequirementsChecked(true);
cachedData.minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
- // Set the scheduler choices to invalid choice indices so that an update of the linEqSolver is enforced
- cachedData.schedulerChoices.assign(epochModel.epochMatrix.getRowGroupCount(), std::numeric_limits<uint64_t>::max());
+ // Clear the scheduler choices so that an update of the linEqSolver is enforced
+ cachedData.schedulerChoices.clear();
+ cachedData.schedulerChoices.reserve(epochModel.epochMatrix.getRowGroupCount());
// Update data for linear equation solving
cachedData.bLinEq.resize(epochModel.epochMatrix.getRowGroupCount());
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 6a7fbab1b..d3a37de46 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -92,6 +92,7 @@ namespace storm {
minMaxSolver = minMaxLinearEquationSolverFactory.create(epochModel.epochMatrix);
minMaxSolver->setOptimizationDirection(dir);
minMaxSolver->setCachingEnabled(true);
+ minMaxSolver->setTrackScheduler(true);
minMaxSolver->setLowerBound(storm::utility::zero<ValueType>());
minMaxSolver->setUpperBound(storm::utility::one<ValueType>());
auto req = minMaxSolver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath, dir);
@@ -99,6 +100,9 @@ namespace storm {
req.clearBounds();
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "A solver requirement is not satisfied.");
minMaxSolver->setRequirementsChecked();
+ } else {
+ auto choicesTmp = minMaxSolver->getSchedulerChoices();
+ minMaxSolver->setInitialScheduler(std::move(choicesTmp));
}
// Prepare the right hand side of the equation system