sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

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: 5cfeb85193
tempestpy_adaptions
dehnert 10 years ago
parent
4f25312a6b
commit
d40573640f
2 changed files with 130 additions and 126 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 229
      src/storage/StronglyConnectedComponentDecomposition.cpp
  2. 27
      src/storage/StronglyConnectedComponentDecomposition.h

229
src/storage/StronglyConnectedComponentDecomposition.cpp
View File

@ -45,27 +45,88 @@ namespace storm {
this->blocks = std::move(other.blocks);
return *this;
}
template <typename ValueType>
void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> 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<uint_fast64_t> tarjanStack;
tarjanStack.reserve(numberOfStates);
storm::storage::BitVector tarjanStackStates(numberOfStates);
std::vector<uint_fast64_t> stateIndices(numberOfStates);
std::vector<uint_fast64_t> lowlinks(numberOfStates);
storm::storage::BitVector visitedStates(numberOfStates);
// Set up the environment of the algorithm.
// Start with the two stacks it maintains.
std::vector<uint_fast64_t> s;
s.reserve(numberOfStates);
std::vector<uint_fast64_t> 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<uint_fast64_t> preorderNumbers(numberOfStates);
storm::storage::BitVector hasPreorderNumber(numberOfStates);
storm::storage::BitVector stateHasScc(numberOfStates);
std::vector<uint_fast64_t> 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<ValueType>::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<Block> 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 <typename ValueType>
void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, bool dropNaiveSccs, bool onlyBottomSccs) {
@ -77,128 +138,68 @@ namespace storm {
}
template <typename ValueType>
void StronglyConnectedComponentDecomposition<ValueType>::performSccDecompositionHelper(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& 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<uint_fast64_t> recursionStateStack;
recursionStateStack.reserve(lowlinks.size());
std::vector<typename storm::storage::SparseMatrix<ValueType>::const_iterator> recursionIteratorStack;
recursionIteratorStack.reserve(lowlinks.size());
std::vector<bool> statesInStack(lowlinks.size());
void StronglyConnectedComponentDecomposition<ValueType>::performSccDecompositionGCM(storm::models::AbstractModel<ValueType> 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<uint_fast64_t>& preorderNumbers, std::vector<uint_fast64_t>& s, std::vector<uint_fast64_t>& p, storm::storage::BitVector& stateHasScc, std::vector<uint_fast64_t>& 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<uint_fast64_t> recursionStateStack;
recursionStateStack.reserve(model.getNumberOfStates());
recursionStateStack.push_back(startState);
std::vector<typename storm::storage::SparseMatrix<ValueType>::const_iterator> recursionIteratorStack;
recursionIteratorStack.push_back(model.getRows(startState).begin());
recursionStepForward:
while (!recursionStateStack.empty()) {
uint_fast64_t currentState = recursionStateStack.back();
typename storm::storage::SparseMatrix<ValueType>::const_iterator successorIt = recursionIteratorStack.back();
typename storm::storage::SparseMatrix<ValueType>::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;
}
}

27
src/storage/StronglyConnectedComponentDecomposition.h
View File

@ -113,24 +113,27 @@ namespace storm {
void performSccDecomposition(storm::models::AbstractModel<ValueType> 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<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs);
void performSccDecompositionGCM(storm::models::AbstractModel<ValueType> 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<uint_fast64_t>& preorderNumbers, std::vector<uint_fast64_t>& s, std::vector<uint_fast64_t>& p, storm::storage::BitVector& stateHasScc, std::vector<uint_fast64_t>& stateToSccMapping, uint_fast64_t& sccCount);
};
}
}

Write Preview
Loading…
Cancel
Save