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

Added iterative version of Tarjan's algorithm for performing SCC decomposition of state-based models.

tempestpy_adaptions
dehnert 12 years ago
parent
df78cccf84
commit
961909877a
1 changed files with 107 additions and 38 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. 145
      src/utility/GraphAnalyzer.h

145
src/utility/GraphAnalyzer.h
View File

@ -34,7 +34,7 @@ public:
* @param statesWithProbability1 A pointer to a bit vector that is initially empty and will contain all states with
* probability 1 after the invocation of the function.
*/
template <class T>
template <typename T>
static void performProb01(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameters.
if (statesWithProbability0 == nullptr) {
@ -62,7 +62,7 @@ public:
* @param statesWithProbabilityGreater0 A pointer to the result of the search for states that possess
* a positive probability of satisfying phi until psi.
*/
template <class T>
template <typename T>
static void performProbGreater0(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) {
// Check for valid parameter.
if (statesWithProbabilityGreater0 == nullptr) {
@ -109,7 +109,7 @@ public:
* @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
* have paths satisfying phi until psi.
*/
template <class T>
template <typename T>
static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameter.
if (statesWithProbability1 == nullptr) {
@ -133,7 +133,7 @@ public:
* @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
* have paths satisfying phi until psi.
*/
template <class T>
template <typename T>
static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameter.
if (statesWithProbability1 == nullptr) {
@ -148,7 +148,7 @@ public:
statesWithProbability1->complement();
}
template <class T>
template <typename T>
static void performProb01Max(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameters.
if (statesWithProbability0 == nullptr) {
@ -165,7 +165,7 @@ public:
GraphAnalyzer::performProb1E(model, phiStates, psiStates, statesWithProbability1);
}
template <class T>
template <typename T>
static void performProb0A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
// Check for valid parameter.
if (statesWithProbability0 == nullptr) {
@ -200,7 +200,7 @@ public:
statesWithProbability0->complement();
}
template <class T>
template <typename T>
static void performProb1E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameters.
if (statesWithProbability1 == nullptr) {
@ -270,7 +270,7 @@ public:
delete currentStates;
}
template <class T>
template <typename T>
static void performProb01Min(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameters.
if (statesWithProbability0 == nullptr) {
@ -287,7 +287,7 @@ public:
GraphAnalyzer::performProb1A(model, phiStates, psiStates, statesWithProbability1);
}
template <class T>
template <typename T>
static void performProb0E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
// Check for valid parameter.
if (statesWithProbability0 == nullptr) {
@ -347,7 +347,7 @@ public:
statesWithProbability0->complement();
}
template <class T>
template <typename T>
static void performProb1A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
// Check for valid parameters.
if (statesWithProbability1 == nullptr) {
@ -416,16 +416,22 @@ public:
delete currentStates;
}
template <class T>
static uint_fast64_t performSccDecomposition(storm::models::AbstractNondeterministicModel<T>& model) {
// Get some temporaries for convenience.
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
uint_fast64_t numberOfStates = model.getNumberOfStates();
template <typename T>
static uint_fast64_t performSccDecomposition(storm::models::AbstractNondeterministicModel<T>& model, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents) {
LOG4CPLUS_INFO(logger, "Computing SCC decomposition...");
// Get the forward transition relation from the model to ease the search.
storm::models::GraphTransitions<T> forwardTransitions(transitionMatrix, nondeterministicChoiceIndices, true);
storm::models::GraphTransitions<T> forwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), true);
// Perform the actual SCC decomposition based on the graph-transitions of the system.
performSccDecomposition(model.getNumberOfStates(), model.getLabeledStates("init"), forwardTransitions, stronglyConnectedComponents);
LOG4CPLUS_INFO(logger, "Done computing SCCs.");
}
private:
template <typename T>
static uint_fast64_t performSccDecomposition(uint_fast64_t numberOfStates, storm::storage::BitVector const* const initialStates, storm::models::GraphTransitions<T> const& forwardTransitions, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents) {
std::vector<uint_fast64_t> tarjanStack;
tarjanStack.reserve(numberOfStates);
storm::storage::BitVector tarjanStackStates(numberOfStates);
@ -435,38 +441,101 @@ public:
storm::storage::BitVector visitedStates(numberOfStates);
uint_fast64_t currentIndex = 0;
for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
if (!visitedStates.get(i)) {
performSccDecompositionHelper(i, currentIndex, stateIndices, lowlinks, tarjanStack, visitedStates, forwardTransitions);
for (auto state : *initialStates) {
if (!visitedStates.get(state)) {
performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, forwardTransitions, stronglyConnectedComponents);
}
}
return 0;
return stronglyConnectedComponents.size();
}
private:
template <class T>
static void performSccDecompositionHelper(uint_fast64_t currentState, 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, storm::models::GraphTransitions<T>& forwardTransitions) {
std::vector<uint_fast64_t> recursionStack;
recursionStack.reserve(lowlinks.size());
template <typename T>
static void performSccDecompositionHelper(uint_fast64_t startState, 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, storm::models::GraphTransitions<T>& forwardTransitions, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents) {
// 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::models::GraphTransitions<T>::stateSuccessorIterator> recursionIteratorStack;
recursionIteratorStack.reserve(lowlinks.size());
std::vector<bool> statesInStack(lowlinks.size());
// Initialize the recursion stacks with the given initial state (and its successor iterator).
recursionStateStack.push_back(startState);
recursionIteratorStack.push_back(forwardTransitions.beginStateSuccessorsIterator(startState));
recursionStepForward:
while (!recursionStateStack.empty()) {
uint_fast64_t currentState = recursionStateStack.back();
typename storm::models::GraphTransitions<T>::stateSuccessorIterator currentIt = recursionIteratorStack.back();
// 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);
// Now, traverse all successors of the current state.
recursionStepBackward:
for(; currentIt != forwardTransitions.endStateSuccessorsIterator(currentState); ++currentIt) {
// If we have not visited the successor already, we need to perform the procedure
// recursively on the newly found state.
if (!visitedStates.get(*currentIt)) {
// Put unvisited successor on top of our recursion stack and remember that.
recursionStateStack.push_back(*currentIt);
statesInStack[*currentIt] = true;
// Save current iterator position so we can continue where we left off later.
recursionIteratorStack.pop_back();
recursionIteratorStack.push_back(currentIt + 1);
// Also, put initial value for iterator on corresponding recursion stack.
recursionIteratorStack.push_back(forwardTransitions.beginStateSuccessorsIterator(*currentIt));
// Perform the actual recursion step in an iterative way.
goto recursionStepForward;
} else if (tarjanStackStates.get(*currentIt)) {
// Update the lowlink of the current state.
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]);
}
}
stateIndices[currentState] = currentIndex;
lowlinks[currentState] = currentIndex;
++currentIndex;
// 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]) {
stronglyConnectedComponents.push_back(std::vector<uint_fast64_t>());
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.
stronglyConnectedComponents.back().push_back(lastState);
} while (lastState != currentState);
}
tarjanStack.push_back(currentState);
tarjanStackStates.set(currentState, true);
// 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();
for(auto it = forwardTransitions.beginStateSuccessorsIterator(currentState); it != forwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
if (!visitedStates.get(*it)) {
// 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();
currentIt = recursionIteratorStack.back();
} else if (tarjanStackStates.get(*it)) {
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*it]);
goto recursionStepBackward;
}
}
}
};

Write Preview
Loading…
Cancel
Save