From d40573640f21ec92a1b5c1daa610d92ef884de6b Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 30 Aug 2014 11:20:29 +0200 Subject: [PATCH] Dropped our current Tarjan-implementation in favour of the path-based algorithm by Gabow (and others) as this seems to perform a lot better (at when comparing our implementations). Former-commit-id: 5cfeb85193cdc4d768bb676851652967a27c56aa --- ...tronglyConnectedComponentDecomposition.cpp | 229 +++++++++--------- .../StronglyConnectedComponentDecomposition.h | 27 ++- 2 files changed, 130 insertions(+), 126 deletions(-) diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index b14559bcb..46990e7eb 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -45,27 +45,88 @@ namespace storm { this->blocks = std::move(other.blocks); return *this; } - + template void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - // Set up the environment of Tarjan's algorithm. uint_fast64_t numberOfStates = model.getNumberOfStates(); - std::vector tarjanStack; - tarjanStack.reserve(numberOfStates); - storm::storage::BitVector tarjanStackStates(numberOfStates); - std::vector stateIndices(numberOfStates); - std::vector lowlinks(numberOfStates); - storm::storage::BitVector visitedStates(numberOfStates); + + // 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; for (auto state : subsystem) { - if (!visitedStates.get(state)) { - performSccDecompositionHelper(model, state, subsystem, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, dropNaiveSccs, onlyBottomSccs); + if (!hasPreorderNumber.get(state)) { + performSccDecompositionGCM(model, state, statesWithSelfLoop, subsystem, 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); + for (uint_fast64_t state = 0; state < numberOfStates; ++state) { + this->blocks[stateToSccMapping[state]].insert(state); + } + + // 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].size() == 1) { + uint_fast64_t onlyState = *this->blocks[sccIndex].begin(); + + if (!statesWithSelfLoop.get(onlyState)) { + blocksToDrop.set(sccIndex); + } + } + } + } + + // If requested, we need to drop all non-bottom SCCs. + if (onlyBottomSccs) { + for (uint_fast64_t state = 0; state < numberOfStates; ++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 (typename storm::storage::SparseMatrix::const_iterator successorIt = model.getRows(state).begin(), successorIte = model.getRows(state).end(); successorIt != successorIte; ++successorIt) { + if (subsystem.get(successorIt->getColumn()) && stateToSccMapping[state] != stateToSccMapping[successorIt->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 void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs, bool onlyBottomSccs) { @@ -77,128 +138,68 @@ namespace storm { } 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, bool onlyBottomSccs) { - // 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::const_iterator> recursionIteratorStack; - recursionIteratorStack.reserve(lowlinks.size()); - std::vector statesInStack(lowlinks.size()); + void StronglyConnectedComponentDecomposition::performSccDecompositionGCM(storm::models::AbstractModel const& model, 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) { - // Store a bit vector of all states with a self-loop to be able to detect non-trivial SCCs with only one - // state. - storm::storage::BitVector statesWithSelfloop; - if (dropNaiveSccs) { - statesWithSelfloop = storm::storage::BitVector(lowlinks.size()); - } - - // Initialize the recursion stacks with the given initial state (and its successor iterator). + // Prepare the stack used for turning the recursive procedure into an iterative one. + std::vector recursionStateStack; + recursionStateStack.reserve(model.getNumberOfStates()); recursionStateStack.push_back(startState); + std::vector::const_iterator> recursionIteratorStack; recursionIteratorStack.push_back(model.getRows(startState).begin()); - - recursionStepForward: + while (!recursionStateStack.empty()) { uint_fast64_t currentState = recursionStateStack.back(); - typename storm::storage::SparseMatrix::const_iterator successorIt = recursionIteratorStack.back(); + typename storm::storage::SparseMatrix::const_iterator& successorIt = recursionIteratorStack.back(); + + if (!hasPreorderNumber.get(currentState)) { + preorderNumbers[currentState] = currentIndex++; + hasPreorderNumber.set(currentState, true); - // Perform the treatment of newly discovered state as defined by Tarjan's algorithm. - visitedStates.set(currentState, true); - stateIndices[currentState] = currentIndex; - lowlinks[currentState] = currentIndex; - ++currentIndex; - tarjanStack.push_back(currentState); - tarjanStackStates.set(currentState, true); + s.push_back(currentState); + p.push_back(currentState); + } - // Now, traverse all successors of the current state. - for(; successorIt != model.getRows(currentState).end(); ++successorIt) { - // Record if the current state has a self-loop if we are to drop naive SCCs later. - if (dropNaiveSccs && currentState == successorIt->getColumn()) { - statesWithSelfloop.set(currentState, true); - } - - // If we have not visited the successor already, we need to perform the procedure recursively on the - // newly found state, but only if it belongs to the subsystem in which we are interested. + bool recursionStepIn = false; + for (; successorIt != model.getRows(currentState).end(); ++successorIt) { if (subsystem.get(successorIt->getColumn())) { - if (!visitedStates.get(successorIt->getColumn())) { - // Save current iterator position so we can continue where we left off later. - recursionIteratorStack.pop_back(); - recursionIteratorStack.push_back(successorIt); - - // Put unvisited successor on top of our recursion stack and remember that. + if (currentState == successorIt->getColumn()) { + statesWithSelfLoop.set(currentState); + } + + if (!hasPreorderNumber.get(successorIt->getColumn())) { + // In this case, we must recursively visit the successor. We therefore push the state onto the recursion stack an break the for-loop. recursionStateStack.push_back(successorIt->getColumn()); - statesInStack[successorIt->getColumn()] = true; + recursionStepIn = true; - // Also, put initial value for iterator on corresponding recursion stack. recursionIteratorStack.push_back(model.getRows(successorIt->getColumn()).begin()); - - // Perform the actual recursion step in an iterative way. - goto recursionStepForward; - - recursionStepBackward: - lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt->getColumn()]); - } else if (tarjanStackStates.get(successorIt->getColumn())) { - // Update the lowlink of the current state. - lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt->getColumn()]); - } - } - } - - // If the current state is the root of a SCC, we need to pop all states of the SCC from the algorithm's - // stack. - if (lowlinks[currentState] == stateIndices[currentState]) { - Block scc; - - uint_fast64_t lastState = 0; - do { - // Pop topmost state from the algorithm's stack. - lastState = tarjanStack.back(); - tarjanStack.pop_back(); - tarjanStackStates.set(lastState, false); - - // Add the state to the current SCC. - scc.insert(lastState); - } while (lastState != currentState); - - bool isBottomScc = true; - if (onlyBottomSccs) { - for (auto const& state : scc) { - for (auto const& successor : model.getRows(state)) { - if (scc.find(successor.getColumn()) == scc.end()) { - isBottomScc = false; - break; + break; + } else { + if (!stateHasScc.get(successorIt->getColumn())) { + while (preorderNumbers[p.back()] > preorderNumbers[successorIt->getColumn()]) { + p.pop_back(); } } } } - - // Now determine whether we want to keep this SCC in the decomposition. - // First, we need to check whether we should drop the SCC because of the requirement to not include - // naive SCCs. - bool keepScc = !dropNaiveSccs || (scc.size() > 1 || statesWithSelfloop.get(*scc.begin())); - // Then, we also need to make sure that it is a bottom SCC if we were required to. - keepScc &= !onlyBottomSccs || isBottomScc; - - // Only add the SCC if we determined to keep it, based on the given parameters. - if (keepScc) { - this->blocks.emplace_back(std::move(scc)); - } } - // If we reach this point, we have completed the recursive descent for the current state. That is, we - // need to pop it from the recursion stacks. - recursionStateStack.pop_back(); - recursionIteratorStack.pop_back(); - - // If there is at least one state under the current one in our recursion stack, we need to restore the - // topmost state as the current state and jump to the part after the original recursive call. - if (recursionStateStack.size() > 0) { - currentState = recursionStateStack.back(); - successorIt = recursionIteratorStack.back(); + if (!recursionStepIn) { + if (currentState == p.back()) { + p.pop_back(); + uint_fast64_t poppedState = 0; + do { + poppedState = s.back(); + s.pop_back(); + stateToSccMapping[poppedState] = sccCount; + stateHasScc.set(poppedState); + } while (poppedState != currentState); + ++sccCount; + } - goto recursionStepBackward; + recursionStateStack.pop_back(); + recursionIteratorStack.pop_back(); } + recursionStepIn = false; } } diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index a8ce0403c..0409c11a1 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -113,24 +113,27 @@ namespace storm { void performSccDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); /*! - * A helper function that performs the SCC decomposition given all auxiliary data structures. As a - * side-effect this fills the vector of blocks of the decomposition. + * 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 model The model to decompose into SCCs. * @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 The subsystem to search. * @param currentIndex The next free index that can be assigned to states. - * @param stateIndices A vector storing the index for each state. - * @param lowlinks A vector storing the lowlink for each state. - * @param tarjanStack A vector that is to be used as the stack in Tarjan's algorithm. - * @param tarjanStackStates A bit vector indicating which states are currently in the stack. - * @param visitedStates A bit vector containing all states that have already been visited. - * @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. + * @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 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, bool onlyBottomSccs); + void performSccDecompositionGCM(storm::models::AbstractModel const& model, 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); }; } }