From fef4b694d443cf6dabd49095bf02ba57f499facf Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 1 Oct 2018 16:36:24 +0200 Subject: [PATCH] topo sort: add first states --- src/storm/utility/graph.cpp | 103 ++++++++++++++++++++---------------- src/storm/utility/graph.h | 2 +- 2 files changed, 57 insertions(+), 48 deletions(-) diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 63dd4e592..193f6a5a5 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1554,9 +1554,56 @@ namespace storm { return SymbolicGameProb01Result(maybePlayer1States, maybePlayer2States, player1StrategyBdd, player2StrategyBdd); } - + + + template + void topologicalSortHelper(storm::storage::SparseMatrix const& matrix, uint64_t state, std::vector& topologicalSort, std::vector& recursionStack, std::vector::const_iterator>& iteratorRecursionStack, storm::storage::BitVector& visitedStates) { + if (!visitedStates.get(state)) { + recursionStack.push_back(state); + iteratorRecursionStack.push_back(matrix.begin(state)); + + recursionStepForward: + while (!recursionStack.empty()) { + uint_fast64_t currentState = recursionStack.back(); + typename storm::storage::SparseMatrix::const_iterator successorIterator = iteratorRecursionStack.back(); + + visitedStates.set(currentState, true); + + recursionStepBackward: + for (; successorIterator != matrix.end(currentState); ++successorIterator) { + if (!visitedStates.get(successorIterator->getColumn())) { + // Put unvisited successor on top of our recursion stack and remember that. + recursionStack.push_back(successorIterator->getColumn()); + + // Also, put initial value for iterator on corresponding recursion stack. + iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn())); + + goto recursionStepForward; + } + } + + topologicalSort.push_back(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. + recursionStack.pop_back(); + iteratorRecursionStack.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 (recursionStack.size() > 0) { + currentState = recursionStack.back(); + successorIterator = iteratorRecursionStack.back(); + + goto recursionStepBackward; + } + } + } + } + template - std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) { + std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates) { if (matrix.getRowCount() != matrix.getColumnCount()) { STORM_LOG_ERROR("Provided matrix is required to be square."); throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square."; @@ -1576,49 +1623,11 @@ namespace storm { // Perform a depth-first search over the given transitions and record states in the reverse order they were visited. storm::storage::BitVector visitedStates(numberOfStates); + for (auto const state : firstStates ) { + topologicalSortHelper(matrix, state, topologicalSort, recursionStack, iteratorRecursionStack, visitedStates); + } for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - if (!visitedStates.get(state)) { - recursionStack.push_back(state); - iteratorRecursionStack.push_back(matrix.begin(state)); - - recursionStepForward: - while (!recursionStack.empty()) { - uint_fast64_t currentState = recursionStack.back(); - typename storm::storage::SparseMatrix::const_iterator successorIterator = iteratorRecursionStack.back(); - - visitedStates.set(currentState, true); - - recursionStepBackward: - for (; successorIterator != matrix.end(currentState); ++successorIterator) { - if (!visitedStates.get(successorIterator->getColumn())) { - // Put unvisited successor on top of our recursion stack and remember that. - recursionStack.push_back(successorIterator->getColumn()); - - // Also, put initial value for iterator on corresponding recursion stack. - iteratorRecursionStack.push_back(matrix.begin(successorIterator->getColumn())); - - goto recursionStepForward; - } - } - - topologicalSort.push_back(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. - recursionStack.pop_back(); - iteratorRecursionStack.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 (recursionStack.size() > 0) { - currentState = recursionStack.back(); - successorIterator = iteratorRecursionStack.back(); - - goto recursionStepBackward; - } - } - } + topologicalSortHelper(matrix, state, topologicalSort, recursionStack, iteratorRecursionStack, visitedStates); } return topologicalSort; @@ -1696,7 +1705,7 @@ namespace storm { template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates) ; // Instantiations for storm::RationalNumber. #ifdef STORM_HAVE_CARL @@ -1752,7 +1761,7 @@ namespace storm { template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1RowGrouping, storm::storage::SparseMatrix const& player1BackwardTransitions, std::vector const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional const& player1Candidates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates); // End of instantiations for storm::RationalNumber. template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional const& choiceFilter); @@ -1804,7 +1813,7 @@ namespace storm { template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); - template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); + template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates); #endif diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 36b86ff69..d42a6be2f 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -683,7 +683,7 @@ namespace storm { * @return A vector of indices that is a topological sort of the states. */ template - std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix) ; + std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix, std::vector const& firstStates = {}) ; } // namespace graph } // namespace utility