Intermediate commit with submatrix computation for scheduler-induced system from MDP.

Former-commit-id: bcdc58c1a7

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -9,6 +9,7 @@
 #define STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_
 
 #include "src/modelchecker/prctl/AbstractModelChecker.h"
+#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
 #include "src/models/Mdp.h"
 #include "src/utility/vector.h"
 #include "src/utility/graph.h"
@@ -440,6 +441,19 @@ public:
 		// Determine the states for which the target predicate holds.
 		storm::storage::BitVector* targetStates = formula.getChild().check(*this);
 
+        std::vector<uint_fast64_t> usedScheduler(this->getModel().getNumberOfStates());
+        
+        storm::models::Dtmc<Type> dtmc(this->getModel().getTransitionMatrix().getSubmatrix(usedScheduler, this->getModel().getNondeterministicChoiceIndices()),
+                                       storm::models::AtomicPropositionsLabeling(this->getModel().getStateLabeling()),
+                                       this->getModel().hasStateRewards() ? boost::optional<std::vector<Type>>(this->getModel().getStateRewardVector()) : boost::optional<std::vector<Type>>(),
+                                       this->getModel().hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<Type>>(this->getModel().getTransitionRewardMatrix().getSubmatrix(usedScheduler, this->getModel().getNondeterministicChoiceIndices(), false)) : boost::optional<storm::storage::SparseMatrix<Type>>());
+        
+        dtmc.printModelInformationToStream(std::cout);
+        
+        storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<Type> mc(dtmc);
+        formula.check(mc, qualitative);
+        exit(-1);
+        
 		// Determine which states have a reward of infinity by definition.
 		storm::storage::BitVector infinityStates;
 		storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
@@ -454,6 +468,8 @@ public:
 		LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states.");
 		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
 
+        
+        
 		// Create resulting vector.
 		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
 

src/storage/SparseMatrix.h

@@ -378,7 +378,7 @@ public:
 	}
     
     /*!
-     * Inserts a value at the given row and column with the given value. After all elements have been added,
+     * Inserts a value at the given row and column with the given value. After all elements have been inserted,
      * a call to finalize() is mandatory.
      * NOTE: This is a linear inserter. It must be called consecutively for each element, row by row *and* column by
      * column.
@@ -871,6 +871,63 @@ public:
 		return result;
 	}
     
+    SparseMatrix getSubmatrix(std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGroupIndices, bool insertDiagonalEntries = true) const {
+        LOG4CPLUS_DEBUG(logger, "Creating a sub-matrix (of unknown size).");
+        
+        // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for diagonal
+        // entries.
+        uint_fast64_t subNonZeroEntries = 0;
+        for (uint_fast64_t rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
+            // Determine which row we need to select from the current row group.
+            uint_fast64_t rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
+            
+            // Iterate through that row and count the number of slots we have to reserve for copying.
+            bool foundDiagonalElement = false;
+            for (uint_fast64_t i = rowIndications[rowToCopy], rowEnd = rowIndications[rowToCopy + 1]; i < rowEnd; ++i) {
+                if (columnIndications[i] == rowGroupIndex) {
+                    foundDiagonalElement = true;
+                }
+                ++subNonZeroEntries;
+            }
+            if (insertDiagonalEntries && !foundDiagonalElement) {
+                ++subNonZeroEntries;
+            }
+        }
+        
+        LOG4CPLUS_DEBUG(logger, "Determined size of submatrix to be " << (rowGroupIndices.size() - 1) << "x" << colCount << " with " << subNonZeroEntries << " non-zero elements.");
+        
+        // Now create the matrix to be returned with the appropriate size.
+        SparseMatrix<T> submatrix(rowGroupIndices.size() - 1, colCount);
+        submatrix.initialize(subNonZeroEntries);
+        
+        // Copy over the selected lines from the source matrix.
+        for (uint_fast64_t rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) {
+            // Determine which row we need to select from the current row group.
+            uint_fast64_t rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex];
+            
+            // Iterate through that row and copy the entries. This also inserts a zero element on the diagonal if there
+            // is no entry yet.
+            bool insertedDiagonalElement = false;
+            for (uint_fast64_t i = rowIndications[rowToCopy], rowEnd = rowIndications[rowToCopy + 1]; i < rowEnd; ++i) {
+                if (columnIndications[i] == rowGroupIndex) {
+                    insertedDiagonalElement = true;
+                } else if (insertDiagonalEntries && !insertedDiagonalElement && columnIndications[i] > rowGroupIndex) {
+                    submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constGetZero<T>());
+                    insertedDiagonalElement = true;
+                }
+                submatrix.addNextValue(rowGroupIndex, columnIndications[i], valueStorage[i]);
+            }
+            if (insertDiagonalEntries && !insertedDiagonalElement) {
+                submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constGetZero<T>());
+            }
+        }
+        
+        // Finalize created matrix and return result.
+        submatrix.finalize();
+        LOG4CPLUS_DEBUG(logger, "Done creating sub-matrix.");
+        return submatrix;
+    }
+
 	/*!
 	 * Performs a change to the matrix that is needed if this matrix is to be interpreted as a
 	 * set of linear equations. In particular, it transforms A to (1-A), meaning that the elements