diff --git a/CMakeLists.txt b/CMakeLists.txt
index 7b7e66ec2..80d5d806f 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -254,6 +254,7 @@ file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SO
file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp)
+file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp)
file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp)
# Test Sources
# Note that the tests also need the source files, except for the main file
@@ -287,6 +288,7 @@ source_group(storage FILES ${STORM_STORAGE_FILES})
source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES})
source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES})
source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES})
+source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES})
source_group(utility FILES ${STORM_UTILITY_FILES})
source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES})
source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES})
diff --git a/src/storage/Block.cpp b/src/storage/Block.cpp
deleted file mode 100644
index 02d4b921f..000000000
--- a/src/storage/Block.cpp
+++ /dev/null
@@ -1,49 +0,0 @@
-#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/StateBlock.cpp b/src/storage/StateBlock.cpp
new file mode 100644
index 000000000..f70e1aa9c
--- /dev/null
+++ b/src/storage/StateBlock.cpp
@@ -0,0 +1,57 @@
+#include "src/storage/StateBlock.h"
+
+namespace storm {
+ namespace storage {
+ template <typename ContainerType>
+ typename StateBlock<ContainerType>::iterator StateBlock<ContainerType>::begin() {
+ return states.begin();
+ }
+
+ template <typename ContainerType>
+ typename StateBlock<ContainerType>::const_iterator StateBlock<ContainerType>::begin() const {
+ return states.begin();
+ }
+
+ template <typename ContainerType>
+ typename StateBlock<ContainerType>::iterator StateBlock<ContainerType>::end() {
+ return states.end();
+ }
+
+ template <typename ContainerType>
+ typename StateBlock<ContainerType>::const_iterator StateBlock<ContainerType>::end() const {
+ return states.end();
+ }
+
+ template <typename ContainerType>
+ std::size_t StateBlock<ContainerType>::size() const {
+ return states.size();
+ }
+
+ template <typename ContainerType>
+ void StateBlock<ContainerType>::insert(value_type const& state) {
+ states.insert(state);
+ }
+
+ template <typename ContainerType>
+ void StateBlock<ContainerType>::erase(value_type const& state) {
+ states.erase(state);
+ }
+
+ template <typename ContainerType>
+ bool StateBlock<ContainerType>::containsState(value_type const& state) const {
+ return this->states.find(state) != this->states.end();
+ }
+
+ std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block) {
+ out << "{";
+ for (auto const& element : block) {
+ out << element << ", ";
+ }
+ out << "}";
+ return out;
+ }
+
+ // Explicitly instantiate template.
+ template Block<FlatSetStateContainer>;
+ }
+}
\ No newline at end of file
diff --git a/src/storage/Block.h b/src/storage/StateBlock.h
similarity index 84%
rename from src/storage/Block.h
rename to src/storage/StateBlock.h
index 235609372..70d08240f 100644
--- a/src/storage/Block.h
+++ b/src/storage/StateBlock.h
@@ -3,10 +3,13 @@
#include <boost/container/flat_set.hpp>
+#include "src/storage/sparse/StateType.h"
+
namespace storm {
namespace storage {
- typedef boost::container::flat_set<uint_fast64_t> FlatSetStateContainer;
+ // Typedef the most common state container
+ typedef boost::container::flat_set<sparse::state_type> FlatSetStateContainer;
/*!
* Writes a string representation of the state block to the given output stream.
@@ -17,10 +20,12 @@ namespace storm {
*/
std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block);
- class Block {
+ template <typename ContainerType = FlatSetStateContainer>
+ class StateBlock {
public:
typedef ContainerType container_type;
typedef typename container_type::value_type value_type;
+ static_assert(std::is_same<value_type, sparse::state_type>::value, "Illegal value type of container.");
typedef typename container_type::iterator iterator;
typedef typename container_type::const_iterator const_iterator;
@@ -86,6 +91,10 @@ namespace storm {
* @return True iff the SCC is empty.
*/
bool empty() const;
+
+ private:
+ // The container that holds the states.
+ ContainerType states;
};
}
}
diff --git a/src/storage/StronglyConnectedComponent.h b/src/storage/StronglyConnectedComponent.h
index 903ac9ea8..ff5305e40 100644
--- a/src/storage/StronglyConnectedComponent.h
+++ b/src/storage/StronglyConnectedComponent.h
@@ -1,25 +1,17 @@
#ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_
#define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENT_H_
-#include "src/storage/Block.h"
+#include "src/storage/StateBlock.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<SccBlock> {
- public:
- typedef SccBlock block_type;
- typedef block_type::value_type value_type;
- typedef block_type::iterator iterator;
- typedef block_type::const_iterator const_iterator;
-
+ class StronglyConnectedComponent : public StateBlock<FlatSetStateContainer> {
/*!
* Creates an empty strongly connected component.
*/
@@ -42,9 +34,6 @@ namespace storm {
private:
// Stores whether this SCC is trivial.
bool isTrivialScc;
-
- // The states in this SCC.
- block_type states;
};
}
diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp
index d8e80a36f..8c7a7761b 100644
--- a/src/storage/StronglyConnectedComponentDecomposition.cpp
+++ b/src/storage/StronglyConnectedComponentDecomposition.cpp
@@ -14,7 +14,8 @@ namespace storm {
}
template <typename ValueType>
- StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
+ template <typename ContainerType>
+ StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock<ContainerType> const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end());
performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs);
}
@@ -203,5 +204,6 @@ namespace storm {
// Explicitly instantiate the SCC decomposition.
template class StronglyConnectedComponentDecomposition<double>;
+ template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<double> const& model, StateBlock<FlatSetStateContainer> 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 53cb1949a..049a7ada5 100644
--- a/src/storage/StronglyConnectedComponentDecomposition.h
+++ b/src/storage/StronglyConnectedComponentDecomposition.h
@@ -46,7 +46,8 @@ 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<ValueType> const& model, Block const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
+ template<typename ContainerType>
+ StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock<ContainerType> const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
/*
* Creates an SCC decomposition of the given subsystem in the given model.
diff --git a/src/storage/sparse/StateType.h b/src/storage/sparse/StateType.h
new file mode 100644
index 000000000..a067c37e9
--- /dev/null
+++ b/src/storage/sparse/StateType.h
@@ -0,0 +1,13 @@
+#ifndef STORM_STORAGE_SPARSE_STATETYPE_H_
+#define STORM_STORAGE_SPARSE_STATETYPE_H_
+
+namespace storm {
+ namespace storage {
+ namespace sparse {
+ typedef uint_fast64_t state_type;
+ }
+ }
+}
+
+
+#endif /* STORM_STORAGE_SPARSE_STATETYPE_H_ */
\ No newline at end of file