diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index f7c314eb4..31c421224 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -15,7 +15,8 @@ namespace storm { } template - MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model) { + template + MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model) { performMaximalEndComponentDecomposition(model.getTransitionMatrix(), model.getBackwardTransitions(), storm::storage::BitVector(model.getNumberOfStates(), true)); } @@ -183,5 +184,7 @@ namespace storm { // Explicitly instantiate the MEC decomposition. template class MaximalEndComponentDecomposition; + template MaximalEndComponentDecomposition::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); + } } diff --git a/src/storage/MaximalEndComponentDecomposition.h b/src/storage/MaximalEndComponentDecomposition.h index 9708bd65a..263683c09 100644 --- a/src/storage/MaximalEndComponentDecomposition.h +++ b/src/storage/MaximalEndComponentDecomposition.h @@ -24,7 +24,8 @@ namespace storm { * * @param model The model to decompose into MECs. */ - MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); + template > + MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); /* * Creates an MEC decomposition of the given model (represented by a row-grouped matrix). diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 0e3938da3..c49e6977f 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -5,68 +5,71 @@ namespace storm { namespace storage { - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition() : Decomposition() { + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition() : Decomposition() { // Intentionally left empty. } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) : Decomposition() { + template + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) : Decomposition() { performSccDecomposition(model, dropNaiveSccs, onlyBottomSccs); } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { + template + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model 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); } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { + template + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs); } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { storm::storage::BitVector subsystem(transitionMatrix.getRowGroupCount(), block.begin(), block.end()); performSccDecomposition(transitionMatrix, subsystem, dropNaiveSccs, onlyBottomSccs); } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs, bool onlyBottomSccs) { + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs, bool onlyBottomSccs) { performSccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), dropNaiveSccs, onlyBottomSccs); } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { performSccDecomposition(transitionMatrix, subsystem, dropNaiveSccs, onlyBottomSccs); } - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other) : Decomposition(other) { + 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::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { + template + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // Set up the environment of the algorithm. @@ -154,8 +157,9 @@ namespace storm { } } - template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) { + template + template + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) { // Prepare a block that contains all states for a call to the other overload of this function. storm::storage::BitVector fullSystem(model.getNumberOfStates(), true); @@ -163,8 +167,8 @@ namespace storm { performSccDecomposition(model.getTransitionMatrix(), fullSystem, dropNaiveSccs, onlyBottomSccs); } - template - void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount) { + template + void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector& preorderNumbers, std::vector& s, std::vector& p, storm::storage::BitVector& stateHasScc, std::vector& stateToSccMapping, uint_fast64_t& sccCount) { // Prepare the stack used for turning the recursive procedure into an iterative one. std::vector recursionStateStack; @@ -224,9 +228,20 @@ namespace storm { // Explicitly instantiate the SCC decomposition. template class StronglyConnectedComponentDecomposition; + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); + template class StronglyConnectedComponentDecomposition; + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); + #ifdef STORM_HAVE_CARL template class StronglyConnectedComponentDecomposition; + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs); + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); #endif } // namespace storage } // namespace storm \ No newline at end of file diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index 8ef054632..12da304da 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -20,7 +20,7 @@ namespace storm { /*! * This class represents the decomposition of a graph-like structure into its strongly connected components. */ - template > + template class StronglyConnectedComponentDecomposition : public Decomposition { public: /* @@ -37,6 +37,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::sparse::Model const& model, bool dropNaiveSccs = false, bool onlyBottomSccs = false); /* @@ -49,6 +50,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::sparse::Model const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); /* @@ -61,6 +63,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::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); /* @@ -139,6 +142,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 > void performSccDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); /*