diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 75437040a..59c5deb03 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -34,7 +34,7 @@ public: * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will contain all states with * probability 1 after the invocation of the function. */ - template + template static void performProb01(storm::models::AbstractDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability0 == nullptr) { @@ -62,7 +62,7 @@ public: * @param statesWithProbabilityGreater0 A pointer to the result of the search for states that possess * a positive probability of satisfying phi until psi. */ - template + template static void performProbGreater0(storm::models::AbstractDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) { // Check for valid parameter. if (statesWithProbabilityGreater0 == nullptr) { @@ -109,7 +109,7 @@ public: * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only * have paths satisfying phi until psi. */ - template + template static void performProb1(storm::models::AbstractDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameter. if (statesWithProbability1 == nullptr) { @@ -133,7 +133,7 @@ public: * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only * have paths satisfying phi until psi. */ - template + template static void performProb1(storm::models::AbstractDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameter. if (statesWithProbability1 == nullptr) { @@ -148,7 +148,7 @@ public: statesWithProbability1->complement(); } - template + template static void performProb01Max(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability0 == nullptr) { @@ -165,7 +165,7 @@ public: GraphAnalyzer::performProb1E(model, phiStates, psiStates, statesWithProbability1); } - template + template static void performProb0A(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { // Check for valid parameter. if (statesWithProbability0 == nullptr) { @@ -200,7 +200,7 @@ public: statesWithProbability0->complement(); } - template + template static void performProb1E(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability1 == nullptr) { @@ -270,7 +270,7 @@ public: delete currentStates; } - template + template static void performProb01Min(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability0 == nullptr) { @@ -287,7 +287,7 @@ public: GraphAnalyzer::performProb1A(model, phiStates, psiStates, statesWithProbability1); } - template + template static void performProb0E(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { // Check for valid parameter. if (statesWithProbability0 == nullptr) { @@ -347,7 +347,7 @@ public: statesWithProbability0->complement(); } - template + template static void performProb1A(storm::models::AbstractNondeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { // Check for valid parameters. if (statesWithProbability1 == nullptr) { @@ -416,16 +416,22 @@ public: delete currentStates; } - template - static uint_fast64_t performSccDecomposition(storm::models::AbstractNondeterministicModel& model) { - // Get some temporaries for convenience. - std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); - std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); - uint_fast64_t numberOfStates = model.getNumberOfStates(); + template + static uint_fast64_t performSccDecomposition(storm::models::AbstractNondeterministicModel& model, std::vector>& stronglyConnectedComponents) { + LOG4CPLUS_INFO(logger, "Computing SCC decomposition..."); // Get the forward transition relation from the model to ease the search. - storm::models::GraphTransitions forwardTransitions(transitionMatrix, nondeterministicChoiceIndices, true); + storm::models::GraphTransitions forwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), true); + + // Perform the actual SCC decomposition based on the graph-transitions of the system. + performSccDecomposition(model.getNumberOfStates(), model.getLabeledStates("init"), forwardTransitions, stronglyConnectedComponents); + LOG4CPLUS_INFO(logger, "Done computing SCCs."); + } + +private: + template + static uint_fast64_t performSccDecomposition(uint_fast64_t numberOfStates, storm::storage::BitVector const* const initialStates, storm::models::GraphTransitions const& forwardTransitions, std::vector>& stronglyConnectedComponents) { std::vector tarjanStack; tarjanStack.reserve(numberOfStates); storm::storage::BitVector tarjanStackStates(numberOfStates); @@ -435,38 +441,101 @@ public: storm::storage::BitVector visitedStates(numberOfStates); uint_fast64_t currentIndex = 0; - - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - if (!visitedStates.get(i)) { - performSccDecompositionHelper(i, currentIndex, stateIndices, lowlinks, tarjanStack, visitedStates, forwardTransitions); + for (auto state : *initialStates) { + if (!visitedStates.get(state)) { + performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, forwardTransitions, stronglyConnectedComponents); } } - - return 0; + return stronglyConnectedComponents.size(); } -private: - template - static void performSccDecompositionHelper(uint_fast64_t currentState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::models::GraphTransitions& forwardTransitions) { - std::vector recursionStack; - recursionStack.reserve(lowlinks.size()); + 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::models::GraphTransitions& forwardTransitions, 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::stateSuccessorIterator> 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(forwardTransitions.beginStateSuccessorsIterator(startState)); + + recursionStepForward: + while (!recursionStateStack.empty()) { + uint_fast64_t currentState = recursionStateStack.back(); + typename storm::models::GraphTransitions::stateSuccessorIterator 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. + recursionStepBackward: + for(; currentIt != forwardTransitions.endStateSuccessorsIterator(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)) { + // Put unvisited successor on top of our recursion stack and remember that. + recursionStateStack.push_back(*currentIt); + statesInStack[*currentIt] = true; + + // Save current iterator position so we can continue where we left off later. + recursionIteratorStack.pop_back(); + recursionIteratorStack.push_back(currentIt + 1); + + // Also, put initial value for iterator on corresponding recursion stack. + recursionIteratorStack.push_back(forwardTransitions.beginStateSuccessorsIterator(*currentIt)); + + // Perform the actual recursion step in an iterative way. + goto recursionStepForward; + } else if (tarjanStackStates.get(*currentIt)) { + // Update the lowlink of the current state. + lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*currentIt]); + } + } - stateIndices[currentState] = currentIndex; - lowlinks[currentState] = currentIndex; - ++currentIndex; + // 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); + } - tarjanStack.push_back(currentState); - tarjanStackStates.set(currentState, true); + // 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(); - for(auto it = forwardTransitions.beginStateSuccessorsIterator(currentState); it != forwardTransitions.endStateSuccessorsIterator(currentState); ++it) { - if (!visitedStates.get(*it)) { + // 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(); - } else if (tarjanStackStates.get(*it)) { - lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[*it]); + goto recursionStepBackward; } } - } };