diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 91ff99c8a..adaed4627 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -24,6 +24,7 @@ #include "storm/solver/LpSolver.h" #include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/settings/modules/MinMaxEquationSolverSettings.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" @@ -845,7 +846,14 @@ namespace storm { [&rewardModel] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); }, - targetStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory, hint); + targetStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory, + [&] () { + return rewardModel.getStatesWithZeroReward(transitionMatrix); + }, + [&] () { + return rewardModel.getChoicesWithZeroReward(transitionMatrix); + }, + hint); } #ifdef STORM_HAVE_CARL @@ -862,8 +870,14 @@ namespace storm { result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper()); } return result; - }, \ - targetStates, qualitative, false, minMaxLinearEquationSolverFactory).values; + }, + targetStates, qualitative, false, minMaxLinearEquationSolverFactory, + [&] () { + return intervalRewardModel.getStatesWithFilter(transitionMatrix, [&](storm::Interval const& i) {return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper());}); + }, + [&] () { + return intervalRewardModel.getChoicesWithFilter(transitionMatrix, [&](storm::Interval const& i) {return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper());}); + }).values; } template<> @@ -875,18 +889,32 @@ namespace storm { struct QualitativeStateSetsReachabilityRewards { storm::storage::BitVector maybeStates; storm::storage::BitVector infinityStates; + storm::storage::BitVector rewardZeroStates; }; template QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewardsFromHint(ModelCheckerHint const& hint, storm::storage::BitVector const& targetStates) { QualitativeStateSetsReachabilityRewards result; result.maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); - result.infinityStates = ~(result.maybeStates | targetStates); + + // Treat the states with reward zero/infinity. + std::vector const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint().getResultHint(); + result.infinityStates = storm::storage::BitVector(result.maybeStates.size()); + result.rewardZeroStates = storm::storage::BitVector(result.maybeStates.size()); + storm::storage::BitVector nonMaybeStates = ~result.maybeStates; + for (auto const& state : nonMaybeStates) { + if (storm::utility::isZero(resultsForNonMaybeStates[state])) { + result.rewardZeroStates.set(state, true); + } else { + STORM_LOG_THROW(storm::utility::isInfinity(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException, "Expected that the result hint specifies probabilities in {0,infinity} for non-maybe states"); + result.infinityStates.set(state, true); + } + } return result; } template - QualitativeStateSetsReachabilityRewards computeQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates) { + QualitativeStateSetsReachabilityRewards computeQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, std::function const& zeroRewardStatesGetter, std::function const& zeroRewardChoicesGetter) { QualitativeStateSetsReachabilityRewards result; storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true); if (goal.minimize()) { @@ -895,33 +923,43 @@ namespace storm { result.infinityStates = storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates); } result.infinityStates.complement(); - result.maybeStates = ~(targetStates | result.infinityStates); + + if (storm::settings::getModule().isFilterRewZeroSet()) { + if (goal.minimize()) { + result.rewardZeroStates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates, zeroRewardChoicesGetter()); + } else { + result.rewardZeroStates = storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, zeroRewardStatesGetter(), targetStates); + } + } else { + result.rewardZeroStates = targetStates; + } + result.maybeStates = ~(result.rewardZeroStates | result.infinityStates); return result; } template - QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, ModelCheckerHint const& hint) { + QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, ModelCheckerHint const& hint, std::function const& zeroRewardStatesGetter, std::function const& zeroRewardChoicesGetter) { if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { return getQualitativeStateSetsReachabilityRewardsFromHint(hint, targetStates); } else { - return computeQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates); + return computeQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates, zeroRewardStatesGetter, zeroRewardChoicesGetter); } } template - void extendScheduler(storm::storage::Scheduler& scheduler, storm::solver::SolveGoal const& goal, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& targetStates) { + void extendScheduler(storm::storage::Scheduler& scheduler, storm::solver::SolveGoal const& goal, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, std::function const& zeroRewardChoicesGetter) { // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for - // the states with reward infinity. Moreover, we have to set some arbitrary choice for the remaining states - // to obtain a fully defined scheduler. - if (!goal.minimize()) { - storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.infinityStates, transitionMatrix, scheduler); - } else { + // the states with reward zero/infinity. + if (goal.minimize()) { + storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.rewardZeroStates, transitionMatrix, backwardTransitions, qualitativeStateSets.rewardZeroStates, targetStates, scheduler, zeroRewardChoicesGetter()); for (auto const& state : qualitativeStateSets.infinityStates) { scheduler.setChoice(0, state); } - } - for (auto const& state : targetStates) { - scheduler.setChoice(0, state); + } else { + storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.infinityStates, transitionMatrix, scheduler); + for (auto const& state : qualitativeStateSets.rewardZeroStates) { + scheduler.setChoice(0, state); + } } } @@ -949,21 +987,21 @@ namespace storm { } template - void computeFixedPointSystemReachabilityRewards(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::BitVector const& targetStates, 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, std::vector* oneStepTargetProbabilities = nullptr) { + void computeFixedPointSystemReachabilityRewards(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, 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, std::vector* oneStepTargetProbabilities = nullptr) { // Remove rows and columns from the original transition probability matrix for states whose reward values are already known. // If there are infinity states, we additionally have to remove choices of maybeState that lead to infinity. if (qualitativeStateSets.infinityStates.empty()) { submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false); b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, qualitativeStateSets.maybeStates); if (oneStepTargetProbabilities) { - (*oneStepTargetProbabilities) = transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, targetStates); + (*oneStepTargetProbabilities) = transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, qualitativeStateSets.rewardZeroStates); } } else { submatrix = transitionMatrix.getSubmatrix(false, *selectedChoices, qualitativeStateSets.maybeStates, false); b = totalStateRewardVectorGetter(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); storm::utility::vector::filterVectorInPlace(b, *selectedChoices); if (oneStepTargetProbabilities) { - (*oneStepTargetProbabilities) = transitionMatrix.getConstrainedRowSumVector(*selectedChoices, targetStates); + (*oneStepTargetProbabilities) = transitionMatrix.getConstrainedRowSumVector(*selectedChoices, qualitativeStateSets.rewardZeroStates); } } @@ -972,7 +1010,7 @@ namespace storm { } template - boost::optional> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::BitVector const& targetStates, 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) { // Start by computing the choices with reward 0, as we only want ECs within this fragment. storm::storage::BitVector zeroRewardChoices(transitionMatrix.getRowCount()); @@ -1019,7 +1057,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 ? &targetStates : 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); // If the solve goal has relevant values, we need to adjust them. if (goal.hasRelevantValues()) { @@ -1037,7 +1075,7 @@ namespace storm { return result; } else { STORM_LOG_DEBUG("Not eliminating ECs as there are none."); - computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, targetStates, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr); + computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr); return boost::none; } } @@ -1056,15 +1094,15 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewardsHelper(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewardsHelper(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, std::function const& zeroRewardStatesGetter, std::function const& zeroRewardChoicesGetter, ModelCheckerHint const& hint) { // Prepare resulting vector. std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // Determine which states have a reward that is infinity or less than infinity. - QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates, hint); + QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates, hint, zeroRewardStatesGetter, zeroRewardChoicesGetter); - STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.infinityStates.getNumberOfSetBits() << " states with reward infinity, " << targetStates.getNumberOfSetBits() << " target states (" << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining)."); + STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.infinityStates.getNumberOfSetBits() << " states with reward infinity, " << qualitativeStateSets.rewardZeroStates.getNumberOfSetBits() << " states with reward zero (" << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining)."); storm::utility::vector::setVectorValues(result, qualitativeStateSets.infinityStates, storm::utility::infinity()); @@ -1091,7 +1129,7 @@ namespace storm { } // Obtain proper hint information either from the provided hint or from requirements of the solver. - SparseMdpHintType hintInformation = computeHints(env, SolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices); + SparseMdpHintType hintInformation = computeHints(env, SolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, minMaxLinearEquationSolverFactory, selectedChoices); // Declare the components of the equation system we will solve. storm::storage::SparseMatrix submatrix; @@ -1107,13 +1145,13 @@ 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, targetStates, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities); + 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."); } else { // Otherwise, we compute the standard equations. - computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, targetStates, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr); + computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr); } // If we need to compute upper bounds, do so now. @@ -1141,7 +1179,7 @@ namespace storm { // Extend scheduler with choices for the states in the qualitative state sets. if (produceScheduler) { - extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, targetStates); + extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, targetStates, zeroRewardChoicesGetter); } // Sanity check for created scheduler. diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index b06b14192..5a6f5ae2b 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -71,7 +71,7 @@ namespace storm { static std::unique_ptr computeConditionalProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: - static MDPSparseModelCheckingHelperReturnType computeReachabilityRewardsHelper(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + static MDPSparseModelCheckingHelperReturnType computeReachabilityRewardsHelper(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, std::function const& zeroRewardStatesGetter, std::function const& zeroRewardChoicesGetter, ModelCheckerHint const& hint = ModelCheckerHint()); template static ValueType computeLraForMaximalEndComponent(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index ccf9b5d71..e37de0562 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -270,11 +270,17 @@ namespace storm { template template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const { - storm::storage::BitVector result = this->hasStateRewards() ? storm::utility::vector::filterZero(this->getStateRewardVector()) : storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); + return getStatesWithFilter(transitionMatrix, storm::utility::isZero); + } + + template + template + storm::storage::BitVector StandardRewardModel::getStatesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const { + storm::storage::BitVector result = this->hasStateRewards() ? storm::utility::vector::filter(this->getStateRewardVector(), filter) : storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); if (this->hasStateActionRewards()) { for (uint_fast64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { for (uint_fast64_t row = transitionMatrix.getRowGroupIndices()[state]; row < transitionMatrix.getRowGroupIndices()[state+1]; ++row) { - if(!storm::utility::isZero(this->getStateActionRewardVector()[row])) { + if(!filter(this->getStateActionRewardVector()[row])) { result.set(state, false); break; } @@ -284,7 +290,7 @@ namespace storm { if (this->hasTransitionRewards()) { for (uint_fast64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { for (auto const& rewardMatrixEntry : this->getTransitionRewardMatrix().getRowGroup(state)) { - if(!storm::utility::isZero(rewardMatrixEntry.getValue())) { + if(!filter(rewardMatrixEntry.getValue())) { result.set(state, false); break; } @@ -293,19 +299,25 @@ namespace storm { } return result; } - + template template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const { + return getChoicesWithFilter(transitionMatrix, storm::utility::isZero); + } + + template + template + storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const { storm::storage::BitVector result; if (this->hasStateActionRewards()) { - result = storm::utility::vector::filterZero(this->getStateActionRewardVector()); + result = storm::utility::vector::filter(this->getStateActionRewardVector(), filter); if (this->hasStateRewards()) { - result &= transitionMatrix.getRowFilter(storm::utility::vector::filterZero(this->getStateRewardVector())); + result &= transitionMatrix.getRowFilter(storm::utility::vector::filter(this->getStateRewardVector(), filter)); } } else { if (this->hasStateRewards()) { - result = transitionMatrix.getRowFilter(storm::utility::vector::filterZero(this->getStateRewardVector())); + result = transitionMatrix.getRowFilter(storm::utility::vector::filter(this->getStateRewardVector(), filter)); } else { result = storm::storage::BitVector(transitionMatrix.getRowCount(), true); } @@ -313,7 +325,7 @@ namespace storm { if (this->hasTransitionRewards()) { for (uint_fast64_t row = 0; row < transitionMatrix.getRowCount(); ++row) { for (auto const& rewardMatrixEntry : this->getTransitionRewardMatrix().getRow(row)) { - if(!storm::utility::isZero(rewardMatrixEntry.getValue())) { + if(!filter(rewardMatrixEntry.getValue())) { result.set(row, false); break; } @@ -396,7 +408,9 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getStatesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template double StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); @@ -421,7 +435,9 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getStatesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template storm::RationalNumber StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); @@ -433,7 +449,9 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getStatesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::RationalFunction StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const; @@ -447,6 +465,8 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; + template storm::storage::BitVector StandardRewardModel::getStatesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; + template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index 33303f380..cdfce6038 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -253,6 +253,13 @@ namespace storm { template storm::storage::BitVector getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; + /*! + * Returns the set of states for which all associated rewards (state, action or transition rewards) satisfy the given filter. + * @param transitionMatrix the transition matrix of the model (used to determine the actions and transitions that belong to a state) + */ + template + storm::storage::BitVector getStatesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; + /*! * Returns the set of choices at which all rewards (state-, action- and transition-rewards) are zero. * @@ -261,7 +268,14 @@ namespace storm { */ template storm::storage::BitVector getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; - + + /*! + * Returns the set of choices for which all associated rewards (state, action or transition rewards) satisfy the given filter. + * @param transitionMatrix the transition matrix of the model (used to determine the actions and transitions that belong to a state) + */ + template + storm::storage::BitVector getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; + /*! * Sets the given value in the state-action reward vector at the given row. This assumes that the reward * model has state-action rewards. diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index a2716ba8d..5bb8cc758 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -479,9 +479,9 @@ namespace storm { } template - void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler) { + void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter) { - // set an arbitrary choice for the psi states. + // set an arbitrary (valid) choice for the psi states. for (auto const& psiState : psiStates) { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { scheduler.setChoice(0, psiState, memState); @@ -504,27 +504,29 @@ namespace storm { // Check whether the predecessor has only successors in the prob1E state set for one of the // nondeterminstic choices. for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { - bool allSuccessorsInProb1EStates = true; - bool hasSuccessorInCurrentStates = false; - for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { - if (!prob1EStates.get(successorEntryIt->getColumn())) { - allSuccessorsInProb1EStates = false; + if (!rowFilter || rowFilter.get().get(row)) { + bool allSuccessorsInProb1EStates = true; + bool hasSuccessorInCurrentStates = false; + for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { + if (!prob1EStates.get(successorEntryIt->getColumn())) { + allSuccessorsInProb1EStates = false; + break; + } else if (currentStates.get(successorEntryIt->getColumn())) { + hasSuccessorInCurrentStates = true; + } + } + + // If all successors for a given nondeterministic choice are in the prob1E state set, we + // perform a backward search from that state. + if (allSuccessorsInProb1EStates && hasSuccessorInCurrentStates) { + for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { + scheduler.setChoice(row - nondeterministicChoiceIndices[predecessorEntryIt->getColumn()], predecessorEntryIt->getColumn(), memState); + } + currentStates.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); break; - } else if (currentStates.get(successorEntryIt->getColumn())) { - hasSuccessorInCurrentStates = true; } } - - // If all successors for a given nondeterministic choice are in the prob1E state set, we - // perform a backward search from that state. - if (allSuccessorsInProb1EStates && hasSuccessorInCurrentStates) { - for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { - scheduler.setChoice(row - nondeterministicChoiceIndices[predecessorEntryIt->getColumn()], predecessorEntryIt->getColumn(), memState); - } - currentStates.set(predecessorEntryIt->getColumn(), true); - stack.push_back(predecessorEntryIt->getColumn()); - break; - } } } } @@ -595,7 +597,7 @@ namespace storm { } template - storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& choiceConstraint) { size_t numberOfStates = phiStates.size(); // Initialize the environment for the iterative algorithm. @@ -620,25 +622,27 @@ namespace storm { // Check whether the predecessor has only successors in the current state set for one of the // nondeterminstic choices. for (uint_fast64_t row = nondeterministicChoiceIndices[predecessorEntryIt->getColumn()]; row < nondeterministicChoiceIndices[predecessorEntryIt->getColumn() + 1]; ++row) { - bool allSuccessorsInCurrentStates = true; - bool hasNextStateSuccessor = false; - for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { - if (!currentStates.get(successorEntryIt->getColumn())) { - allSuccessorsInCurrentStates = false; + if (!choiceConstraint || choiceConstraint.get().get(row)) { + bool allSuccessorsInCurrentStates = true; + bool hasNextStateSuccessor = false; + for (typename storm::storage::SparseMatrix::const_iterator successorEntryIt = transitionMatrix.begin(row), successorEntryIte = transitionMatrix.end(row); successorEntryIt != successorEntryIte; ++successorEntryIt) { + if (!currentStates.get(successorEntryIt->getColumn())) { + allSuccessorsInCurrentStates = false; + break; + } else if (nextStates.get(successorEntryIt->getColumn())) { + hasNextStateSuccessor = true; + } + } + + // If all successors for a given nondeterministic choice are in the current state set, we + // add it to the set of states for the next iteration and perform a backward search from + // that state. + if (allSuccessorsInCurrentStates && hasNextStateSuccessor) { + nextStates.set(predecessorEntryIt->getColumn(), true); + stack.push_back(predecessorEntryIt->getColumn()); break; - } else if (nextStates.get(successorEntryIt->getColumn())) { - hasNextStateSuccessor = true; } } - - // If all successors for a given nondeterministic choice are in the current state set, we - // add it to the set of states for the next iteration and perform a backward search from - // that state. - if (allSuccessorsInCurrentStates && hasNextStateSuccessor) { - nextStates.set(predecessorEntryIt->getColumn(), true); - stack.push_back(predecessorEntryIt->getColumn()); - break; - } } } } @@ -1381,13 +1385,13 @@ namespace storm { template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); - template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler); + template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& choiceConstraint = boost::none); template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1446,13 +1450,13 @@ namespace storm { template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::Scheduler& scheduler); - template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler); + template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& choiceConstraint = boost::none); template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -1503,7 +1507,7 @@ namespace storm { template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& choiceConstraint = boost::none); template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 0f9b3c66e..79103700b 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -297,9 +297,10 @@ namespace storm { * @param phiStates The set of states satisfying phi. * @param psiStates The set of states satisfying psi. * @param scheduler The resulting scheduler for the prob1EStates. The scheduler is not set at the remaining states. + * @param rowFilter If given, only scheduler choices within this filter are taken. This filter is ignored for the psiStates. */ template - void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler); + void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler& scheduler, boost::optional const& rowFilter = boost::none); /*! * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least @@ -330,10 +331,11 @@ namespace storm { * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. + * @param choiceConstraint If given, only the selected choices are considered. * @return A bit vector that represents all states with probability 1. */ template - storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); + storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& choiceConstraint = boost::none); /*! * Computes the sets of states that have probability 1 of satisfying phi until psi under at least