From 736a9864ac0d4e3138522661d5eef445d2cd5daa Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 17 Jun 2013 17:47:30 +0200 Subject: [PATCH 1/3] Added model information output for explicit input. Former-commit-id: df722a3035e60c433257c9dac533ba6445136a4e --- src/storm.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm.cpp b/src/storm.cpp index dec23fffc..7785122fc 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -285,10 +285,10 @@ int main(const int argc, const char* argv[]) { // Depending on the model type, the appropriate model checking procedure is chosen. storm::modelchecker::prctl::AbstractModelChecker* modelchecker = nullptr; + parser.getModel>()->printModelInformationToStream(std::cout); switch (parser.getType()) { case storm::models::DTMC: LOG4CPLUS_INFO(logger, "Model is a DTMC."); - parser.getModel>()->writeDotToStream(std::cout); modelchecker = createPrctlModelChecker(*parser.getModel>()); checkPrctlFormulae(*modelchecker); break; From f040264660f6131fe8d02442db90a039d73f54f0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 17 Jun 2013 17:56:29 +0200 Subject: [PATCH 2/3] 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 From 04c7d5ba129eadfc506bc3b9e5e410fc665c999c Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 17 Jun 2013 21:16:31 +0200 Subject: [PATCH 3/3] On my way of implementing scheduler-guessing. Former-commit-id: b2717de2b6d0d8534a653c64bad6eb90c8ffef64 --- .../prctl/GmmxxMdpPrctlModelChecker.h | 8 +++ .../prctl/SparseMdpPrctlModelChecker.h | 61 +++++++++++-------- 2 files changed, 44 insertions(+), 25 deletions(-) diff --git a/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h index a1190a0fa..ff3ebd971 100644 --- a/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h @@ -126,6 +126,7 @@ private: // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. while (!converged && iterations < maxIterations) { + std::cout << "iter: " << iterations << std::endl; // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, multiplyResult); gmm::add(b, multiplyResult); @@ -140,6 +141,13 @@ private: // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative); + if (!converged) { + for (uint_fast64_t i = 0; i < newX->size(); ++i) { + std::cout << (*currentX)[i] << " vs. " << (*newX)[i] << std::endl; + } + } + + // Update environment variables. swap = currentX; currentX = newX; diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 8cbbd3474..eea889769 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -68,7 +68,7 @@ public: * @param formula The formula to check. * @returns The set of states satisfying the formula represented by a bit vector. */ - std::vector* checkNoBoundOperator(const storm::property::prctl::AbstractNoBoundOperator& formula) const { + virtual std::vector* checkNoBoundOperator(const storm::property::prctl::AbstractNoBoundOperator& formula) const { // Check if the operator was an non-optimality operator and report an error in that case. if (!formula.isOptimalityOperator()) { LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); @@ -261,7 +261,7 @@ public: * @return The probabilities for the given formula to hold on every state of the model associated with this model * checker. If the qualitative flag is set, exact probabilities might not be computed. */ - std::vector* checkUntil(bool minimize, const storm::property::prctl::Until& formula, bool qualitative, std::vector* scheduler) const { + virtual std::vector* checkUntil(bool minimize, const storm::property::prctl::Until& formula, bool qualitative, std::vector* scheduler) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. storm::storage::BitVector* leftStates = formula.getLeft().check(*this); storm::storage::BitVector* rightStates = formula.getRight().check(*this); @@ -310,13 +310,13 @@ public: // Get the "new" nondeterministic choice indices for the submatrix. std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - // Create vector for results for maybe states. - std::vector x(maybeStates.getNumberOfSetBits()); - // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. std::vector b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount()); + // Create vector for results for maybe states. + std::vector x = this->getInitialValueIterationValues(submatrix, formula); + // Solve the corresponding system of equations. this->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices); @@ -431,7 +431,7 @@ public: * @return The reward values for the given formula for every state of the model associated with this model * checker. If the qualitative flag is set, exact values might not be computed. */ - std::vector* checkReachabilityReward(bool minimize, const storm::property::prctl::ReachabilityReward& formula, bool qualitative, std::vector* scheduler) const { + virtual std::vector* checkReachabilityReward(bool minimize, const storm::property::prctl::ReachabilityReward& formula, bool qualitative, std::vector* scheduler) const { // Only compute the result if the model has at least one reward model. if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); @@ -441,19 +441,6 @@ 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); @@ -468,8 +455,6 @@ 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()); @@ -490,9 +475,6 @@ public: // Get the "new" nondeterministic choice indices for the submatrix. std::vector subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - // Create vector for results for maybe states. - std::vector x(submatrix.getColumnCount()); - // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. std::vector b(submatrix.getRowCount()); @@ -521,6 +503,9 @@ public: storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), this->getModel().getStateRewardVector()); } + // Create vector for results for maybe states. + std::vector x = this->getInitialValueIterationValues(submatrix, formula); + // Solve the corresponding system of equations. this->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices, scheduler); @@ -613,7 +598,9 @@ private: * @returns The solution vector x of the system of linear equations as the content of the parameter x. */ virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* takenChoices = nullptr) const { - // Get the settings object to customize solving. + LOG4CPLUS_INFO(logger, "Starting iterative solver."); + + // Get the settings object to customize solving. storm::settings::Settings* s = storm::settings::instance(); // Get relevant user-defined settings for solving the equations. @@ -708,6 +695,30 @@ private: return subNondeterministicChoiceIndices; } + + /*! + * Retrieves the values to be used as the initial values for the value iteration techniques. + * + * @param submatrix The matrix that will be used for value iteration later. + */ + std::vector getInitialValueIterationValues(storm::storage::SparseMatrix const& submatrix, storm::property::prctl::AbstractPathFormula const& formula) const { + // std::vector scheduler(submatrix.getColumnCount()); + std::vector scheduler(this->getModel().getNumberOfStates()); + + storm::models::Dtmc dtmc(this->getModel().getTransitionMatrix().getSubmatrix(scheduler, 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(scheduler, this->getModel().getNondeterministicChoiceIndices(), false)) : boost::optional>()); + + storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker modelChecker(dtmc); + + std::vector* modelCheckingResult = formula.check(modelChecker, false); + std::vector result(std::move(*modelCheckingResult)); + delete modelCheckingResult; + + return result; + } + }; } // namespace prctl