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

Properly produce schedulers for models with end components.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
d098c2d27c
commit
af8f901d4a
3 changed files with 92 additions and 31 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. 76
      src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp
  2. 9
      src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h
  3. 30
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

76
src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp
View File

@ -2,6 +2,8 @@
#include "storm/storage/BitVector.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/Scheduler.h"
#include "storm/utility/graph.h"
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/adapters/RationalFunctionAdapter.h"
@ -11,7 +13,7 @@ namespace storm {
namespace helper {
template<typename ValueType>
SparseMdpEndComponentInformation<ValueType>::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits<uint64_t>::max()), eliminatedEndComponents(false), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) {
SparseMdpEndComponentInformation<ValueType>::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits<uint64_t>::max()), eliminatedEndComponents(!endComponentDecomposition.empty()), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) {
// (1) Compute how many maybe states there are before each other maybe state.
maybeStatesBefore = maybeStates.getNumberOfSetBitsBeforeIndices();
@ -90,7 +92,7 @@ namespace storm {
}
template<typename ValueType>
SparseMdpEndComponentInformation<ValueType> SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector<ValueType> const* summand, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>* columnSumVector, std::vector<ValueType>* summandResultVector) {
SparseMdpEndComponentInformation<ValueType> SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector<ValueType> const* summand, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>* columnSumVector, std::vector<ValueType>* summandResultVector, bool gatherExitChoices) {
SparseMdpEndComponentInformation<ValueType> result(endComponentDecomposition, maybeStates);
@ -163,7 +165,7 @@ namespace storm {
// (3) Create the parts of the submatrix and vector b that belong to states contained in ECs.
for (auto const& mec : endComponentDecomposition) {
builder.newRowGroup(currentRow);
std::vector<uint64_t> exitChoices;
for (auto const& stateActions : mec) {
uint64_t const& state = stateActions.first;
for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) {
@ -207,9 +209,16 @@ namespace storm {
}
}
if (gatherExitChoices) {
exitChoices.push_back(row);
}
++currentRow;
}
}
if (gatherExitChoices) {
result.ecToExitChoicesBefore.push_back(std::move(exitChoices));
}
}
submatrix = builder.build(currentRow);
@ -217,7 +226,7 @@ namespace storm {
}
template<typename ValueType>
SparseMdpEndComponentInformation<ValueType> SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& subvector) {
SparseMdpEndComponentInformation<ValueType> SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& subvector, bool gatherExitChoices) {
SparseMdpEndComponentInformation<ValueType> result(endComponentDecomposition, maybeStates);
@ -271,7 +280,7 @@ namespace storm {
// (3) Create the parts of the submatrix and vector b that belong to states contained in ECs.
for (auto const& mec : endComponentDecomposition) {
builder.newRowGroup(currentRow);
std::vector<uint64_t> exitChoices;
for (auto const& stateActions : mec) {
uint64_t const& state = stateActions.first;
for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) {
@ -304,9 +313,16 @@ namespace storm {
}
}
if (gatherExitChoices) {
exitChoices.push_back(row);
}
++currentRow;
}
}
if (gatherExitChoices) {
result.ecToExitChoicesBefore.push_back(std::move(exitChoices));
}
}
submatrix = builder.build();
@ -315,23 +331,65 @@ namespace storm {
template<typename ValueType>
void SparseMdpEndComponentInformation<ValueType>::setValues(std::vector<ValueType>& result, storm::storage::BitVector const& maybeStates, std::vector<ValueType> const& fromResult) {
auto notInEcResultIt = result.begin();
// The following assumes that row groups associated to EC states are at the very end.
auto notInEcResultIt = fromResult.begin();
for (auto state : maybeStates) {
if (this->isStateInEc(state)) {
result[state] = result[this->getRowGroupAfterElimination(state)];
STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix.");
result[state] = fromResult[this->getRowGroupAfterElimination(state)];
} else {
result[state] = *notInEcResultIt;
++notInEcResultIt;
}
}
STORM_LOG_ASSERT(notInEcResultIt == result.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators.");
STORM_LOG_ASSERT(notInEcResultIt == fromResult.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators.");
}
template<typename ValueType>
void SparseMdpEndComponentInformation<ValueType>::setScheduler(storm::storage::Scheduler<ValueType>& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<uint64_t> const& fromResult) {
// The following assumes that row groups associated to EC states are at the very end.
storm::storage::BitVector maybeStatesWithoutChoice(maybeStates.size(), false);
storm::storage::BitVector ecStayChoices(transitionMatrix.getRowCount(), false);
auto notInEcResultIt = fromResult.begin();
for (auto const& state : maybeStates) {
if (this->isStateInEc(state)) {
STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix.");
STORM_LOG_ASSERT(!ecToExitChoicesBefore.empty(), "No EC exit choices available. End Components have probably been build without.");
uint64_t ec = getEc(state);
auto const& exitChoices = ecToExitChoicesBefore[ec];
uint64_t afterEliminationChoice = fromResult[this->getRowGroupAfterElimination(state)];
uint64_t beforeEliminationGlobalChoiceIndex = exitChoices[afterEliminationChoice];
bool noChoice = true;
for (uint64_t globalChoice = transitionMatrix.getRowGroupIndices()[state]; globalChoice < transitionMatrix.getRowGroupIndices()[state+1]; ++globalChoice) {
// Is this the selected exit choice?
if (globalChoice == beforeEliminationGlobalChoiceIndex) {
scheduler.setChoice(beforeEliminationGlobalChoiceIndex - transitionMatrix.getRowGroupIndices()[state], state);
noChoice = false;
} else {
// Check if this is an exit choice
if (std::find(exitChoices.begin(), exitChoices.end(), globalChoice) == exitChoices.end()) {
ecStayChoices.set(globalChoice, true);
}
}
}
maybeStatesWithoutChoice.set(state, noChoice);
} else {
scheduler.setChoice(*notInEcResultIt, state);
++notInEcResultIt;
}
}
STORM_LOG_ASSERT(notInEcResultIt == fromResult.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators.");
// The maybeStates without a choice shall reach maybeStates with a choice with probability 1
storm::utility::graph::computeSchedulerProb1E(maybeStates, transitionMatrix, backwardTransitions, maybeStatesWithoutChoice, ~maybeStatesWithoutChoice, scheduler, ecStayChoices);
}
template class SparseMdpEndComponentInformation<double>;
#ifdef STORM_HAVE_CARL
template class SparseMdpEndComponentInformation<storm::RationalNumber>;
template class SparseMdpEndComponentInformation<storm::RationalFunction>;
//template class SparseMdpEndComponentInformation<storm::RationalFunction>;
#endif
}

9
src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h
View File

@ -12,6 +12,9 @@ namespace storm {
template <typename ValueType>
class MaximalEndComponentDecomposition;
template <typename ValueType>
class Scheduler;
}
namespace modelchecker {
@ -50,11 +53,12 @@ namespace storm {
uint64_t getNotInEcMarker() const;
static SparseMdpEndComponentInformation<ValueType> eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector<ValueType> const* summand, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>* columnSumVector, std::vector<ValueType>* summandResultVector);
static SparseMdpEndComponentInformation<ValueType> eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector<ValueType> const* summand, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>* columnSumVector, std::vector<ValueType>* summandResultVector, bool gatherExitChoices = false);
static SparseMdpEndComponentInformation<ValueType> eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& subvector);
static SparseMdpEndComponentInformation<ValueType> eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition<ValueType> const& endComponentDecomposition, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& subvector, bool gatherExitChoices = false);
void setValues(std::vector<ValueType>& result, storm::storage::BitVector const& maybeStates, std::vector<ValueType> const& fromResult);
void setScheduler(storm::storage::Scheduler<ValueType>& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<uint64_t> const& fromResult);
private:
// A constant that marks that a state is not contained in any EC.
@ -70,6 +74,7 @@ namespace storm {
uint64_t numberOfMaybeStatesNotInEc;
uint64_t numberOfEc;
std::vector<uint64_t> maybeStateToEc;
std::vector<std::vector<uint64_t>> ecToExitChoicesBefore; // Only available, if gatherExitChoices was enabled. Empty otherwise.
};
}

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

