From 170306e46d9916c752df0fc52112f070c916a376 Mon Sep 17 00:00:00 2001 From: masawei Date: Mon, 25 Nov 2013 21:15:36 +0100 Subject: [PATCH] Moved SparseMatrix transposition function from AbstractModel (named: getBackwardsTransitions) to SparseMatrix (named: transpose) where it belongs. - Fixed one problem marked FIXME in the transpose function. The need for a "sentinel" element was created by an off by one in the prior loop. - Changed all occurences of SparseMatrix to SparseMatrix. Now the only two types for which SparseMatrix is instantiated are double and int. - Compiles again. |-> Compile time seems to be roughly the same for clean; make all. For incremental builds I haven't tested yet. Former-commit-id: 6d829e090346c51b8cafc049b202e10bf18ea017 --- .../MILPMinimalLabelSetGenerator.h | 4 +- .../SMTMinimalCommandSetGenerator.h | 6 +- ...ogicalValueIterationMdpPrctlModelChecker.h | 2 +- src/models/AbstractModel.h | 73 ++----------------- src/storage/SparseMatrix.cpp | 53 +++++++++++++- src/storage/SparseMatrix.h | 9 ++- src/utility/counterexamples.h | 2 +- src/utility/graph.h | 18 ++--- test/performance/graph/GraphTest.cpp | 4 +- 9 files changed, 84 insertions(+), 87 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 8e9e23503..ea02db662 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -99,7 +99,7 @@ namespace storm { */ static struct StateInformation determineRelevantAndProblematicStates(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { StateInformation result; - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); result.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates); result.relevantStates &= ~psiStates; result.problematicStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates); @@ -912,7 +912,7 @@ namespace storm { * @return The total number of constraints that were created. */ static uint_fast64_t assertSchedulerCuts(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); uint_fast64_t numberOfConstraintsCreated = 0; int error = 0; std::vector variables; diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index e3fa9e394..8bd56c2dc 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -84,7 +84,7 @@ namespace storm { // Compute all relevant states, i.e. states for which there exists a scheduler that has a non-zero // probabilitiy of satisfying phi until psi. - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates); relevancyInformation.relevantStates &= ~psiStates; @@ -214,7 +214,7 @@ namespace storm { std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates(); std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); for (auto currentState : relevancyInformation.relevantStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { @@ -484,7 +484,7 @@ namespace storm { // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); // Compute the set of labels that may precede a given action. for (auto currentState : relevancyInformation.relevantStates) { diff --git a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h index 69f62c15c..77fa27543 100644 --- a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h @@ -69,7 +69,7 @@ private: // Now, we need to determine the SCCs of the MDP and a topological sort. std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); - storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); + storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Set up the environment for the power method. diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 84663dbc0..0a02028d3 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -145,10 +145,10 @@ class AbstractModel: public std::enable_shared_from_this> { /*! * Extracts the dependency graph from the model according to the given partition. * - * @param partition A vector containing the blocks of the partition of the system. + * @param decomposition A decomposition containing the blocks of the partition of the system. * @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition. */ - storm::storage::SparseMatrix extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const { + storm::storage::SparseMatrix extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const { uint_fast64_t numberOfStates = decomposition.size(); // First, we need to create a mapping of states to their SCC index, to ease the computation of dependency transitions later. @@ -160,7 +160,7 @@ class AbstractModel: public std::enable_shared_from_this> { } // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition. - storm::storage::SparseMatrix dependencyGraph(numberOfStates); + storm::storage::SparseMatrix dependencyGraph(numberOfStates); dependencyGraph.initialize(); for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) { @@ -191,76 +191,15 @@ class AbstractModel: public std::enable_shared_from_this> { dependencyGraph.finalize(true); return dependencyGraph; } - - /*! - * Retrieves the backward transition relation of the model, i.e. a set of transitions - * between states that correspond to the reversed transition relation of this model. - * - * @return A sparse matrix that represents the backward transitions of this model. - */ - storm::storage::SparseMatrix getBackwardTransitions() const { - return getBackwardTransitions([](T const& value) -> bool { return value != 0; }); - } - + /*! * Retrieves the backward transition relation of the model, i.e. a set of transitions * between states that correspond to the reversed transition relation of this model. * * @return A sparse matrix that represents the backward transitions of this model. */ - template - storm::storage::SparseMatrix getBackwardTransitions(std::function const& selectionFunction) const { - uint_fast64_t numberOfStates = this->getNumberOfStates(); - uint_fast64_t numberOfTransitions = this->getNumberOfTransitions(); - - std::vector rowIndications(numberOfStates + 1); - std::vector columnIndications(numberOfTransitions); - std::vector values(numberOfTransitions, TransitionType()); - - // First, we need to count how many backward transitions each state has. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - typename storm::storage::SparseMatrix::Rows rows = this->getRows(i); - for (auto const& transition : rows) { - if (transition.value() > 0) { - ++rowIndications[transition.column() + 1]; - } - } - } - - // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i < numberOfStates; ++i) { - rowIndications[i] = rowIndications[i - 1] + rowIndications[i]; - } - - // Put a sentinel element at the end of the indices list. This way, - // for each state i the range of indices can be read off between - // state_indices_list[i] and state_indices_list[i + 1]. - // FIXME: This should not be necessary and already be implied by the first steps. - rowIndications[numberOfStates] = numberOfTransitions; - - // Create an array that stores the next index for each state. Initially - // this corresponds to the previously computed accumulated offsets. - std::vector nextIndices = rowIndications; - - // Now we are ready to actually fill in the list of predecessors for - // every state. Again, we start by considering all but the last row. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - typename storm::storage::SparseMatrix::Rows rows = this->getRows(i); - for (auto& transition : rows) { - if (transition.value() > 0) { - values[nextIndices[transition.column()]] = selectionFunction(transition.value()); - columnIndications[nextIndices[transition.column()]++] = i; - } - } - } - - storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, numberOfStates, - numberOfTransitions, - std::move(rowIndications), - std::move(columnIndications), - std::move(values)); - - return backwardTransitionMatrix; + storm::storage::SparseMatrix getBackwardTransitions() const { + return this->transitionMatrix.transpose(); } /*! diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 6cc37eca9..50c73d96e 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -662,6 +662,57 @@ namespace storage { negateAllNonDiagonalElements(); } + template + SparseMatrix SparseMatrix::transpose() const { + + uint_fast64_t rowCount = this->colCount; + uint_fast64_t colCount = this->rowCount; + uint_fast64_t nonZeroEntryCount = this->nonZeroEntryCount; + + std::vector rowIndications(rowCount + 1); + std::vector columnIndications(nonZeroEntryCount); + std::vector values(nonZeroEntryCount, T()); + + // First, we need to count how many entries each column has. + for (uint_fast64_t i = 0; i < this->rowCount; ++i) { + typename storm::storage::SparseMatrix::Rows rows = this->getRow(i); + for (auto const& transition : rows) { + if (transition.value() > 0) { + ++rowIndications[transition.column() + 1]; + } + } + } + + // Now compute the accumulated offsets. + for (uint_fast64_t i = 1; i < rowCount + 1; ++i) { + rowIndications[i] = rowIndications[i - 1] + rowIndications[i]; + } + + // Create an array that stores the index for the next value to be added for + // each row in the transposed matrix. Initially this corresponds to the previously + // computed accumulated offsets. + std::vector nextIndices = rowIndications; + + // Now we are ready to actually fill in the values of the transposed matrix. + for (uint_fast64_t i = 0; i < this->rowCount; ++i) { + typename storm::storage::SparseMatrix::Rows rows = this->getRow(i); + for (auto& transition : rows) { + if (transition.value() > 0) { + values[nextIndices[transition.column()]] = transition.value(); + columnIndications[nextIndices[transition.column()]++] = i; + } + } + } + + storm::storage::SparseMatrix transposedMatrix(rowCount, colCount, + nonZeroEntryCount, + std::move(rowIndications), + std::move(columnIndications), + std::move(values)); + + return transposedMatrix; + } + template void SparseMatrix::invertDiagonal() { // Check if the matrix is square, because only then it makes sense to perform this @@ -1000,7 +1051,7 @@ namespace storage { // Explicit instantiations of specializations of this template here. template class SparseMatrix; - template class SparseMatrix; + template class SparseMatrix; // Functions of the tbbHelper_MatrixRowVectorScalarProduct friend class. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 0bd275e73..669b8b692 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -538,6 +538,13 @@ public: */ void convertToEquationSystem(); + /*! + * Transposes the matrix. + * + * @return A sparse matrix that represents the transpose of this matrix. + */ + storm::storage::SparseMatrix transpose() const; + /*! * Inverts all elements on the diagonal, i.e. sets the diagonal values to 1 minus their previous * value. Requires the matrix to contain each diagonal element and to be square. @@ -791,7 +798,7 @@ private: // Extern template declaration to tell the compiler that there already is an instanciation of this template somewhere. // The extern instance will be found by the linker. Prevents multiple instantiations of the same template specialisation. extern template class SparseMatrix; -extern template class SparseMatrix; +extern template class SparseMatrix; #ifdef STORM_HAVE_INTELTBB /*! diff --git a/src/utility/counterexamples.h b/src/utility/counterexamples.h index 0ac816236..bd441a048 100644 --- a/src/utility/counterexamples.h +++ b/src/utility/counterexamples.h @@ -25,7 +25,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); // Now we compute the set of labels that is present on all paths from the initial to the target states. std::vector> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels); diff --git a/src/utility/graph.h b/src/utility/graph.h index e0e68402b..c9c58a86a 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -50,7 +50,7 @@ namespace storm { storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbabilityGreater0 |= psiStates; @@ -177,7 +177,7 @@ namespace storm { * @return A bit vector that represents all states with probability 0. */ template - storm::storage::BitVector performProbGreater0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { + storm::storage::BitVector performProbGreater0E(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { // Prepare resulting bit vector. storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); @@ -245,7 +245,7 @@ namespace storm { * @return A bit vector that represents all states with probability 0. */ template - 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) { storm::storage::BitVector statesWithProbability0 = performProbGreater0E(model, backwardTransitions, phiStates, psiStates); statesWithProbability0.complement(); return statesWithProbability0; @@ -264,7 +264,7 @@ namespace storm { * @return A bit vector that represents all states with probability 1. */ template - 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. storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); @@ -338,7 +338,7 @@ namespace storm { std::pair result; // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); result.first = performProb0A(model, backwardTransitions, phiStates, psiStates); result.second = performProb1E(model, backwardTransitions, phiStates, psiStates); @@ -360,7 +360,7 @@ namespace storm { * @return A bit vector that represents all states with probability 0. */ template - storm::storage::BitVector performProbGreater0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { + storm::storage::BitVector performProbGreater0A(storm::models::AbstractNondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { // Prepare resulting bit vector. storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); @@ -451,7 +451,7 @@ namespace storm { * @return A bit vector that represents all states with probability 0. */ template - 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) { storm::storage::BitVector statesWithProbability0 = performProbGreater0A(model, backwardTransitions, phiStates, psiStates); statesWithProbability0.complement(); return statesWithProbability0; @@ -470,7 +470,7 @@ namespace storm { * @return A bit vector that represents all states with probability 0. */ template - 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. storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); @@ -543,7 +543,7 @@ namespace storm { std::pair result; // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); result.first = performProb0E(model, backwardTransitions, phiStates, psiStates); result.second = performProb1A(model, backwardTransitions, phiStates, psiStates); diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index a050be516..0f1459e52 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -98,7 +98,7 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDecomposition.size(), 1290297ull); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5..."); - storm::storage::SparseMatrix sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition))); + storm::storage::SparseMatrix sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition))); LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253ull); @@ -155,4 +155,4 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) { ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 7888ull); mdp2 = nullptr; -} \ No newline at end of file +}