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

reward infinity scheduler extraction is now correct

tempestpy_adaptions
Sebastian Junges 6 years ago
parent
93ca559c83
commit
43688d09ea
3 changed files with 26 additions and 3 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. 2
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  2. 13
      src/storm/utility/graph.cpp
  3. 10
      src/storm/utility/graph.h

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

@ -1053,7 +1053,7 @@ namespace storm {
scheduler.setChoice(0, state);
}
} else {
storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.infinityStates, transitionMatrix, scheduler);
storm::utility::graph::computeSchedulerRewInf(qualitativeStateSets.infinityStates, transitionMatrix, scheduler);
for (auto const& state : qualitativeStateSets.rewardZeroStates) {
scheduler.setChoice(0, state);
}

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

@ -429,6 +429,7 @@ namespace storm {
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
for (auto const& state : states) {
bool setValue = false;
for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
bool oneSuccessorInStates = false;
for (auto const& element : transitionMatrix.getRow(choice)) {
@ -441,9 +442,11 @@ namespace storm {
for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) {
scheduler.setChoice(choice - nondeterministicChoiceIndices[state], state, memState);
}
setValue = true;
break;
}
}
STORM_LOG_ASSERT(setValue, "Expected that at least one action for state " << state << " leads with positive probability to the selected state");
}
}
@ -495,6 +498,11 @@ namespace storm {
computeSchedulerStayingInStates(prob0EStates, transitionMatrix, scheduler);
}
template <typename T>
void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::Scheduler<T>& scheduler) {
computeSchedulerWithOneSuccessorInStates(rewInfStates, transitionMatrix, scheduler);
}
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, boost::optional<storm::storage::BitVector> const& rowFilter) {
@ -1666,6 +1674,9 @@ namespace storm {
template void computeSchedulerProb0E(storm::storage::BitVector const& prob0EStates, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::Scheduler<double>& scheduler);
template void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, 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, 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) ;
@ -1735,6 +1746,8 @@ 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 computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, 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, 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) ;

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

@ -284,6 +284,16 @@ namespace storm {
template <typename T>
void computeSchedulerProbGreater0E(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 a scheduler for the given states that have a scheduler that has a reward infinity.
*
* @param rewInfStates The states that have a scheduler achieving reward infinity.
* @param transitionMatrix The transition matrix of the system.
* @param scheduler The resulting scheduler for the rewInf States. The scheduler is not set at other states.
*/
template <typename T>
void computeSchedulerRewInf(storm::storage::BitVector const& rewInfStates, storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::Scheduler<T>& scheduler);
/*!
* Computes a scheduler for the given states that have a scheduler that has a probability 0.
*

Write Preview
Loading…
Cancel
Save