Merge branch 'master' into imca

Conflicts:
	src/storage/SparseMatrix.h

Former-commit-id: 7e28105e8b

CMakeLists.txt

@@ -110,7 +110,7 @@ if(CMAKE_COMPILER_IS_GNUCC)
     message(STATUS "StoRM - Using Compiler Configuration: GCC")
     # Set standard flags for GCC
     set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++0x -Wall -pedantic")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic")
     # -Werror is atm removed as this gave some problems with existing code
     # May be re-set later
     # (Thomas Heinemann, 2012-12-21)
@@ -482,5 +482,5 @@ add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PRO
 add_custom_target(memcheck-functional-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-functional-tests -v --fix-deadlocks	DEPENDS storm-functional-tests)
 add_custom_target(memcheck-performance-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-performance-tests -v --fix-deadlocks DEPENDS storm-performance-tests)
 
-set (CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams)
-add_custom_target(style python cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp"`)
+set(CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams)
+add_custom_target(style python cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp" `)

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -8,6 +8,8 @@
 #ifndef STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_
 #define STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_
 
+#include <chrono>
+
 #include "src/models/Mdp.h"
 #include "src/ir/Program.h"
 #include "src/exceptions/NotImplementedException.h"
@@ -88,7 +90,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 +674,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) {
@@ -902,7 +902,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();
 
                 // First, we add the formulas that encode
                 // (1) if an incoming transition is chosen, an outgoing one is chosen as well (for non-initial states)

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@@ -103,7 +103,7 @@ namespace storm {
                     // Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules.
                     uint_fast64_t rowIndex = 0;
                     for (auto state : markovianNonGoalStates) {
-                        typename storm::storage::SparseMatrix<ValueType>::MutableRows row = aMarkovian.getRow(rowIndex);
+                        typename storm::storage::SparseMatrix<ValueType>::MutableRows row = aMarkovian.getMutableRow(rowIndex);
                         for (auto element : row) {
                             ValueType eTerm = std::exp(-exitRates[state] * delta);
                             if (element.column() == rowIndex) {
@@ -118,7 +118,7 @@ namespace storm {
                     // Digitize aMarkovianToProbabilistic. As there are no self-loops in this case, we only need to apply the digitization formula for regular successors.
                     rowIndex = 0;
                     for (auto state : markovianNonGoalStates) {
-                        typename storm::storage::SparseMatrix<ValueType>::MutableRows row = aMarkovianToProbabilistic.getRow(rowIndex);
+                        typename storm::storage::SparseMatrix<ValueType>::MutableRows row = aMarkovianToProbabilistic.getMutableRow(rowIndex);
                         for (auto element : row) {
                             element.value() = (1 - std::exp(-exitRates[state] * delta)) * element.value();
                         }

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/models/MarkovAutomaton.h

@@ -100,7 +100,7 @@ namespace storm {
                 return this->exitRates[state];
             }
             
-            T const& getMaximalExitRate() const {
+            T getMaximalExitRate() const {
                 T result = storm::utility::constGetZero<T>();
                 for (auto markovianState : this->markovianStates) {
                     result = std::max(result, this->exitRates[markovianState]);

src/solver/GurobiLpSolver.h

@@ -2,6 +2,7 @@
 #define STORM_SOLVER_GUROBILPSOLVER
 
 #include "src/solver/LpSolver.h"
+#include "src/exceptions/NotImplementedException.h"
 
 // To detect whether the usage of Gurobi is possible, this include is neccessary.
 #include "storm-config.h"
@@ -58,6 +59,16 @@ namespace storm {
 #else
         // If Gurobi is not available, we provide a stub implementation that emits an error if any of its methods is called.
         class GurobiLpSolver : public LpSolver {
+        public:
+
+        	GurobiLpSolver(std::string const& name) : LpSolver(MINIMIZE) {
+        		throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+        	}
+
+        	virtual ~GurobiLpSolver() {
+        		throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+        	}
+
             virtual uint_fast64_t createContinuousVariable(std::string const& name, VariableType const& variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override {
                 throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
             }
@@ -66,7 +77,7 @@ namespace storm {
                 throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
             }
             
-            virtual uint_fast64_t createBinaryVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) override {
+            virtual uint_fast64_t createBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override {
                 throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
             }
             

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();
             
@@ -55,7 +55,12 @@ namespace storm {
             endComponentStateSets.emplace_back(subsystem);
             storm::storage::BitVector statesToCheck(model.getNumberOfStates());
             
-            for (std::list<StateBlock>::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) {
+
+            // The iterator used here should really be a const_iterator.
+            // However, gcc 4.8 (and assorted libraries) does not provide an erase(const_iterator) method for std::list but only an erase(iterator).
+            // This is in compliance with the c++11 draft N3337, which specifies the change from iterator to const_iterator only for "set, multiset, map [and] multimap".
+            // FIXME: As soon as gcc provides an erase(const_iterator) method, change this iterator back to a const_iterator.
+            for (std::list<StateBlock>::iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) {
                 StateBlock const& mec = *mecIterator;
 
                 // Keep track of whether the MEC changed during this iteration.
@@ -121,7 +126,7 @@ namespace storm {
                         }
                     }
 
-                    std::list<StateBlock>::const_iterator eraseIterator(mecIterator);
+                    std::list<StateBlock>::iterator eraseIterator(mecIterator);
                     ++mecIterator;
                     endComponentStateSets.erase(eraseIterator);
                 } else {
@@ -163,4 +168,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

@@ -196,7 +196,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        typename VectorSet<ValueType>::iterator VectorSet<ValueType>::insert(typename VectorSet<ValueType>::const_iterator pos, ValueType const& element) {
+        typename VectorSet<ValueType>::iterator VectorSet<ValueType>::insert(typename VectorSet<ValueType>::iterator pos, ValueType const& element) {
             dirty = true;
             return data.insert(pos, element);
         }
@@ -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/storage/VectorSet.h

@@ -84,7 +84,8 @@ namespace storm  {
             
             void insert(ValueType const& element);
             
-            iterator insert(const_iterator pos, ValueType const& element);
+            // FIXME: As soon as gcc provides an erase(const_iterator) method, change this iterator back to a const_iterator.
+            iterator insert(iterator pos, ValueType const& element);
             
             void insert(VectorSet<ValueType> const& other);
             

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