sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

filtering reward zero states for MDPs

tempestpy_adaptions
TimQu 7 years ago
parent
a9f72198a0
commit
a1c10cac37
6 changed files with 162 additions and 84 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 98
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  2. 2
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
  3. 36
      src/storm/models/sparse/StandardRewardModel.cpp
  4. 16
      src/storm/models/sparse/StandardRewardModel.h
  5. 88
      src/storm/utility/graph.cpp
  6. 6
      src/storm/utility/graph.h

98
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -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<ValueType> 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<typename ValueType>
QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewardsFromHint(ModelCheckerHint const& hint, storm::storage::BitVector const& targetStates) {
QualitativeStateSetsReachabilityRewards result;
result.maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
result.infinityStates = ~(result.maybeStates | targetStates);
// Treat the states with reward zero/infinity.
std::vector<ValueType> const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().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<typename ValueType>
QualitativeStateSetsReachabilityRewards computeQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal<ValueType> const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates) {
QualitativeStateSetsReachabilityRewards computeQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal<ValueType> const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter, std::function<storm::storage::BitVector()> 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<storm::settings::modules::ModelCheckerSettings>().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<typename ValueType>
QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal<ValueType> const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, ModelCheckerHint const& hint) {
QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal<ValueType> const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, ModelCheckerHint const& hint, std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter, std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
return getQualitativeStateSetsReachabilityRewardsFromHint<ValueType>(hint, targetStates);
} else {
return computeQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates);
return computeQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates, zeroRewardStatesGetter, zeroRewardChoicesGetter);
}
}
template<typename ValueType>
void extendScheduler(storm::storage::Scheduler<ValueType>& scheduler, storm::solver::SolveGoal<ValueType> const& goal, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& targetStates) {
void extendScheduler(storm::storage::Scheduler<ValueType>& scheduler, storm::solver::SolveGoal<ValueType> const& goal, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, std::function<storm::storage::BitVector()> 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<typename ValueType>
void computeFixedPointSystemReachabilityRewards(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::BitVector const& targetStates, boost::optional<storm::storage::BitVector> const& selectedChoices, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, std::vector<ValueType>* oneStepTargetProbabilities = nullptr) {
void computeFixedPointSystemReachabilityRewards(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional<storm::storage::BitVector> const& selectedChoices, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, std::vector<ValueType>* 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<typename ValueType>
boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::BitVector const& targetStates, boost::optional<storm::storage::BitVector> const& selectedChoices, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, boost::optional<std::vector<ValueType>>& oneStepTargetProbabilities) {
boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional<storm::storage::BitVector> const& selectedChoices, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, boost::optional<std::vector<ValueType>>& 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<ValueType> result = SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &targetStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b);
SparseMdpEndComponentInformation<ValueType> result = SparseMdpEndComponentInformation<ValueType>::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<typename ValueType>
MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) {
MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter, std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter, ModelCheckerHint const& hint) {
// Prepare resulting vector.
std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
// 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<ValueType>());
@ -1091,7 +1129,7 @@ namespace storm {
}
// Obtain proper hint information either from the provided hint or from requirements of the solver.
SparseMdpHintType<ValueType> hintInformation = computeHints(env, SolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices);
SparseMdpHintType<ValueType> 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<ValueType> 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<SparseMdpEndComponentInformation<ValueType>> 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.

2
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
View File

@ -71,7 +71,7 @@ namespace storm {
static std::unique_ptr<CheckResult> computeConditionalProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
private:
static MDPSparseModelCheckingHelperReturnType<ValueType> computeReachabilityRewardsHelper(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
static MDPSparseModelCheckingHelperReturnType<ValueType> computeReachabilityRewardsHelper(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter, std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter, ModelCheckerHint const& hint = ModelCheckerHint());
template<typename RewardModelType>
static ValueType computeLraForMaximalEndComponent(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);

36
src/storm/models/sparse/StandardRewardModel.cpp
View File

@ -270,11 +270,17 @@ namespace storm {
template<typename ValueType>
template<typename MatrixValueType>
storm::storage::BitVector StandardRewardModel<ValueType>::getStatesWithZeroReward(storm::storage::SparseMatrix<MatrixValueType> 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<ValueType>);
}
template<typename ValueType>
template<typename MatrixValueType>
storm::storage::BitVector StandardRewardModel<ValueType>::getStatesWithFilter(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::function<bool(ValueType const&)> 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<typename ValueType>
template<typename MatrixValueType>
storm::storage::BitVector StandardRewardModel<ValueType>::getChoicesWithZeroReward(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
return getChoicesWithFilter(transitionMatrix, storm::utility::isZero<ValueType>);
}
template<typename ValueType>
template<typename MatrixValueType>
storm::storage::BitVector StandardRewardModel<ValueType>::getChoicesWithFilter(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::function<bool(ValueType const&)> 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<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template std::vector<double> StandardRewardModel<double>::getTotalActionRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& stateRewardWeights) const;
template storm::storage::BitVector StandardRewardModel<double>::getStatesWithZeroReward(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<double>::getStatesWithFilter(storm::storage::SparseMatrix<double> const& transitionMatrix, std::function<bool(double const&)> const& filter) const;
template storm::storage::BitVector StandardRewardModel<double>::getChoicesWithZeroReward(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<double>::getChoicesWithFilter(storm::storage::SparseMatrix<double> const& transitionMatrix, std::function<bool(double const&)> const& filter) const;
template double StandardRewardModel<double>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<double> const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const;
template void StandardRewardModel<double>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards, std::vector<double> const* weights);
@ -421,7 +435,9 @@ namespace storm {
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalActionRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& stateRewardWeights) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalNumber>::getStatesWithZeroReward(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalNumber>::getStatesWithFilter(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::function<bool(storm::RationalNumber const&)> const& filter) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalNumber>::getChoicesWithZeroReward(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalNumber>::getChoicesWithFilter(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::function<bool(storm::RationalNumber const&)> const& filter) const;
template storm::RationalNumber StandardRewardModel<storm::RationalNumber>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const;
template void StandardRewardModel<storm::RationalNumber>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, bool reduceToStateRewards, std::vector<storm::RationalNumber> const* weights);
template void StandardRewardModel<storm::RationalNumber>::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue);
@ -433,7 +449,9 @@ namespace storm {
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getStatesWithZeroReward(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getStatesWithFilter(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::function<bool(storm::RationalFunction const&)> const& filter) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getChoicesWithZeroReward(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getChoicesWithFilter(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::function<bool(storm::RationalFunction const&)> const& filter) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalActionRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& stateRewardWeights) const;
template storm::RationalFunction StandardRewardModel<storm::RationalFunction>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const;
@ -447,6 +465,8 @@ namespace storm {
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalActionRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& stateRewardWeights) const;
template storm::storage::BitVector StandardRewardModel<storm::Interval>::getStatesWithFilter(storm::storage::SparseMatrix<double> const& transitionMatrix, std::function<bool(storm::Interval const&)> const& filter) const;
template storm::storage::BitVector StandardRewardModel<storm::Interval>::getChoicesWithFilter(storm::storage::SparseMatrix<double> const& transitionMatrix, std::function<bool(storm::Interval const&)> const& filter) const;
template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue);
template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue);
template void StandardRewardModel<storm::Interval>::setStateReward(uint_fast64_t state, double const & newValue);

16
src/storm/models/sparse/StandardRewardModel.h
View File

@ -253,6 +253,13 @@ namespace storm {
template<typename MatrixValueType>
storm::storage::BitVector getStatesWithZeroReward(storm::storage::SparseMatrix<MatrixValueType> 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<typename MatrixValueType>
storm::storage::BitVector getStatesWithFilter(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::function<bool(ValueType const&)> 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<typename MatrixValueType>
storm::storage::BitVector getChoicesWithZeroReward(storm::storage::SparseMatrix<MatrixValueType> 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<typename MatrixValueType>
storm::storage::BitVector getChoicesWithFilter(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::function<bool(ValueType const&)> 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.

88
src/storm/utility/graph.cpp
View File

@ -479,9 +479,9 @@ namespace storm {
}
template <typename T>
void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<T>& scheduler) {
void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<T>& scheduler, boost::optional<storm::storage::BitVector> 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<T>::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<T>::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 <typename T>
storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> 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<T>::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<T>::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<double> const& transitionMatrix, storm::storage::Scheduler<double>& scheduler);
template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<double>& scheduler);
template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<double>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<double> 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<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& choiceConstraint = boost::none);
template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> 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<storm::RationalNumber> const& transitionMatrix, storm::storage::Scheduler<storm::RationalNumber>& scheduler);
template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<storm::RationalNumber>& scheduler);
template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<storm::RationalNumber>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<storm::RationalNumber> 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<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& choiceConstraint = boost::none);
template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::SparseMatrix<storm::RationalNumber> 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<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& choiceConstraint = boost::none);
template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);

6
src/storm/utility/graph.h
View File

@ -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 <typename T>
void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<T>& scheduler);
void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<T>& scheduler, boost::optional<storm::storage::BitVector> 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 <typename T>
storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& choiceConstraint = boost::none);
/*!
* Computes the sets of states that have probability 1 of satisfying phi until psi under at least

Write Preview
Loading…
Cancel
Save