Rough sketch of MEC decomposition.

Former-commit-id: 027b58d380

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<typename InputIterator>
+    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.

src/storage/MaximalEndComponent.cpp

@@ -30,7 +30,7 @@ namespace storm {
             stateToChoicesMapping[state] = choices;
         }
         
-        std::vector<uint_fast64_t> const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const {
+        storm::storage::VectorSet<uint_fast64_t> 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<uint_fast64_t> MaximalEndComponent::getStateSet() const {
+            std::vector<uint_fast64_t> states;
+            states.reserve(stateToChoicesMapping.size());
+            
+            for (auto const& stateChoicesPair : stateToChoicesMapping) {
+                states.push_back(stateChoicesPair.first);
+            }
+            
+            return storm::storage::VectorSet<uint_fast64_t>(states);
+        }
     }
 }

src/storage/MaximalEndComponent.h

@@ -2,7 +2,8 @@
 #define STORM_STORAGE_MAXIMALENDCOMPONENT_H_
 
 #include <unordered_map>
-#include <vector>
+
+#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<uint_fast64_t> const& getChoicesForState(uint_fast64_t state) const;
+            storm::storage::VectorSet<uint_fast64_t> 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<uint_fast64_t> getStateSet() const;
+            
         private:
             // This stores the mapping from states contained in the MEC to the choices in this MEC.
-            std::unordered_map<uint_fast64_t, std::vector<uint_fast64_t>> stateToChoicesMapping;
+            std::unordered_map<uint_fast64_t, storm::storage::VectorSet<uint_fast64_t>> stateToChoicesMapping;
         };
     }
 }

src/storage/MaximalEndComponentDecomposition.cpp

@@ -1,5 +1,8 @@
 #include "src/storage/MaximalEndComponentDecomposition.h"
 
+#include <list>
+#include <queue>
+
 namespace storm {
     namespace storage {
         
@@ -37,7 +40,60 @@ namespace storm {
         
         template <typename ValueType>
         void MaximalEndComponentDecomposition<ValueType>::performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model) {
-            // TODO.
+            // Get some references for convenient access.
+            storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
+            std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
+            storm::storage::SparseMatrix<ValueType> const& transitionMatrix = model.getTransitionMatrix();
+            
+            // Initialize the maximal end component list to be the full state space.
+            std::list<StateBlock> endComponentStateSets;
+            endComponentStateSets.emplace_back(0, model.getNumberOfStates());
+            
+            do {
+                StronglyConnectedComponentDecomposition<ValueType> 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<ValueType>::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<uint_fast64_t> statesToRemoveList = statesToRemove.getSetIndicesList();
+                        scc.erase(storm::storage::VectorSet<uint_fast64_t>(statesToRemoveList.begin(), statesToRemoveList.end()));
+
+                        // Now check which states should be reconsidered, because successors of them were removed.
+                    }
+                    
+                }
+                
+                
+            } while (true);
         }
         
         template class MaximalEndComponentDecomposition<double>;

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -90,6 +90,9 @@ namespace storm {
             recursionIteratorStack.reserve(lowlinks.size());
             std::vector<bool> 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));
                     }
                 }

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<typename InputIterator>
             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<T>::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 */