From 5869a1f5fda7f844d09b286bb518b251fb0d0f5c Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 28 Mar 2019 18:06:33 +0100 Subject: [PATCH] Simplified StronglyConnectedComponentDecomposition. --- .../csl/helper/SparseCtmcCslHelper.cpp | 2 +- .../helper/SparseMarkovAutomatonCslHelper.cpp | 3 +- .../SparseDtmcEliminationModelChecker.cpp | 5 +- ...ologicalCudaMinMaxLinearEquationSolver.cpp | 3 +- .../TopologicalLinearEquationSolver.cpp | 7 +- .../TopologicalMinMaxLinearEquationSolver.cpp | 7 +- .../MaximalEndComponentDecomposition.cpp | 7 +- ...tronglyConnectedComponentDecomposition.cpp | 408 ++++++------------ .../StronglyConnectedComponentDecomposition.h | 183 ++------ src/storm/utility/graph.cpp | 2 +- ...glyConnectedComponentDecompositionTest.cpp | 28 +- 11 files changed, 209 insertions(+), 446 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 476c3cf2c..a6bee0577 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -413,7 +413,7 @@ namespace storm { uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); // Start by decomposing the CTMC into its BSCCs. - storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(probabilityMatrix, storm::storage::BitVector(probabilityMatrix.getRowCount(), true), false, true); + storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(probabilityMatrix, storm::storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs()); STORM_LOG_DEBUG("Found " << bsccDecomposition.size() << " BSCCs."); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index b2fcad350..f813564c2 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -244,8 +244,7 @@ namespace storm { storm::storage::BitVector probabilisticStates = ~markovianStates; // Searching for SCCs in probabilistic fragment to decide which algorithm is applied. - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(transitionMatrix, probabilisticStates, true, false); - bool cycleFree = sccDecomposition.empty(); + bool cycleFree = !storm::utility::graph::hasCycle(transitionMatrix, probabilisticStates); // Vectors to store computed vectors. UnifPlusVectors unifVectors; diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 2798d9c74..38af2e3ac 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -179,7 +179,7 @@ namespace storm { // Start by decomposing the DTMC into its BSCCs. std::chrono::high_resolution_clock::time_point sccDecompositionStart = std::chrono::high_resolution_clock::now(); - storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true); + storm::storage::StronglyConnectedComponentDecomposition bsccDecomposition(transitionMatrix, storm::storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs()); auto sccDecompositionEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); @@ -896,7 +896,8 @@ namespace storm { STORM_LOG_TRACE("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further."); // Here, we further decompose the SCC into sub-SCCs. - storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, false, false); + storm::storage::BitVector nonEntrySccStates = scc & ~entryStates; + storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, storm::storage::StronglyConnectedComponentDecompositionOptions().subsystem(&nonEntrySccStates)); STORM_LOG_TRACE("Decomposed SCC into " << decomposition.size() << " sub-SCCs."); // Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which diff --git a/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp index f31d1cde3..17acb643d 100644 --- a/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp @@ -136,8 +136,7 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!"; #endif } else { - storm::storage::BitVector fullSystem(this->A->getRowGroupCount(), true); - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*this->A, fullSystem, false, false); + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*this->A); STORM_LOG_THROW(sccDecomposition.size() > 0, storm::exceptions::IllegalArgumentException, "Can not solve given equation system as the SCC decomposition returned no SCCs."); diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index 5b31509fa..649843521 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -105,12 +105,9 @@ namespace storm { template void TopologicalLinearEquationSolver::createSortedSccDecomposition(bool needLongestChainSize) const { // Obtain the scc decomposition - this->sortedSccDecomposition = std::make_unique>(*this->A); + this->sortedSccDecomposition = std::make_unique>(*this->A, storm::storage::StronglyConnectedComponentDecompositionOptions().forceTobologicalSort().computeSccDepths(needLongestChainSize)); if (needLongestChainSize) { - this->longestSccChainSize = 0; - this->sortedSccDecomposition->sortTopologically(*this->A, &(this->longestSccChainSize.get())); - } else { - this->sortedSccDecomposition->sortTopologically(*this->A); + this->longestSccChainSize = this->sortedSccDecomposition->getMaxSccDepth() + 1; } } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 1f517fc10..7afb90bb6 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -113,12 +113,9 @@ namespace storm { template void TopologicalMinMaxLinearEquationSolver::createSortedSccDecomposition(bool needLongestChainSize) const { // Obtain the scc decomposition - this->sortedSccDecomposition = std::make_unique>(*this->A); + this->sortedSccDecomposition = std::make_unique>(*this->A, storm::storage::StronglyConnectedComponentDecompositionOptions().forceTobologicalSort().computeSccDepths(needLongestChainSize)); if (needLongestChainSize) { - this->longestSccChainSize = 0; - this->sortedSccDecomposition->sortTopologically(*this->A, &(this->longestSccChainSize.get())); - } else { - this->sortedSccDecomposition->sortTopologically(*this->A); + this->longestSccChainSize = this->sortedSccDecomposition->getMaxSccDepth() + 1; } } diff --git a/src/storm/storage/MaximalEndComponentDecomposition.cpp b/src/storm/storage/MaximalEndComponentDecomposition.cpp index ec5484912..f3401e09b 100644 --- a/src/storm/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storm/storage/MaximalEndComponentDecomposition.cpp @@ -93,15 +93,18 @@ namespace storm { } else { includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount(), true); } + storm::storage::BitVector currMecAsBitVector(transitionMatrix.getRowGroupCount()); for (std::list::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) { StateBlock const& mec = *mecIterator; - + currMecAsBitVector.clear(); + currMecAsBitVector.set(mec.begin(), mec.end(), true); // Keep track of whether the MEC changed during this iteration. bool mecChanged = false; // Get an SCC decomposition of the current MEC candidate. - StronglyConnectedComponentDecomposition sccs(transitionMatrix, mec, includedChoices, true); + + StronglyConnectedComponentDecomposition sccs(transitionMatrix, StronglyConnectedComponentDecompositionOptions().subsystem(&currMecAsBitVector).choices(&includedChoices).dropNaiveSccs()); // 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. diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp index 509eb196c..16d4fbfb6 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp @@ -1,3 +1,4 @@ +#include #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -14,49 +15,8 @@ namespace storm { } template - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) : Decomposition() { - performSccDecomposition(model, dropNaiveSccs, 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, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::sparse::Model const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(model.getTransitionMatrix(), &subsystem, nullptr, dropNaiveSccs, 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, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, storm::storage::BitVector const& choices, bool dropNaiveSccs, bool onlyBottomSccs) { - storm::storage::BitVector subsystem(transitionMatrix.getRowGroupCount(), block.begin(), block.end()); - performSccDecomposition(transitionMatrix, &subsystem, &choices, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(transitionMatrix, nullptr, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(transitionMatrix, &subsystem, nullptr, dropNaiveSccs, onlyBottomSccs); - } - - template - StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(transitionMatrix, &subsystem, &choices, dropNaiveSccs, onlyBottomSccs); + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options) { + performSccDecomposition(transitionMatrix, options); } template @@ -80,142 +40,31 @@ namespace storm { this->blocks = std::move(other.blocks); return *this; } - - template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, bool dropNaiveSccs, bool onlyBottomSccs) { - - STORM_LOG_ASSERT(!choices || subsystem, "Expecting subsystem if choices are given."); - - uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); - - // Set up the environment of the algorithm. - // Start with the two stacks it maintains. - std::vector s; - s.reserve(numberOfStates); - std::vector p; - p.reserve(numberOfStates); - - // We also need to store the preorder numbers of states and which states have been assigned to which SCC. - std::vector preorderNumbers(numberOfStates); - storm::storage::BitVector hasPreorderNumber(numberOfStates); - storm::storage::BitVector stateHasScc(numberOfStates); - std::vector stateToSccMapping(numberOfStates); - uint_fast64_t sccCount = 0; - - // Finally, we need to keep track of the states with a self-loop to identify naive SCCs. - storm::storage::BitVector statesWithSelfLoop(numberOfStates); - - // Start the search for SCCs from every state in the block. - uint_fast64_t currentIndex = 0; - if (subsystem) { - for (auto state : *subsystem) { - if (!hasPreorderNumber.get(state)) { - performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, choices, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); - } - } - } else { - for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { - if (!hasPreorderNumber.get(state)) { - performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, choices, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount); - } - } - } - - // After we obtained the state-to-SCC mapping, we build the actual blocks. - this->blocks.resize(sccCount); - if (subsystem) { - for (auto state : *subsystem) { - this->blocks[stateToSccMapping[state]].insert(state); - } - } else { - for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { - this->blocks[stateToSccMapping[state]].insert(state); - } - } - - // Now flag all trivial SCCs as such. - for (uint_fast64_t sccIndex = 0; sccIndex < sccCount; ++sccIndex) { - if (this->blocks[sccIndex].size() == 1) { - uint_fast64_t onlyState = *this->blocks[sccIndex].begin(); - - if (!statesWithSelfLoop.get(onlyState)) { - this->blocks[sccIndex].setIsTrivial(true); - } - } - } - - // If requested, we need to drop some SCCs. - if (onlyBottomSccs || dropNaiveSccs) { - storm::storage::BitVector blocksToDrop(sccCount); - - // If requested, we need to delete all naive SCCs. - if (dropNaiveSccs) { - for (uint_fast64_t sccIndex = 0; sccIndex < sccCount; ++sccIndex) { - if (this->blocks[sccIndex].isTrivial()) { - blocksToDrop.set(sccIndex); - } - } - } - - // If requested, we need to drop all non-bottom SCCs. - if (onlyBottomSccs) { - if (subsystem) { - for (uint64_t state : *subsystem) { - // If the block of the state is already known to be dropped, we don't need to check the transitions. - if (!blocksToDrop.get(stateToSccMapping[state])) { - for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row != endRow; ++row) { - if (choices && !choices->get(row)) { - continue; - } - for (auto const& entry : transitionMatrix.getRow(row)) { - if (subsystem->get(entry.getColumn()) && stateToSccMapping[state] != stateToSccMapping[entry.getColumn()]) { - blocksToDrop.set(stateToSccMapping[state]); - break; - } - } - } - } - } - } else { - for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { - // If the block of the state is already known to be dropped, we don't need to check the transitions. - if (!blocksToDrop.get(stateToSccMapping[state])) { - for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row != endRow; ++row) { - for (auto const& entry : transitionMatrix.getRow(row)) { - if (stateToSccMapping[state] != stateToSccMapping[entry.getColumn()]) { - blocksToDrop.set(stateToSccMapping[state]); - break; - } - } - } - } - } - } - } - - // Create the new set of blocks by moving all the blocks we need to keep into it. - 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)) { - newBlocks[currentBlock] = std::move(this->blocks[blockIndex]); - ++currentBlock; - } - } - - // Now set this new set of blocks as the result of the decomposition. - this->blocks = std::move(newBlocks); - } - } - - template - template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(model.getTransitionMatrix(), nullptr, nullptr, dropNaiveSccs, onlyBottomSccs); - } + /*! + * Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to + * compute a mapping of states to their SCCs. All arguments given by (non-const) reference are modified by + * the function as a side-effect. + * + * @param transitionMatrix The transition matrix of the system to decompose. + * @param startState The starting state for the search of Tarjan's algorithm. + * @param nonTrivialStates A bit vector where entries for non-trivial states (states that either have a selfloop or whose SCC is not a singleton) will be set to true + * @param subsystem An optional bit vector indicating which subsystem to consider. + * @param choices An optional bit vector indicating which choices belong to the subsystem. + * @param currentIndex The next free index that can be assigned to states. + * @param hasPreorderNumber A bit that is used to keep track of the states that already have a preorder number. + * @param preorderNumbers A vector storing the preorder number for each state. + * @param s The stack S used by the algorithm. + * @param p The stack S used by the algorithm. + * @param stateHasScc A bit vector containing all states that have already been assigned to an SCC. + * @param stateToSccMapping A mapping from states to the SCC indices they belong to. As a side effect of this + * function this mapping is filled (for all states reachable from the starting state). + * @param sccCount The number of SCCs that have been computed. As a side effect of this function, this count + * is increased. + */ template - void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, 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) { + void performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& nonTrivialStates, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, 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, bool /*forceTopologicalSort*/, std::vector* sccDepths) { + // The forceTopologicalSort flag can be ignored as this method always generates a topological sort. // Prepare the stack used for turning the recursive procedure into an iterative one. std::vector recursionStateStack; @@ -242,7 +91,7 @@ namespace storm { for (auto const& successor : transitionMatrix.getRow(row)) { if ((!subsystem || subsystem->get(successor.getColumn())) && successor.getValue() != storm::utility::zero()) { if (currentState == successor.getColumn()) { - statesWithSelfLoop.set(currentState); + nonTrivialStates.set(currentState, true); } if (!hasPreorderNumber.get(successor.getColumn())) { @@ -264,12 +113,35 @@ namespace storm { // on the current state. if (currentState == p.back()) { p.pop_back(); + if (sccDepths) { + uint_fast64_t sccDepth = 0; + // Find the largest depth over successor SCCs. + auto stateIt = s.end(); + do { + --stateIt; + for (uint64_t row = transitionMatrix.getRowGroupIndices()[*stateIt], rowEnd = transitionMatrix.getRowGroupIndices()[*stateIt + 1]; row != rowEnd; ++row) { + if (choices && !choices->get(row)) { + continue; + } + for (auto const& successor : transitionMatrix.getRow(row)) { + if ((!subsystem || subsystem->get(successor.getColumn())) && successor.getValue() != storm::utility::zero() && stateHasScc.get(successor.getColumn())) { + sccDepth = std::max(sccDepth, (*sccDepths)[stateToSccMapping[successor.getColumn()]] + 1); + } + } + } + } while (*stateIt != currentState); + sccDepths->push_back(sccDepth); + } + bool nonSingletonScc = s.back() != currentState; uint_fast64_t poppedState = 0; do { poppedState = s.back(); s.pop_back(); stateToSccMapping[poppedState] = sccCount; stateHasScc.set(poppedState); + if (nonSingletonScc) { + nonTrivialStates.set(poppedState, true); + } } while (poppedState != currentState); ++sccCount; } @@ -278,117 +150,107 @@ namespace storm { } } } - + template - void StronglyConnectedComponentDecomposition::sortTopologically(storm::storage::SparseMatrix const& transitions, uint64_t* longestChainSize) { + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options) { - // Get a mapping from state to the corresponding scc - STORM_LOG_THROW(this->size() < std::numeric_limits::max(), storm::exceptions::UnexpectedException, "The number of SCCs is too large."); - std::vector sccIndices(transitions.getRowGroupCount(), std::numeric_limits::max()); - uint32_t sccIndex = 0; - for (auto const& scc : *this) { - for (auto const& state : scc) { - sccIndices[state] = sccIndex; - } - ++sccIndex; + STORM_LOG_ASSERT(!options.choicesPtr || options.subsystemPtr, "Expecting subsystem if choices are given."); + + uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); + + // Set up the environment of the algorithm. + // Start with the two stacks it maintains. + std::vector s; + s.reserve(numberOfStates); + std::vector p; + p.reserve(numberOfStates); + + // We also need to store the preorder numbers of states and which states have been assigned to which SCC. + std::vector preorderNumbers(numberOfStates); + storm::storage::BitVector hasPreorderNumber(numberOfStates); + storm::storage::BitVector stateHasScc(numberOfStates); + std::vector stateToSccMapping(numberOfStates); + uint_fast64_t sccCount = 0; + + // Store scc depths if requested + std::vector* sccDepthsPtr = nullptr; + sccDepths = boost::none; + if (options.isComputeSccDepthsSet || options.areOnlyBottomSccsConsidered) { + sccDepths = std::vector(); + sccDepthsPtr = &sccDepths.get(); } - // Prepare the resulting set of sorted sccs - std::vector sortedSCCs; - sortedSCCs.reserve(this->size()); + // Finally, we need to keep of trivial states (singleton SCCs without selfloop). + storm::storage::BitVector nonTrivialStates(numberOfStates, false); - // Find a topological sort via DFS. - storm::storage::BitVector unsortedSCCs(this->size(), true); - std::vector sccStack, chainSizes; - if (longestChainSize != nullptr) { - chainSizes.resize(this->size(), 1u); - *longestChainSize = 0; + // Start the search for SCCs from every state in the block. + uint_fast64_t currentIndex = 0; + if (options.subsystemPtr) { + for (auto state : *options.subsystemPtr) { + if (!hasPreorderNumber.get(state)) { + performSccDecompositionGCM(transitionMatrix, state, nonTrivialStates, options.subsystemPtr, options.choicesPtr, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount, options.isTopologicalSortForced, sccDepthsPtr); + } + } + } else { + for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { + if (!hasPreorderNumber.get(state)) { + performSccDecompositionGCM(transitionMatrix, state, nonTrivialStates, options.subsystemPtr, options.choicesPtr, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount, options.isTopologicalSortForced, sccDepthsPtr); + } + } } - uint32_t const token = std::numeric_limits::max(); - std::set successorSCCs; - - for (uint32_t firstUnsortedScc = 0; firstUnsortedScc < unsortedSCCs.size(); firstUnsortedScc = unsortedSCCs.getNextSetIndex(firstUnsortedScc + 1)) { - - sccStack.push_back(firstUnsortedScc); - while (!sccStack.empty()) { - uint32_t currentSccIndex = sccStack.back(); - if (currentSccIndex != token) { - // Check whether the SCC is still unprocessed - if (unsortedSCCs.get(currentSccIndex)) { - // Explore the successors of the scc. - storm::storage::StronglyConnectedComponent const& currentScc = this->getBlock(currentSccIndex); - // We first push a token on the stack in order to recognize later when all successors of this SCC have been explored already. - sccStack.push_back(token); - // Now add all successors that are not already sorted. - // Successors should only be added once, so we first prepare a set of them and add them afterwards. - successorSCCs.clear(); - for (auto const& state : currentScc) { - for (auto const& entry : transitions.getRowGroup(state)) { - if (!storm::utility::isZero(entry.getValue())) { - auto const& successorSCC = sccIndices[entry.getColumn()]; - if (successorSCC != currentSccIndex && unsortedSCCs.get(successorSCC)) { - successorSCCs.insert(successorSCC); - } - } - } - } - sccStack.insert(sccStack.end(), successorSCCs.begin(), successorSCCs.end()); - - } - } else { - // all successors of the current scc have already been explored. - sccStack.pop_back(); // pop the token - - currentSccIndex = sccStack.back(); - storm::storage::StronglyConnectedComponent& scc = this->getBlock(currentSccIndex); - - // Compute the longest chain size for this scc - if (longestChainSize != nullptr) { - uint32_t& currentChainSize = chainSizes[currentSccIndex]; - for (auto const& state : scc) { - for (auto const& entry : transitions.getRowGroup(state)) { - if (!storm::utility::isZero(entry.getValue())) { - auto const& successorSCC = sccIndices[entry.getColumn()]; - if (successorSCC != currentSccIndex) { - currentChainSize = std::max(currentChainSize, chainSizes[successorSCC] + 1); - } - } - } + + // After we obtained the state-to-SCC mapping, we build the actual blocks. + this->blocks.resize(sccCount); + for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { + // Check if this state (and is SCC) should be considered in this decomposition. + if ((!options.subsystemPtr || options.subsystemPtr->get(state))) { + if (!options.areNaiveSccsDropped || nonTrivialStates.get(state)) { + uint_fast64_t sccIndex = stateToSccMapping[state]; + if (!options.areOnlyBottomSccsConsidered || sccDepths.get()[sccIndex] == 0) { + this->blocks[sccIndex].insert(state); + if (!nonTrivialStates.get(state)) { + this->blocks[sccIndex].setIsTrivial(true); + STORM_LOG_ASSERT(this->blocks[sccIndex].size() == 1, "Unexpected number of states in a trivial SCC."); } - *longestChainSize = std::max(*longestChainSize, currentChainSize); } - - unsortedSCCs.set(currentSccIndex, false); - sccStack.pop_back(); // pop the current scc index - sortedSCCs.push_back(std::move(scc)); } } } - this->blocks = std::move(sortedSCCs); + + // If requested, we need to delete all naive SCCs. + if (options.areOnlyBottomSccsConsidered || options.areNaiveSccsDropped) { + storm::storage::BitVector blocksToDrop(sccCount); + for (uint_fast64_t sccIndex = 0; sccIndex < sccCount; ++sccIndex) { + if (this->blocks[sccIndex].empty()) { + blocksToDrop.set(sccIndex, true); + } + } + // Create the new set of blocks by moving all the blocks we need to keep into it. + storm::utility::vector::filterVectorInPlace(this->blocks, ~blocksToDrop); + if (this->sccDepths) { + storm::utility::vector::filterVectorInPlace(this->sccDepths.get(), ~blocksToDrop); + } + } } - - // 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 + uint_fast64_t StronglyConnectedComponentDecomposition::getSccDepth(uint_fast64_t const& sccIndex) const { + STORM_LOG_THROW(sccDepths.is_initialized(), storm::exceptions::InvalidOperationException, "Tried to get the SCC depth but SCC depths were not computed upon construction."); + STORM_LOG_ASSERT(sccIndex < sccDepths->size(), "SCC index " << sccIndex << " is out of range (" << sccDepths->size() << ")"); + return sccDepths.get()[sccIndex]; + } + + template + uint_fast64_t StronglyConnectedComponentDecomposition::getMaxSccDepth() const { + STORM_LOG_THROW(sccDepths.is_initialized(), storm::exceptions::InvalidOperationException, "Tried to get the maximum SCC depth but SCC depths were not computed upon construction."); + STORM_LOG_THROW(!sccDepths->empty(), storm::exceptions::InvalidOperationException, "Tried to get the maximum SCC depth but this SCC decomposition seems to be empty."); + return *std::max_element(sccDepths->begin(), sccDepths->end()); + } + // 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); - -#ifdef STORM_HAVE_CARL + template class StronglyConnectedComponentDecomposition; 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); -#endif } // namespace storage } // namespace storm diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.h b/src/storm/storage/StronglyConnectedComponentDecomposition.h index 7d244b914..da8b1dc25 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.h @@ -1,12 +1,12 @@ #ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ #define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_ +#include #include "storm/storage/SparseMatrix.h" #include "storm/storage/Decomposition.h" #include "storm/storage/StronglyConnectedComponent.h" #include "storm/storage/BitVector.h" #include "storm/utility/constants.h" - namespace storm { namespace models { namespace sparse { @@ -17,119 +17,51 @@ namespace storm { namespace storage { + + struct StronglyConnectedComponentDecompositionOptions { + /// Sets a bit vector indicating which subsystem to consider for the decomposition into SCCs. + StronglyConnectedComponentDecompositionOptions& subsystem(storm::storage::BitVector const* subsystem) { subsystemPtr = subsystem; return *this; } + /// Sets a bit vector indicating which choices of the states are contained in the subsystem. + StronglyConnectedComponentDecompositionOptions& choices(storm::storage::BitVector const* choices) { choicesPtr = choices; return *this; } + /// Sets if trivial SCCs (i.e. SCCs consisting of just one state without a self-loop) are to be kept in the decomposition. + StronglyConnectedComponentDecompositionOptions& dropNaiveSccs(bool value = true) { areNaiveSccsDropped = value; return *this; } + /// Sets if only bottom SCCs, i.e. SCCs in which all states have no way of leaving the SCC), are kept. + StronglyConnectedComponentDecompositionOptions& onlyBottomSccs(bool value = true) { areOnlyBottomSccsConsidered = value; return *this; } + /// Enforces that the returned SCCs are sorted in a topological order. + StronglyConnectedComponentDecompositionOptions& forceTobologicalSort(bool value = true) { isTopologicalSortForced = value; return *this; } + /// Sets if scc depths can be retrieved. + StronglyConnectedComponentDecompositionOptions& computeSccDepths(bool value = true) { isComputeSccDepthsSet = value; return *this; } + + storm::storage::BitVector const* subsystemPtr = nullptr; + storm::storage::BitVector const* choicesPtr = nullptr; + bool areNaiveSccsDropped = false; + bool areOnlyBottomSccsConsidered = false; + bool isTopologicalSortForced = false; + bool isComputeSccDepthsSet = false; + + }; + /*! * This class represents the decomposition of a graph-like structure into its strongly connected components. */ template class StronglyConnectedComponentDecomposition : public Decomposition { - public: + public: + /* * Creates an empty SCC decomposition. */ StronglyConnectedComponentDecomposition(); - /* - * 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 - * without a self-loop) are to be kept in the decomposition. - * @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); - - /* - * Creates an SCC decomposition of the given block in the given model. - * - * @param model The model whose block to decompose. - * @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 - * without a self-loop) are to be kept in the decomposition. - * @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); - - /* - * Creates an SCC decomposition of the given subsystem in the given model. - * - * @param model The model that contains the block. - * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @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); - - /* - * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is - * given by a sparse matrix). - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @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 - * without a self-loop) are to be kept in the decomposition. - * @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::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - /* * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is * given by a sparse matrix). * * @param transitionMatrix The transition matrix of the system to decompose. - * @param block The block to decompose into SCCs. - * @param choices A bit vector indicating which choices of the states are contained in the subsystem. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @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::storage::SparseMatrix const& transitionMatrix, StateBlock const& block, storm::storage::BitVector const& choices, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + * @param options options for the decomposition - /* - * Creates an SCC decomposition of the given system (whose transition relation is given by a sparse matrix). - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @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::storage::SparseMatrix const& transitionMatrix, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - - /* - * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is - * given by a sparse matrix). - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @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::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); - - /* - * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is - * given by a sparse matrix). - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. - * @param choices A bit vector indicating which choices of the states are contained in the subsystem. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @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::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options = StronglyConnectedComponentDecompositionOptions()); /*! * Creates an SCC decomposition by copying the given SCC decomposition. @@ -159,65 +91,30 @@ namespace storm { */ StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other); - /*! - * Sorts the SCCs topologically: The ith block can only reach states in block j const& transitions, uint64_t* longestChainSize = nullptr); + uint_fast64_t getSccDepth(uint_fast64_t const& sccIndex) const; - private: /*! - * Performs the SCC decomposition of the given model. As a side-effect this fills the vector of - * blocks of the decomposition. - * - * @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 - * without a self-loop) are to be kept in the decomposition. - * @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. + * Gets the maximum depth of an SCC. */ - template > - void performSccDecomposition(storm::models::sparse::Model const& model, bool dropNaiveSccs, bool onlyBottomSccs); + uint_fast64_t getMaxSccDepth() const; + private: /* * Performs the SCC decomposition of the given block in the given model. As a side-effect this fills * the vector of blocks of the decomposition. * * @param transitionMatrix The transition matrix of the system to decompose. - * @param subsystem An optional bit vector indicating which subsystem to consider. - * @param choices An optional bit vector indicating which choices belong to the subsystem. - * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state - * without a self-loop) are to be kept in the decomposition. - * @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. */ - void performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, bool dropNaiveSccs, bool onlyBottomSccs); + void performSccDecomposition(storm::storage::SparseMatrix const& transitionMatrix, StronglyConnectedComponentDecompositionOptions const& options); - /*! - * Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to - * compute a mapping of states to their SCCs. All arguments given by (non-const) reference are modified by - * the function as a side-effect. - * - * @param transitionMatrix The transition matrix of the system to decompose. - * @param startState The starting state for the search of Tarjan's algorithm. - * @param statesWithSelfLoop A bit vector that is to be filled with all states that have a self-loop. This - * is later needed for identification of the naive SCCs. - * @param subsystem An optional bit vector indicating which subsystem to consider. - * @param choices An optional bit vector indicating which choices belong to the subsystem. - * @param currentIndex The next free index that can be assigned to states. - * @param hasPreorderNumber A bit that is used to keep track of the states that already have a preorder number. - * @param preorderNumbers A vector storing the preorder number for each state. - * @param s The stack S used by the algorithm. - * @param p The stack S used by the algorithm. - * @param stateHasScc A bit vector containing all states that have already been assigned to an SCC. - * @param stateToSccMapping A mapping from states to the SCC indices they belong to. As a side effect of this - * function this mapping is filled (for all states reachable from the starting state). - * @param sccCount The number of SCCs that have been computed. As a side effect of this function, this count - * is increased. - */ - void performSccDecompositionGCM(storm::storage::SparseMatrix const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const* subsystem, storm::storage::BitVector const* choices, 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); + + boost::optional> sccDepths; }; } } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 1515a31f7..c1f1216ad 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -106,7 +106,7 @@ namespace storm { template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix) { storm::storage::BitVector result(transitionMatrix.getRowGroupCount()); - storm::storage::StronglyConnectedComponentDecomposition decomposition(transitionMatrix, false, true); + storm::storage::StronglyConnectedComponentDecomposition decomposition(transitionMatrix, storm::storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs()); // Take the first state out of each BSCC. for (auto const& scc : decomposition) { diff --git a/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp index 821b721a7..429f7de2a 100644 --- a/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -21,17 +21,19 @@ TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix) { storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = matrixBuilder.build()); - storm::storage::BitVector allBits(6, true); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + storm::storage::StronglyConnectedComponentDecompositionOptions options; - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, false, false)); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options)); ASSERT_EQ(4ul, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, true, false)); + options.dropNaiveSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options)); ASSERT_EQ(3ul, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, true, true)); + options.onlyBottomSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, options)); ASSERT_EQ(1ul, sccDecomposition.size()); } @@ -41,14 +43,17 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem1) { std::shared_ptr> markovAutomaton = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + storm::storage::StronglyConnectedComponentDecompositionOptions options; - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton)); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(5ul, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true)); + options.dropNaiveSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(2ul, sccDecomposition.size()); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, true)); + options.onlyBottomSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(2ul, sccDecomposition.size()); markovAutomaton = nullptr; @@ -60,8 +65,10 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem2) { std::shared_ptr> markovAutomaton = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, false)); - + storm::storage::StronglyConnectedComponentDecompositionOptions options; + + options.dropNaiveSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(2ul, sccDecomposition.size()); // Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way. @@ -73,7 +80,8 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem2) { 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())); - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*markovAutomaton, true, true)); + options.onlyBottomSccs(); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(markovAutomaton->getTransitionMatrix(), options)); ASSERT_EQ(1ul, sccDecomposition.size()); markovAutomaton = nullptr;