From fc67cf4e3f66399d2db75cc9d0b1cdd5cd5d0331 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 9 May 2013 23:16:35 +0200 Subject: [PATCH] Further refactoring of GraphAnalyzer class. --- .../SparseDtmcPrctlModelChecker.h | 10 +- src/modelchecker/SparseMdpPrctlModelChecker.h | 15 +- src/storage/BitVector.h | 9 ++ src/utility/GraphAnalyzer.h | 131 +++++++++--------- 4 files changed, 89 insertions(+), 76 deletions(-) diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/SparseDtmcPrctlModelChecker.h index a6d132745..f55f79db5 100644 --- a/src/modelchecker/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/SparseDtmcPrctlModelChecker.h @@ -212,12 +212,9 @@ 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); - storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; - storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; + storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); + storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); - std::cout << statesWithProbability0.toString() << std::endl; - std::cout << statesWithProbability1.toString() << std::endl; - // Delete intermediate results that are obsolete now. delete leftStates; delete rightStates; @@ -361,9 +358,8 @@ public: storm::storage::BitVector* targetStates = formula.getChild().check(*this); // Determine which states have a reward of infinity by definition. - storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, infinityStates); + storm::storage::BitVector infinityStates = storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates); infinityStates.complement(); // Create resulting vector. diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/SparseMdpPrctlModelChecker.h index 50b20c81d..b9c80e24b 100644 --- a/src/modelchecker/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/SparseMdpPrctlModelChecker.h @@ -213,13 +213,14 @@ 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. - storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); - storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); + std::pair statesWithProbability01; if (this->minimumOperatorStack.top()) { - storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates, statesWithProbability0, statesWithProbability1); + statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates); } else { - storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates, statesWithProbability0, statesWithProbability1); + statesWithProbability01 = storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates); } + storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); + storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); // Delete sub-results that are obsolete now. delete leftStates; @@ -356,12 +357,12 @@ public: storm::storage::BitVector* targetStates = formula.getChild().check(*this); // Determine which states have a reward of infinity by definition. - storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); + storm::storage::BitVector infinityStates; storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); if (this->minimumOperatorStack.top()) { - storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates, infinityStates); + infinityStates = storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates); } else { - storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates, infinityStates); + infinityStates = storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates); } infinityStates.complement(); diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 6787fe0e3..fe5cb5a30 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -191,6 +191,7 @@ public: * given bit vector by means of a deep copy. */ BitVector& operator=(BitVector const& bv) { + LOG4CPLUS_DEBUG(logger, "Performing copy assignment."); // Check if we need to dispose of our current storage. if (this->bucketArray != nullptr) { delete[] this->bucketArray; @@ -204,7 +205,15 @@ public: return *this; } + /*! + * Move assigns the given bit vector to the current bit vector. + * + * @param bv The bit vector whose content is moved to the current bit vector. + * @return A reference to this bit vector after the contents of the given bit vector + * have been moved into it. + */ BitVector& operator=(BitVector&& bv) { + LOG4CPLUS_DEBUG(logger, "Performing move assignment."); // Only perform the assignment if the source and target are not identical. if (this != &bv) { // Check if we need to dispose of our current storage. diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 573d2baa6..17971a407 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -120,10 +120,8 @@ public: */ 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(model.getNumberOfStates()); - storm::storage::BitVector statesWithProbability1(model.getNumberOfStates()); - GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbabilityGreater0); - GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0), statesWithProbability1); + storm::storage::BitVector statesWithProbabilityGreater0 = GraphAnalyzer::performProbGreater0(model, phiStates, psiStates); + storm::storage::BitVector statesWithProbability1 = GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0)); statesWithProbability1.complement(); return statesWithProbability1; } @@ -136,15 +134,14 @@ public: * @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. - * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will - * contain all states with probability 0 after the invocation of the function. - * @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. + * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. */ template - static void performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability0, storm::storage::BitVector& statesWithProbability1) { - GraphAnalyzer::performProb0A(model, phiStates, psiStates, statesWithProbability0); - GraphAnalyzer::performProb1E(model, phiStates, psiStates, statesWithProbability1); + static std::pair performProb01Max(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + result.first = GraphAnalyzer::performProb0A(model, phiStates, psiStates); + result.second = GraphAnalyzer::performProb1E(model, phiStates, psiStates); + return result; } /*! @@ -156,11 +153,13 @@ public: * @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. - * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will - * contain all states with probability 0 after the invocation of the function. + * @return A bit vector that represents all states with probability 0. */ template - static void performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability0) { + static storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + // Prepare the resulting bit vector. + storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); + // Get the backwards transition relation from the model to ease the search. storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); @@ -185,8 +184,9 @@ public: } } - // Finally, invert the computed set of states. + // Finally, invert the computed set of states and return result. statesWithProbability0.complement(); + return statesWithProbability0; } /*! @@ -198,19 +198,18 @@ public: * @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. - * @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. + * @return A bit vector that represents all states with probability 1. */ template - static void performProb1E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability1) { - // Get some temporaries for convenience. + static storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel const& model, 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(); // Get the backwards transition relation from the model to ease the search. storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); - storm::storage::BitVector* currentStates = new storm::storage::BitVector(model.getNumberOfStates(), true); + storm::storage::BitVector currentStates(model.getNumberOfStates(), true); std::vector stack; stack.reserve(model.getNumberOfStates()); @@ -219,7 +218,7 @@ public: bool done = false; while (!done) { stack.clear(); - storm::storage::BitVector* nextStates = new storm::storage::BitVector(psiStates); + storm::storage::BitVector nextStates(psiStates); psiStates.addSetIndicesToVector(stack); while (!stack.empty()) { @@ -227,13 +226,13 @@ public: stack.pop_back(); for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { - if (phiStates.get(*it) && !nextStates->get(*it)) { + if (phiStates.get(*it) && !nextStates.get(*it)) { // Check whether the predecessor has only successors in the current state set for one of the // nondeterminstic choices. for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) { bool allSuccessorsInCurrentStates = true; for (auto colIt = transitionMatrix->constColumnIteratorBegin(row); colIt != transitionMatrix->constColumnIteratorEnd(row); ++colIt) { - if (!currentStates->get(*colIt)) { + if (!currentStates.get(*colIt)) { allSuccessorsInCurrentStates = false; break; } @@ -243,7 +242,7 @@ public: // add it to the set of states for the next iteration and perform a backward search from // that state. if (allSuccessorsInCurrentStates) { - nextStates->set(*it, true); + nextStates.set(*it, true); stack.push_back(*it); break; } @@ -253,16 +252,14 @@ public: } // Check whether we need to perform an additional iteration. - if (*currentStates == *nextStates) { + if (currentStates == nextStates) { done = true; } else { - *currentStates = *nextStates; + currentStates = std::move(nextStates); } - delete nextStates; } - statesWithProbability1 = *currentStates; - delete currentStates; + return currentStates; } /*! * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi @@ -272,15 +269,14 @@ public: * @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. - * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will - * contain all states with probability 0 after the invocation of the function. - * @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. + * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. */ template - static void performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability0, storm::storage::BitVector& statesWithProbability1) { - GraphAnalyzer::performProb0E(model, phiStates, psiStates, statesWithProbability0); - GraphAnalyzer::performProb1A(model, phiStates, psiStates, statesWithProbability1); + static std::pair performProb01Min(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + std::pair result; + result.first = GraphAnalyzer::performProb0E(model, phiStates, psiStates); + result.second = GraphAnalyzer::performProb1A(model, phiStates, psiStates); + return result; } /*! @@ -292,11 +288,13 @@ public: * @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. - * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will - * contain all states with probability 0 after the invocation of the function. + * @return A bit vector that represents all states with probability 0. */ template - static void performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability0) { + static storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + // Prepare resulting bit vector. + storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); + // Get some temporaries for convenience. std::shared_ptr> transitionMatrix = model.getTransitionMatrix(); std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); @@ -347,6 +345,7 @@ public: } statesWithProbability0.complement(); + return statesWithProbability0; } /*! @@ -358,11 +357,10 @@ public: * @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. - * @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. + * @return A bit vector that represents all states with probability 0. */ template - static void performProb1A(storm::models::AbstractNondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector& statesWithProbability1) { + static storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel const& model, 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(); @@ -370,7 +368,7 @@ public: // Get the backwards transition relation from the model to ease the search. storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); - storm::storage::BitVector* currentStates = new storm::storage::BitVector(model.getNumberOfStates(), true); + storm::storage::BitVector currentStates(model.getNumberOfStates(), true); std::vector stack; stack.reserve(model.getNumberOfStates()); @@ -379,7 +377,7 @@ public: bool done = false; while (!done) { stack.clear(); - storm::storage::BitVector* nextStates = new storm::storage::BitVector(psiStates); + storm::storage::BitVector nextStates(psiStates); psiStates.addSetIndicesToVector(stack); while (!stack.empty()) { @@ -387,13 +385,13 @@ public: stack.pop_back(); for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { - if (phiStates.get(*it) && !nextStates->get(*it)) { + if (phiStates.get(*it) && !nextStates.get(*it)) { // Check whether the predecessor has only successors in the current state set for all of the // nondeterminstic choices. bool allSuccessorsInCurrentStatesForAllChoices = true; for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) { for (auto colIt = transitionMatrix->constColumnIteratorBegin(row); colIt != transitionMatrix->constColumnIteratorEnd(row); ++colIt) { - if (!currentStates->get(*colIt)) { + if (!currentStates.get(*colIt)) { allSuccessorsInCurrentStatesForAllChoices = false; goto afterCheckLoop; } @@ -405,7 +403,7 @@ public: // add it to the set of states for the next iteration and perform a backward search from // that state. if (allSuccessorsInCurrentStatesForAllChoices) { - nextStates->set(*it, true); + nextStates.set(*it, true); stack.push_back(*it); } } @@ -413,39 +411,46 @@ public: } // Check whether we need to perform an additional iteration. - if (*currentStates == *nextStates) { + if (currentStates == nextStates) { done = true; } else { - *currentStates = *nextStates; + currentStates = std::move(nextStates); } - delete nextStates; } - - statesWithProbability1 = *currentStates; - delete currentStates; + return currentStates; } - /* - * Performs a decomposition of the given matrix and vector indicating the nondeterministic - * choices into SCCs. + /*! + * Performs a decomposition of the given matrix belonging to a nondeterministic model and vector indicating the + * nondeterministic choices into SCCs. * - * @param + * @param matrix The matrix of the nondeterminstic model to decompose. + * @param nondeterministicChoiceIndices A vector indicating the non-deterministic choices of each state in the matrix. + * @return A pair whose first component represents the SCCs and whose second component represents the dependency + * transitions of the SCCs. */ template - static void performSccDecomposition(storm::storage::SparseMatrix const& matrix, std::vector const& nondeterministicChoiceIndices, std::vector>& stronglyConnectedComponents, storm::models::GraphTransitions& stronglyConnectedComponentsDependencyGraph) { + static std::pair>, storm::models::GraphTransitions> performSccDecomposition(storm::storage::SparseMatrix const& matrix, std::vector const& nondeterministicChoiceIndices) { 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); // Perform the actual SCC decomposition based on the graph-transitions of the system. - performSccDecomposition(nondeterministicChoiceIndices.size() - 1, forwardTransitions, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); - + std::pair>, storm::models::GraphTransitions> result = performSccDecomposition(nondeterministicChoiceIndices.size() - 1, forwardTransitions); LOG4CPLUS_INFO(logger, "Done computing SCC decomposition."); + + return result; } + /*! + * Performs a topological sort of the states of the system according to the given transitions. + * + * @param transitions The transitions of the graph structure. + * @return A vector of indices that is a topological sort of the states. + */ template - static void getTopologicalSort(storm::models::GraphTransitions const& transitions, std::vector& topologicalSort) { + static std::vector getTopologicalSort(storm::models::GraphTransitions const& transitions) { + std::vector topologicalSort; topologicalSort.reserve(transitions.getNumberOfStates()); std::vector recursionStack; @@ -503,6 +508,8 @@ public: } } } + + return topologicalSort; } private: