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."; }