From 5a9d778a2321e2d8117af227530608b5635d5899 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 19 Nov 2013 14:02:15 +0100 Subject: [PATCH] First version of MEC decomposition for nondeterministic models. Former-commit-id: 45f67b2a16703b12ea32791fdb2ae5195676a1dc --- src/storage/BitVector.h | 24 +++++- src/storage/Decomposition.cpp | 3 + src/storage/Decomposition.h | 3 +- src/storage/MaximalEndComponent.cpp | 14 ++++ src/storage/MaximalEndComponent.h | 10 +++ .../MaximalEndComponentDecomposition.cpp | 75 ++++++++++++++++--- src/storm.cpp | 4 +- 7 files changed, 121 insertions(+), 12 deletions(-) diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index f5869fb0d..66f07dcf2 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -321,7 +321,7 @@ public: * @param index The index where to set the truth value. * @param value The truth value to set. */ - void set(const uint_fast64_t index, const bool value) { + void set(const uint_fast64_t index, bool value = true) { uint_fast64_t bucket = index >> 6; if (bucket >= this->bucketCount) throw storm::exceptions::OutOfRangeException() << "Written index " << index << " out of bounds."; uint_fast64_t mask = static_cast(1) << (index & mod64mask); @@ -334,6 +334,19 @@ public: truncateLastBucket(); } } + + /*! + * Sets all bits in the given iterator range. + * + * @param begin The begin of the iterator range. + * @param end The element past the last element of the iterator range. + */ + template + void set(InputIterator begin, InputIterator end) { + for (InputIterator it = begin; it != end; ++it) { + this->set(*it); + } + } /*! * Retrieves the truth value at the given index. @@ -573,6 +586,15 @@ public: return false; } + /*! + * Removes all set bits from the bit vector. + */ + void clear() { + for (uint_fast64_t i = 0; i < this->bucketCount; ++i) { + this->bucketArray[i] = 0; + } + } + /*! * Returns a list containing all indices such that the bits at these indices are set to true * in the bit vector. diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp index fd7380f3d..531f3571e 100644 --- a/src/storage/Decomposition.cpp +++ b/src/storage/Decomposition.cpp @@ -80,6 +80,9 @@ namespace storm { } template class Decomposition; + template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); + template class Decomposition; + template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); } // namespace storage } // namespace storm \ No newline at end of file diff --git a/src/storage/Decomposition.h b/src/storage/Decomposition.h index 27f12648b..c3711152e 100644 --- a/src/storage/Decomposition.h +++ b/src/storage/Decomposition.h @@ -46,7 +46,8 @@ namespace storm { Block const& operator[](uint_fast64_t index) const; - friend std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); + template + friend std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); protected: // The blocks of the decomposition. diff --git a/src/storage/MaximalEndComponent.cpp b/src/storage/MaximalEndComponent.cpp index 975afdec0..81c1c6175 100644 --- a/src/storage/MaximalEndComponent.cpp +++ b/src/storage/MaximalEndComponent.cpp @@ -30,6 +30,10 @@ namespace storm { stateToChoicesMapping[state] = choices; } + void MaximalEndComponent::addState(uint_fast64_t state, std::vector&& choices) { + stateToChoicesMapping.emplace(state, choices); + } + storm::storage::VectorSet const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const { auto stateChoicePair = stateToChoicesMapping.find(state); @@ -89,5 +93,15 @@ namespace storm { return storm::storage::VectorSet(states); } + + std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component) { + out << "{"; + for (auto const& stateChoicesPair : component.stateToChoicesMapping) { + out << "{" << stateChoicesPair.first << ", " << stateChoicesPair.second << "}"; + } + out << "}"; + + return out; + } } } \ No newline at end of file diff --git a/src/storage/MaximalEndComponent.h b/src/storage/MaximalEndComponent.h index c973a90d8..b4f90ebd5 100644 --- a/src/storage/MaximalEndComponent.h +++ b/src/storage/MaximalEndComponent.h @@ -32,6 +32,14 @@ namespace storm { * @param choices The choices to add for the state. */ void addState(uint_fast64_t state, std::vector const& choices); + + /*! + * Adds the given state and the given choices to the MEC. + * + * @param state The state for which to add the choices. + * @param choices The choices to add for the state. + */ + void addState(uint_fast64_t state, std::vector&& choices); /*! * Retrieves the choices for the given state that are contained in this MEC under the @@ -81,6 +89,8 @@ namespace storm { */ storm::storage::VectorSet getStateSet() const; + friend std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component); + private: // This stores the mapping from states contained in the MEC to the choices in this MEC. std::unordered_map> stateToChoicesMapping; diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index de33913fb..0a4fe4441 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -48,18 +48,26 @@ namespace storm { // Initialize the maximal end component list to be the full state space. std::list endComponentStateSets; endComponentStateSets.emplace_back(0, model.getNumberOfStates()); + storm::storage::BitVector statesToCheck(model.getNumberOfStates()); - do { - StronglyConnectedComponentDecomposition sccs(model, true); + for (std::list::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) { + StateBlock const& mec = *mecIterator; + + // Keep track of whether the MEC changed during this iteration. + bool mecChanged = false; + + // Get an SCC decomposition of the current MEC candidate. + StronglyConnectedComponentDecomposition sccs(model, mec, true); + mecChanged |= sccs.size() > 1; // Check for each of the SCCs whether there is at least one action for each state that does not leave the SCC. for (auto& scc : sccs) { - storm::storage::BitVector statesToCheck(model.getNumberOfStates(), scc.begin(), scc.end()); + statesToCheck.set(scc.begin(), scc.end()); while (!statesToCheck.empty()) { storm::storage::BitVector statesToRemove(model.getNumberOfStates()); - - for (auto state : scc) { + + for (auto state : statesToCheck) { bool keepStateInMEC = false; for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { @@ -82,18 +90,67 @@ namespace storm { statesToRemove.set(state, true); } } - + // Now erase the states that have no option to stay inside the MEC with all successors. + mecChanged |= !statesToRemove.empty(); std::vector statesToRemoveList = statesToRemove.getSetIndicesList(); scc.erase(storm::storage::VectorSet(statesToRemoveList.begin(), statesToRemoveList.end())); - + // Now check which states should be reconsidered, because successors of them were removed. + statesToCheck.clear(); + for (auto state : statesToRemove) { + for (typename storm::storage::SparseMatrix::ConstIndexIterator predIt = backwardTransitions.constColumnIteratorBegin(state), predIte = backwardTransitions.constColumnIteratorEnd(state); predIt != predIte; ++predIt) { + if (scc.contains(*predIt)) { + statesToCheck.set(*predIt); + } + } + } } - } + // If the MEC changed, we delete it from the list of MECs and append the possible new MEC candidates to the list instead. + if (mecChanged) { + std::list::const_iterator eraseIterator(mecIterator); + for (StateBlock& scc : sccs) { + endComponentStateSets.push_back(std::move(scc)); + ++mecIterator; + } + endComponentStateSets.erase(eraseIterator); + } else { + // Otherwise, we proceed with the next MEC candidate. + ++mecIterator; + } - } while (true); + } // end of loop over all MEC candidates + + // Now that we computed the underlying state sets of the MECs, we need to properly identify the choices contained in the MEC. + this->blocks.reserve(endComponentStateSets.size()); + for (auto const& mecStateSet : endComponentStateSets) { + MaximalEndComponent newMec; + + for (auto state : mecStateSet) { + std::vector containedChoices; + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + bool choiceContained = true; + for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(choice), successorIte = transitionMatrix.constColumnIteratorEnd(choice); successorIt != successorIte; ++successorIt) { + if (!mecStateSet.contains(*successorIt)) { + choiceContained = false; + break; + } + } + + if (choiceContained) { + containedChoices.push_back(choice); + } + } + + newMec.addState(state, std::move(containedChoices)); + } + + this->blocks.emplace_back(std::move(newMec)); + } + + LOG4CPLUS_INFO(logger, "Computed MEC decomposition of size " << this->size() << "."); } template class MaximalEndComponentDecomposition; diff --git a/src/storm.cpp b/src/storm.cpp index c82d2ac2e..6531bd008 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -467,9 +467,11 @@ int main(const int argc, const char* argv[]) { LOG4CPLUS_INFO(logger, "Model is a CTMDP."); LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); break; - case storm::models::MA: + case storm::models::MA: { LOG4CPLUS_INFO(logger, "Model is a Markov automaton."); + storm::storage::MaximalEndComponentDecomposition mecDecomposition(*parser.getModel>()); break; + } case storm::models::Unknown: default: LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");