From af8f901d4a16950d06c254a59542c1e684c70aa8 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 8 Apr 2020 17:06:09 +0200 Subject: [PATCH] Properly produce schedulers for models with end components. --- .../SparseMdpEndComponentInformation.cpp | 76 ++++++++++++++++--- .../helper/SparseMdpEndComponentInformation.h | 9 ++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 38 +++++----- 3 files changed, 92 insertions(+), 31 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp index 62dba3778..8db9a6c75 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp @@ -2,6 +2,8 @@ #include "storm/storage/BitVector.h" #include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/storage/Scheduler.h" +#include "storm/utility/graph.h" #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -11,7 +13,7 @@ namespace storm { namespace helper { template - SparseMdpEndComponentInformation::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits::max()), eliminatedEndComponents(false), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) { + SparseMdpEndComponentInformation::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits::max()), eliminatedEndComponents(!endComponentDecomposition.empty()), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) { // (1) Compute how many maybe states there are before each other maybe state. maybeStatesBefore = maybeStates.getNumberOfSetBitsBeforeIndices(); @@ -90,7 +92,7 @@ namespace storm { } template - SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector) { + SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector, bool gatherExitChoices) { SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); @@ -163,7 +165,7 @@ namespace storm { // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs. for (auto const& mec : endComponentDecomposition) { builder.newRowGroup(currentRow); - + std::vector exitChoices; for (auto const& stateActions : mec) { uint64_t const& state = stateActions.first; for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { @@ -207,9 +209,16 @@ namespace storm { } } + if (gatherExitChoices) { + exitChoices.push_back(row); + } + ++currentRow; } } + if (gatherExitChoices) { + result.ecToExitChoicesBefore.push_back(std::move(exitChoices)); + } } submatrix = builder.build(currentRow); @@ -217,7 +226,7 @@ namespace storm { } template - SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector) { + SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector, bool gatherExitChoices) { SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); @@ -271,7 +280,7 @@ namespace storm { // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs. for (auto const& mec : endComponentDecomposition) { builder.newRowGroup(currentRow); - + std::vector exitChoices; for (auto const& stateActions : mec) { uint64_t const& state = stateActions.first; for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { @@ -304,9 +313,16 @@ namespace storm { } } + if (gatherExitChoices) { + exitChoices.push_back(row); + } + ++currentRow; } } + if (gatherExitChoices) { + result.ecToExitChoicesBefore.push_back(std::move(exitChoices)); + } } submatrix = builder.build(); @@ -315,23 +331,65 @@ namespace storm { template void SparseMdpEndComponentInformation::setValues(std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult) { - auto notInEcResultIt = result.begin(); + // The following assumes that row groups associated to EC states are at the very end. + auto notInEcResultIt = fromResult.begin(); for (auto state : maybeStates) { if (this->isStateInEc(state)) { - result[state] = result[this->getRowGroupAfterElimination(state)]; + STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix."); + result[state] = fromResult[this->getRowGroupAfterElimination(state)]; } else { result[state] = *notInEcResultIt; ++notInEcResultIt; } } - STORM_LOG_ASSERT(notInEcResultIt == result.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators."); + STORM_LOG_ASSERT(notInEcResultIt == fromResult.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators."); + } + + template + void SparseMdpEndComponentInformation::setScheduler(storm::storage::Scheduler& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& fromResult) { + // The following assumes that row groups associated to EC states are at the very end. + storm::storage::BitVector maybeStatesWithoutChoice(maybeStates.size(), false); + storm::storage::BitVector ecStayChoices(transitionMatrix.getRowCount(), false); + auto notInEcResultIt = fromResult.begin(); + for (auto const& state : maybeStates) { + if (this->isStateInEc(state)) { + STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix."); + STORM_LOG_ASSERT(!ecToExitChoicesBefore.empty(), "No EC exit choices available. End Components have probably been build without."); + uint64_t ec = getEc(state); + auto const& exitChoices = ecToExitChoicesBefore[ec]; + uint64_t afterEliminationChoice = fromResult[this->getRowGroupAfterElimination(state)]; + uint64_t beforeEliminationGlobalChoiceIndex = exitChoices[afterEliminationChoice]; + bool noChoice = true; + for (uint64_t globalChoice = transitionMatrix.getRowGroupIndices()[state]; globalChoice < transitionMatrix.getRowGroupIndices()[state+1]; ++globalChoice) { + // Is this the selected exit choice? + if (globalChoice == beforeEliminationGlobalChoiceIndex) { + scheduler.setChoice(beforeEliminationGlobalChoiceIndex - transitionMatrix.getRowGroupIndices()[state], state); + noChoice = false; + } else { + // Check if this is an exit choice + if (std::find(exitChoices.begin(), exitChoices.end(), globalChoice) == exitChoices.end()) { + ecStayChoices.set(globalChoice, true); + } + } + } + maybeStatesWithoutChoice.set(state, noChoice); + } else { + scheduler.setChoice(*notInEcResultIt, state); + ++notInEcResultIt; + } + } + + STORM_LOG_ASSERT(notInEcResultIt == fromResult.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators."); + // The maybeStates without a choice shall reach maybeStates with a choice with probability 1 + storm::utility::graph::computeSchedulerProb1E(maybeStates, transitionMatrix, backwardTransitions, maybeStatesWithoutChoice, ~maybeStatesWithoutChoice, scheduler, ecStayChoices); + } template class SparseMdpEndComponentInformation; #ifdef STORM_HAVE_CARL template class SparseMdpEndComponentInformation; - template class SparseMdpEndComponentInformation; + //template class SparseMdpEndComponentInformation; #endif } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h index 513ffb49c..f93fb8dce 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h @@ -12,6 +12,9 @@ namespace storm { template class MaximalEndComponentDecomposition; + + template + class Scheduler; } namespace modelchecker { @@ -50,11 +53,12 @@ namespace storm { uint64_t getNotInEcMarker() const; - static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector); + static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector, bool gatherExitChoices = false); - static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector); + static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector, bool gatherExitChoices = false); void setValues(std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult); + void setScheduler(storm::storage::Scheduler& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& fromResult); private: // A constant that marks that a state is not contained in any EC. @@ -70,6 +74,7 @@ namespace storm { uint64_t numberOfMaybeStatesNotInEc; uint64_t numberOfEc; std::vector maybeStateToEc; + std::vector> ecToExitChoicesBefore; // Only available, if gatherExitChoices was enabled. Empty otherwise. }; } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 174cf739f..1e9722d7a 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -583,7 +583,7 @@ namespace storm { } template - boost::optional> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix& submatrix, std::vector& b) { + boost::optional> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix& submatrix, std::vector& b, bool produceScheduler) { // Get the set of states that (under some scheduler) can stay in the set of maybestates forever storm::storage::BitVector candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.maybeStates); @@ -599,7 +599,7 @@ namespace storm { // Only do more work if there are actually end-components. if (doDecomposition && !endComponentDecomposition.empty()) { STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s)."); - SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr); + SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr, produceScheduler); // If the solve goal has relevant values, we need to adjust them. if (goal.hasRelevantValues()) { @@ -663,10 +663,7 @@ namespace storm { // If the hint information tells us that we have to eliminate MECs, we do so now. boost::optional> ecInformation; if (hintInformation.getEliminateEndComponents()) { - ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b); - - // Make sure we are not supposed to produce a scheduler if we actually eliminate end components. - STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver."); + ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b, produceScheduler); } else { // Otherwise, we compute the standard equations. computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b); @@ -678,13 +675,15 @@ namespace storm { // If we eliminated end components, we need to extract the result differently. if (ecInformation && ecInformation.get().getEliminatedEndComponents()) { ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); + if (produceScheduler) { + ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler()); + } } else { // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); - } - - if (produceScheduler) { - extractSchedulerChoices(*scheduler, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates); + if (produceScheduler) { + extractSchedulerChoices(*scheduler, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates); + } } } } @@ -1028,7 +1027,7 @@ namespace storm { } template - boost::optional> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional const& selectedChoices, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix& submatrix, std::vector& b, boost::optional>& oneStepTargetProbabilities) { + boost::optional> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional const& selectedChoices, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix& submatrix, std::vector& b, boost::optional>& oneStepTargetProbabilities, bool produceScheduler) { // Start by computing the choices with reward 0, as we only want ECs within this fragment. storm::storage::BitVector zeroRewardChoices(transitionMatrix.getRowCount()); @@ -1075,7 +1074,7 @@ namespace storm { // Only do more work if there are actually end-components. if (doDecomposition && !endComponentDecomposition.empty()) { STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs."); - SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b); + SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b, produceScheduler); // If the solve goal has relevant values, we need to adjust them. if (goal.hasRelevantValues()) { @@ -1163,10 +1162,7 @@ namespace storm { // If the hint information tells us that we have to eliminate MECs, we do so now. boost::optional> ecInformation; if (hintInformation.getEliminateEndComponents()) { - ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities); - - // Make sure we are not supposed to produce a scheduler if we actually eliminate end components. - STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver."); + ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities, produceScheduler); } else { // Otherwise, we compute the standard equations. computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr); @@ -1184,13 +1180,15 @@ namespace storm { // If we eliminated end components, we need to extract the result differently. if (ecInformation && ecInformation.get().getEliminatedEndComponents()) { ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); + if (produceScheduler) { + ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler()); + } } else { // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); - } - - if (produceScheduler) { - extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates, selectedChoices); + if (produceScheduler) { + extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates, selectedChoices); + } } } }