Browse Source

Fixed performance tests, they now run fine.

main
dehnert 12 years ago
parent
commit
307911ca13
  1. 1
      src/modelchecker/EigenDtmcPrctlModelChecker.h
  2. 6
      src/modelchecker/SparseDtmcPrctlModelChecker.h
  3. 10
      src/modelchecker/SparseMdpPrctlModelChecker.h
  4. 15
      src/utility/Settings.h
  5. 323
      src/utility/graph.h
  6. 54
      test/performance/graph/GraphTest.cpp
  7. 4
      test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp

1
src/modelchecker/EigenDtmcPrctlModelChecker.h

@ -12,7 +12,6 @@
#include "src/models/Dtmc.h"
#include "src/modelchecker/SparseDtmcPrctlModelChecker.h"
#include "src/utility/GraphAnalyzer.h"
#include "src/utility/ConstTemplates.h"
#include "src/exceptions/NoConvergenceException.h"

6
src/modelchecker/SparseDtmcPrctlModelChecker.h

@ -11,7 +11,7 @@
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/models/Dtmc.h"
#include "src/utility/Vector.h"
#include "src/utility/GraphAnalyzer.h"
#include "src/utility/graph.h"
#include <vector>
@ -209,7 +209,7 @@ public:
// Then, we need to identify the states which have to be taken out of the matrix, i.e.
// all states that have probability 0 and 1 of satisfying the until-formula.
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates);
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), *leftStates, *rightStates);
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
@ -357,7 +357,7 @@ public:
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
storm::storage::BitVector infinityStates = storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates);
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), trueStates, *targetStates);
infinityStates.complement();
// Create resulting vector.

10
src/modelchecker/SparseMdpPrctlModelChecker.h

@ -11,7 +11,7 @@
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/models/Mdp.h"
#include "src/utility/Vector.h"
#include "src/utility/GraphAnalyzer.h"
#include "src/utility/graph.h"
#include <vector>
#include <stack>
@ -215,9 +215,9 @@ public:
// all states that have probability 0 and 1 of satisfying the until-formula.
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
if (this->minimumOperatorStack.top()) {
statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates);
statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel(), *leftStates, *rightStates);
} else {
statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates);
statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel(), *leftStates, *rightStates);
}
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
@ -360,9 +360,9 @@ public:
storm::storage::BitVector infinityStates;
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
if (this->minimumOperatorStack.top()) {
infinityStates = storm::utility::GraphAnalyzer::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates);
infinityStates = storm::utility::graph::performProb1A(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates);
} else {
infinityStates = storm::utility::GraphAnalyzer::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates);
infinityStates = storm::utility::graph::performProb1E(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, *targetStates);
}
infinityStates.complement();

15
src/utility/Settings.h

