Adapted SCC-interface such that it can also be given a matrix instead of a model. More work on SCC-based mc.

Former-commit-id: 21d2482e4c

src/modelchecker/reachability/SparseSccModelChecker.cpp

@@ -58,7 +58,7 @@ namespace storm {
                 if (level <= 2) {
                     std::cout << "1" << std::endl;
                     // Here, we further decompose the SCC into sub-SCCs.
-                    storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(dtmc, scc & ~entryStates, true, false);
+                    storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(forwardTransitions, scc & ~entryStates, true, false);
                     std::cout << decomposition << std::endl;
 
                     // To eliminate the remaining one-state SCCs, we need to keep track of them.
@@ -147,12 +147,16 @@ namespace storm {
                     typename FlexibleSparseMatrix<ValueType>::row_type row = matrix.getRow(predecessorEntry.getColumn());
                     typename FlexibleSparseMatrix<ValueType>::row_type::iterator multiplyElement = std::find_if(row.begin(), row.end(), [=](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
                     
-                    // Now scale all the entries in the current row and insert them in the transitions of the predecessor.
-                    row.reserve(row.size() + newEntries);
-                    std::for_each(matrix.getRow(state).begin(), matrix.getRow(state).end(), [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { row.emplace_back(a.getColumn(), multiplyElement->getValue() * a.getValue()); });
-
+                    ValueType multiplyFactor = storm::utility::constantOne<ValueType>();
+                    if (multiplyElement != row.end()) {
                         // Remove the transition to the state that is to be eliminated.
                         multiplyElement->setValue(0);
+                        multiplyFactor = multiplyElement->getValue();
+                    }
+                    
+                    // Now scale all the entries in the current row and insert them in the transitions of the predecessor.
+                    row.reserve(row.size() + newEntries);
+                    std::for_each(matrix.getRow(state).begin(), matrix.getRow(state).end(), [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { row.emplace_back(a.getColumn(), multiplyFactor * a.getValue()); });
 
                     // Then sort the vector according to their column indices.
                     std::sort(row.begin(), row.end(), [](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a, storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& b){ return a.getColumn() < b.getColumn(); });

src/storage/StronglyConnectedComponentDecomposition.cpp

@@ -16,12 +16,17 @@ namespace storm {
         template <typename ValueType>
         StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
             storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end());
-            performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs);
+            performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs);
         }
         
         template <typename ValueType>
         StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) {
-            performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs);
+            performSccDecomposition(model.getTransitionMatrix(), subsystem, dropNaiveSccs, onlyBottomSccs);
+        }
+        
+        template <typename ValueType>
+        StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) {
+            performSccDecomposition(transitionMatrix, subsystem, dropNaiveSccs, onlyBottomSccs);
         }
         
         template <typename ValueType>
@@ -47,8 +52,8 @@ namespace storm {
         }
 
         template <typename ValueType>
-        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) {
-            uint_fast64_t numberOfStates = model.getNumberOfStates();
+        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) {
+            uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
 
             // Set up the environment of the algorithm.
             // Start with the two stacks it maintains.
@@ -71,7 +76,7 @@ namespace storm {
             uint_fast64_t currentIndex = 0;
             for (auto state : subsystem) {
                 if (!hasPreorderNumber.get(state)) {
-                    performSccDecompositionGCM(model, state, statesWithSelfLoop, subsystem, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount);
+                    performSccDecompositionGCM(transitionMatrix, state, statesWithSelfLoop, subsystem, currentIndex, hasPreorderNumber, preorderNumbers, s, p, stateHasScc, stateToSccMapping, sccCount);
                 }
             }
 
@@ -103,7 +108,7 @@ namespace storm {
                     for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
                         // If the block of the state is already known to be dropped, we don't need to check the transitions.
                         if (!blocksToDrop.get(stateToSccMapping[state])) {
-                            for (typename storm::storage::SparseMatrix<ValueType>::const_iterator successorIt = model.getRows(state).begin(), successorIte = model.getRows(state).end(); successorIt != successorIte; ++successorIt) {
+                            for (typename storm::storage::SparseMatrix<ValueType>::const_iterator successorIt = transitionMatrix.getRowGroup(state).begin(), successorIte = transitionMatrix.getRowGroup(state).end(); successorIt != successorIte; ++successorIt) {
                                 if (subsystem.get(successorIt->getColumn()) && stateToSccMapping[state] != stateToSccMapping[successorIt->getColumn()]) {
                                     blocksToDrop.set(stateToSccMapping[state]);
                                     break;
@@ -134,15 +139,15 @@ namespace storm {
             storm::storage::BitVector fullSystem(model.getNumberOfStates(), true);
             
             // Call the overloaded function.
-            performSccDecomposition(model, fullSystem, dropNaiveSccs, onlyBottomSccs);
+            performSccDecomposition(model.getTransitionMatrix(), fullSystem, dropNaiveSccs, onlyBottomSccs);
         }
         
         template <typename ValueType>
-        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecompositionGCM(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector<uint_fast64_t>& preorderNumbers, std::vector<uint_fast64_t>& s, std::vector<uint_fast64_t>& p, storm::storage::BitVector& stateHasScc, std::vector<uint_fast64_t>& stateToSccMapping, uint_fast64_t& sccCount) {
+        void StronglyConnectedComponentDecomposition<ValueType>::performSccDecompositionGCM(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector<uint_fast64_t>& preorderNumbers, std::vector<uint_fast64_t>& s, std::vector<uint_fast64_t>& p, storm::storage::BitVector& stateHasScc, std::vector<uint_fast64_t>& stateToSccMapping, uint_fast64_t& sccCount) {
             
             // Prepare the stack used for turning the recursive procedure into an iterative one.
             std::vector<uint_fast64_t> recursionStateStack;
-            recursionStateStack.reserve(model.getNumberOfStates());
+            recursionStateStack.reserve(transitionMatrix.getRowGroupCount());
             recursionStateStack.push_back(startState);
 
             while (!recursionStateStack.empty()) {
@@ -157,7 +162,7 @@ namespace storm {
                     s.push_back(currentState);
                     p.push_back(currentState);
                 
-                    for (auto const& successor : model.getRows(currentState)) {
+                    for (auto const& successor : transitionMatrix.getRowGroup(currentState)) {
                         if (subsystem.get(successor.getColumn()) && successor.getValue() != storm::utility::constantZero<ValueType>()) {
                             if (currentState == successor.getColumn()) {
                                 statesWithSelfLoop.set(currentState);

src/storage/StronglyConnectedComponentDecomposition.h

@@ -1,6 +1,7 @@
 #ifndef STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_
 #define STORM_STORAGE_STRONGLYCONNECTEDCOMPONENTDECOMPOSITION_H_
 
+#include "src/storage/SparseMatrix.h"
 #include "src/storage/Decomposition.h"
 #include "src/storage/BitVector.h"
 
@@ -58,6 +59,19 @@ namespace storm {
              */
             StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
 
+            /*
+             * Creates an SCC decomposition of the given subsystem in the given system (whose transition relation is 
+             * given by a sparse matrix).
+             *
+             * @param transitionMatrix The transition matrix of the system to decompose.
+             * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs.
+             * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
+             * without a self-loop) are to be kept in the decomposition.
+             * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
+             * leaving the SCC), are kept.
+             */
+            StronglyConnectedComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false);
+            
             /*!
              * Creates an SCC decomposition by copying the given SCC decomposition.
              *
@@ -103,21 +117,21 @@ namespace storm {
              * Performs the SCC decomposition of the given block in the given model. As a side-effect this fills
              * the vector of blocks of the decomposition.
              *
-             * @param model The model that contains the block.
+             * @param transitionMatrix The transition matrix of the system to decompose.
              * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs.
              * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state
              * without a self-loop) are to be kept in the decomposition.
              * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of
              * leaving the SCC), are kept.
              */
-            void performSccDecomposition(storm::models::AbstractModel<ValueType> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
+            void performSccDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
             
             /*!
              * Uses the algorithm by Gabow/Cheriyan/Mehlhorn ("Path-based strongly connected component algorithm") to
              * compute a mapping of states to their SCCs. All arguments given by (non-const) reference are modified by
              * the function as a side-effect.
              *
-             * @param model The model to decompose into SCCs.
+             * @param transitionMatrix The transition matrix of the system to decompose.
              * @param startState The starting state for the search of Tarjan's algorithm.
              * @param statesWithSelfLoop A bit vector that is to be filled with all states that have a self-loop. This
              * is later needed for identification of the naive SCCs.
@@ -133,7 +147,7 @@ namespace storm {
              * @param sccCount The number of SCCs that have been computed. As a side effect of this function, this count
              * is increased.
              */
-            void performSccDecompositionGCM(storm::models::AbstractModel<ValueType> const& model, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector<uint_fast64_t>& preorderNumbers, std::vector<uint_fast64_t>& s, std::vector<uint_fast64_t>& p, storm::storage::BitVector& stateHasScc, std::vector<uint_fast64_t>& stateToSccMapping, uint_fast64_t& sccCount);
+            void performSccDecompositionGCM(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, uint_fast64_t startState, storm::storage::BitVector& statesWithSelfLoop, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, storm::storage::BitVector& hasPreorderNumber, std::vector<uint_fast64_t>& preorderNumbers, std::vector<uint_fast64_t>& s, std::vector<uint_fast64_t>& p, storm::storage::BitVector& stateHasScc, std::vector<uint_fast64_t>& stateToSccMapping, uint_fast64_t& sccCount);
         };
     }
 }