diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h index 248749624..1466c02ec 100644 --- a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h @@ -67,11 +67,11 @@ private: bool relative = s->get("relative"); // Now, we need to determine the SCCs of the MDP and a topological sort. - std::vector> stronglyConnectedComponents; - storm::models::GraphTransitions stronglyConnectedComponentsDependencyGraph; - storm::utility::GraphAnalyzer::performSccDecomposition(matrix, nondeterministicChoiceIndices, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); - std::vector topologicalSort; - storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph, topologicalSort); + std::pair>, storm::models::GraphTransitions> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + std::vector> stronglyConnectedComponents = std::move(sccDecomposition.first); + storm::models::GraphTransitions stronglyConnectedComponentsDependencyGraph = std::move(sccDecomposition.second); + + std::vector topologicalSort = storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Set up the environment for the power method. std::vector multiplyResult(matrix.getRowCount()); diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 17971a407..9f33a2f7f 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -430,10 +430,12 @@ public: * transitions of the SCCs. */ template - static std::pair>, storm::models::GraphTransitions> performSccDecomposition(storm::storage::SparseMatrix const& matrix, std::vector const& nondeterministicChoiceIndices) { + static std::pair>, storm::models::GraphTransitions> performSccDecomposition(storm::models::AbstractNondeterministicModel const& model) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); - // Get the forward transition relation from the model to ease the search. - storm::models::GraphTransitions forwardTransitions(matrix, nondeterministicChoiceIndices, true); + + // Get the forward transition relation from the model to ease the search. + std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + storm::models::GraphTransitions forwardTransitions(model.getTransitionMatrix(), nondeterministicChoiceIndices, true); // Perform the actual SCC decomposition based on the graph-transitions of the system. std::pair>, storm::models::GraphTransitions> result = performSccDecomposition(nondeterministicChoiceIndices.size() - 1, forwardTransitions); @@ -514,7 +516,9 @@ public: private: template - static void performSccDecomposition(uint_fast64_t numberOfStates, storm::models::GraphTransitions const& forwardTransitions, std::vector>& stronglyConnectedComponents, storm::models::GraphTransitions& stronglyConnectedComponentsDependencyGraph) { + static std::pair>, storm::models::GraphTransitions> performSccDecomposition(uint_fast64_t numberOfStates, storm::models::GraphTransitions const& forwardTransitions) { + std::pair>, storm::models::GraphTransitions> sccDecomposition; + std::vector tarjanStack; tarjanStack.reserve(numberOfStates); storm::storage::BitVector tarjanStackStates(numberOfStates); @@ -528,11 +532,12 @@ private: 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, forwardTransitions, stronglyConnectedComponents, stateToSccMap); + performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, forwardTransitions, sccDecomposition.first, stateToSccMap); } } - stronglyConnectedComponentsDependencyGraph = storm::models::GraphTransitions(forwardTransitions, stronglyConnectedComponents, stateToSccMap); + sccDecomposition.second = storm::models::GraphTransitions(forwardTransitions, sccDecomposition.first, stateToSccMap); + return sccDecomposition; } template