diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 73357743c..a74c801f9 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -73,7 +73,7 @@ namespace storm { template void SparseSccModelChecker::treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) { - // If the SCCs are still quite large, we try to split them further. + // If the SCCs are large enough, we try to split them further. if (scc.getNumberOfSetBits() > SparseSccModelChecker::maximalSccSize) { // Here, we further decompose the SCC into sub-SCCs. storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, true, false); diff --git a/src/storage/Block.cpp b/src/storage/Block.cpp new file mode 100644 index 000000000..02d4b921f --- /dev/null +++ b/src/storage/Block.cpp @@ -0,0 +1,49 @@ +#include "src/storage/Block.h" + +namespace storm { + namespace storage { + Block::iterator Block::begin() { + return states.begin(); + } + + Block::const_iterator Block::begin() const { + return states.begin(); + } + + StronglyConnectedComponent::iterator Block::end() { + return states.end(); + } + + StronglyConnectedComponent::const_iterator Block::end() const { + return states.end(); + } + + std::size_t Block::size() const { + return states.size(); + } + + void Block::insert(value_type const& state) { + states.insert(state); + } + + void Block::erase(value_type const& state) { + states.erase(state); + } + + bool Block::containsState(value_type const& state) const { + return this->states.find(state) != this->states.end(); + } + + std::ostream& operator<<(std::ostream& out, StateBlock const& block) { + out << "{"; + for (auto const& element : block) { + out << element << ", "; + } + out << "}"; + return out; + } + + // Explicitly instantiate template. + template Block<>; + } +} \ No newline at end of file diff --git a/src/storage/Block.h b/src/storage/Block.h new file mode 100644 index 000000000..235609372 --- /dev/null +++ b/src/storage/Block.h @@ -0,0 +1,93 @@ +#ifndef STORM_STORAGE_BLOCK_H_ +#define STORM_STORAGE_BLOCK_H_ + +#include + +namespace storm { + namespace storage { + + 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); + + class Block { + public: + typedef ContainerType container_type; + typedef typename container_type::value_type value_type; + typedef typename container_type::iterator iterator; + typedef typename container_type::const_iterator const_iterator; + + /*! + * Returns an iterator to the states in this SCC. + * + * @return An iterator to the states in this SCC. + */ + iterator begin(); + + /*! + * Returns a const iterator to the states in this SCC. + * + * @return A const iterator to the states in this SCC. + */ + const_iterator begin() const; + + /*! + * Returns an iterator that points one past the end of the states in this SCC. + * + * @return An iterator that points one past the end of the states in this SCC. + */ + iterator end(); + + /*! + * Returns a const iterator that points one past the end of the states in this SCC. + * + * @return A const iterator that points one past the end of the states in this SCC. + */ + const_iterator end() const; + + /*! + * Retrieves whether the given state is in the SCC. + * + * @param state The state for which to query membership. + */ + bool containsState(value_type const& state) const; + + /*! + * Inserts the given element into this SCC. + * + * @param state The state to add to this SCC. + */ + void insert(value_type const& state); + + /*! + * Removes the given element from this SCC. + * + * @param state The element to remove. + */ + void erase(value_type const& state); + + /*! + * Retrieves the number of states in this SCC. + * + * @return The number of states in this SCC. + */ + std::size_t size() const; + + /*! + * Retrieves whether this SCC is empty. + * + * @return True iff the SCC is empty. + */ + bool empty() const; + }; + } +} + +#endif /* STORM_STORAGE_BLOCK_H_ */ \ No newline at end of file diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp index ccb14ee46..36f22c50c 100644 --- a/src/storage/Decomposition.cpp +++ b/src/storage/Decomposition.cpp @@ -76,15 +76,6 @@ namespace storm { return blocks[index]; } - std::ostream& operator<<(std::ostream& out, StateBlock const& block) { - out << "{"; - for (auto const& element : block) { - out << element << ", "; - } - 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 0c44943c9..3d47417e0 100644 --- a/src/storage/Decomposition.h +++ b/src/storage/Decomposition.h @@ -2,21 +2,9 @@ #define STORM_STORAGE_DECOMPOSITION_H_ #include -#include 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); /*! * This class represents the decomposition of a model into blocks which are of the template type. @@ -24,9 +12,9 @@ namespace storm { template class Decomposition { public: - typedef BlockType Block; - typedef typename std::vector::iterator iterator; - typedef typename std::vector::const_iterator const_iterator; + typedef BlockType block_type; + typedef typename std::vector::iterator iterator; + typedef typename std::vector::const_iterator const_iterator; /*! * Creates an empty decomposition. @@ -104,7 +92,7 @@ namespace storm { * @param index The index of the block to retrieve. * @return The block with the given index. */ - Block const& getBlock(uint_fast64_t index) const; + block_type 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. @@ -112,7 +100,7 @@ namespace storm { * @param index The index of the block to retrieve. * @return The block with the given index. */ - Block& getBlock(uint_fast64_t index); + block_type& getBlock(uint_fast64_t index); /*! * Retrieves the block with the given index. If the index is out-of-bounds, an behaviour is undefined. @@ -120,7 +108,7 @@ namespace storm { * @param index The index of the block to retrieve. * @return The block with the given index. */ - Block const& operator[](uint_fast64_t index) const; + block_type 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. @@ -128,7 +116,7 @@ namespace storm { * @param index The index of the block to retrieve. * @return The block with the given index. */ - Block& operator[](uint_fast64_t index); + block_type& operator[](uint_fast64_t index); // Declare the streaming operator as a friend function to enable output of decompositions. template @@ -136,7 +124,7 @@ namespace storm { protected: // The blocks of the decomposition. - std::vector blocks; + std::vector blocks; }; } } diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 0f6a44f65..683083d32 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -88,7 +88,7 @@ namespace storm { for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { bool choiceContainedInMEC = true; for (auto const& entry : transitionMatrix.getRow(choice)) { - if (scc.find(entry.getColumn()) == scc.end()) { + if (!scc.containsState(entry.getColumn())) { choiceContainedInMEC = false; break; } @@ -116,7 +116,7 @@ namespace storm { statesToCheck.clear(); for (auto state : statesToRemove) { for (auto const& entry : backwardTransitions.getRow(state)) { - if (scc.find(entry.getColumn()) != scc.end()) { + if (!scc.containsState(entry.getColumn())) { statesToCheck.set(entry.getColumn()); } } @@ -127,7 +127,7 @@ 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 (mecChanged) { - for (StateBlock& scc : sccs) { + for (StronglyConnectedComponent& scc : sccs) { if (!scc.empty()) { endComponentStateSets.push_back(std::move(scc)); } diff --git a/src/storage/StronglyConnectedComponent.cpp b/src/storage/StronglyConnectedComponent.cpp new file mode 100644 index 000000000..6540a8acf --- /dev/null +++ b/src/storage/StronglyConnectedComponent.cpp @@ -0,0 +1,13 @@ +#include "src/storage/StronglyConnectedComponent.h" + +namespace storm { + namespace storage { + void StronglyConnectedComponent::setIsTrivial(bool trivial) { + this->isTrivialScc = trivial; + } + + bool StronglyConnectedComponent::isTrivial() const { + return isTrivialScc; + } + } +} \ No newline at end of file diff --git a/src/storage/StronglyConnectedComponent.h b/src/storage/StronglyConnectedComponent.h new file mode 100644 index 000000000..903ac9ea8 --- /dev/null +++ b/src/storage/StronglyConnectedComponent.h @@ -0,0 +1,53 @@ +#ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_ +#define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_ + +#include "src/storage/Block.h" +#include "src/storage/Decomposition.h" + +namespace storm { + namespace storage { + + typedef FlatSetStateContainer SccBlock; + + /*! + * 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 Block { + public: + typedef SccBlock block_type; + typedef block_type::value_type value_type; + typedef block_type::iterator iterator; + typedef block_type::const_iterator const_iterator; + + /*! + * Creates an empty strongly connected component. + */ + StronglyConnectedComponent(); + + /*! + * Sets whether this SCC is trivial or not. + * + * @param trivial A flag indicating whether this SCC is trivial or not. + */ + void setIsTrivial(bool trivial); + + /*! + * Retrieves whether this SCC is trivial. + * + * @return True iff this SCC is trivial. + */ + bool isTrivial() const; + + private: + // Stores whether this SCC is trivial. + bool isTrivialScc; + + // The states in this SCC. + block_type states; + }; + + } +} + +#endif /* STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_ */ \ No newline at end of file diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index f519fc8ae..d8e80a36f 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -119,7 +119,7 @@ namespace storm { } // Create the new set of blocks by moving all the blocks we need to keep into it. - std::vector newBlocks((~blocksToDrop).getNumberOfSetBits()); + std::vector newBlocks((~blocksToDrop).getNumberOfSetBits()); uint_fast64_t currentBlock = 0; for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) { if (!blocksToDrop.get(blockIndex)) { diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index a83f6fe17..53cb1949a 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -3,6 +3,7 @@ #include "src/storage/SparseMatrix.h" #include "src/storage/Decomposition.h" +#include "src/storage/StronglyConnectedComponent.h" #include "src/storage/BitVector.h" namespace storm { @@ -17,8 +18,8 @@ namespace storm { * This class represents the decomposition of a graph-like structure into its strongly connected components. */ template - class StronglyConnectedComponentDecomposition : public Decomposition { - public: + class StronglyConnectedComponentDecomposition : public Decomposition { + public: /* * Creates an empty SCC decomposition. */ @@ -45,7 +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. */ - StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, Block const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); /* * Creates an SCC decomposition of the given subsystem in the given model.