diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 20c30aa73..f5869fb0d 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -154,6 +154,20 @@ public: } } + /*! + * Creates a bit vector that has exactly the bits set that are given by the provided iterator range. + * + * @param The length of the bit vector. + * @param begin The begin of the iterator range. + * @param end The end of the iterator range. + */ + template + BitVector(uint_fast64_t length, InputIterator begin, InputIterator end) : BitVector(length) { + for (InputIterator it = begin; it != end; ++it) { + this->set(*it, true); + } + } + /*! * Copy Constructor. Performs a deep copy of the given bit vector. * @param bv A reference to the bit vector to be copied. @@ -545,6 +559,20 @@ public: return result; } + /*! + * Retrieves whether there is at least one bit set in the vector. + * + * @return True if there is at least one bit set in this vector. + */ + bool empty() const { + for (uint_fast64_t i = 0; i < this->bucketCount; ++i) { + if (this->bucketArray[i] != 0) { + return true; + } + } + return false; + } + /*! * 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/MaximalEndComponent.cpp b/src/storage/MaximalEndComponent.cpp index 54e0d950b..975afdec0 100644 --- a/src/storage/MaximalEndComponent.cpp +++ b/src/storage/MaximalEndComponent.cpp @@ -30,7 +30,7 @@ namespace storm { stateToChoicesMapping[state] = choices; } - std::vector const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const { + storm::storage::VectorSet const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const { auto stateChoicePair = stateToChoicesMapping.find(state); if (stateChoicePair == stateToChoicesMapping.end()) { @@ -48,5 +48,46 @@ namespace storm { } return true; } + + void MaximalEndComponent::removeChoice(uint_fast64_t state, uint_fast64_t choice) { + auto stateChoicePair = stateToChoicesMapping.find(state); + + if (stateChoicePair == stateToChoicesMapping.end()) { + throw storm::exceptions::InvalidStateException() << "Cannot delete choice for state not contained in MEC."; + } + + stateChoicePair->second.erase(choice); + } + + void MaximalEndComponent::removeState(uint_fast64_t state) { + auto stateChoicePair = stateToChoicesMapping.find(state); + + if (stateChoicePair == stateToChoicesMapping.end()) { + throw storm::exceptions::InvalidStateException() << "Cannot delete choice for state not contained in MEC."; + } + + stateToChoicesMapping.erase(stateChoicePair); + } + + bool MaximalEndComponent::containsChoice(uint_fast64_t state, uint_fast64_t choice) const { + auto stateChoicePair = stateToChoicesMapping.find(state); + + if (stateChoicePair == stateToChoicesMapping.end()) { + throw storm::exceptions::InvalidStateException() << "Cannot delete choice for state not contained in MEC."; + } + + return stateChoicePair->second.contains(choice); + } + + storm::storage::VectorSet MaximalEndComponent::getStateSet() const { + std::vector states; + states.reserve(stateToChoicesMapping.size()); + + for (auto const& stateChoicesPair : stateToChoicesMapping) { + states.push_back(stateChoicesPair.first); + } + + return storm::storage::VectorSet(states); + } } } \ No newline at end of file diff --git a/src/storage/MaximalEndComponent.h b/src/storage/MaximalEndComponent.h index c80e7e817..c973a90d8 100644 --- a/src/storage/MaximalEndComponent.h +++ b/src/storage/MaximalEndComponent.h @@ -2,7 +2,8 @@ #define STORM_STORAGE_MAXIMALENDCOMPONENT_H_ #include -#include + +#include "src/storage/VectorSet.h" namespace storm { namespace storage { @@ -39,7 +40,22 @@ namespace storm { * @param state The state for which to retrieve the choices. * @return A list of choices of the state in the MEC. */ - std::vector const& getChoicesForState(uint_fast64_t state) const; + storm::storage::VectorSet const& getChoicesForState(uint_fast64_t state) const; + + /*! + * Removes the given choice from the list of choices of the named state. + * + * @param state The state for which to remove the choice. + * @param choice The choice to remove from the state's choices. + */ + void removeChoice(uint_fast64_t state, uint_fast64_t choice); + + /*! + * Removes the given state and all of its choices from the MEC. + * + * @param state The state to remove froom the MEC. + */ + void removeState(uint_fast64_t state); /*! * Retrieves whether the given state is contained in this MEC. @@ -49,9 +65,25 @@ namespace storm { */ bool containsState(uint_fast64_t state) const; + /*! + * Retrievs whether the given choice for the given state is contained in the MEC. + * + * @param state The state for which to check whether the given choice is contained in the MEC. + * @param choice The choice for which to check whether it is contained in the MEC. + * @return True if the given choice is contained in the MEC. + */ + bool containsChoice(uint_fast64_t state, uint_fast64_t choice) const; + + /*! + * Retrieves the set of states contained in the MEC. + * + * @return The set of states contained in the MEC. + */ + storm::storage::VectorSet getStateSet() const; + private: // This stores the mapping from states contained in the MEC to the choices in this MEC. - std::unordered_map> stateToChoicesMapping; + std::unordered_map> stateToChoicesMapping; }; } } diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 97a893b67..de33913fb 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -1,5 +1,8 @@ #include "src/storage/MaximalEndComponentDecomposition.h" +#include +#include + namespace storm { namespace storage { @@ -37,7 +40,60 @@ namespace storm { template void MaximalEndComponentDecomposition::performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel const& model) { - // TODO. + // Get some references for convenient access. + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + + // Initialize the maximal end component list to be the full state space. + std::list endComponentStateSets; + endComponentStateSets.emplace_back(0, model.getNumberOfStates()); + + do { + StronglyConnectedComponentDecomposition sccs(model, true); + + // 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()); + + while (!statesToCheck.empty()) { + storm::storage::BitVector statesToRemove(model.getNumberOfStates()); + + for (auto state : scc) { + bool keepStateInMEC = false; + + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + bool choiceContainedInMEC = true; + for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(choice), successorIte = transitionMatrix.constColumnIteratorEnd(choice); successorIt != successorIte; ++successorIt) { + if (!scc.contains(*successorIt)) { + choiceContainedInMEC = false; + break; + } + } + + // If there is at least one choice whose successor states are fully contained in the MEC, we can leave the state in the MEC. + if (choiceContainedInMEC) { + keepStateInMEC = true; + break; + } + } + + if (!keepStateInMEC) { + statesToRemove.set(state, true); + } + } + + // Now erase the states that have no option to stay inside the MEC with all successors. + 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. + } + + } + + + } while (true); } template class MaximalEndComponentDecomposition; diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index abdd6ec1e..22e7bbbb1 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -90,6 +90,9 @@ namespace storm { recursionIteratorStack.reserve(lowlinks.size()); std::vector statesInStack(lowlinks.size()); + // Store a bit vector of all states with a self-loop to be able to detect non-trivial SCCs with only one state. + storm::storage::BitVector statesWithSelfloop(lowlinks.size()); + // Initialize the recursion stacks with the given initial state (and its successor iterator). recursionStateStack.push_back(startState); recursionIteratorStack.push_back(model.getRows(startState).begin()); @@ -109,6 +112,11 @@ namespace storm { // Now, traverse all successors of the current state. for(; successorIt != model.getRows(currentState).end(); ++successorIt) { + // Record if the current state has a self-loop. + if (currentState == successorIt.column()) { + statesWithSelfloop.set(currentState, true); + } + // If we have not visited the successor already, we need to perform the procedure // recursively on the newly found state. if (!visitedStates.get(successorIt.column()) && subsystem.get(successorIt.column())) { @@ -151,7 +159,7 @@ namespace storm { } while (lastState != currentState); // Only add the SCC if it is non-trivial if the corresponding flag was set. - if (scc.size() > 1 || !dropNaiveSccs) { + if (!dropNaiveSccs || scc.size() > 1 || statesWithSelfloop.get(*scc.begin())) { this->blocks.emplace_back(std::move(scc)); } } diff --git a/src/storage/VectorSet.h b/src/storage/VectorSet.h index 8b42f3895..78057d684 100644 --- a/src/storage/VectorSet.h +++ b/src/storage/VectorSet.h @@ -48,6 +48,14 @@ namespace storm { } } + VectorSet(uint_fast64_t from, uint_fast64_t to) : dirty(false) { + data.reserve(to - from); + + for (uint_fast64_t element = from; element < to; ++element) { + data.push_back(element); + } + } + template VectorSet(InputIterator first, InputIterator last) : data(first, last), dirty(true) { ensureSet(); @@ -224,6 +232,25 @@ namespace storm { return false; } + void erase(VectorSet const& eraseSet) { + if (eraseSet.size() > 0) { + ensureSet(); + eraseSet.ensureSet(); + + for (typename std::vector::reverse_iterator delIt = eraseSet.data.rbegin(), setIt = data.rbegin(); delIt != eraseSet.data.rend() && setIt != eraseSet.data.rend(); ++delIt) { + while (setIt != eraseSet.data.rend() && *setIt > *delIt) { + ++setIt; + } + if (setIt != data.rend()) break; + + if (*setIt == *delIt) { + data.erase((setIt + 1).base()); + ++setIt; + } + } + } + } + friend std::ostream& operator<< (std::ostream& stream, VectorSet const& set) { set.ensureSet(); stream << "VectorSet(" << set.size() << ") { "; @@ -245,9 +272,4 @@ namespace storm { } } -namespace std { - -} - - #endif /* STORM_STORAGE_VECTORSET_H */