|
|
|
@ -5,8 +5,8 @@ |
|
|
|
* Author: Christian Dehnert |
|
|
|
*/ |
|
|
|
|
|
|
|
#ifndef STORM_UTILITY_GRAPHANALYZER_H_ |
|
|
|
#define STORM_UTILITY_GRAPHANALYZER_H_ |
|
|
|
#ifndef STORM_UTILITY_GRAPH_H_ |
|
|
|
#define STORM_UTILITY_GRAPH_H_ |
|
|
|
|
|
|
|
#include "src/models/AbstractDeterministicModel.h" |
|
|
|
#include "src/models/AbstractNondeterministicModel.h" |
|
|
|
@ -20,27 +20,8 @@ extern log4cplus::Logger logger; |
|
|
|
namespace storm { |
|
|
|
|
|
|
|
namespace utility { |
|
|
|
|
|
|
|
class GraphAnalyzer { |
|
|
|
public: |
|
|
|
/*! |
|
|
|
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a |
|
|
|
* deterministic model. |
|
|
|
* |
|
|
|
* @param model The model whose graph structure to search. |
|
|
|
* @param phiStates The set of all states satisfying phi. |
|
|
|
* @param psiStates The set of all states satisfying psi. |
|
|
|
* @return A pair of bit vectors such that the first bit vector stores the indices of all states |
|
|
|
* with probability 0 and the second stores all indices of states with probability 1. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> result; |
|
|
|
result.first = GraphAnalyzer::performProbGreater0(model, phiStates, psiStates); |
|
|
|
result.second = GraphAnalyzer::performProb1(model, phiStates, psiStates, result.first); |
|
|
|
result.first.complement(); |
|
|
|
return result; |
|
|
|
} |
|
|
|
|
|
|
|
namespace graph { |
|
|
|
|
|
|
|
/*! |
|
|
|
* Performs a backwards breadt-first search trough the underlying graph structure |
|
|
|
@ -53,12 +34,12 @@ public: |
|
|
|
* @return A bit vector with all indices of states that have a probability greater than 0. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
// Prepare the resulting bit vector. |
|
|
|
storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); |
|
|
|
|
|
|
|
// Get the backwards transition relation from the model to ease the search. |
|
|
|
storm::models::GraphTransitions<T> backwardTransitions(*model.getTransitionMatrix(), false); |
|
|
|
storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions(); |
|
|
|
|
|
|
|
// Add all psi states as the already satisfy the condition. |
|
|
|
statesWithProbabilityGreater0 |= psiStates; |
|
|
|
@ -73,7 +54,7 @@ public: |
|
|
|
uint_fast64_t currentState = stack.back(); |
|
|
|
stack.pop_back(); |
|
|
|
|
|
|
|
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|
|
|
for(auto it = backwardTransitions.constColumnIteratorBegin(currentState); it != backwardTransitions.constColumnIteratorEnd(currentState); ++it) { |
|
|
|
if (phiStates.get(*it) && !statesWithProbabilityGreater0.get(*it)) { |
|
|
|
statesWithProbabilityGreater0.set(*it, true); |
|
|
|
stack.push_back(*it); |
|
|
|
@ -100,8 +81,8 @@ public: |
|
|
|
* @return A bit vector with all indices of states that have a probability greater than 1. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { |
|
|
|
storm::storage::BitVector statesWithProbability1 = GraphAnalyzer::performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0); |
|
|
|
storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { |
|
|
|
storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0); |
|
|
|
statesWithProbability1.complement(); |
|
|
|
return statesWithProbability1; |
|
|
|
} |
|
|
|
@ -119,28 +100,29 @@ public: |
|
|
|
* @return A bit vector with all indices of states that have a probability greater than 1. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
storm::storage::BitVector statesWithProbabilityGreater0 = GraphAnalyzer::performProbGreater0(model, phiStates, psiStates); |
|
|
|
storm::storage::BitVector statesWithProbability1 = GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0)); |
|
|
|
storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(model, phiStates, psiStates); |
|
|
|
storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0)); |
|
|
|
statesWithProbability1.complement(); |
|
|
|
return statesWithProbability1; |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi |
|
|
|
* until psi in a non-deterministic model in which all non-deterministic choices are resolved |
|
|
|
* such that the probability is maximized. |
|
|
|
/*! |
|
|
|
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a |
|
|
|
* deterministic model. |
|
|
|
* |
|
|
|
* @param model The model whose graph structure to search. |
|
|
|
* @param phiStates The set of all states satisfying phi. |
|
|
|
* @param psiStates The set of all states satisfying psi. |
|
|
|
* @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. |
|
|
|
* @return A pair of bit vectors such that the first bit vector stores the indices of all states |
|
|
|
* with probability 0 and the second stores all indices of states with probability 1. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> result; |
|
|
|
result.first = GraphAnalyzer::performProb0A(model, phiStates, psiStates); |
|
|
|
result.second = GraphAnalyzer::performProb1E(model, phiStates, psiStates); |
|
|
|
static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> result; |
|
|
|
result.first = performProbGreater0(model, phiStates, psiStates); |
|
|
|
result.second = performProb1(model, phiStates, psiStates, result.first); |
|
|
|
result.first.complement(); |
|
|
|
return result; |
|
|
|
} |
|
|
|
|
|
|
|
@ -151,17 +133,15 @@ public: |
|
|
|
* scheduler tries to maximize this probability. |
|
|
|
* |
|
|
|
* @param model The model whose graph structure to search. |
|
|
|
* @param backwardTransitions The reversed transition relation of the model. |
|
|
|
* @param phiStates The set of all states satisfying phi. |
|
|
|
* @param psiStates The set of all states satisfying psi. |
|
|
|
* @return A bit vector that represents all states with probability 0. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
// Prepare the resulting bit vector. |
|
|
|
storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); |
|
|
|
|
|
|
|
// Get the backwards transition relation from the model to ease the search. |
|
|
|
storm::models::GraphTransitions<T> backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); |
|
|
|
|
|
|
|
// Add all psi states as the already satisfy the condition. |
|
|
|
statesWithProbability0 |= psiStates; |
|
|
|
@ -176,7 +156,7 @@ public: |
|
|
|
uint_fast64_t currentState = stack.back(); |
|
|
|
stack.pop_back(); |
|
|
|
|
|
|
|
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|
|
|
for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { |
|
|
|
if (phiStates.get(*it) && !statesWithProbability0.get(*it)) { |
|
|
|
statesWithProbability0.set(*it, true); |
|
|
|
stack.push_back(*it); |
|
|
|
@ -196,19 +176,17 @@ public: |
|
|
|
* scheduler tries to maximize this probability. |
|
|
|
* |
|
|
|
* @param model The model whose graph structure to search. |
|
|
|
* @param backwardTransitions The reversed transition relation of the model. |
|
|
|
* @param phiStates The set of all states satisfying phi. |
|
|
|
* @param psiStates The set of all states satisfying psi. |
|
|
|
* @return A bit vector that represents all states with probability 1. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
// 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(); |
|
|
|
|
|
|
|
// Get the backwards transition relation from the model to ease the search. |
|
|
|
storm::models::GraphTransitions<T> backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); |
|
|
|
|
|
|
|
storm::storage::BitVector currentStates(model.getNumberOfStates(), true); |
|
|
|
|
|
|
|
std::vector<uint_fast64_t> stack; |
|
|
|
@ -225,7 +203,7 @@ public: |
|
|
|
uint_fast64_t currentState = stack.back(); |
|
|
|
stack.pop_back(); |
|
|
|
|
|
|
|
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|
|
|
for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { |
|
|
|
if (phiStates.get(*it) && !nextStates.get(*it)) { |
|
|
|
// Check whether the predecessor has only successors in the current state set for one of the |
|
|
|
// nondeterminstic choices. |
|
|
|
@ -261,21 +239,26 @@ public: |
|
|
|
|
|
|
|
return currentStates; |
|
|
|
} |
|
|
|
/*! |
|
|
|
|
|
|
|
/*! |
|
|
|
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi |
|
|
|
* until psi in a non-deterministic model in which all non-deterministic choices are resolved |
|
|
|
* such that the probability is minimized. |
|
|
|
* such that the probability is maximized. |
|
|
|
* |
|
|
|
* @param model The model whose graph structure to search. |
|
|
|
* @param phiStates The set of all states satisfying phi. |
|
|
|
* @param psiStates The set of all states satisfying psi. |
|
|
|
* @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
template <typename T> |
|
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> result; |
|
|
|
result.first = GraphAnalyzer::performProb0E(model, phiStates, psiStates); |
|
|
|
result.second = GraphAnalyzer::performProb1A(model, phiStates, psiStates); |
|
|
|
|
|
|
|
// Get the backwards transition relation from the model to ease the search. |
|
|
|
storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions(); |
|
|
|
|
|
|
|
result.first = performProb0A(model, backwardTransitions, phiStates, psiStates); |
|
|
|
result.second = performProb1E(model, backwardTransitions, phiStates, psiStates); |
|
|
|
return result; |
|
|
|
} |
|
|
|
|
|
|
|
@ -286,12 +269,13 @@ public: |
|
|
|
* scheduler tries to minimize this probability. |
|
|
|
* |
|
|
|
* @param model The model whose graph structure to search. |
|
|
|
* @param backwardTransitions The reversed transition relation of the model. |
|
|
|
* @param phiStates The set of all states satisfying phi. |
|
|
|
* @param psiStates The set of all states satisfying psi. |
|
|
|
* @return A bit vector that represents all states with probability 0. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
// Prepare resulting bit vector. |
|
|
|
storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); |
|
|
|
|
|
|
|
@ -299,9 +283,6 @@ public: |
|
|
|
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix(); |
|
|
|
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); |
|
|
|
|
|
|
|
// Get the backwards transition relation from the model to ease the search. |
|
|
|
storm::models::GraphTransitions<T> backwardTransitions(*transitionMatrix, *nondeterministicChoiceIndices, false); |
|
|
|
|
|
|
|
// Add all psi states as the already satisfy the condition. |
|
|
|
statesWithProbability0 |= psiStates; |
|
|
|
|
|
|
|
@ -315,7 +296,7 @@ public: |
|
|
|
uint_fast64_t currentState = stack.back(); |
|
|
|
stack.pop_back(); |
|
|
|
|
|
|
|
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|
|
|
for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { |
|
|
|
if (phiStates.get(*it) && !statesWithProbability0.get(*it)) { |
|
|
|
// Check whether the predecessor has at least one successor in the current state |
|
|
|
// set for every nondeterministic choice. |
|
|
|
@ -355,19 +336,17 @@ public: |
|
|
|
* scheduler tries to minimize this probability. |
|
|
|
* |
|
|
|
* @param model The model whose graph structure to search. |
|
|
|
* @param backwardTransitions The reversed transition relation of the model. |
|
|
|
* @param phiStates The set of all states satisfying phi. |
|
|
|
* @param psiStates The set of all states satisfying psi. |
|
|
|
* @return A bit vector that represents all states with probability 0. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
// 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(); |
|
|
|
|
|
|
|
// Get the backwards transition relation from the model to ease the search. |
|
|
|
storm::models::GraphTransitions<T> backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); |
|
|
|
|
|
|
|
storm::storage::BitVector currentStates(model.getNumberOfStates(), true); |
|
|
|
|
|
|
|
std::vector<uint_fast64_t> stack; |
|
|
|
@ -384,7 +363,7 @@ public: |
|
|
|
uint_fast64_t currentState = stack.back(); |
|
|
|
stack.pop_back(); |
|
|
|
|
|
|
|
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|
|
|
for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { |
|
|
|
if (phiStates.get(*it) && !nextStates.get(*it)) { |
|
|
|
// Check whether the predecessor has only successors in the current state set for all of the |
|
|
|
// nondeterminstic choices. |
|
|
|
@ -421,17 +400,142 @@ public: |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* Performs a decomposition of the given nondeterministic model into its SCCs. |
|
|
|
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi |
|
|
|
* until psi in a non-deterministic model in which all non-deterministic choices are resolved |
|
|
|
* such that the probability is minimized. |
|
|
|
* |
|
|
|
* @param model The model whose graph structure to search. |
|
|
|
* @param phiStates The set of all states satisfying phi. |
|
|
|
* @param psiStates The set of all states satisfying psi. |
|
|
|
* @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { |
|
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> result; |
|
|
|
|
|
|
|
// Get the backwards transition relation from the model to ease the search. |
|
|
|
storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions(); |
|
|
|
|
|
|
|
result.first = performProb0E(model, backwardTransitions, phiStates, psiStates); |
|
|
|
result.second = performProb1A(model, backwardTransitions, phiStates, psiStates); |
|
|
|
return result; |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* Performs an SCC decomposition using Tarjan's algorithm. |
|
|
|
* |
|
|
|
* @param startState The state at which the search is started. |
|
|
|
* @param currentIndex The index that is to be used as the next free index. |
|
|
|
* @param stateIndices The vector that stores the index for each state. |
|
|
|
* @param lowlinks A vector that stores the lowlink of each state, i.e. the lowest index of a state reachable from |
|
|
|
* a particular state. |
|
|
|
* @param tarjanStack A stack used for Tarjan's algorithm. |
|
|
|
* @param tarjanStackStates A bit vector that represents all states that are currently contained in tarjanStack. |
|
|
|
* @param visitedStates A bit vector that stores all states that have already been visited. |
|
|
|
* @param matrix The transition matrix representing the graph structure. |
|
|
|
* @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
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::storage::SparseMatrix<T> const& matrix, 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::storage::SparseMatrix<T>::ConstIndexIterator> 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(matrix.constColumnIteratorBegin(startState)); |
|
|
|
|
|
|
|
recursionStepForward: |
|
|
|
while (!recursionStateStack.empty()) { |
|
|
|
uint_fast64_t currentState = recursionStateStack.back(); |
|
|
|
typename storm::storage::SparseMatrix<T>::ConstIndexIterator 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. |
|
|
|
for(; currentIt != matrix.constColumnIteratorEnd(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)) { |
|
|
|
// Save current iterator position so we can continue where we left off later. |
|
|
|
recursionIteratorStack.pop_back(); |
|
|
|
recursionIteratorStack.push_back(currentIt); |
|
|
|
|
|
|
|
// Put unvisited successor on top of our recursion stack and remember that. |
|
|
|
recursionStateStack.push_back(*currentIt); |
|
|
|
statesInStack[*currentIt] = true; |
|
|
|
|
|
|
|
// Also, put initial value for iterator on corresponding recursion stack. |
|
|
|
recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*currentIt)); |
|
|
|
|
|
|
|
// Perform the actual recursion step in an iterative way. |
|
|
|
goto recursionStepForward; |
|
|
|
|
|
|
|
recursionStepBackward: |
|
|
|
lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*currentIt]); |
|
|
|
} else if (tarjanStackStates.get(*currentIt)) { |
|
|
|
// Update the lowlink of the current state. |
|
|
|
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
// 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); |
|
|
|
} |
|
|
|
|
|
|
|
// 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(); |
|
|
|
currentIt = recursionIteratorStack.back(); |
|
|
|
|
|
|
|
goto recursionStepBackward; |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* Performs a decomposition of the given model into its SCCs. |
|
|
|
* |
|
|
|
* @param model The nondeterminstic model to decompose. |
|
|
|
* @return A pair whose first component represents the SCCs and whose second component represents the dependency |
|
|
|
* graph of the SCCs. |
|
|
|
* @return A vector of SCCs of the model. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> performSccDecomposition(storm::models::AbstractNondeterministicModel<T> const& model) { |
|
|
|
std::vector<std::vector<uint_fast64_t>> performSccDecomposition(storm::models::AbstractModel<T> const& model) { |
|
|
|
LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); |
|
|
|
|
|
|
|
std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> sccDecomposition; |
|
|
|
std::vector<std::vector<uint_fast64_t>> scc; |
|
|
|
uint_fast64_t numberOfStates = model.getNumberOfStates(); |
|
|
|
|
|
|
|
// Set up the environment of Tarjan's algorithm. |
|
|
|
@ -441,21 +545,17 @@ public: |
|
|
|
std::vector<uint_fast64_t> stateIndices(numberOfStates); |
|
|
|
std::vector<uint_fast64_t> lowlinks(numberOfStates); |
|
|
|
storm::storage::BitVector visitedStates(numberOfStates); |
|
|
|
std::map<uint_fast64_t, uint_fast64_t> stateToSccMap; |
|
|
|
|
|
|
|
// Start the search for SCCs from every vertex in the graph structure, because there is. |
|
|
|
uint_fast64_t currentIndex = 0; |
|
|
|
for (uint_fast64_t state = 0; state < numberOfStates; ++state) { |
|
|
|
if (!visitedStates.get(state)) { |
|
|
|
performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, model.getTransitionMatrix(), sccDecomposition.first, stateToSccMap); |
|
|
|
performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), scc); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
// Finally, determine the dependency graph over the SCCs and return result. |
|
|
|
sccDecomposition.second = model.extractSccDependencyGraph(sccDecomposition.first, stateToSccMap); |
|
|
|
|
|
|
|
LOG4CPLUS_INFO(logger, "Done computing SCC decomposition."); |
|
|
|
return sccDecomposition; |
|
|
|
return scc; |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
@ -465,7 +565,7 @@ public: |
|
|
|
* @return A vector of indices that is a topological sort of the states. |
|
|
|
*/ |
|
|
|
template <typename T> |
|
|
|
static std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix) { |
|
|
|
std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix) { |
|
|
|
if (matrix.getRowCount() != matrix.getColumnCount()) { |
|
|
|
LOG4CPLUS_ERROR(logger, "Provided matrix is required to be square."); |
|
|
|
throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square."; |
|
|
|
@ -536,117 +636,11 @@ public: |
|
|
|
|
|
|
|
return topologicalSort; |
|
|
|
} |
|
|
|
|
|
|
|
private: |
|
|
|
/*! |
|
|
|
* Performs an SCC decomposition using Tarjan's algorithm. |
|
|
|
* |
|
|
|
* @param startState The state at which the search is started. |
|
|
|
* @param currentIndex The index that is to be used as the next free index. |
|
|
|
* @param stateIndices The vector that stores the index for each state. |
|
|
|
* @param lowlinks A vector that stores the lowlink of each state, i.e. the lowest index of a state reachable from |
|
|
|
* a particular state. |
|
|
|
* @param tarjanStack A stack used for Tarjan's algorithm. |
|
|
|
* @param tarjanStackStates A bit vector that represents all states that are currently contained in tarjanStack. |
|
|
|
* @param visitedStates A bit vector that stores all states that have already been visited. |
|
|
|
* @param matrix The transition matrix representing the graph structure. |
|
|
|
* @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. |
|
|
|
* @param stateToSccMap A mapping from state indices to SCC indices that maps each state to its SCC. |
|
|
|
*/ |
|
|
|
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::storage::SparseMatrix<T> const& matrix, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t>& stateToSccMap) { |
|
|
|
// 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<T>::ConstIndexIterator> 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(matrix.constColumnIteratorBegin(startState)); |
|
|
|
|
|
|
|
recursionStepForward: |
|
|
|
while (!recursionStateStack.empty()) { |
|
|
|
uint_fast64_t currentState = recursionStateStack.back(); |
|
|
|
typename storm::storage::SparseMatrix<T>::ConstIndexIterator 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. |
|
|
|
for(; currentIt != matrix.constColumnIteratorEnd(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)) { |
|
|
|
// Save current iterator position so we can continue where we left off later. |
|
|
|
recursionIteratorStack.pop_back(); |
|
|
|
recursionIteratorStack.push_back(currentIt); |
|
|
|
|
|
|
|
// Put unvisited successor on top of our recursion stack and remember that. |
|
|
|
recursionStateStack.push_back(*currentIt); |
|
|
|
statesInStack[*currentIt] = true; |
|
|
|
|
|
|
|
// Also, put initial value for iterator on corresponding recursion stack. |
|
|
|
recursionIteratorStack.push_back(matrix.constColumnIteratorBegin(*currentIt)); |
|
|
|
|
|
|
|
// Perform the actual recursion step in an iterative way. |
|
|
|
goto recursionStepForward; |
|
|
|
|
|
|
|
recursionStepBackward: |
|
|
|
lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[*currentIt]); |
|
|
|
} else if (tarjanStackStates.get(*currentIt)) { |
|
|
|
// Update the lowlink of the current state. |
|
|
|
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]); |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
// 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); |
|
|
|
stateToSccMap[lastState] = stronglyConnectedComponents.size() - 1; |
|
|
|
} while (lastState != currentState); |
|
|
|
} |
|
|
|
|
|
|
|
// 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(); |
|
|
|
currentIt = recursionIteratorStack.back(); |
|
|
|
|
|
|
|
goto recursionStepBackward; |
|
|
|
} |
|
|
|
} |
|
|
|
} |
|
|
|
}; |
|
|
|
|
|
|
|
} // namespace graph |
|
|
|
|
|
|
|
} // namespace utility |
|
|
|
|
|
|
|
} // namespace storm |
|
|
|
|
|
|
|
#endif /* STORM_UTILITY_GRAPHANALYZER_H_ */ |
|
|
|
#endif /* STORM_UTILITY_GRAPH_H_ */ |
gereon
12 years ago