diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 67d495408..b115e2551 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -147,7 +147,8 @@ class AbstractModel: public std::enable_shared_from_this> { * @param decomposition A decomposition containing the blocks of the partition of the system. * @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition. */ - storm::storage::SparseMatrix extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const { + template + storm::storage::SparseMatrix extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const { uint_fast64_t numberOfStates = decomposition.size(); // First, we need to create a mapping of states to their SCC index, to ease the computation of dependency transitions later. @@ -163,7 +164,7 @@ class AbstractModel: public std::enable_shared_from_this> { for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) { // Get the next block. - typename storm::storage::StateBlock const& block = decomposition[currentBlockIndex]; + typename storm::storage::Decomposition::block_type const& block = decomposition[currentBlockIndex]; // Now, we determine the blocks which are reachable (in one step) from the current block. boost::container::flat_set allTargetBlocks; diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp index 36f22c50c..3e9d2e003 100644 --- a/src/storage/Decomposition.cpp +++ b/src/storage/Decomposition.cpp @@ -1,4 +1,5 @@ #include "src/storage/Decomposition.h" +#include "src/storage/StronglyConnectedComponent.h" #include "src/storage/MaximalEndComponent.h" namespace storm { @@ -89,8 +90,8 @@ namespace storm { return out; } - template class Decomposition; - template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); + template class Decomposition; + template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); template class Decomposition; template std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); diff --git a/src/storage/Decomposition.h b/src/storage/Decomposition.h index 3d47417e0..f20d1ede9 100644 --- a/src/storage/Decomposition.h +++ b/src/storage/Decomposition.h @@ -119,8 +119,8 @@ namespace storm { block_type& 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); + template + friend std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); protected: // The blocks of the decomposition. diff --git a/src/storage/MaximalEndComponent.h b/src/storage/MaximalEndComponent.h index 114f12378..ee0b6289b 100644 --- a/src/storage/MaximalEndComponent.h +++ b/src/storage/MaximalEndComponent.h @@ -4,6 +4,8 @@ #include #include +#include "src/storage/sparse/StateType.h" + namespace storm { namespace storage { @@ -12,7 +14,7 @@ namespace storm { */ class MaximalEndComponent { public: - typedef boost::container::flat_set set_type; + 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; diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 683083d32..f96857be3 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -1,5 +1,6 @@ #include #include +#include #include "src/storage/MaximalEndComponentDecomposition.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" @@ -56,7 +57,7 @@ namespace storm { endComponentStateSets.emplace_back(subsystem.begin(), subsystem.end()); storm::storage::BitVector statesToCheck(model.getNumberOfStates()); - + std::cout << " starting... " << std::endl; // 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 @@ -69,7 +70,9 @@ namespace storm { bool mecChanged = false; // Get an SCC decomposition of the current MEC candidate. + std::cout << "boom" << std::endl; StronglyConnectedComponentDecomposition sccs(model, mec, true); + std::cout << "boom1" << std::endl; // We need to do another iteration in case we have either more than once SCC or the SCC is smaller than // the MEC canditate itself. @@ -80,6 +83,7 @@ namespace storm { statesToCheck.set(scc.begin(), scc.end()); while (!statesToCheck.empty()) { + std::cout << "not empty!" << std::endl; storm::storage::BitVector statesToRemove(model.getNumberOfStates()); for (auto state : statesToCheck) { @@ -116,7 +120,7 @@ namespace storm { statesToCheck.clear(); for (auto state : statesToRemove) { for (auto const& entry : backwardTransitions.getRow(state)) { - if (!scc.containsState(entry.getColumn())) { + if (scc.containsState(entry.getColumn())) { statesToCheck.set(entry.getColumn()); } } @@ -142,7 +146,9 @@ namespace storm { } } // End of loop over all MEC candidates. - + + std::cout << " got here... " << std::endl; + // 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()); @@ -154,7 +160,7 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool choiceContained = true; for (auto const& entry : transitionMatrix.getRow(choice)) { - if (mecStateSet.find(entry.getColumn()) == mecStateSet.end()) { + if (!mecStateSet.containsState(entry.getColumn())) { choiceContained = false; break; } diff --git a/src/storage/StateBlock.cpp b/src/storage/StateBlock.cpp index f70e1aa9c..9f87d324d 100644 --- a/src/storage/StateBlock.cpp +++ b/src/storage/StateBlock.cpp @@ -2,46 +2,46 @@ namespace storm { namespace storage { - template - typename StateBlock::iterator StateBlock::begin() { + typename StateBlock::iterator StateBlock::begin() { return states.begin(); } - template - typename StateBlock::const_iterator StateBlock::begin() const { + typename StateBlock::const_iterator StateBlock::begin() const { return states.begin(); } - template - typename StateBlock::iterator StateBlock::end() { + typename StateBlock::iterator StateBlock::end() { return states.end(); } - template - typename StateBlock::const_iterator StateBlock::end() const { + typename StateBlock::const_iterator StateBlock::end() const { return states.end(); } - template - std::size_t StateBlock::size() const { + std::size_t StateBlock::size() const { return states.size(); } - template - void StateBlock::insert(value_type const& state) { + bool StateBlock::empty() const { + return states.empty(); + } + + void StateBlock::insert(value_type const& state) { states.insert(state); } - template - void StateBlock::erase(value_type const& state) { + void StateBlock::erase(value_type const& state) { states.erase(state); } - template - bool StateBlock::containsState(value_type const& state) const { + bool StateBlock::containsState(value_type const& state) const { return this->states.find(state) != this->states.end(); } + StateBlock::container_type const& StateBlock::getStates() const { + return this->states; + } + std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block) { out << "{"; for (auto const& element : block) { @@ -51,7 +51,9 @@ namespace storm { return out; } - // Explicitly instantiate template. - template Block; + std::ostream& operator<<(std::ostream& out, StateBlock const& block) { + out << block.getStates(); + return out; + } } } \ No newline at end of file diff --git a/src/storage/StateBlock.h b/src/storage/StateBlock.h index 70d08240f..ad80fd62e 100644 --- a/src/storage/StateBlock.h +++ b/src/storage/StateBlock.h @@ -3,6 +3,7 @@ #include +#include "src/utility/OsDetection.h" #include "src/storage/sparse/StateType.h" namespace storm { @@ -11,24 +12,54 @@ namespace storm { // Typedef the most common state container typedef boost::container::flat_set FlatSetStateContainer; - /*! - * 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, FlatSetStateContainer const& block); - - template + class StateBlock { public: - typedef ContainerType container_type; + typedef FlatSetStateContainer container_type; typedef typename container_type::value_type value_type; static_assert(std::is_same::value, "Illegal value type of container."); typedef typename container_type::iterator iterator; typedef typename container_type::const_iterator const_iterator; + // Default constructors. + StateBlock() = default; + StateBlock(StateBlock const& other) = default; + StateBlock(StateBlock&& other) = default; +#ifndef WINDOWS + StateBlock& operator=(StateBlock const& other) = default; + StateBlock& operator=(StateBlock&& other) = default; +#endif + /*! + * Creates a state block and inserts all elements in the given range. + * + * @param first The first element of the range to insert. + * @param last The last element of the range (that is itself not inserted). + */ + template + StateBlock(InputIterator first, InputIterator last) : states(first, last) { + // Intentionally left empty. + } + + /*! + * Constructs a state block from the given initializer list. + * + * @param list The list of states to add to this state block. + */ + StateBlock(std::initializer_list list) : states(list.begin(), list.end()) { + // Intentionally left empty. + } + + /*! + * Checks whether the two state blocks contain exactly the same states. + * + * @param other The state block with which to compare the current one. + * @return True iff the two state blocks contain exactly the same states. + */ + bool operator==(StateBlock const& other) const { + return this->states == other.states; + } + /*! * Returns an iterator to the states in this SCC. * @@ -92,10 +123,26 @@ namespace storm { */ bool empty() const; + /*! + * Retrieves the set of states contained in the StateBlock. + * + * @return The set of states contained in the StateBlock. + */ + container_type const& getStates() const; + private: // The container that holds the states. - ContainerType states; + container_type states; }; + + /*! + * 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); } } diff --git a/src/storage/StronglyConnectedComponent.h b/src/storage/StronglyConnectedComponent.h index ff5305e40..10915d940 100644 --- a/src/storage/StronglyConnectedComponent.h +++ b/src/storage/StronglyConnectedComponent.h @@ -3,6 +3,7 @@ #include "src/storage/StateBlock.h" #include "src/storage/Decomposition.h" +#include "src/utility/OsDetection.h" namespace storm { namespace storage { @@ -11,11 +12,15 @@ namespace storm { * This class represents a strongly connected component, i.e., a set of states such that every state can reach * every other state. */ - class StronglyConnectedComponent : public StateBlock { - /*! - * Creates an empty strongly connected component. - */ - StronglyConnectedComponent(); + class StronglyConnectedComponent : public StateBlock { + public: + StronglyConnectedComponent() = default; + StronglyConnectedComponent(StronglyConnectedComponent const& other) = default; + StronglyConnectedComponent(StronglyConnectedComponent&& other) = default; +#ifndef WINDOWS + StronglyConnectedComponent& operator=(StronglyConnectedComponent const& other) = default; + StronglyConnectedComponent& operator=(StronglyConnectedComponent&& other) = default; +#endif /*! * Sets whether this SCC is trivial or not. diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 8c7a7761b..d8e80a36f 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -14,8 +14,7 @@ namespace storm { } template - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end()); performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs); } @@ -204,6 +203,5 @@ namespace storm { // Explicitly instantiate the SCC decomposition. template class StronglyConnectedComponentDecomposition; - template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); } // namespace storage } // namespace storm \ No newline at end of file diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index 049a7ada5..a14d05953 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -46,8 +46,7 @@ namespace storm { * @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. */ - template - StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + 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. diff --git a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp index 21939d1bf..a5872a921 100644 --- a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -37,8 +37,8 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem2) { storm::storage::StateBlock const& scc1 = sccDecomposition[0]; storm::storage::StateBlock const& scc2 = sccDecomposition[1]; - std::vector correctScc1 = {1, 3, 8, 9, 10}; - std::vector correctScc2 = {4, 5, 6, 7}; + storm::storage::StateBlock correctScc1 = {1, 3, 8, 9, 10}; + storm::storage::StateBlock correctScc2 = {4, 5, 6, 7}; ASSERT_TRUE(scc1 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc1 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end())); ASSERT_TRUE(scc2 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc2 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));