First version of MEC decomposition for nondeterministic models.

Former-commit-id: 45f67b2a16

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<uint_fast64_t>(1) << (index & mod64mask);
@@ -335,6 +335,19 @@ public:
 		}
 	}
     
+    /*!
+     * 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<typename InputIterator>
+    void set(InputIterator begin, InputIterator end) {
+        for (InputIterator it = begin; it != end; ++it) {
+            this->set(*it);
+        }
+    }
+
 	/*!
 	 * Retrieves the truth value at the given index.
 	 * @param index The index from which to retrieve the truth value.
@@ -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.

src/storage/Decomposition.cpp

@@ -80,6 +80,9 @@ namespace storm {
         }
         
         template class Decomposition<StateBlock>;
+        template std::ostream& operator<<(std::ostream& out, Decomposition<StateBlock> const& decomposition);
+        
         template class Decomposition<MaximalEndComponent>;
+        template std::ostream& operator<<(std::ostream& out, Decomposition<MaximalEndComponent> const& decomposition);
     } // namespace storage
 } // namespace storm

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<typename BlockTimePrime>
+            friend std::ostream& operator<<(std::ostream& out, Decomposition<BlockTimePrime> const& decomposition);
 
         protected:
             // The blocks of the decomposition.

src/storage/MaximalEndComponent.cpp

@@ -30,6 +30,10 @@ namespace storm {
             stateToChoicesMapping[state] = choices;
         }
         
+        void MaximalEndComponent::addState(uint_fast64_t state, std::vector<uint_fast64_t>&& choices) {
+            stateToChoicesMapping.emplace(state, choices);
+        }
+        
         storm::storage::VectorSet<uint_fast64_t> const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const {
             auto stateChoicePair = stateToChoicesMapping.find(state);
             
@@ -89,5 +93,15 @@ namespace storm {
             
             return storm::storage::VectorSet<uint_fast64_t>(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;
+        }        
     }
 }

src/storage/MaximalEndComponent.h

@@ -33,6 +33,14 @@ namespace storm {
              */
             void addState(uint_fast64_t state, std::vector<uint_fast64_t> 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<uint_fast64_t>&& choices);
+            
             /*!
              * Retrieves the choices for the given state that are contained in this MEC under the
              * assumption that the state is in the MEC.
@@ -81,6 +89,8 @@ namespace storm {
              */
             storm::storage::VectorSet<uint_fast64_t> 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<uint_fast64_t, storm::storage::VectorSet<uint_fast64_t>> stateToChoicesMapping;

src/storage/MaximalEndComponentDecomposition.cpp

@@ -48,18 +48,26 @@ namespace storm {
             // Initialize the maximal end component list to be the full state space.
             std::list<StateBlock> endComponentStateSets;
             endComponentStateSets.emplace_back(0, model.getNumberOfStates());
+            storm::storage::BitVector statesToCheck(model.getNumberOfStates());
             
-            do {
-                StronglyConnectedComponentDecomposition<ValueType> sccs(model, true);
+            for (std::list<StateBlock>::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<ValueType> 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) {
@@ -84,16 +92,65 @@ namespace storm {
                         }
                         
                         // Now erase the states that have no option to stay inside the MEC with all successors.
+                        mecChanged |= !statesToRemove.empty();
                         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.
+                        statesToCheck.clear();
+                        for (auto state : statesToRemove) {
+                            for (typename storm::storage::SparseMatrix<ValueType>::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<StateBlock>::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;
+                }
+                
+            } // 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<uint_fast64_t> containedChoices;
+                    for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
+                        bool choiceContained = true;
+                        for (typename storm::storage::SparseMatrix<ValueType>::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));
+            }
             
-            } while (true);
+            LOG4CPLUS_INFO(logger, "Computed MEC decomposition of size " << this->size() << ".");
         }
         
         template class MaximalEndComponentDecomposition<double>;

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<double> mecDecomposition(*parser.getModel<storm::models::MarkovAutomaton<double>>());
                     break;
+                }
 				case storm::models::Unknown:
 				default:
 					LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly.");