@ -52,7 +52,7 @@ namespace settings {
* @brief Get value of a generic option.
*/
template <typename T>
inline const T& get( std::string const & name) const {
const T& get(std::string const& name) const {
if (this->vm.count(name) == 0) throw storm::exceptions::InvalidSettingsException() << "Could not read option " << name << ".";
return this->vm[name].as<T>();
}
@ -60,32 +60,33 @@ namespace settings {
/*!
* @brief Get value of string option.
*/
inline const std::string& getString(std::string const & name) const {
const std::string& getString(std::string const& name) const {
return this->get<std::string>(name);
}
/*!
* @brief Check if an option is set.
*/
inline const bool isSet(std::string const & name) const {
const bool isSet(std::string const& name) const {
return this->vm.count(name) > 0;
}
/*!
* @brief Set an option.
*/
inline void set(std::string const & name) {
void set(std::string const& name) {
bpo::variable_value val;
this->vm.insert( std::make_pair(name, val) );
this->vm.insert(std::make_pair(name, val));
}
/*!
* @brief Set value for an option.
*/
template <typename T>
inline void set(std::string const & name, T const & value) {
void set(std::string const& name, T const& value) {
bpo::variable_value val(value, false);
this->vm.insert( std::make_pair(name, val) );
this->vm.erase(name);
this->vm.insert(std::make_pair(name, val));
}
/*!

323
src/utility/GraphAnalyzer.h → src/utility/graph.h

@ -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,7 +34,7 @@ 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());
@ -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,32 +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;
// Get the backwards transition relation from the model to ease the search.
storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
result.first = GraphAnalyzer::performProb0A(model, backwardTransitions, phiStates, psiStates);
result.second = GraphAnalyzer::performProb1E(model, backwardTransitions, 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;
}
@ -161,7 +139,7 @@ public:
* @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::SparseMatrix<bool> const& backwardTransitions, 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());
@ -204,7 +182,7 @@ public:
* @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::SparseMatrix<bool> const& backwardTransitions, 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();
@ -261,25 +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;
// Get the backwards transition relation from the model to ease the search.
storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
result.first = GraphAnalyzer::performProb0E(model, backwardTransitions, phiStates, psiStates);
result.second = GraphAnalyzer::performProb1A(model, backwardTransitions, phiStates, psiStates);
result.first = performProb0A(model, backwardTransitions, phiStates, psiStates);
result.second = performProb1E(model, backwardTransitions, phiStates, psiStates);
return result;
}
@ -296,7 +275,7 @@ public:
* @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::SparseMatrix<bool> const& backwardTransitions, 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());
@ -363,7 +342,7 @@ public:
* @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::SparseMatrix<bool> const& backwardTransitions, 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();
@ -420,6 +399,132 @@ 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.
*
* @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.
*
@ -427,7 +532,7 @@ public:
* @return A vector of SCCs of the model.
*/
template <typename T>
static std::vector<std::vector<uint_fast64_t>> performSccDecomposition(storm::models::AbstractModel<T> const& model) {
std::vector<std::vector<uint_fast64_t>> performSccDecomposition(storm::models::AbstractModel<T> const& model) {
LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
std::vector<std::vector<uint_fast64_t>> scc;
@ -460,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.";
@ -531,115 +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.
*/
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) {
// 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;
}
}
}
};
} // namespace graph
} // namespace utility
} // namespace storm
#endif /* STORM_UTILITY_GRAPHANALYZER_H_ */
#endif /* STORM_UTILITY_GRAPH_H_ */

54
test/performance/graph/GraphTest.cpp

@ -2,25 +2,25 @@
#include "storm-config.h"
#include "src/utility/Settings.h"
#include "src/parser/AutoParser.h"
#include "src/utility/GraphAnalyzer.h"
#include "src/utility/graph.h"
TEST(GraphAnalyzerTest, PerformProb01) {
TEST(GraphTest, PerformProb01) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
LOG4CPLUS_WARN(logger, "Computing prob01 (3 times) for crowds/crowds20_5...");
std::pair<storm::storage::BitVector, storm::storage::BitVector> prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1")));
std::pair<storm::storage::BitVector, storm::storage::BitVector> prob01 = storm::utility::graph::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1")));
ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414u);
ASSERT_EQ(prob01.second.getNumberOfSetBits(), 46046u);
prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeIGreater1")));
prob01 = storm::utility::graph::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeIGreater1")));
ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016u);
ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797u);
prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender")));
prob01 = storm::utility::graph::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender")));
ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309u);
ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992u);
@ -28,12 +28,12 @@ TEST(GraphAnalyzerTest, PerformProb01) {
dtmc = nullptr;
storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
LOG4CPLUS_WARN(logger, "Computing prob01 for synchronous_leader/leader6_8...");
prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc2, storm::storage::BitVector(dtmc2->getNumberOfStates(), true), storm::storage::BitVector(dtmc2->getLabeledStates("elected")));
prob01 = storm::utility::graph::performProb01(*dtmc2, storm::storage::BitVector(dtmc2->getNumberOfStates(), true), storm::storage::BitVector(dtmc2->getLabeledStates("elected")));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
@ -42,19 +42,19 @@ TEST(GraphAnalyzerTest, PerformProb01) {
dtmc2 = nullptr;
}
TEST(GraphAnalyzerTest, PerformProb01MinMax) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
TEST(GraphTest, PerformProb01MinMax) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", "");
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_WARN(logger, "Computing prob01min for asynchronous_leader/leader7...");
std::pair<storm::storage::BitVector, storm::storage::BitVector> prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected"));
std::pair<storm::storage::BitVector, storm::storage::BitVector> prob01 = storm::utility::graph::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected"));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u);
LOG4CPLUS_WARN(logger, "Computing prob01max for asynchronous_leader/leader7...");
prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected"));
prob01 = storm::utility::graph::performProb01Max(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected"));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
@ -62,18 +62,18 @@ TEST(GraphAnalyzerTest, PerformProb01MinMax) {
mdp = nullptr;
storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", "");
std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser2.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_WARN(logger, "Computing prob01min for consensus/coin4_6...");
prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished"));
prob01 = storm::utility::graph::performProb01Min(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished"));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u);
LOG4CPLUS_WARN(logger, "Computing prob01max for consensus/coin4_6...");
prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished"));
prob01 = storm::utility::graph::performProb01Max(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished"));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u);
@ -82,12 +82,12 @@ TEST(GraphAnalyzerTest, PerformProb01MinMax) {
mdp2 = nullptr;
}
TEST(GraphAnalyzerTest, PerformSCCDecompositionAndGetDependencyGraph) {
TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of crowds/crowds20_5...");
std::vector<std::vector<uint_fast64_t>> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc);
std::vector<std::vector<uint_fast64_t>> sccDecomposition = storm::utility::graph::performSccDecomposition(*dtmc);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 1290297u);
@ -100,11 +100,11 @@ TEST(GraphAnalyzerTest, PerformSCCDecompositionAndGetDependencyGraph) {
dtmc = nullptr;
storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8...");
sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc2);
sccDecomposition = storm::utility::graph::performSccDecomposition(*dtmc2);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 1279673u);
@ -117,30 +117,28 @@ TEST(GraphAnalyzerTest, PerformSCCDecompositionAndGetDependencyGraph) {
dtmc2 = nullptr;
/*
storm::parser::AutoParser<double> parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
storm::parser::AutoParser<double> parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", "");
std::shared_ptr<storm::models::Mdp<double>> mdp = parser3.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader7...");
sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp);
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader6...");
sccDecomposition = storm::utility::graph::performSccDecomposition(*mdp);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 1914691u);
ASSERT_EQ(sccDecomposition.size(), 214675);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader7...");
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6...");
sccDependencyGraph = mdp->extractSccDependencyGraph(sccDecomposition);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 7023587u);
ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093u);
mdp = nullptr;
*/
storm::parser::AutoParser<double> parser4(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
storm::parser::AutoParser<double> parser4(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", "");
std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser4.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6...");
sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp2);
sccDecomposition = storm::utility::graph::performSccDecomposition(*mdp2);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 63611u);

4
test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp

@ -110,7 +110,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
storm::settings::Settings* s = storm::settings::instance();
s->set<unsigned>("maxiter", 20000);
std::cout << s->get<unsigned>("maxiter") << std::endl;
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
ASSERT_EQ(parser.getType(), storm::models::MDP);
@ -149,7 +149,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[31168] - 0.4370098591707694546393), s->get<double>("precision"));
ASSERT_LT(std::abs((*result)[31168] - 0.43742828319177884388579), s->get<double>("precision"));
delete probFormula;
delete result;

Loading…
Cancel
Save