diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 84663dbc0..e8283a59f 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -148,7 +148,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @param partition A vector 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 { + 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. @@ -165,7 +165,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::Decomposition::Block const& block = decomposition[currentBlockIndex]; + typename storm::storage::StateBlock const& block = decomposition[currentBlockIndex]; // Now, we determine the blocks which are reachable (in one step) from the current block. storm::storage::VectorSet allTargetBlocks; diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 72ad4434c..20c30aa73 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -6,6 +6,8 @@ #include #include +#include "src/storage/VectorSet.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" @@ -138,6 +140,19 @@ public: this->bucketArray = new uint64_t[bucketCount](); } } + + /*! + * Creates a bit vector that has exactly those bits set that are defined by the given set. + * + * @param length The length of the bit vector to create. + * @param bitsToSet A set of indices whose bits to set in the bit vector. + * @param initTrue The initial value of the first |length| bits. + */ + BitVector(uint_fast64_t length, storm::storage::VectorSet const& bitsToSet, bool initTrue = false) : BitVector(length, initTrue) { + for (auto bit : bitsToSet) { + this->set(bit, true); + } + } /*! * Copy Constructor. Performs a deep copy of the given bit vector. diff --git a/src/storage/Decomposition.cpp b/src/storage/Decomposition.cpp index dace4879a..fd7380f3d 100644 --- a/src/storage/Decomposition.cpp +++ b/src/storage/Decomposition.cpp @@ -1,57 +1,85 @@ #include "src/storage/Decomposition.h" +#include "src/storage/MaximalEndComponent.h" namespace storm { namespace storage { - Decomposition::Decomposition() : blocks() { + template + Decomposition::Decomposition() : blocks() { // Intentionally left empty. } - Decomposition::Decomposition(Decomposition const& other) : blocks(other.blocks) { + template + Decomposition::Decomposition(Decomposition const& other) : blocks(other.blocks) { // Intentionally left empty. } - Decomposition& Decomposition::operator=(Decomposition const& other) { + template + Decomposition& Decomposition::operator=(Decomposition const& other) { this->blocks = other.blocks; return *this; } - Decomposition::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) { + template + Decomposition::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) { // Intentionally left empty. } - Decomposition& Decomposition::operator=(Decomposition&& other) { + template + Decomposition& Decomposition::operator=(Decomposition&& other) { this->blocks = std::move(other.blocks); return *this; } - size_t Decomposition::size() const { + template + size_t Decomposition::size() const { return blocks.size(); } - Decomposition::iterator Decomposition::begin() { + template + typename Decomposition::iterator Decomposition::begin() { return blocks.begin(); } - Decomposition::iterator Decomposition::end() { + template + typename Decomposition::iterator Decomposition::end() { return blocks.end(); } - Decomposition::const_iterator Decomposition::begin() const { + template + typename Decomposition::const_iterator Decomposition::begin() const { return blocks.begin(); } - Decomposition::const_iterator Decomposition::end() const { + template + typename Decomposition::const_iterator Decomposition::end() const { return blocks.end(); } - Decomposition::Block const& Decomposition::getBlock(uint_fast64_t index) const { + template + BlockType const& Decomposition::getBlock(uint_fast64_t index) const { return blocks.at(index); } - Decomposition::Block const& Decomposition::operator[](uint_fast64_t index) const { + template + BlockType const& Decomposition::operator[](uint_fast64_t index) const { return blocks[index]; } + template + std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition) { + out << "{"; + if (decomposition.size() > 0) { + for (uint_fast64_t blockIndex = 0; blockIndex < decomposition.size() - 1; ++blockIndex) { + out << decomposition.blocks[blockIndex] << ", "; + } + out << decomposition.blocks[decomposition.size() - 1]; + } + out << "}"; + return out; + } + + template class Decomposition; + template class Decomposition; } // namespace storage } // namespace storm \ No newline at end of file diff --git a/src/storage/Decomposition.h b/src/storage/Decomposition.h index 4bf8cc9c8..27f12648b 100644 --- a/src/storage/Decomposition.h +++ b/src/storage/Decomposition.h @@ -7,15 +7,17 @@ namespace storm { namespace storage { + typedef storm::storage::VectorSet StateBlock; /*! - * This class represents the decomposition of a model into state sets. + * This class represents the decomposition of a model into blocks which are of the template type. */ + template class Decomposition { public: - typedef storm::storage::VectorSet Block; - typedef std::vector::iterator iterator; - typedef std::vector::const_iterator const_iterator; + typedef BlockType Block; + typedef typename std::vector::iterator iterator; + typedef typename std::vector::const_iterator const_iterator; /* * Creates an empty SCC decomposition. @@ -44,6 +46,8 @@ namespace storm { Block const& operator[](uint_fast64_t index) const; + 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 new file mode 100644 index 000000000..54e0d950b --- /dev/null +++ b/src/storage/MaximalEndComponent.cpp @@ -0,0 +1,52 @@ +#include "src/storage/MaximalEndComponent.h" +#include "src/exceptions/InvalidStateException.h" + +namespace storm { + namespace storage { + + MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() { + // Intentionally left empty. + } + + MaximalEndComponent::MaximalEndComponent(MaximalEndComponent const& other) : stateToChoicesMapping(other.stateToChoicesMapping) { + // Intentionally left empty. + } + + MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent const& other) { + stateToChoicesMapping = other.stateToChoicesMapping; + return *this; + } + + MaximalEndComponent::MaximalEndComponent(MaximalEndComponent&& other) : stateToChoicesMapping(std::move(other.stateToChoicesMapping)) { + // Intentionally left empty. + } + + MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent&& other) { + stateToChoicesMapping = std::move(other.stateToChoicesMapping); + return *this; + } + + void MaximalEndComponent::addState(uint_fast64_t state, std::vector const& choices) { + stateToChoicesMapping[state] = choices; + } + + std::vector 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."; + } + + return stateChoicePair->second; + } + + bool MaximalEndComponent::containsState(uint_fast64_t state) const { + auto stateChoicePair = stateToChoicesMapping.find(state); + + if (stateChoicePair == stateToChoicesMapping.end()) { + return false; + } + return true; + } + } +} \ No newline at end of file diff --git a/src/storage/MaximalEndComponent.h b/src/storage/MaximalEndComponent.h new file mode 100644 index 000000000..c80e7e817 --- /dev/null +++ b/src/storage/MaximalEndComponent.h @@ -0,0 +1,59 @@ +#ifndef STORM_STORAGE_MAXIMALENDCOMPONENT_H_ +#define STORM_STORAGE_MAXIMALENDCOMPONENT_H_ + +#include +#include + +namespace storm { + namespace storage { + /*! + * This class represents a maximal end-component of a nondeterministic model. + */ + class MaximalEndComponent { + public: + /*! + * Creates an empty MEC. + */ + MaximalEndComponent(); + + MaximalEndComponent(MaximalEndComponent const& other); + + MaximalEndComponent& operator=(MaximalEndComponent const& other); + + MaximalEndComponent(MaximalEndComponent&& other); + + MaximalEndComponent& operator=(MaximalEndComponent&& other); + + /*! + * Adds the given state and the given choices to the MEC. + * + * @param state The state for which to add the choices. + * @param choices The choices to add for the state. + */ + void addState(uint_fast64_t state, std::vector const& choices); + + /*! + * 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. + */ + std::vector const& getChoicesForState(uint_fast64_t state) const; + + /*! + * Retrieves whether the given state is contained in this MEC. + * + * @param state The state for which to query membership in the MEC. + * @return True if the given state is contained in the MEC. + */ + bool containsState(uint_fast64_t state) const; + + private: + // This stores the mapping from states contained in the MEC to the choices in this MEC. + std::unordered_map> stateToChoicesMapping; + }; + } +} + +#endif /* STORM_STORAGE_MAXIMALENDCOMPONENT_H_ */ diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp new file mode 100644 index 000000000..97a893b67 --- /dev/null +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -0,0 +1,45 @@ +#include "src/storage/MaximalEndComponentDecomposition.h" + +namespace storm { + namespace storage { + + template + MaximalEndComponentDecomposition::MaximalEndComponentDecomposition() : Decomposition() { + // Intentionally left empty. + } + + template + MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel const& model) { + performMaximalEndComponentDecomposition(model); + } + + template + MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(MaximalEndComponentDecomposition const& other) : Decomposition(other) { + // Intentionally left empty. + } + + template + MaximalEndComponentDecomposition& MaximalEndComponentDecomposition::operator=(MaximalEndComponentDecomposition const& other) { + Decomposition::operator=(other); + return *this; + } + + template + MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(MaximalEndComponentDecomposition&& other) : Decomposition(std::move(other)) { + // Intentionally left empty. + } + + template + MaximalEndComponentDecomposition& MaximalEndComponentDecomposition::operator=(MaximalEndComponentDecomposition&& other) { + Decomposition::operator=(std::move(other)); + return *this; + } + + template + void MaximalEndComponentDecomposition::performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel const& model) { + // TODO. + } + + template class MaximalEndComponentDecomposition; + } +} \ No newline at end of file diff --git a/src/storage/MaximalEndComponentDecomposition.h b/src/storage/MaximalEndComponentDecomposition.h new file mode 100644 index 000000000..a530bd698 --- /dev/null +++ b/src/storage/MaximalEndComponentDecomposition.h @@ -0,0 +1,47 @@ +#ifndef STORM_STORAGE_MAXIMALENDCOMPONENTDECOMPOSITION_H_ +#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 { + + template + class MaximalEndComponentDecomposition : public Decomposition { + public: + /* + * Creates an empty MEC decomposition. + */ + MaximalEndComponentDecomposition(); + + /* + * Creates an MEC decomposition of the given model. + * + * @param model The model to decompose into MECs. + */ + MaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel const& model); + + MaximalEndComponentDecomposition(MaximalEndComponentDecomposition const& other); + + MaximalEndComponentDecomposition& operator=(MaximalEndComponentDecomposition const& other); + + MaximalEndComponentDecomposition(MaximalEndComponentDecomposition&& other); + + 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. + * + * @param model The model to decompose. + */ + void performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel const& model); + }; + } +} + +#endif /* STORM_STORAGE_MAXIMALENDCOMPONENTDECOMPOSITION_H_ */ diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 751337d01..abdd6ec1e 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -3,40 +3,46 @@ namespace storm { namespace storage { - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition() : Decomposition() { + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition() : Decomposition() { // Intentionally left empty. } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model) : Decomposition() { - performSccDecomposition(model); + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs) : Decomposition() { + performSccDecomposition(model, dropNaiveSccs); } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other) : Decomposition(other) { + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs) { + storm::storage::BitVector subsystem(model.getNumberOfStates(), block); + performSccDecomposition(model, subsystem, dropNaiveSccs); + } + + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other) : Decomposition(other) { // Intentionally left empty. } - template - StronglyConnectedComponentDecomposition& StronglyConnectedComponentDecomposition::operator=(StronglyConnectedComponentDecomposition const& other) { + template + StronglyConnectedComponentDecomposition& StronglyConnectedComponentDecomposition::operator=(StronglyConnectedComponentDecomposition const& other) { this->blocks = other.blocks; return *this; } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other) : Decomposition(std::move(other)) { + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other) : Decomposition(std::move(other)) { // Intentionally left empty. } - template - StronglyConnectedComponentDecomposition& StronglyConnectedComponentDecomposition::operator=(StronglyConnectedComponentDecomposition&& other) { + template + StronglyConnectedComponentDecomposition& StronglyConnectedComponentDecomposition::operator=(StronglyConnectedComponentDecomposition&& other) { this->blocks = std::move(other.blocks); return *this; } - template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel const& model) { + template + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); uint_fast64_t numberOfStates = model.getNumberOfStates(); @@ -49,26 +55,38 @@ namespace storm { std::vector lowlinks(numberOfStates); storm::storage::BitVector visitedStates(numberOfStates); - // Start the search for SCCs from every vertex in the graph structure, because there is. + // Start the search for SCCs from every vertex in the block. uint_fast64_t currentIndex = 0; - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { + for (auto state : subsystem) { if (!visitedStates.get(state)) { - performSccDecompositionHelper(model, state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates); + performSccDecompositionHelper(model, state, subsystem, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, dropNaiveSccs); } } LOG4CPLUS_INFO(logger, "Done computing SCC decomposition."); } + + + template + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs) { + 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); + + // Call the overloaded function. + performSccDecomposition(model, fullSystem, dropNaiveSccs); + } - template - void StronglyConnectedComponentDecomposition::performSccDecompositionHelper(storm::models::AbstractModel const& model, uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates) { + 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) { // 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::ConstIterator> recursionIteratorStack; + std::vector::ConstIterator> recursionIteratorStack; recursionIteratorStack.reserve(lowlinks.size()); std::vector statesInStack(lowlinks.size()); @@ -79,9 +97,9 @@ namespace storm { recursionStepForward: while (!recursionStateStack.empty()) { uint_fast64_t currentState = recursionStateStack.back(); - typename storm::storage::SparseMatrix::ConstIterator successorIt = recursionIteratorStack.back(); + typename storm::storage::SparseMatrix::ConstIterator successorIt = recursionIteratorStack.back(); - // Perform the treatment of newly discovered state as defined by Tarjan's algorithm + // Perform the treatment of newly discovered state as defined by Tarjan's algorithm. visitedStates.set(currentState, true); stateIndices[currentState] = currentIndex; lowlinks[currentState] = currentIndex; @@ -93,7 +111,7 @@ namespace storm { for(; successorIt != model.getRows(currentState).end(); ++successorIt) { // If we have not visited the successor already, we need to perform the procedure // recursively on the newly found state. - if (!visitedStates.get(successorIt.column())) { + if (!visitedStates.get(successorIt.column()) && subsystem.get(successorIt.column())) { // Save current iterator position so we can continue where we left off later. recursionIteratorStack.pop_back(); recursionIteratorStack.push_back(successorIt); @@ -131,7 +149,11 @@ namespace storm { // Add the state to the current SCC. scc.insert(lastState); } while (lastState != currentState); - this->blocks.emplace_back(std::move(scc)); + + // Only add the SCC if it is non-trivial if the corresponding flag was set. + if (scc.size() > 1 || !dropNaiveSccs) { + this->blocks.emplace_back(std::move(scc)); + } } // If we reach this point, we have completed the recursive descent for the current state. diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index a2f3e365b..f1348fafd 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -9,7 +9,7 @@ namespace storm { namespace models { // Forward declare the abstract model class. - template class AbstractModel; + template class AbstractModel; } namespace storage { @@ -17,8 +17,8 @@ namespace storm { /*! * This class represents the decomposition of a graph-like structure into its strongly connected components. */ - template - class StronglyConnectedComponentDecomposition : public Decomposition { + template + class StronglyConnectedComponentDecomposition : public Decomposition { public: /* * Creates an empty SCC decomposition. @@ -27,8 +27,22 @@ namespace storm { /* * Creates an SCC decomposition of the given model. + * + * @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. */ - StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model); + StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs = false); + + /* + * Creates an SCC decomposition of given block in the given model. + * + * @param model The model that contains the block. + * @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. + */ + StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs = false); StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other); @@ -39,9 +53,11 @@ namespace storm { StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other); private: - void performSccDecomposition(storm::models::AbstractModel const& model); + void performSccDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs); + + void performSccDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs); - void performSccDecompositionHelper(storm::models::AbstractModel const& model, uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates); + 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); }; } } diff --git a/src/storage/VectorSet.h b/src/storage/VectorSet.h index 7ceaa466f..8b42f3895 100644 --- a/src/storage/VectorSet.h +++ b/src/storage/VectorSet.h @@ -14,6 +14,8 @@ #include #include +#include "src/exceptions/InvalidStateException.h" + namespace storm { namespace storage { @@ -149,6 +151,24 @@ namespace storm { return data.end(); } + T const& min() const { + if (this->size() == 0) { + throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; + } + + ensureSet(); + return data.first; + } + + T const& max() const { + if (this->size() == 0) { + throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; + } + + ensureSet(); + return data.back; + } + void insert(T const& element) { data.push_back(element); dirty = true; diff --git a/src/storm.cpp b/src/storm.cpp index b6dd20bc6..c82d2ac2e 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -24,6 +24,7 @@ #include "src/models/Dtmc.h" #include "src/models/MarkovAutomaton.h" #include "src/storage/SparseMatrix.h" +#include "src/storage/MaximalEndComponentDecomposition.h" #include "src/models/AtomicPropositionsLabeling.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"