Beautified remaining storage classes a bit.

Former-commit-id: 93f272727f

src/storage/Decomposition.cpp

@@ -61,11 +61,21 @@ namespace storm {
             return blocks.at(index);
         }
         
+        template <typename BlockType>
+        BlockType& Decomposition<BlockType>::getBlock(uint_fast64_t index) {
+            return blocks.at(index);
+        }
+        
         template <typename BlockType>
         BlockType const& Decomposition<BlockType>::operator[](uint_fast64_t index) const {
             return blocks[index];
         }
         
+        template <typename BlockType>
+        BlockType& Decomposition<BlockType>::operator[](uint_fast64_t index) {
+            return blocks[index];
+        }
+        
         std::ostream& operator<<(std::ostream& out, StateBlock const& block) {
             out << "{";
             for (auto const& element : block) {

src/storage/Decomposition.h

@@ -6,8 +6,16 @@
 
 namespace storm {
     namespace storage {
+        // A typedef that specifies the type of a block consisting of states only.
         typedef boost::container::flat_set<uint_fast64_t> StateBlock;
         
+        /*!
+         * Writes a string representation of the state block to the given output stream.
+         *
+         * @param out The output stream to write to.
+         * @param block The block to print to the stream.
+         * @return The given output stream.
+         */
         std::ostream& operator<<(std::ostream& out, StateBlock const& block);
         
         /*!
@@ -20,33 +28,109 @@ namespace storm {
             typedef typename std::vector<Block>::iterator iterator;
             typedef typename std::vector<Block>::const_iterator const_iterator;
             
-            /*
-             * Creates an empty SCC decomposition.
+            /*!
+             * Creates an empty decomposition.
              */
             Decomposition();
             
+            /*!
+             * Creates a decomposition by copying the given decomposition.
+             *
+             * @param other The decomposition to copy.
+             */
             Decomposition(Decomposition const& other);
             
+            /*!
+             * Assigns the contents of the given decomposition to the current one by copying the contents.
+             *
+             * @param other The decomposition whose values to copy.
+             * @return The current decomposition.
+             */
             Decomposition& operator=(Decomposition const& other);
             
+            /*!
+             * Creates a decomposition by moving the given decomposition.
+             *
+             * @param other The decomposition to move.
+             */
             Decomposition(Decomposition&& other);
             
+            /*!
+             * Assigns the contents of the given decomposition to the current one by moving the contents.
+             *
+             * @param other The decomposition whose values to move.
+             * @return The current decomposition.
+             */
             Decomposition& operator=(Decomposition&& other);
             
+            /*!
+             * Retrieves the number of blocks of this decomposition.
+             *
+             * @return The number of blocks of this decomposition.
+             */
             size_t size() const;
             
+            /*!
+             * Retrieves an iterator that points to the first block of this decomposition.
+             *
+             * @return An iterator that points to the first block of this decomposition.
+             */
             iterator begin();
             
+            /*!
+             * Retrieves an iterator that points past the last block of this decomposition.
+             *
+             * @return An iterator that points past the last block of this decomposition.
+             */
             iterator end();
             
+            /*!
+             * Retrieves a const iterator that points to the first block of this decomposition.
+             *
+             * @return A const iterator that points to the first block of this decomposition.
+             */
             const_iterator begin() const;
             
+            /*!
+             * Retrieves a const iterator that points past the last block of this decomposition.
+             *
+             * @return A const iterator that points past the last block of this decomposition.
+             */
             const_iterator end() const;
             
+            /*!
+             * Retrieves the block with the given index. If the index is out-of-bounds, an exception is thrown.
+             *
+             * @param index The index of the block to retrieve.
+             * @return The block with the given index.
+             */
             Block const& getBlock(uint_fast64_t index) const;
             
+            /*!
+             * Retrieves the block with the given index. If the index is out-of-bounds, an exception is thrown.
+             *
+             * @param index The index of the block to retrieve.
+             * @return The block with the given index.
+             */
+            Block& getBlock(uint_fast64_t index);
+            
+            /*!
+             * Retrieves the block with the given index. If the index is out-of-bounds, an behaviour is undefined.
+             *
+             * @param index The index of the block to retrieve.
+             * @return The block with the given index.
+             */
             Block const& operator[](uint_fast64_t index) const;
             
+            /*!
+             * Retrieves the block with the given index. If the index is out-of-bounds, an behaviour is undefined.
+             *
+             * @param index The index of the block to retrieve.
+             * @return The block with the given index.
+             */
+            Block& operator[](uint_fast64_t index);
+            
+            // Declare the streaming operator as a friend function to enable output of decompositions.
             template<typename BlockTimePrime>
             friend std::ostream& operator<<(std::ostream& out, Decomposition<BlockTimePrime> const& decomposition);
             

src/storage/MaximalEndComponent.cpp

@@ -28,48 +28,48 @@ namespace storm {
             return *this;
         }
         
-        void MaximalEndComponent::addState(uint_fast64_t state, std::vector<uint_fast64_t> const& choices) {
-            stateToChoicesMapping[state] = boost::container::flat_set<uint_fast64_t>(choices.begin(), choices.end());
+        void MaximalEndComponent::addState(uint_fast64_t state, set_type const& choices) {
+            stateToChoicesMapping[state] = choices;
         }
         
-        void MaximalEndComponent::addState(uint_fast64_t state, std::vector<uint_fast64_t>&& choices) {
-            stateToChoicesMapping.emplace(state, boost::container::flat_set<uint_fast64_t>(choices.begin(), choices.end()));
+        void MaximalEndComponent::addState(uint_fast64_t state, set_type&& choices) {
+            stateToChoicesMapping.emplace(state, std::move(choices));
         }
         
-        boost::container::flat_set<uint_fast64_t> const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const {
+        MaximalEndComponent::set_type const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const {
             auto stateChoicePair = stateToChoicesMapping.find(state);
             
             if (stateChoicePair == stateToChoicesMapping.end()) {
-                throw storm::exceptions::InvalidStateException() << "Cannot retrieve choices for state not contained in MEC.";
+                throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC.";
             }
             
             return stateChoicePair->second;
         }
         
-        bool MaximalEndComponent::containsState(uint_fast64_t state) const {
+        MaximalEndComponent::set_type& MaximalEndComponent::getChoicesForState(uint_fast64_t state) {
             auto stateChoicePair = stateToChoicesMapping.find(state);
             
             if (stateChoicePair == stateToChoicesMapping.end()) {
-                return false;
+                throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC.";
             }
-            return true;
+            
+            return stateChoicePair->second;
         }
         
-        void MaximalEndComponent::removeChoice(uint_fast64_t state, uint_fast64_t choice) {
+        bool MaximalEndComponent::containsState(uint_fast64_t state) const {
             auto stateChoicePair = stateToChoicesMapping.find(state);
             
             if (stateChoicePair == stateToChoicesMapping.end()) {
-                throw storm::exceptions::InvalidStateException() << "Cannot delete choice for state not contained in MEC.";
+                return false;
             }
-
-            stateChoicePair->second.erase(choice);
+            return true;
         }
         
         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.";
+                throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::removeState: cannot remove state not contained in MEC.";
             }
             
             stateToChoicesMapping.erase(stateChoicePair);
@@ -79,21 +79,21 @@ namespace storm {
             auto stateChoicePair = stateToChoicesMapping.find(state);
             
             if (stateChoicePair == stateToChoicesMapping.end()) {
-                throw storm::exceptions::InvalidStateException() << "Cannot delete choice for state not contained in MEC.";
+                throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::containsChoice: cannot obtain choices for state not contained in MEC.";
             }
             
             return stateChoicePair->second.find(choice) != stateChoicePair->second.end();
         }
         
-        boost::container::flat_set<uint_fast64_t> MaximalEndComponent::getStateSet() const {
-            std::vector<uint_fast64_t> states;
+        MaximalEndComponent::set_type MaximalEndComponent::getStateSet() const {
+            set_type states;
             states.reserve(stateToChoicesMapping.size());
             
             for (auto const& stateChoicesPair : stateToChoicesMapping) {
-                states.push_back(stateChoicesPair.first);
+                states.insert(stateChoicesPair.first);
             }
             
-            return boost::container::flat_set<uint_fast64_t>(states.begin(), states.end());
+            return states;
         }
         
         std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component) {

src/storage/MaximalEndComponent.h

@@ -6,25 +6,48 @@
 
 namespace storm {
     namespace storage {
+        
         /*!
          * This class represents a maximal end-component of a nondeterministic model.
          */
         class MaximalEndComponent {
         public:
-            typedef std::unordered_map<uint_fast64_t, boost::container::flat_set<uint_fast64_t>>::iterator iterator;
-            typedef std::unordered_map<uint_fast64_t, boost::container::flat_set<uint_fast64_t>>::const_iterator const_iterator;
+            typedef boost::container::flat_set<uint_fast64_t> set_type;
+            typedef std::unordered_map<uint_fast64_t, set_type> map_type;
+            typedef map_type::iterator iterator;
+            typedef map_type::const_iterator const_iterator;
             
             /*!
              * Creates an empty MEC.
              */
             MaximalEndComponent();
             
+            /*!
+             * Creates an MEC by copying the given one.
+             *
+             * @param other The MEC to copy.
+             */
             MaximalEndComponent(MaximalEndComponent const& other);
             
+            /*!
+             * Assigns the contents of the given MEC to the current one via copying.
+             *
+             * @param other The MEC whose contents to copy.
+             */
             MaximalEndComponent& operator=(MaximalEndComponent const& other);
             
+            /*!
+             * Creates an MEC by moving the given one.
+             *
+             * @param other The MEC to move.
+             */
             MaximalEndComponent(MaximalEndComponent&& other);
             
+            /*!
+             * Assigns the contents of the given MEC to the current one via moving.
+             *
+             * @param other The MEC whose contents to move.
+             */
             MaximalEndComponent& operator=(MaximalEndComponent&& other);
             
             /*!
@@ -33,7 +56,7 @@ namespace storm {
              * @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> const& choices);
+            void addState(uint_fast64_t state, set_type const& choices);
 
             /*!
              * Adds the given state and the given choices to the MEC.
@@ -41,24 +64,25 @@ namespace storm {
              * @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);
+            void addState(uint_fast64_t state, set_type&& choices);
             
             /*!
-             * Retrieves the choices for the given state that are contained in this MEC under the
-             * assumption that the state is in the MEC.
+             * Retrieves the choices for the given state that are contained in this MEC under the assumption that the
+             * state is in the MEC.
              *
              * @param state The state for which to retrieve the choices.
-             * @return A list of choices of the state in the MEC.
+             * @return A set of choices of the state in the MEC.
              */
-            boost::container::flat_set<uint_fast64_t> const& getChoicesForState(uint_fast64_t state) const;
+            set_type const& getChoicesForState(uint_fast64_t state) const;
             
             /*!
-             * Removes the given choice from the list of choices of the named state.
+             * Retrieves the choices for the given state that are contained in this MEC under the assumption that the
+             * state is in the MEC.
              *
-             * @param state The state for which to remove the choice.
-             * @param choice The choice to remove from the state's choices.
+             * @param state The state for which to retrieve the choices.
+             * @return A set of choices of the state in the MEC.
              */
-            void removeChoice(uint_fast64_t state, uint_fast64_t choice);
+            set_type& getChoicesForState(uint_fast64_t state);
             
             /*!
              * Removes the given state and all of its choices from the MEC.
@@ -76,7 +100,7 @@ namespace storm {
             bool containsState(uint_fast64_t state) const;
             
             /*!
-             * Retrievs whether the given choice for the given state is contained in the MEC.
+             * Retrieves 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.
@@ -89,21 +113,42 @@ namespace storm {
              *
              * @return The set of states contained in the MEC.
              */
-            boost::container::flat_set<uint_fast64_t> getStateSet() const;
+            set_type getStateSet() const;
             
+            /*!
+             * Retrieves an iterator that points to the first state and its choices in the MEC.
+             *
+             * @return An iterator that points to the first state and its choices in the MEC.
+             */
             iterator begin();
             
+            /*!
+             * Retrieves an iterator that points past the last state and its choices in the MEC.
+             *
+             * @return An iterator that points past the last state and its choices in the MEC.
+             */
             iterator end();
             
+            /*!
+             * Retrieves an iterator that points to the first state and its choices in the MEC.
+             *
+             * @return An iterator that points to the first state and its choices in the MEC.
+             */
             const_iterator begin() const;
             
+            /*!
+             * Retrieves an iterator that points past the last state and its choices in the MEC.
+             *
+             * @return An iterator that points past the last state and its choices in the MEC.
+             */
             const_iterator end() const;
             
+            // Declare the streaming operator as a friend function.
             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, boost::container::flat_set<uint_fast64_t>> stateToChoicesMapping;
+            map_type stateToChoicesMapping;
         };
     }
 }

src/storage/MaximalEndComponentDecomposition.cpp

@@ -1,8 +1,9 @@
-#include "src/storage/MaximalEndComponentDecomposition.h"
-
 #include <list>
 #include <queue>
 
+#include "src/storage/MaximalEndComponentDecomposition.h"
+#include "src/storage/StronglyConnectedComponentDecomposition.h"
+
 namespace storm {
     namespace storage {
         
@@ -57,8 +58,9 @@ namespace storm {
             
             
             // The iterator used here should really be a const_iterator.
-            // However, gcc 4.8 (and assorted libraries) does not provide an erase(const_iterator) method for std::list but only an erase(iterator).
-            // This is in compliance with the c++11 draft N3337, which specifies the change from iterator to const_iterator only for "set, multiset, map [and] multimap".
+            // However, gcc 4.8 (and assorted libraries) does not provide an erase(const_iterator) method for std::list
+            // but only an erase(iterator). This is in compliance with the c++11 draft N3337, which specifies the change
+            // from iterator to const_iterator only for "set, multiset, map [and] multimap".
             // FIXME: As soon as gcc provides an erase(const_iterator) method, change this iterator back to a const_iterator.
             for (std::list<StateBlock>::iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) {
                 StateBlock const& mec = *mecIterator;
@@ -119,7 +121,8 @@ namespace storm {
                     }
                 }
                 
-                // If the MEC changed, we delete it from the list of MECs and append the possible new MEC candidates to the list instead.
+                // 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) {
                     for (StateBlock& scc : sccs) {
                         if (!scc.empty()) {
@@ -135,15 +138,16 @@ namespace storm {
                     ++mecIterator;
                 }
                 
-            } // end of loop over all MEC candidates
+            } // 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.
+            // Now that we computed the underlying state sets of the MECs, we need to properly identify the choices
+            // contained in the MEC and store them as actual MECs.
             this->blocks.reserve(endComponentStateSets.size());
             for (auto const& mecStateSet : endComponentStateSets) {
                 MaximalEndComponent newMec;
                 
                 for (auto state : mecStateSet) {
-                    std::vector<uint_fast64_t> containedChoices;
+                    MaximalEndComponent::set_type containedChoices;
                     for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
                         bool choiceContained = true;
                         for (auto const& entry : transitionMatrix.getRow(choice)) {
@@ -154,7 +158,7 @@ namespace storm {
                         }
                         
                         if (choiceContained) {
-                            containedChoices.push_back(choice);
+                            containedChoices.insert(choice);
                         }
                     }
                     
@@ -163,10 +167,9 @@ namespace storm {
                 
                 this->blocks.emplace_back(std::move(newMec));
             }
-            
-            LOG4CPLUS_INFO(logger, "Computed MEC decomposition of size " << this->size() << ".");
         }
         
+        // Explicitly instantiate the MEC decomposition.
         template class MaximalEndComponentDecomposition<double>;
     }
 }

src/storage/MaximalEndComponentDecomposition.h

@@ -2,13 +2,15 @@
 #define STORM_STORAGE_MAXIMALENDCOMPONENTDECOMPOSITION_H_
 
 #include "src/storage/Decomposition.h"
-#include "src/storage/StronglyConnectedComponentDecomposition.h"
 #include "src/storage/MaximalEndComponent.h"
 #include "src/models/AbstractNondeterministicModel.h"
 
 namespace storm  {
     namespace storage {
         
+        /*!
+         * This class represents the decomposition of a nondeterministic model into its maximal end components.
+         */
         template <typename ValueType>
         class MaximalEndComponentDecomposition : public Decomposition<MaximalEndComponent> {
         public:
@@ -24,22 +26,49 @@ namespace storm  {
              */
             MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model);
             
+            /*!
+             * Creates an MEC decomposition of the given subsystem in the given model.
+             *
+             * @param model The model whose subsystem to decompose into MECs.
+             * @param subsystem The subsystem to decompose.
+             */
             MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model, storm::storage::BitVector const& subsystem);
             
+            /*!
+             * Creates an MEC decomposition by copying the contents of the given MEC decomposition.
+             *
+             * @param other The MEC decomposition to copy.
+             */
             MaximalEndComponentDecomposition(MaximalEndComponentDecomposition const& other);
             
+            /*!
+             * Assigns the contents of the given MEC decomposition to the current one by copying its contents.
+             *
+             * @param other The MEC decomposition from which to copy-assign.
+             */
             MaximalEndComponentDecomposition& operator=(MaximalEndComponentDecomposition const& other);
             
+            /*!
+             * Creates an MEC decomposition by moving the contents of the given MEC decomposition.
+             *
+             * @param other The MEC decomposition to move.
+             */
             MaximalEndComponentDecomposition(MaximalEndComponentDecomposition&& other);
             
+            /*!
+             * Assigns the contents of the given MEC decomposition to the current one by moving its contents.
+             *
+             * @param other The MEC decomposition from which to move-assign.
+             */
             MaximalEndComponentDecomposition& operator=(MaximalEndComponentDecomposition&& other);
             
         private:
             /*!
-             * Performs the actual decomposition of the given model into MECs. Stores the MECs found in the current decomposition
-             * as a side-effect.
+             * Performs the actual decomposition of the given subsystem in the given model into MECs. As a side-effect
+             * this stores the MECs found in the current decomposition.
              *
-             * @param model The model to decompose.
+             * @param model The model whose subsystem to decompose into MECs.
+             * @param subsystem The subsystem to decompose.
              */
             void performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model, storm::storage::BitVector const& subsystem);
         };

src/storage/PartialScheduler.cpp

@@ -5,27 +5,27 @@ namespace storm {
     namespace storage {
         
         void PartialScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) {
-            choices[state] = choice;
+            stateToChoiceMapping[state] = choice;
         }
         
         bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const {
-            return choices.find(state) != choices.end();
+            return stateToChoiceMapping.find(state) != choices.end();
         }
         
         uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const {
-            auto stateChoicePair = choices.find(state);
+            auto stateChoicePair = stateToChoiceMapping.find(state);
             
-            if (stateChoicePair == choices.end()) {
-                throw storm::exceptions::InvalidArgumentException() << "Scheduler does not define a choice for state " << state;
+            if (stateChoicePair == stateToChoiceMapping.end()) {
+                throw storm::exceptions::InvalidArgumentException() << "Invalid call to PartialScheduler::getChoice: scheduler does not define a choice for state " << state << ".";
             }
             
             return stateChoicePair->second;
         }
         
         std::ostream& operator<<(std::ostream& out, PartialScheduler const& scheduler) {
-            out << "partial scheduler (defined on " << scheduler.choices.size() << " states) [ ";
-            uint_fast64_t remainingEntries = scheduler.choices.size();
-            for (auto stateChoicePair : scheduler.choices) {
+            out << "partial scheduler (defined on " << scheduler.stateToChoiceMapping.size() << " states) [ ";
+            uint_fast64_t remainingEntries = scheduler.stateToChoiceMapping.size();
+            for (auto const& stateChoicePair : scheduler.stateToChoiceMapping) {
                 out << stateChoicePair.first << " -> " << stateChoicePair.second;
                 --remainingEntries;
                 if (remainingEntries > 0) {

src/storage/PartialScheduler.h

@@ -11,6 +11,8 @@ namespace storm {
         
         class PartialScheduler : public Scheduler {
         public:
+            typedef std::unordered_map<uint_fast64_t, uint_fast64_t> map_type;
+            
             void setChoice(uint_fast64_t state, uint_fast64_t choice) override;
             
             bool isChoiceDefined(uint_fast64_t state) const override;
@@ -21,7 +23,7 @@ namespace storm {
 
         private:
             // A mapping from all states that have defined choices to their respective choices.
-            std::unordered_map<uint_fast64_t, uint_fast64_t> choices;
+            map_type stateToChoiceMapping;
         };
     }
 }

src/storage/Scheduler.h

@@ -7,8 +7,9 @@ namespace storm {
     namespace storage {
         
         /*
-         * This class is the abstract base class of all scheduler classes. Scheduler classes define which action is chosen in a particular state of a non-deterministic model.
-         * More concretely, a scheduler maps a state s to i if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states).
+         * This class is the abstract base class of all scheduler classes. Scheduler classes define which action is
+         * chosen in a particular state of a non-deterministic model. More concretely, a scheduler maps a state s to i
+         * if the scheduler takes the i-th action available in s (i.e. the choices are relative to the states).
          */
         class Scheduler {
         public:

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -48,11 +48,8 @@ namespace storm {
         
         template <typename ValueType>
         void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) {
-            LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
-            
-            uint_fast64_t numberOfStates = model.getNumberOfStates();
-            
             // Set up the environment of Tarjan's algorithm.
+            uint_fast64_t numberOfStates = model.getNumberOfStates();
             std::vector<uint_fast64_t> tarjanStack;
             tarjanStack.reserve(numberOfStates);
             storm::storage::BitVector tarjanStackStates(numberOfStates);
@@ -60,24 +57,20 @@ namespace storm {
             std::vector<uint_fast64_t> lowlinks(numberOfStates);
             storm::storage::BitVector visitedStates(numberOfStates);
             
-            // Start the search for SCCs from every vertex in the block.
+            // Start the search for SCCs from every state in the block.
             uint_fast64_t currentIndex = 0;
             for (auto state : subsystem) {
                 if (!visitedStates.get(state)) {
                     performSccDecompositionHelper(model, state, subsystem, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, dropNaiveSccs, onlyBottomSccs);
                 }
             }
-            
-            LOG4CPLUS_INFO(logger, "Done computing SCC decomposition.");
         }
 
         
         template <typename ValueType>
         void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs, bool onlyBottomSccs) {
-            uint_fast64_t numberOfStates = model.getNumberOfStates();
-
             // Prepare a block that contains all states for a call to the other overload of this function.
-            storm::storage::BitVector fullSystem(numberOfStates, true);
+            storm::storage::BitVector fullSystem(model.getNumberOfStates(), true);
             
             // Call the overloaded function.
             performSccDecomposition(model, fullSystem, dropNaiveSccs, onlyBottomSccs);
@@ -85,17 +78,17 @@ namespace storm {
         
         template <typename ValueType>
         void StronglyConnectedComponentDecomposition<ValueType>::performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs) {
-            // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm
-            // into an iterative version. In particular, we keep one stack for states and one stack
-            // for the iterators. The last one is not strictly needed, but reduces iteration work when
-            // all successors of a particular state are considered.
+            // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm into an iterative
+            // version. In particular, we keep one stack for states and one stack for the iterators. The last one is not
+            // strictly needed, but reduces iteration work when all successors of a particular state are considered.
             std::vector<uint_fast64_t> recursionStateStack;
             recursionStateStack.reserve(lowlinks.size());
             std::vector<typename storm::storage::SparseMatrix<ValueType>::const_iterator> recursionIteratorStack;
             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.
+            // 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;
             if (dropNaiveSccs) {
                 statesWithSelfloop = storm::storage::BitVector(lowlinks.size());
@@ -131,9 +124,8 @@ namespace storm {
                         statesWithSelfloop.set(currentState, true);
                     }
                     
-                    // If we have not visited the successor already, we need to perform the procedure
-                    // recursively on the newly found state, but only if it belongs to the subsystem in
-                    // which we are interested.
+                    // If we have not visited the successor already, we need to perform the procedure recursively on the
+                    // newly found state, but only if it belongs to the subsystem in which we are interested.
                     if (subsystem.get(successorIt->first)) {
                         if (!visitedStates.get(successorIt->first)) {
                             // Save current iterator position so we can continue where we left off later.
@@ -162,14 +154,14 @@ namespace storm {
                             // Update the lowlink of the current state.
                             lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt->first]);
                             
-                            // Since it is known that in this case, the successor state is in the same SCC as the current state
-                            // we don't need to update the bit vector of states that can leave their SCC.
+                            // Since it is known that in this case, the successor state is in the same SCC as the
+                            // current state we don't need to update the bit vector of states that can leave their SCC.
                         }
                     }
                 }
                 
-                // If the current state is the root of a SCC, we need to pop all states of the SCC from
-                // the algorithm's stack.
+                // If the current state is the root of a SCC, we need to pop all states of the SCC from the algorithm's
+                // stack.
                 if (lowlinks[currentState] == stateIndices[currentState]) {
                     Block scc;
                     
@@ -190,7 +182,8 @@ namespace storm {
                     } while (lastState != currentState);
                     
                     // Now determine whether we want to keep this SCC in the decomposition.
-                    // First, we need to check whether we should drop the SCC because of the requirement to not include naive SCCs.
+                    // First, we need to check whether we should drop the SCC because of the requirement to not include
+                    // naive SCCs.
                     bool keepScc = !dropNaiveSccs || (scc.size() > 1 || statesWithSelfloop.get(*scc.begin()));
                     // Then, we also need to make sure that it is a bottom SCC if we were required to.
                     keepScc &= !onlyBottomSccs || isBottomScc;
@@ -201,14 +194,13 @@ namespace storm {
                     }
                 }
                 
-                // If we reach this point, we have completed the recursive descent for the current state.
-                // That is, we need to pop it from the recursion stacks.
+                // If we reach this point, we have completed the recursive descent for the current state. That is, we
+                // need to pop it from the recursion stacks.
                 recursionStateStack.pop_back();
                 recursionIteratorStack.pop_back();
                 
-                // If there is at least one state under the current one in our recursion stack, we need
-                // to restore the topmost state as the current state and jump to the part after the
-                // original recursive call.
+                // If there is at least one state under the current one in our recursion stack, we need to restore the
+                // topmost state as the current state and jump to the part after the original recursive call.
                 if (recursionStateStack.size() > 0) {
                     currentState = recursionStateStack.back();
                     successorIt = recursionIteratorStack.back();
@@ -218,6 +210,7 @@ namespace storm {
             }
         }
         
+        // Explicitly instantiate the SCC decomposition.
         template class StronglyConnectedComponentDecomposition<double>;
     } // namespace storage
 } // namespace storm

src/storage/StronglyConnectedComponentDecomposition.h

@@ -1,13 +1,9 @@
 #ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_
 #define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_
 
-#include <boost/container/flat_set.hpp>
-
-#include "src/storage/SparseMatrix.h"
 #include "src/storage/Decomposition.h"
 #include "src/storage/BitVector.h"
 
-
 namespace storm {
     namespace models {
         // Forward declare the abstract model class.
@@ -32,35 +28,108 @@ namespace storm {
              *
              * @param model The model to decompose into SCCs.
              * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
-             * are to be kept in the decomposition.
+             * without a self-loop) are to be kept in the decomposition.
+             * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
+             * leaving the SCC), are kept.
              */
             StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
             
             /*
-             * Creates an SCC decomposition of given block in the given model.
+             * Creates an SCC decomposition of the given block in the given model.
              *
-             * @param model The model that contains the block.
+             * @param model The model whose block to decompose.
              * @param block The block to decompose into SCCs.
              * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
-             * are to be kept in the decomposition.
+             * without a self-loop) are to be kept in the decomposition.
+             * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
+             * leaving the SCC), are kept.
              */
             StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
             
+            /*
+             * Creates an SCC decomposition of the given subsystem in the given model.
+             *
+             * @param model The model that contains the block.
+             * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs.
+             * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
+             * without a self-loop) are to be kept in the decomposition.
+             * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
+             * leaving the SCC), are kept.
+             */
             StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
             
+            /*!
+             * Creates an SCC decomposition by copying the given SCC decomposition.
+             *
+             * @oaram other The SCC decomposition to copy.
+             */
             StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other);
             
+            /*!
+             * Assigns the contents of the given SCC decomposition to the current one by copying its contents.
+             *
+             * @oaram other The SCC decomposition from which to copy-assign.
+             */
             StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition const& other);
             
+            /*!
+             * Creates an SCC decomposition by moving the given SCC decomposition.
+             *
+             * @oaram other The SCC decomposition to move.
+             */
             StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other);
             
+            /*!
+             * Assigns the contents of the given SCC decomposition to the current one by moving its contents.
+             *
+             * @oaram other The SCC decomposition from which to copy-assign.
+             */
             StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other);
             
         private:
+            /*!
+             * Performs the SCC decomposition of the given model. As a side-effect this fills the vector of
+             * blocks of the decomposition.
+             *
+             * @param model The model to decompose into SCCs.
+             * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
+             * without a self-loop) are to be kept in the decomposition.
+             * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
+             * leaving the SCC), are kept.
+             */
             void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
             
+            /*
+             * Performs the SCC decomposition of the given block in the given model. As a side-effect this fills
+             * the vector of blocks of the decomposition.
+             *
+             * @param model The model that contains the block.
+             * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs.
+             * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
+             * without a self-loop) are to be kept in the decomposition.
+             * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
+             * leaving the SCC), are kept.
+             */
             void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
             
+            /*!
+             * A helper function that performs the SCC decomposition given all auxiliary data structures. As a
+             * side-effect this fills the vector of blocks of the decomposition.
+             *
+             * @param model The model to decompose into SCCs.
+             * @param startState The starting state for the search of Tarjan's algorithm.
+             * @param subsystem The subsystem to search.
+             * @param currentIndex The next free index that can be assigned to states.
+             * @param stateIndices A vector storing the index for each state.
+             * @param lowlinks A vector storing the lowlink for each state.
+             * @param tarjanStack A vector that is to be used as the stack in Tarjan's algorithm.
+             * @param tarjanStackStates A bit vector indicating which states are currently in the stack.
+             * @param visitedStates A bit vector containing all states that have already been visited.
+             * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
+             * without a self-loop) are to be kept in the decomposition.
+             * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
+             * leaving the SCC), are kept.
+             */
             void performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs);
         };
     }

src/storage/TotalScheduler.cpp

@@ -15,7 +15,7 @@ namespace storm {
         }
         
         bool TotalScheduler::isChoiceDefined(uint_fast64_t state) const {
-            return true;
+            return state < choices.size();
         }
         
         uint_fast64_t TotalScheduler::getChoice(uint_fast64_t state) const {

src/storage/TotalScheduler.h

@@ -11,8 +11,19 @@ namespace storm {
         
         class TotalScheduler : public Scheduler {
         public:
-            TotalScheduler(uint_fast64_t numberOfStates);
-            
+            /*!
+             * Creates a total scheduler that defines a choice for the given number of states. By default, all choices
+             * are initialized to zero.
+             *
+             * @param numberOfStates The number of states for which the scheduler defines a choice.
+             */
+            TotalScheduler(uint_fast64_t numberOfStates = 0);
+            
+            /*!
+             * Creates a total scheduler that defines the choices for states according to the given vector.
+             *
+             * @param choices A vector whose i-th entry defines the choice of state i.
+             */
             TotalScheduler(std::vector<uint_fast64_t> const& choices);
             
             void setChoice(uint_fast64_t state, uint_fast64_t choice) override;