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 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::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()); minMaxSolver->setUpperBound(storm::utility::one()); 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