diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index fcc9fa1c6..55358c68a 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -8,7 +8,6 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/solver/MinMaxLinearEquationSolver.h" -#include "storm/transformer/EndComponentEliminator.h" #include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -154,26 +153,14 @@ namespace storm { return; } - // Only consider the states from which a transition with non-zero reward is reachable. (The remaining states always have reward zero). - storm::storage::BitVector zeroRewardActions = storm::utility::vector::filterZero(weightedRewardVector); - storm::storage::BitVector nonZeroRewardActions = ~zeroRewardActions; - storm::storage::BitVector nonZeroRewardStates(this->model.getNumberOfStates(), false); - for(uint_fast64_t state = 0; state < this->model.getNumberOfStates(); ++state){ - if(nonZeroRewardActions.getNextSetIndex(this->model.getTransitionMatrix().getRowGroupIndices()[state]) < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]) { - nonZeroRewardStates.set(state); - } - } - storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(this->model.getTransitionMatrix().transpose(true), storm::storage::BitVector(this->model.getNumberOfStates(), true), nonZeroRewardStates); - - // Remove neutral end components, i.e., ECs in which no reward is earned. - auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(this->model.getTransitionMatrix(), subsystemStates, possibleECActions & zeroRewardActions, possibleBottomStates); + updateEcElimResult(weightedRewardVector); - std::vector subRewardVector(ecEliminatorResult.newToOldRowMapping.size()); - storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector); - std::vector subResult(ecEliminatorResult.matrix.getRowGroupCount()); + std::vector subRewardVector(cachedEcElimResult->newToOldRowMapping.size()); + storm::utility::vector::selectVectorValues(subRewardVector, cachedEcElimResult->newToOldRowMapping, weightedRewardVector); + std::vector subResult(cachedEcElimResult->matrix.getRowGroupCount()); storm::solver::GeneralMinMaxLinearEquationSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(ecEliminatorResult.matrix); + std::unique_ptr> solver = solverFactory.create(cachedEcElimResult->matrix); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->setTrackScheduler(true); if (lowerResultBound) { @@ -186,7 +173,7 @@ namespace storm { this->weightedResult = std::vector(this->model.getNumberOfStates()); - transformReducedSolutionToOriginalModel(ecEliminatorResult.matrix, subResult, solver->getSchedulerChoices(), ecEliminatorResult.newToOldRowMapping, ecEliminatorResult.oldToNewStateMapping, this->weightedResult, this->optimalChoices); + transformReducedSolutionToOriginalModel(cachedEcElimResult->matrix, subResult, solver->getSchedulerChoices(), cachedEcElimResult->newToOldRowMapping, cachedEcElimResult->oldToNewStateMapping, this->weightedResult, this->optimalChoices); } template @@ -274,6 +261,29 @@ namespace storm { } } + template + void SparsePcaaWeightVectorChecker::updateEcElimResult(std::vector const& weightedRewardVector) { + // Check whether we need to update the currently cached ecElimResult + storm::storage::BitVector newZeroRewardChoices = storm::utility::vector::filterZero(weightedRewardVector); + if (!cachedZeroRewardChoices || cachedZeroRewardChoices.get() != newZeroRewardChoices) { + cachedZeroRewardChoices = std::move(newZeroRewardChoices); + + // It is sufficient to consider the states from which a transition with non-zero reward is reachable. (The remaining states always have reward zero). + storm::storage::BitVector nonZeroRewardStates(this->model.getNumberOfStates(), false); + for (uint_fast64_t state = 0; state < this->model.getNumberOfStates(); ++state){ + if (cachedZeroRewardChoices->getNextUnsetIndex(this->model.getTransitionMatrix().getRowGroupIndices()[state]) < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]) { + nonZeroRewardStates.set(state); + } + } + storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(this->model.getTransitionMatrix().transpose(true), storm::storage::BitVector(this->model.getNumberOfStates(), true), nonZeroRewardStates); + + // Remove neutral end components, i.e., ECs in which no reward is earned. + cachedEcElimResult = storm::transformer::EndComponentEliminator::transform(this->model.getTransitionMatrix(), subsystemStates, possibleECActions & cachedZeroRewardChoices.get(), possibleBottomStates); + } + STORM_LOG_ASSERT(cachedEcElimResult, "Updating the ecElimResult was not successfull."); + } + + template void SparsePcaaWeightVectorChecker::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix const& reducedMatrix, std::vector const& reducedSolution, diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index 8eaf8a892..a30227066 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -3,6 +3,7 @@ #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/Scheduler.h" +#include "storm/transformer/EndComponentEliminator.h" #include "storm/modelchecker/multiobjective/Objective.h" #include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" #include "storm/utility/vector.h" @@ -90,6 +91,8 @@ namespace storm { */ virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) = 0; + void updateEcElimResult(std::vector const& weightedRewardVector); + /*! * Transforms the results of a min-max-solver that considers a reduced model (without end components) to a result for the original (unreduced) model */ @@ -127,6 +130,10 @@ namespace storm { std::vector offsetsToOverApproximation; // The scheduler choices that optimize the weighted rewards of undounded objectives. std::vector optimalChoices; + // Caches the result of the ec elimination (avoiding recomputations for each weightvector) + boost::optional::EndComponentEliminatorReturnType> cachedEcElimResult; + // Stores which choices are considered to have zero reward in the current cachedEcElimiResult. + boost::optional cachedZeroRewardChoices; };