diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp index 8d06c625c..ccb14ee46 100644 --- a/src/storage/Decomposition.cpp +++ b/src/storage/Decomposition.cpp @@ -61,11 +61,21 @@ namespace storm { return blocks.at(index); } + template + BlockType& Decomposition::getBlock(uint_fast64_t index) { + return blocks.at(index); + } + template BlockType const& Decomposition::operator[](uint_fast64_t index) const { return blocks[index]; } + template + BlockType& Decomposition::operator[](uint_fast64_t index) { + return blocks[index]; + } + std::ostream& operator<<(std::ostream& out, StateBlock const& block) { out << "{"; for (auto const& element : block) { @@ -74,7 +84,7 @@ namespace storm { out << "}"; return out; } - + template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition) { out << "["; diff --git a/src/storage/Decomposition.h b/src/storage/Decomposition.h index 707e5d0b8..0c44943c9 100644 --- a/src/storage/Decomposition.h +++ b/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 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,36 +28,112 @@ namespace storm { typedef typename std::vector::iterator iterator; typedef typename std::vector::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 friend std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); - + protected: // The blocks of the decomposition. std::vector blocks; diff --git a/src/storage/MaximalEndComponent.cpp b/src/storage/MaximalEndComponent.cpp index eb61a4fa2..907de3167 100644 --- a/src/storage/MaximalEndComponent.cpp +++ b/src/storage/MaximalEndComponent.cpp @@ -5,7 +5,7 @@ namespace storm { namespace storage { std::ostream& operator<<(std::ostream& out, boost::container::flat_set const& block); - + MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() { // Intentionally left empty. } @@ -28,48 +28,48 @@ namespace storm { return *this; } - void MaximalEndComponent::addState(uint_fast64_t state, std::vector const& choices) { - stateToChoicesMapping[state] = boost::container::flat_set(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&& choices) { - stateToChoicesMapping.emplace(state, boost::container::flat_set(choices.begin(), choices.end())); + void MaximalEndComponent::addState(uint_fast64_t state, set_type&& choices) { + stateToChoicesMapping.emplace(state, std::move(choices)); } - boost::container::flat_set 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 MaximalEndComponent::getStateSet() const { - std::vector 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(states.begin(), states.end()); + return states; } std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component) { diff --git a/src/storage/MaximalEndComponent.h b/src/storage/MaximalEndComponent.h index 3efc70386..114f12378 100644 --- a/src/storage/MaximalEndComponent.h +++ b/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>::iterator iterator; - typedef std::unordered_map>::const_iterator const_iterator; + typedef boost::container::flat_set set_type; + typedef std::unordered_map 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 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&& 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 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 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> stateToChoicesMapping; + map_type stateToChoicesMapping; }; } } diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 7fb3a31be..5955a58d3 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -1,8 +1,9 @@ -#include "src/storage/MaximalEndComponentDecomposition.h" - #include #include +#include "src/storage/MaximalEndComponentDecomposition.h" +#include "src/storage/StronglyConnectedComponentDecomposition.h" + namespace storm { namespace storage { @@ -55,14 +56,15 @@ namespace storm { endComponentStateSets.emplace_back(subsystem.begin(), subsystem.end()); storm::storage::BitVector statesToCheck(model.getNumberOfStates()); - + // 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::iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) { StateBlock const& mec = *mecIterator; - + // Keep track of whether the MEC changed during this iteration. bool mecChanged = false; @@ -119,14 +121,15 @@ 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()) { endComponentStateSets.push_back(std::move(scc)); } } - + std::list::iterator eraseIterator(mecIterator); ++mecIterator; endComponentStateSets.erase(eraseIterator); @@ -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 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; } } diff --git a/src/storage/MaximalEndComponentDecomposition.h b/src/storage/MaximalEndComponentDecomposition.h index d21ee6dd7..b05795c4f 100644 --- a/src/storage/MaximalEndComponentDecomposition.h +++ b/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 class MaximalEndComponentDecomposition : public Decomposition { public: @@ -24,22 +26,49 @@ namespace storm { */ MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel 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 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 const& model, storm::storage::BitVector const& subsystem); }; diff --git a/src/storage/PartialScheduler.cpp b/src/storage/PartialScheduler.cpp index 850d54a92..a3a0a20d9 100644 --- a/src/storage/PartialScheduler.cpp +++ b/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) { diff --git a/src/storage/PartialScheduler.h b/src/storage/PartialScheduler.h index ca33165d2..e5f9fffb2 100644 --- a/src/storage/PartialScheduler.h +++ b/src/storage/PartialScheduler.h @@ -11,6 +11,8 @@ namespace storm { class PartialScheduler : public Scheduler { public: + typedef std::unordered_map 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 choices; + map_type stateToChoiceMapping; }; } } diff --git a/src/storage/Scheduler.h b/src/storage/Scheduler.h index d9363c8fb..a98a6bd50 100644 --- a/src/storage/Scheduler.h +++ b/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: diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index d8c571c7b..b7bd88dd2 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -48,11 +48,8 @@ namespace storm { template void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel 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 tarjanStack; tarjanStack.reserve(numberOfStates); storm::storage::BitVector tarjanStackStates(numberOfStates); @@ -60,24 +57,20 @@ namespace storm { std::vector 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 void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel 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 void StronglyConnectedComponentDecomposition::performSccDecompositionHelper(storm::models::AbstractModel const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& 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 recursionStateStack; recursionStateStack.reserve(lowlinks.size()); std::vector::const_iterator> recursionIteratorStack; 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. + // 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; } // namespace storage } // namespace storm \ No newline at end of file diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index 56a142e2f..a8ce0403c 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -1,13 +1,9 @@ #ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ #define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ -#include - -#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 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 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 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 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 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 const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs); }; } diff --git a/src/storage/TotalScheduler.cpp b/src/storage/TotalScheduler.cpp index 41b75119c..bcbc22e61 100644 --- a/src/storage/TotalScheduler.cpp +++ b/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 { diff --git a/src/storage/TotalScheduler.h b/src/storage/TotalScheduler.h index 2e29471f7..32173ac63 100644 --- a/src/storage/TotalScheduler.h +++ b/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 const& choices); void setChoice(uint_fast64_t state, uint_fast64_t choice) override;