diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h index 7c5b06ad0..c6e4840c7 100644 --- a/src/modelchecker/EigenDtmcPrctlModelChecker.h +++ b/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" diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index 56c7a9525..c19cc471a 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/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 @@ -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 statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates); + std::pair 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. diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index f76092cd2..8849cd222 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/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 #include @@ -215,9 +215,9 @@ public: // all states that have probability 0 and 1 of satisfying the until-formula. std::pair 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(); diff --git a/src/utility/Settings.h b/src/utility/Settings.h index 900b34673..b68aa4e6f 100644 --- a/src/utility/Settings.h +++ b/src/utility/Settings.h @@ -52,7 +52,7 @@ namespace settings { * @brief Get value of a generic option. */ template - 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(); } @@ -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(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 - 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)); } /*! diff --git a/src/utility/GraphAnalyzer.h b/src/utility/graph.h similarity index 87% rename from src/utility/GraphAnalyzer.h rename to src/utility/graph.h index b3eab9727..d3494877d 100644 --- a/src/utility/GraphAnalyzer.h +++ b/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 - static std::pair performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair 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 - static storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel 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 - static storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel 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 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 - static storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel 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 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 - static std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - std::pair result; - - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - - result.first = GraphAnalyzer::performProb0A(model, backwardTransitions, phiStates, psiStates); - result.second = GraphAnalyzer::performProb1E(model, backwardTransitions, phiStates, psiStates); + static std::pair performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair 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 - static storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix 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 - static storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> 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 - static std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + template + std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; // Get the backwards transition relation from the model to ease the search. storm::storage::SparseMatrix 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 - static storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix 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 - static storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> 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 + std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + + // Get the backwards transition relation from the model to ease the search. + storm::storage::SparseMatrix 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 + void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& 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 recursionStateStack; + recursionStateStack.reserve(lowlinks.size()); + std::vector::ConstIndexIterator> recursionIteratorStack; + recursionIteratorStack.reserve(lowlinks.size()); + std::vector 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::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 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 - static std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { + std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); std::vector> scc; @@ -460,7 +565,7 @@ public: * @return A vector of indices that is a topological sort of the states. */ template - static std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) { + std::vector getTopologicalSort(storm::storage::SparseMatrix 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 - static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& 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 recursionStateStack; - recursionStateStack.reserve(lowlinks.size()); - std::vector::ConstIndexIterator> recursionIteratorStack; - recursionIteratorStack.reserve(lowlinks.size()); - std::vector 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::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 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_ */ diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 84f264004..4696ad8e5 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/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 parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); std::shared_ptr> dtmc = parser.getModel>(); LOG4CPLUS_WARN(logger, "Computing prob01 (3 times) for crowds/crowds20_5..."); - std::pair prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1"))); + std::pair 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 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 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> dtmc2 = parser2.getModel>(); 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 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 parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); std::shared_ptr> mdp = parser.getModel>(); LOG4CPLUS_WARN(logger, "Computing prob01min for asynchronous_leader/leader7..."); - std::pair prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); + std::pair 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 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 parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); std::shared_ptr> mdp2 = parser2.getModel>(); 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 parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); std::shared_ptr> dtmc = parser.getModel>(); LOG4CPLUS_WARN(logger, "Computing SCC decomposition of crowds/crowds20_5..."); - std::vector> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc); + std::vector> 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 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 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> dtmc2 = parser2.getModel>(); 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 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 parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", ""); std::shared_ptr> mdp = parser3.getModel>(); - 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 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 parser4(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); std::shared_ptr> mdp2 = parser4.getModel>(); 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); diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index cf8e91581..971c7ec09 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -110,7 +110,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::settings::Settings* s = storm::settings::instance(); s->set("maxiter", 20000); - std::cout << s->get("maxiter") << std::endl; + storm::parser::AutoParser 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("precision")); + ASSERT_LT(std::abs((*result)[31168] - 0.43742828319177884388579), s->get("precision")); delete probFormula; delete result;