From f040264660f6131fe8d02442db90a039d73f54f0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 17 Jun 2013 17:56:29 +0200 Subject: [PATCH] Intermediate commit with submatrix computation for scheduler-induced system from MDP. Former-commit-id: e497f03c00ffec761a20ea90bead614d9963fa7c --- .../prctl/SparseMdpPrctlModelChecker.h | 16 +++++ src/storage/SparseMatrix.h | 59 ++++++++++++++++++- 2 files changed, 74 insertions(+), 1 deletion(-) diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index f9f329c58..8cbbd3474 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/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 usedScheduler(this->getModel().getNumberOfStates()); + + storm::models::Dtmc dtmc(this->getModel().getTransitionMatrix().getSubmatrix(usedScheduler, this->getModel().getNondeterministicChoiceIndices()), + storm::models::AtomicPropositionsLabeling(this->getModel().getStateLabeling()), + this->getModel().hasStateRewards() ? boost::optional>(this->getModel().getStateRewardVector()) : boost::optional>(), + this->getModel().hasTransitionRewards() ? boost::optional>(this->getModel().getTransitionRewardMatrix().getSubmatrix(usedScheduler, this->getModel().getNondeterministicChoiceIndices(), false)) : boost::optional>()); + + dtmc.printModelInformationToStream(std::cout); + + storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker 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* result = new std::vector(this->getModel().getNumberOfStates()); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 12a0a6e93..6c9361e97 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -374,7 +374,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. @@ -866,6 +866,63 @@ public: LOG4CPLUS_DEBUG(logger, "Done creating sub-matrix."); return result; } + + SparseMatrix getSubmatrix(std::vector const& rowGroupToRowIndexMapping, std::vector 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 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()); + insertedDiagonalElement = true; + } + submatrix.addNextValue(rowGroupIndex, columnIndications[i], valueStorage[i]); + } + if (insertDiagonalEntries && !insertedDiagonalElement) { + submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constGetZero()); + } + } + + // 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