@ -583,7 +583,7 @@ namespace storm {
}
template<typename ValueType>
boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b) {
boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal<ValueType>& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, bool produceScheduler) {
// Get the set of states that (under some scheduler) can stay in the set of maybestates forever
storm::storage::BitVector candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.maybeStates);
@ -599,7 +599,7 @@ namespace storm {
// Only do more work if there are actually end-components.
if (doDecomposition && !endComponentDecomposition.empty()) {
STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s).");
SparseMdpEndComponentInformation<ValueType> result = SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr);
SparseMdpEndComponentInformation<ValueType> result = SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr, produceScheduler);
// If the solve goal has relevant values, we need to adjust them.
if (goal.hasRelevantValues()) {
@ -663,10 +663,7 @@ namespace storm {
// If the hint information tells us that we have to eliminate MECs, we do so now.
boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
if (hintInformation.getEliminateEndComponents()) {
ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b);
// Make sure we are not supposed to produce a scheduler if we actually eliminate end components.
STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver.");
ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b, produceScheduler);
} else {
// Otherwise, we compute the standard equations.
computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b);
@ -678,16 +675,18 @@ namespace storm {
// If we eliminated end components, we need to extract the result differently.
if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
if (produceScheduler) {
ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler());
}
} else {
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
}
if (produceScheduler) {
extractSchedulerChoices(*scheduler, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates);
}
}
}
}
// Extend scheduler with choices for the states in the qualitative state sets.
if (produceScheduler) {
@ -1028,7 +1027,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, 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, bool produceScheduler) {
// Start by computing the choices with reward 0, as we only want ECs within this fragment.
storm::storage::BitVector zeroRewardChoices(transitionMatrix.getRowCount());
@ -1075,7 +1074,7 @@ namespace storm {
// Only do more work if there are actually end-components.
if (doDecomposition && !endComponentDecomposition.empty()) {
STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs.");
SparseMdpEndComponentInformation<ValueType> result = SparseMdpEndComponentInformation<ValueType>::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : 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, produceScheduler);
// If the solve goal has relevant values, we need to adjust them.
if (goal.hasRelevantValues()) {
@ -1163,10 +1162,7 @@ namespace storm {
// If the hint information tells us that we have to eliminate MECs, we do so now.
boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
if (hintInformation.getEliminateEndComponents()) {
ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities);
// Make sure we are not supposed to produce a scheduler if we actually eliminate end components.
STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver.");
ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities, produceScheduler);
} else {
// Otherwise, we compute the standard equations.
computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr);
@ -1184,16 +1180,18 @@ namespace storm {
// If we eliminated end components, we need to extract the result differently.
if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
if (produceScheduler) {
ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler());
}
} else {
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
}
if (produceScheduler) {
extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates, selectedChoices);
}
}
}
}
// Extend scheduler with choices for the states in the qualitative state sets.
if (produceScheduler) {

Write Preview
Loading…
Cancel
Save