From bc4eb661ba4b5ea10ac6b09de3d613a8ebf61dad Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 6 Mar 2013 11:45:43 +0100 Subject: [PATCH] Fixed some memory leaks. Fixed bug in vector utility. Fixed bug in sparse matrix printing. Fixed bug in DTMC model checker (computing reachability rewards). Included full reward model checking for MDPs. --- src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 4 ++-- src/modelchecker/GmmxxMdpPrctlModelChecker.h | 22 ++++++++++++++----- src/storage/SparseMatrix.h | 2 +- src/utility/GraphAnalyzer.h | 3 +++ src/utility/Vector.h | 14 +++++++++++- 5 files changed, 35 insertions(+), 10 deletions(-) diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index d43acf2c1..9213df3fa 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -300,7 +300,7 @@ public: // that we still consider (i.e. maybeStates), we need to extract these values // first. std::vector* subStateRewards = new std::vector(maybeStatesSetBitCount); - storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); + storm::utility::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); gmm::add(*subStateRewards, *b); delete subStateRewards; } @@ -309,7 +309,7 @@ public: // right-hand side. As the state reward vector contains entries not just for the // states that we still consider (i.e. maybeStates), we need to extract these values // first. - storm::utility::setVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); + storm::utility::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); } // Solve the corresponding system of linear equations. diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index a10281822..9514cb048 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -292,17 +292,21 @@ public: storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); if (this->minimumOperatorStack.top()) { - storm::utility::GraphAnalyzer::performProb1A(this->getModel(), *trueStates, *targetStates, &infinityStates); + storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates, &infinityStates); } else { - storm::utility::GraphAnalyzer::performProb1E(this->getModel(), *trueStates, *targetStates, &infinityStates); + storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates, &infinityStates); } infinityStates.complement(); + LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); + LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states."); + storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + // Create resulting vector. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); // Check whether there are states for which we have to compute the result. - storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); if (maybeStatesSetBitCount > 0) { // First, we can eliminate the rows and columns from the original transition probability matrix for states @@ -328,7 +332,7 @@ public: // side to the vector resulting from summing the rows of the pointwise product // of the transition probability matrix and the transition reward matrix. std::vector* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - storm::utility::selectVectorValues(b, maybeStates, *pointwiseProductRowSumVector); + storm::utility::selectVectorValues(&b, maybeStates, *pointwiseProductRowSumVector); delete pointwiseProductRowSumVector; if (this->getModel().hasStateRewards()) { @@ -338,7 +342,7 @@ public: // first. std::vector* subStateRewards = new std::vector(maybeStatesSetBitCount); storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); - gmm::add(*subStateRewards, *b); + gmm::add(*subStateRewards, b); delete subStateRewards; } } else { @@ -346,7 +350,7 @@ public: // right-hand side. As the state reward vector contains entries not just for the // states that we still consider (i.e. maybeStates), we need to extract these values // first. - storm::utility::setVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); + storm::utility::selectVectorValues(&b, maybeStates, *subNondeterministicChoiceIndices, *this->getModel().getStateRewardVector()); } // Solve the corresponding system of equations. @@ -355,6 +359,7 @@ public: // Set values of resulting vector according to result. storm::utility::setVectorValues(result, maybeStates, *x); delete x; + delete gmmxxMatrix; } // Set values of resulting vector that are known exactly. @@ -417,6 +422,11 @@ private: ++iterations; } + if (iterations % 2 == 1) { + delete x; + } else { + delete newX; + } delete temporaryResult; // Check if the solver converged and issue a warning otherwise. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 503d7ccc8..0b7737604 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -1151,7 +1151,7 @@ public: result << i << "\t(\t"; uint_fast64_t currentRealIndex = 0; while (currentRealIndex < colCount) { - if (currentRealIndex == columnIndications[nextIndex] && nextIndex < rowIndications[i + 1]) { + if (nextIndex < rowIndications[i + 1] && currentRealIndex == columnIndications[nextIndex]) { result << valueStorage[nextIndex] << "\t"; ++nextIndex; } else { diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index c7325befd..f9b6b783a 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -262,6 +262,8 @@ public: } else { *currentStates = *nextStates; } + + delete nextStates; } *statesWithProbability1 = *currentStates; @@ -407,6 +409,7 @@ public: } else { *currentStates = *nextStates; } + delete nextStates; } *statesWithProbability1 = *currentStates; diff --git a/src/utility/Vector.h b/src/utility/Vector.h index 7e5224af4..87ed40b29 100644 --- a/src/utility/Vector.h +++ b/src/utility/Vector.h @@ -51,6 +51,18 @@ void selectVectorValues(std::vector* vector, const storm::storage::BitVector& } } +template +void selectVectorValues(std::vector* vector, const storm::storage::BitVector& positions, const std::vector& rowMapping, std::vector const& values) { + uint_fast64_t oldPosition = 0; + uint_fast64_t rowMappingPosition = 0; + for (auto position : positions) { + for (uint_fast64_t i = rowMapping[rowMappingPosition]; i < rowMapping[rowMappingPosition + 1]; ++i) { + (*vector)[oldPosition++] = values[position]; + } + ++rowMappingPosition; + } +} + template void subtractFromConstantOneVector(std::vector* vector) { for (auto it = vector->begin(); it != vector->end(); ++it) { @@ -101,7 +113,7 @@ void reduceVectorMax(std::vector const& source, std::vector* target, std:: template bool equalModuloPrecision(std::vector const& vectorLeft, std::vector const& vectorRight, T precision, bool relativeError) { if (vectorLeft.size() != vectorRight.size()) { - LOG4CPLUS_ERROR(logger, "Length of vectors does not match and makes comparison impossible."); + LOG4CPLUS_ERROR(logger, "Lengths of vectors does not match and makes comparison impossible."); throw storm::exceptions::InvalidArgumentException() << "Length of vectors does not match and makes comparison impossible."; }