From cbf4a2ff3b6a02f8456e72a80dec0d4c8ed8159c Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 4 Mar 2013 16:52:03 +0100 Subject: [PATCH] Small update to model checking reward formulae over MDPs. --- src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 2 +- src/modelchecker/GmmxxMdpPrctlModelChecker.h | 69 +++++++++++-------- 2 files changed, 40 insertions(+), 31 deletions(-) diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index a5a3b567d..d43acf2c1 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -225,7 +225,7 @@ public: totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); } - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. std::vector* swap = nullptr; diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index 52e371eb3..a10281822 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -234,6 +234,10 @@ public: throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; } + // Get the starting row indices for the non-deterministic choices to reduce the resulting + // vector properly. + std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); + // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); @@ -248,23 +252,27 @@ public: totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); } - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); + + // Create vector for result of multiplication, which is reduced to the result vector after + // each multiplication. + std::vector* multiplyResult = new std::vector(this->getModel().getTransitionMatrix()->getRowCount(), 0); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - std::vector* swap = nullptr; - std::vector* tmpResult = new std::vector(this->getModel().getNumberOfStates()); for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { - gmm::mult(*gmmxxMatrix, *result, *tmpResult); - swap = tmpResult; - tmpResult = result; - result = swap; + gmm::mult(*gmmxxMatrix, *result, *multiplyResult); + if (this->minimumOperatorStack.top()) { + storm::utility::reduceVectorMin(*multiplyResult, result, *nondeterministicChoiceIndices); + } else { + storm::utility::reduceVectorMax(*multiplyResult, result, *nondeterministicChoiceIndices); + } // Add the reward vector to the result. gmm::add(*totalRewardVector, *result); } + delete multiplyResult; // Delete temporary variables and return result. - delete tmpResult; delete gmmxxMatrix; delete totalRewardVector; return result; @@ -283,8 +291,11 @@ public: // Determine which states have a reward of infinity by definition. storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - // TODO: just commented out to make it compile - //storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates); + if (this->minimumOperatorStack.top()) { + storm::utility::GraphAnalyzer::performProb1A(this->getModel(), *trueStates, *targetStates, &infinityStates); + } else { + storm::utility::GraphAnalyzer::performProb1E(this->getModel(), *trueStates, *targetStates, &infinityStates); + } infinityStates.complement(); // Create resulting vector. @@ -294,22 +305,24 @@ public: storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); if (maybeStatesSetBitCount > 0) { - // Now we can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); - // Converting the matrix from the fixpoint notation to the form needed for the equation - // system. That is, we go from x = A*x + b to (I-A)x = b. - submatrix->convertToEquationSystem(); + // First, we can eliminate the rows and columns from the original transition probability matrix for states + // whose probabilities are already known. + storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); + + // Get the "new" nondeterministic choice indices for the submatrix. + std::shared_ptr> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - // Transform the submatrix to the gmm++ format to use its solvers. + // Transform the submatrix to the gmm++ format to use its capabilities. gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*submatrix); - delete submatrix; - // Initialize the x vector with 1 for each element. This is the initial guess for - // the iterative solvers. - std::vector x(maybeStatesSetBitCount, storm::utility::constGetOne()); + // Create vector for results for maybe states. + std::vector* x = new std::vector(maybeStatesSetBitCount); + + // 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()); + delete submatrix; - // Prepare the right-hand side of the equation system. - std::vector* b = new std::vector(maybeStatesSetBitCount); if (this->getModel().hasTransitionRewards()) { // If a transition-based reward model is available, we initialize the right-hand // side to the vector resulting from summing the rows of the pointwise product @@ -336,16 +349,12 @@ public: storm::utility::setVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); } - // Solve the corresponding system of linear equations. - // TODO: just commented out to make it compile - // this->solveEquationSystem(*gmmxxMatrix, x, *b); + // Solve the corresponding system of equations. + this->solveEquationSystem(*gmmxxMatrix, x, b, *subNondeterministicChoiceIndices); // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, x); - - // Delete temporary matrix and right-hand side. - delete gmmxxMatrix; - delete b; + storm::utility::setVectorValues(result, maybeStates, *x); + delete x; } // Set values of resulting vector that are known exactly.