Fixed the method for making rows absorbing for nondeterministic models.

src/modelchecker/GmmxxDtmcPrctlModelChecker.h

@@ -131,7 +131,7 @@ public:
 
 		// Only try to solve system if there are states for which the probability is unknown.
 		uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits();
-		if (mayBeStatesSetBitCount > 0) {
+		if (mayBeStatesSetBitCount > 0 && !qualitative) {
 			// Now we can eliminate the rows and columns from the original transition probability matrix.
 			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
 			// Converting the matrix from the fixpoint notation to the form needed for the equation
@@ -160,6 +160,10 @@ public:
 
 			// Delete temporary matrix.
 			delete gmmxxMatrix;
+		} else if (qualitative) {
+			// If we only need a qualitative result, we can safely assume that the results will only be compared to
+			// bounds which are either 0 or 1. Setting the value to 0.5 is thus safe.
+			storm::utility::setVectorValues<Type>(result, maybeStates, Type(0.5));
 		}
 
 		// Set values of resulting vector that are known exactly.

src/modelchecker/GmmxxMdpPrctlModelChecker.h

@@ -56,7 +56,7 @@ public:
 		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
 
 		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
-		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
+		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *nondeterministicChoiceIndices);
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
 		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(tmpMatrix);
@@ -67,12 +67,11 @@ public:
 
 		// Create vector for result of multiplication, which is reduced to the result vector after
 		// each multiplication.
-		std::vector<Type>* multiplyResult = new std::vector<Type>(this->getModel().getTransitionMatrix()->getRowCount());
+		std::vector<Type>* multiplyResult = new std::vector<Type>(this->getModel().getTransitionMatrix()->getRowCount(), 0);
 
 		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
 		for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
 			gmm::mult(*gmmxxMatrix, *result, *multiplyResult);
-
 			if (this->minimumOperatorStack.top()) {
 				storm::utility::reduceVectorMin(*multiplyResult, result, *nondeterministicChoiceIndices);
 			} else {

src/storage/SparseMatrix.h

@@ -641,12 +641,29 @@ public:
 	bool makeRowsAbsorbing(const storm::storage::BitVector rows) {
 		bool result = true;
 		for (auto row : rows) {
-			result &= makeRowAbsorbing(row);
+			result &= makeRowAbsorbing(row, row);
 		}
 
 		return result;
 	}
 
+	/*!
+	 * This function makes the groups of rows given by the bit vector absorbing.
+	 * @param rows A bit vector indicating which row groups to make absorbing.
+	 * @return True iff the operation was successful.
+	 */
+	bool makeRowsAbsorbing(const storm::storage::BitVector rows, std::vector<uint_fast64_t> const& nondeterministicChoices) {
+		bool result = true;
+		for (auto index : rows) {
+			for (uint_fast64_t row = nondeterministicChoices[index]; row < nondeterministicChoices[index + 1]; ++row) {
+				result &= makeRowAbsorbing(row, index);
+			}
+		}
+
+		return result;
+	}
+
+
 	/*!
 	 * This function makes the given row absorbing. This means that all
 	 * entries in will be set to 0 and the value 1 will be written
@@ -654,7 +671,7 @@ public:
 	 * @param row The row to be made absorbing.
 	 * @returns True iff the operation was successful.
 	 */
-	bool makeRowAbsorbing(const uint_fast64_t row) {
+	bool makeRowAbsorbing(const uint_fast64_t row, const uint_fast64_t column) {
 		// Check whether the accessed state exists.
 		if (row > rowCount) {
 			LOG4CPLUS_ERROR(logger, "Trying to make an illegal row " << row << " absorbing.");
@@ -668,28 +685,16 @@ public:
 		uint_fast64_t rowEnd = rowIndications[row + 1];
 
 		if (rowStart >= rowEnd) {
-			LOG4CPLUS_ERROR(logger, "Cannot make row absorbing, because there is no entry in this row.");
-			throw storm::exceptions::InvalidStateException("Cannot make row absorbing, because there is no entry in this row.");
+			LOG4CPLUS_ERROR(logger, "Cannot make row " << row << " absorbing, because there is no entry in this row.");
+			throw storm::exceptions::InvalidStateException() << "Cannot make row " << row << " absorbing, because there is no entry in this row.";
 		}
-		uint_fast64_t pseudoDiagonal = row % colCount;
 
-		bool foundDiagonal = false;
-		while (rowStart < rowEnd) {
-			if (!foundDiagonal && columnIndications[rowStart] >= pseudoDiagonal) {
-				foundDiagonal = true;
-				// insert/replace the diagonal entry
-				columnIndications[rowStart] = pseudoDiagonal;
 		valueStorage[rowStart] = storm::utility::constGetOne<T>();
-			} else {
-				valueStorage[rowStart] = storm::utility::constGetZero<T>();
-			}
-			++rowStart;
-		}
+		columnIndications[rowStart] = column;
 
-		if (!foundDiagonal) {
-			--rowStart;
-			columnIndications[rowStart] = pseudoDiagonal;
-			valueStorage[rowStart] = storm::utility::constGetOne<T>();
+		for (uint_fast64_t index = rowStart + 1; index < rowEnd; ++index) {
+			valueStorage[index] = storm::utility::constGetZero<T>();
+			columnIndications[index] = 0;
 		}
 
 		return true;

src/storm.cpp

@@ -226,20 +226,34 @@ void testCheckingDice(storm::models::Mdp<double>& mdp) {
 void testCheckingAsynchLeader(storm::models::Mdp<double>& mdp) {
 	storm::formula::Ap<double>* electedFormula = new storm::formula::Ap<double>("elected");
 	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probMinFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
 
 	storm::modelChecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker<double>(mdp);
 
+	mc->check(*probMinFormula);
+	delete probMinFormula;
+
+	electedFormula = new storm::formula::Ap<double>("elected");
+	eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
 	mc->check(*probMaxFormula);
 	delete probMaxFormula;
 
 	electedFormula = new storm::formula::Ap<double>("elected");
-	eventuallyFormula = new storm::formula::Eventually<double>(electedFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probMinFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+	storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(electedFormula, 50);
+	probMinFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
 
 	mc->check(*probMinFormula);
 	delete probMinFormula;
 
+	electedFormula = new storm::formula::Ap<double>("elected");
+	boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(electedFormula, 50);
+	probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
+
+	mc->check(*probMaxFormula);
+	delete probMaxFormula;
+
 	delete mc;
 }