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

@@ -300,7 +300,7 @@ public:
 					// that we still consider (i.e. maybeStates), we need to extract these values
 					// first.
 					std::vector<Type>* subStateRewards = new std::vector<Type>(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.

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<Type>* result = new std::vector<Type>(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<Type>* 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<Type>* subStateRewards = new std::vector<Type>(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<Type>(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.

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 {

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;

src/utility/Vector.h

@@ -51,6 +51,18 @@ void selectVectorValues(std::vector<T>* vector, const storm::storage::BitVector&
 	}
 }
 
+template<class T>
+void selectVectorValues(std::vector<T>* vector, const storm::storage::BitVector& positions, const std::vector<uint_fast64_t>& rowMapping, std::vector<T> 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<class T>
 void subtractFromConstantOneVector(std::vector<T>* vector) {
 	for (auto it = vector->begin(); it != vector->end(); ++it) {
@@ -101,7 +113,7 @@ void reduceVectorMax(std::vector<T> const& source, std::vector<T>* target, std::
 template<class T>
 bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> 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.";
 	}