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<bool> to SparseMatrix<T>. 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: 6d829e0903

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -99,7 +99,7 @@ namespace storm {
              */
             static struct StateInformation determineRelevantAndProblematicStates(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
                 StateInformation result;
-                storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> 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<T> const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
-                storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
                 uint_fast64_t numberOfConstraintsCreated = 0;
                 int error = 0;
                 std::vector<int> variables;

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<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
                 relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates);
                 relevancyInformation.relevantStates &= ~psiStates;
 
@@ -214,7 +214,7 @@ namespace storm {
                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
                 storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates();
                 std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
-                storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> 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<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
                 std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
-                storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> backwardTransitions = labeledMdp.getBackwardTransitions();
                 
                 // Compute the set of labels that may precede a given action.
                 for (auto currentState : relevancyInformation.relevantStates) {

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<std::vector<uint_fast64_t>> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph);
-        storm::storage::SparseMatrix<bool> stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents);
+        storm::storage::SparseMatrix<T> stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents);
 		std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
 
 		// Set up the environment for the power method.

src/models/AbstractModel.h

@@ -145,10 +145,10 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
         /*!
          * 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<bool> extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const {
+        storm::storage::SparseMatrix<T> 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<AbstractModel<T>> {
             }
             
             // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition.
-            storm::storage::SparseMatrix<bool> dependencyGraph(numberOfStates);
+            storm::storage::SparseMatrix<T> 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<AbstractModel<T>> {
             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<bool> getBackwardTransitions() const {
-            return getBackwardTransitions<bool>([](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 <typename TransitionType>
-        storm::storage::SparseMatrix<TransitionType> getBackwardTransitions(std::function<TransitionType(T const&)> const& selectionFunction) const {
-            uint_fast64_t numberOfStates = this->getNumberOfStates();
-            uint_fast64_t numberOfTransitions = this->getNumberOfTransitions();
-            
-            std::vector<uint_fast64_t> rowIndications(numberOfStates + 1);
-            std::vector<uint_fast64_t> columnIndications(numberOfTransitions);
-            std::vector<TransitionType> 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<T>::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<uint_fast64_t> 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<T>::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<TransitionType> backwardTransitionMatrix(numberOfStates, numberOfStates,
-                                                                                  numberOfTransitions,
-                                                                                  std::move(rowIndications),
-                                                                                  std::move(columnIndications),
-                                                                                  std::move(values));
-            
-            return backwardTransitionMatrix;
+        storm::storage::SparseMatrix<T> getBackwardTransitions() const {
+            return this->transitionMatrix.transpose();
         }
 
         /*!

src/storage/SparseMatrix.cpp

@@ -662,6 +662,57 @@ namespace storage {
 		negateAllNonDiagonalElements();
 	}
 
+	template <typename T>
+	SparseMatrix<T> SparseMatrix<T>::transpose() const {
+
+		uint_fast64_t rowCount = this->colCount;
+		uint_fast64_t colCount = this->rowCount;
+		uint_fast64_t nonZeroEntryCount = this->nonZeroEntryCount;
+
+		std::vector<uint_fast64_t> rowIndications(rowCount + 1);
+		std::vector<uint_fast64_t> columnIndications(nonZeroEntryCount);
+		std::vector<T> 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<T>::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<uint_fast64_t> 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<T>::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<T> transposedMatrix(rowCount, colCount,
+														 nonZeroEntryCount,
+														 std::move(rowIndications),
+														 std::move(columnIndications),
+														 std::move(values));
+
+		return transposedMatrix;
+	}
+
 	template<typename T>
 	void SparseMatrix<T>::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<double>;
-	template class SparseMatrix<bool>;
+	template class SparseMatrix<int>;
 
 	// Functions of the tbbHelper_MatrixRowVectorScalarProduct friend class.
 

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<T> 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<double>;
-extern template class SparseMatrix<bool>;
+extern template class SparseMatrix<int>;
 
 #ifdef STORM_HAVE_INTELTBB
 	/*!

src/utility/counterexamples.h

@@ -25,7 +25,7 @@ namespace storm {
                 storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
                 std::vector<storm::storage::VectorSet<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
-                storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> 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<storm::storage::VectorSet<uint_fast64_t>> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels);

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<bool> backwardTransitions = model.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> 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 <typename T>
-            storm::storage::BitVector performProbGreater0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> 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<T> const& model, storm::storage::SparseMatrix<T> 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 <typename T>
-            storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+            storm::storage::BitVector performProb0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> 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 <typename T>
-            storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+            storm::storage::BitVector performProb1E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
                 // Get some temporaries for convenience.
                 storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
@@ -338,7 +338,7 @@ namespace storm {
                 std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
                 
                 // Get the backwards transition relation from the model to ease the search.
-                storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> 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 <typename T>
-            storm::storage::BitVector performProbGreater0A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> 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<T> const& model, storm::storage::SparseMatrix<T> 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 <typename T>
-            storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+            storm::storage::BitVector performProb0E(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> 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 <typename T>
-            storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<bool> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+            storm::storage::BitVector performProb1A(storm::models::AbstractNondeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
                 // Get some temporaries for convenience.
                 storm::storage::SparseMatrix<T> const& transitionMatrix = model.getTransitionMatrix();
                 std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
@@ -543,7 +543,7 @@ namespace storm {
                 std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
                 
                 // Get the backwards transition relation from the model to ease the search.
-                storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
+                storm::storage::SparseMatrix<T> backwardTransitions = model.getBackwardTransitions();
                 
                 result.first = performProb0E(model, backwardTransitions, phiStates, psiStates);
                 result.second = performProb1A(model, backwardTransitions, phiStates, psiStates);

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<bool> sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition)));
+    storm::storage::SparseMatrix<double> 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;
-}
+}