Merge branch 'reduceCompiletime'

Conflicts:
	src/counterexamples/MILPMinimalLabelSetGenerator.h
	src/models/AbstractModel.h
	src/storage/SparseMatrix.h
	src/storm.cpp

Former-commit-id: 4c3dd2751a

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -88,7 +88,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);
@@ -672,7 +672,7 @@ namespace storm {
              * @return The total number of constraints that were created.
              */
             static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver& solver, 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;
                 std::vector<uint_fast64_t> variables;
                 std::vector<double> coefficients;

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -102,7 +102,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;
 
@@ -295,7 +295,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)) {
@@ -565,7 +565,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<storm::storage::StateBlock> const& decomposition) const {
+        storm::storage::SparseMatrix<T> extractPartitionDependencyGraph(storm::storage::Decomposition<storm::storage::StateBlock> 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/models/AbstractNondeterministicModel.h

@@ -122,6 +122,62 @@ namespace storm {
             return this->transitionMatrix.end(nondeterministicChoiceIndices[state + 1] - 1);
             }
 
+            /*!
+             * 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.
+             * Note: This overwrites the getBackwardsTransitions of the AbstractModel, since the simple
+             * transposition of the state matrix does not yield correct results for non-deterministic models.
+             *
+             * @return A sparse matrix that represents the backward transitions of this model.
+             */
+            storm::storage::SparseMatrix<T> getBackwardTransitions() 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<T> values(numberOfTransitions, T());
+
+                // 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 + 1; ++i) {
+                    rowIndications[i] = rowIndications[i - 1] + rowIndications[i];
+                }
+
+                // 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()]] = transition.value();
+                            columnIndications[nextIndices[transition.column()]++] = i;
+                        }
+                    }
+                }
+
+                storm::storage::SparseMatrix<T> backwardTransitionMatrix(numberOfStates, numberOfStates,
+                                                                         numberOfTransitions,
+                                                                         std::move(rowIndications),
+                                                                         std::move(columnIndications),
+                                                                         std::move(values));
+
+                return backwardTransitionMatrix;
+            }
+
             /*!
              * Calculates a hash over all values contained in this Model.
              * @return size_t A Hash Value

src/storage/MaximalEndComponentDecomposition.cpp

@@ -46,7 +46,7 @@ namespace storm {
         template <typename ValueType>
         void MaximalEndComponentDecomposition<ValueType>::performMaximalEndComponentDecomposition(storm::models::AbstractNondeterministicModel<ValueType> const& model, storm::storage::BitVector const& subsystem) {
             // Get some references for convenient access.
-            storm::storage::SparseMatrix<bool> backwardTransitions = model.getBackwardTransitions();
+            storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
             std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
             storm::storage::SparseMatrix<ValueType> const& transitionMatrix = model.getTransitionMatrix();
             
@@ -163,4 +163,4 @@ namespace storm {
         
         template class MaximalEndComponentDecomposition<double>;
     }
-}
+}

src/storage/StronglyConnectedComponentDecomposition.h

@@ -1,10 +1,11 @@
 #ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_
 #define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_
 
+#include "src/storage/SparseMatrix.h"
 #include "src/storage/Decomposition.h"
 #include "src/storage/VectorSet.h"
 #include "src/storage/BitVector.h"
-#include "src/storage/SparseMatrix.h"
+
 
 namespace storm {
     namespace models {

src/storage/VectorSet.cpp

@@ -289,4 +289,4 @@ namespace storm {
         template std::ostream& operator<<(std::ostream& stream, VectorSet<uint_fast64_t> const& set);
         template std::ostream& operator<<(std::ostream& stream, VectorSet<VectorSet<uint_fast64_t>> const& set);
     }
-}
+}

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;
-}
+}