Merge branch 'master' of https://sselab.de/lab9/private/git/storm

src/modelchecker/AbstractModelChecker.h

@@ -71,6 +71,85 @@ public:
 		return nullptr;
 	}
 
+	/*!
+	 * Checks the given state formula on the DTMC and prints the result (true/false) for all initial
+	 * states.
+	 * @param stateFormula The formula to be checked.
+	 */
+	void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const {
+		std::cout << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
+		std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
+		storm::storage::BitVector* result = nullptr;
+		try {
+			result = stateFormula.check(*this);
+			LOG4CPLUS_INFO(logger, "Result for initial states:");
+			std::cout << "Result for initial states:" << std::endl;
+			for (auto initialState : model.getLabeledStates("init")) {
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
+				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+			}
+			delete result;
+		} catch (std::exception& e) {
+			std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
+			if (result != nullptr) {
+				delete result;
+			}
+		}
+		std::cout << std::endl;
+		storm::utility::printSeparationLine(std::cout);
+	}
+
+	/*!
+	 * Checks the given operator (with no bound) on the DTMC and prints the result
+	 * (probability/rewards) for all initial states.
+	 * @param noBoundFormula The formula to be checked.
+	 */
+	void check(const storm::formula::NoBoundOperator<Type>& noBoundFormula) const {
+		std::cout << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
+		std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
+		std::vector<Type>* result = nullptr;
+		try {
+			result = noBoundFormula.check(*this);
+			LOG4CPLUS_INFO(logger, "Result for initial states:");
+			std::cout << "Result for initial states:" << std::endl;
+			for (auto initialState : *model.getLabeledStates("init")) {
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
+				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+			}
+			delete result;
+		} catch (std::exception& e) {
+			std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
+			if (result != nullptr) {
+				delete result;
+			}
+		}
+		std::cout << std::endl;
+		storm::utility::printSeparationLine(std::cout);
+	}
+
+	/*!
+	 * The check method for a formula with an AP node as root in its formula tree
+	 *
+	 * @param formula The Ap state formula to check
+	 * @returns The set of states satisfying the formula, represented by a bit vector
+	 */
+	storm::storage::BitVector* checkAp(const storm::formula::Ap<Type>& formula) const {
+		if (formula.getAp().compare("true") == 0) {
+			return new storm::storage::BitVector(model.getNumberOfStates(), true);
+		} else if (formula.getAp().compare("false") == 0) {
+			return new storm::storage::BitVector(model.getNumberOfStates());
+		}
+
+		if (!model.hasAtomicProposition(formula.getAp())) {
+			LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid.");
+			throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
+		}
+
+		return new storm::storage::BitVector(*model.getLabeledStates(formula.getAp()));
+	}
+
 	/*!
 	 * The check method for a state formula with an And node as root in its formula tree
 	 *

src/modelchecker/DtmcPrctlModelChecker.h

@@ -8,6 +8,8 @@
 #ifndef STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_
 #define STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_
 
+#include <vector>
+
 #include "src/formula/Formulas.h"
 #include "src/utility/Vector.h"
 #include "src/storage/SparseMatrix.h"
@@ -16,12 +18,11 @@
 #include "src/storage/BitVector.h"
 #include "src/exceptions/InvalidPropertyException.h"
 #include "src/utility/Vector.h"
+#include "src/utility/GraphAnalyzer.h"
 #include "src/modelchecker/AbstractModelChecker.h"
-#include <vector>
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
-
 extern log4cplus::Logger logger;
 
 namespace storm {
@@ -38,8 +39,7 @@ namespace modelChecker {
  * @attention This class is abstract.
  */
 template<class Type>
-class DtmcPrctlModelChecker : 
-	public AbstractModelChecker<Type> {
+class DtmcPrctlModelChecker : public AbstractModelChecker<Type> {
 
 public:
 	/*!
@@ -47,8 +47,7 @@ public:
 	 *
 	 * @param model The dtmc model which is checked.
 	 */
-	explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model)
-		: AbstractModelChecker<Type>(model) {
+	explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model) : AbstractModelChecker<Type>(model) {
 		// Intentionally left empty.
 	}
 
@@ -58,6 +57,7 @@ public:
 	 * @param modelChecker The model checker that is copied.
 	 */
 	explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) : AbstractModelChecker<Type>(modelChecker) {
+		// Intentionally left empty.
 	}
 
 	/*!
@@ -74,93 +74,6 @@ public:
 		return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>();
 	}
 
-	/*!
-	 * Sets the DTMC model which is checked
-	 * @param model
-	 */
-	void setModel(storm::models::Dtmc<Type>& model) {
-		AbstractModelChecker<Type>::setModel(model);
-	}
-
-	/*!
-	 * The check method for a formula with an AP node as root in its formula tree
-	 *
-	 * @param formula The Ap state formula to check
-	 * @returns The set of states satisfying the formula, represented by a bit vector
-	 */
-	storm::storage::BitVector* checkAp(const storm::formula::Ap<Type>& formula) const {
-		if (formula.getAp().compare("true") == 0) {
-			return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true);
-		} else if (formula.getAp().compare("false") == 0) {
-			return new storm::storage::BitVector(this->getModel().getNumberOfStates());
-		}
-
-		if (!this->getModel().hasAtomicProposition(formula.getAp())) {
-			LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid.");
-			throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
-		}
-
-		return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp()));
-	}
-
-	/*!
-	 * Checks the given state formula on the DTMC and prints the result (true/false) for all initial
-	 * states.
-	 * @param stateFormula The formula to be checked.
-	 */
-	void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const {
-		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
-		std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
-		storm::storage::BitVector* result = nullptr;
-		try {
-			result = stateFormula.check(*this);
-			LOG4CPLUS_INFO(logger, "Result for initial states:");
-			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : *this->getModel().getLabeledStates("init")) {
-				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
-				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
-			}
-			delete result;
-		} catch (std::exception& e) {
-			std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
-			if (result != nullptr) {
-				delete result;
-			}
-		}
-		std::cout << std::endl;
-		storm::utility::printSeparationLine(std::cout);
-	}
-
-	/*!
-	 * Checks the given operator (with no bound) on the DTMC and prints the result
-	 * (probability/rewards) for all initial states.
-	 * @param noBoundFormula The formula to be checked.
-	 */
-	void check(const storm::formula::NoBoundOperator<Type>& noBoundFormula) const {
-		std::cout << std::endl;
-		LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
-		std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
-		std::vector<Type>* result = nullptr;
-		try {
-			result = noBoundFormula.check(*this);
-			LOG4CPLUS_INFO(logger, "Result for initial states:");
-			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : *this->getModel().getLabeledStates("init")) {
-				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
-				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
-			}
-			delete result;
-		} catch (std::exception& e) {
-			std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
-			if (result != nullptr) {
-				delete result;
-			}
-		}
-		std::cout << std::endl;
-		storm::utility::printSeparationLine(std::cout);
-	}
-
 	/*!
 	 * The check method for a state formula with a probabilistic operator node without bounds as root
 	 * in its formula tree
@@ -182,7 +95,31 @@ public:
 	 * @param formula The Bounded Until path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const {
+		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
+		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
+		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
+
+		// Copy the matrix before we make any changes.
+		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
+
+		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
+		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
+
+		// Delete obsolete intermediates.
+		delete leftStates;
+		delete rightStates;
+
+		// Create the vector with which to multiply.
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+		storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
+
+		// Perform the matrix vector multiplication as often as required by the formula bound.
+		this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound());
+
+		// Return result.
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with a Next operator node as root in its formula tree
@@ -190,7 +127,23 @@ public:
 	 * @param formula The Next path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const {
+		// First, we need to compute the states that satisfy the child formula of the next-formula.
+		storm::storage::BitVector* nextStates = formula.getChild().check(*this);
+
+		// Create the vector with which to multiply and initialize it correctly.
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+		storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne<Type>());
+
+		// Delete obsolete intermediate.
+		delete nextStates;
+
+		// Perform one single matrix-vector multiplication.
+		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result);
+
+		// Return result.
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with a Bounded Eventually operator node as root in its
@@ -239,7 +192,68 @@ public:
 	 * @param formula The Until path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const {
+		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
+		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
+		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
+
+		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
+		// all states that have probability 0 and 1 of satisfying the until-formula.
+		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
+		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
+		storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
+
+		// Delete intermediate results that are obsolete now.
+		delete leftStates;
+		delete rightStates;
+
+		// Perform some logging.
+		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
+		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
+		storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
+		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+
+		// Create resulting vector.
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+
+		// Only try to solve system if there are states for which the probability is unknown.
+		uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
+		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
+			// system. That is, we go from x = A*x + b to (I-A)x = b.
+			submatrix->convertToEquationSystem();
+
+			// Initialize the x vector with 0.5 for each element. This is the initial guess for
+			// the iterative solvers. It should be safe as for all 'maybe' states we know that the
+			// probability is strictly larger than 0.
+			std::vector<Type> x(maybeStatesSetBitCount, Type(0.5));
+
+			// 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<Type> b(maybeStatesSetBitCount);
+			this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1, &b);
+
+			this->solveEquationSystem(*submatrix, x, b);
+
+			// Delete the created submatrix.
+			delete submatrix;
+
+			// Set values of resulting vector according to result.
+			storm::utility::setVectorValues<Type>(result, maybeStates, x);
+		} 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.
+		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
+
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with an Instantaneous Reward operator node as root in its
@@ -248,7 +262,22 @@ public:
 	 * @param formula The Instantaneous Reward formula to check
 	 * @returns for each state the reward that the instantaneous reward yields
 	 */
-	virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const {
+		// Only compute the result if the model has a state-based reward model.
+		if (!this->getModel().hasStateRewards()) {
+			LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
+			throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula.";
+		}
+
+		// Initialize result to state rewards of the model.
+		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+
+		// Perform the actual matrix-vector multiplication as long as the bound of the formula is met.
+		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound());
+
+		// Return result.
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with a Cumulative Reward operator node as root in its
@@ -257,7 +286,32 @@ public:
 	 * @param formula The Cumulative Reward formula to check
 	 * @returns for each state the reward that the cumulative reward yields
 	 */
-	virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const {
+		// Only compute the result if the model has at least one reward model.
+		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
+			LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
+			throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
+		}
+
+		// Compute the reward vector to add in each step based on the available reward models.
+		std::vector<Type>* totalRewardVector = nullptr;
+		if (this->getModel().hasTransitionRewards()) {
+			totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
+			if (this->getModel().hasStateRewards()) {
+				gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector);
+			}
+		} else {
+			totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector());
+		}
+
+		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+
+		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound());
+
+		// Delete temporary variables and return result.
+		delete totalRewardVector;
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with a Reachability Reward operator node as root in its
@@ -266,10 +320,88 @@ public:
 	 * @param formula The Reachbility Reward formula to check
 	 * @returns for each state the reward that the reachability reward yields
 	 */
-	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const {
+		// Only compute the result if the model has at least one reward model.
+		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
+			LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
+			throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
+		}
+
+		// Determine the states for which the target predicate holds.
+		storm::storage::BitVector* targetStates = formula.getChild().check(*this);
+
+		// 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);
+		storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates);
+		infinityStates.complement();
+
+		// 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) {
+			// 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
+			// system. That is, we go from x = A*x + b to (I-A)x = b.
+			submatrix->convertToEquationSystem();
+
+			// Initialize the x vector with 1 for each element. This is the initial guess for
+			// the iterative solvers.
+			std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
+
+			// Prepare the right-hand side of the equation system.
+			std::vector<Type> b(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
+				// 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);
+				delete pointwiseProductRowSumVector;
+
+				if (this->getModel().hasStateRewards()) {
+					// If a state-based reward model is also available, we need to add this vector
+					// as well. 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.
+					std::vector<Type> subStateRewards(maybeStatesSetBitCount);
+					storm::utility::selectVectorValues(&subStateRewards, maybeStates, *this->getModel().getStateRewardVector());
+					gmm::add(subStateRewards, b);
+				}
+			} else {
+				// If only a state-based reward model is  available, we take this vector as the
+				// 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::selectVectorValues(&b, maybeStates, *this->getModel().getStateRewardVector());
+			}
+
+			this->solveEquationSystem(*submatrix, x, b);
+
+			// Set values of resulting vector according to result.
+			storm::utility::setVectorValues<Type>(result, maybeStates, x);
+
+			// Delete temporary matrix and right-hand side.
+			delete submatrix;
+		}
+
+		// Set values of resulting vector that are known exactly.
+		storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero<Type>());
+		storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
+
+		// Delete temporary storages and return result.
+		delete targetStates;
+		return result;
+	}
 
 private:
-//	storm::models::Dtmc<Type>& model;
+	virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand = nullptr, uint_fast64_t repetitions = 1) const = 0;
+
+	virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type> const& b) const = 0;
 };
 
 } //namespace modelChecker

src/modelchecker/EigenDtmcPrctlModelChecker.h

@@ -38,183 +38,101 @@ namespace modelChecker {
 template <class Type>
 class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
 
-public:
-	explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) { }
-
-	virtual ~EigenDtmcPrctlModelChecker() { }
-
-	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula) const {
-		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
-		storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft());
-		storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
-
-		// Copy the matrix before we make any changes.
-		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
-
-		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
-		tmpMatrix.makeRowsAbsorbing((~*leftStates | *rightStates) | *rightStates);
-
-		// Transform the transition probability matrix to the eigen format to use its arithmetic.
-		Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(tmpMatrix);
-
-		// Create the vector with which to multiply.
-		uint_fast64_t stateCount = this->getModel().getNumberOfStates();
-
-		typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
-		typedef Eigen::Map<VectorType> MapType;
-
-		std::vector<Type>* result = new std::vector<Type>(stateCount);
-		
-		storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
-
-		Type *p = &((*result)[0]); // get the address storing the data for result
-		MapType vectorMap(p, result->size()); // vectorMap shares data 
-		
+typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
+typedef Eigen::Map<VectorType> MapType;
 
-		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
-		for (uint_fast64_t i = 0, bound = formula.getBound(); i < bound; ++i) {
-			vectorMap = (*eigenMatrix) * vectorMap;
-		}
-
-		// Delete intermediate results.
-		delete leftStates;
-		delete rightStates;
-		delete eigenMatrix;
-
-		return result;
+public:
+	explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) {
+		// Intentionally left empty.
 	}
 
-	virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula) const {
-		// First, we need to compute the states that satisfy the sub-formula of the next-formula.
-		storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
+	virtual ~EigenDtmcPrctlModelChecker() {
+		// Intentionally left empty.
+	}
 
+private:
+	virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>* summand, uint_fast64_t repetitions = 1) const {
 		// Transform the transition probability matrix to the eigen format to use its arithmetic.
-		Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(this->getModel().getTransitionProbabilityMatrix());
-
-		// Create the vector with which to multiply and initialize it correctly.
-		std::vector<Type> x(this->getModel().getNumberOfStates());
-
-		storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne<Type>());
-
-		// Delete not needed next states bit vector.
-		delete nextStates;
-
-		typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
-		typedef Eigen::Map<VectorType> MapType;
-
-		Type *px = &(x[0]); // get the address storing the data for x
-		MapType vectorX(px, x.size()); // vectorX shares data 
+		Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(matrix);
 
-		// Create resulting vector.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+		Type* p = &((**vector)[0]); // get the address storing the data for result
+		MapType vectorMap(p, (*vector)->size()); // vectorMap shares data
 
-		// Type *pr = &((*result)[0]); // get the address storing the data for result
-		MapType vectorResult(px, result->size()); // vectorResult shares data 
+		p = &((*summand)[0]);
+		MapType summandMap(p, summand->size());
 
-		// Perform the actual computation.
-		vectorResult = (*eigenMatrix) * vectorX;
+		// Now perform matrix-vector multiplication as long as we meet the bound.
+		std::vector<Type>* swap = nullptr;
+		std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
+		for (uint_fast64_t i = 0; i < repetitions; ++i) {
+			vectorMap = (*eigenMatrix) * (vectorMap);
 
-		// Delete temporary matrix and return result.
+			// If requested, add an offset to the current result vector.
+			if (summand != nullptr) {
+				vectorMap = vectorMap + summandMap;
+			}
+		}
 		delete eigenMatrix;
-		return result;
 	}
 
-	virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula) const {
-		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
-		storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft());
-		storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
-
-		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
-		// all states that have probability 0 and 1 of satisfying the until-formula.
-		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
-		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
-		storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
-
-		delete leftStates;
-		delete rightStates;
-
-		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
-		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
-		storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
-		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
-
-		// Create resulting vector and set values accordingly.
-		uint_fast64_t stateCount = this->getModel().getNumberOfStates();
-		std::vector<Type>* result = new std::vector<Type>(stateCount);
-
-		// Only try to solve system if there are states for which the probability is unknown.
-		if (maybeStates.getNumberOfSetBits() > 0) {
-			typedef Eigen::Matrix<Type, -1, 1, 0, -1, 1> VectorType;
-			typedef Eigen::Map<VectorType> MapType;
-
-			// Now we can eliminate the rows and columns from the original transition probability matrix.
-			storm::storage::SparseMatrix<double>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
-			// Converting the matrix to the form needed for the equation system. That is, we go from
-			// x = A*x + b to (I-A)x = b.
-			submatrix->convertToEquationSystem();
-
-			// Transform the submatric matrix to the eigen format to use its solvers
-			Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenSubMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix<Type>(submatrix);
-			delete submatrix;
-
-			// Initialize the x vector with 0.5 for each element. This is the initial guess for
-			// the iterative solvers. It should be safe as for all 'maybe' states we know that the
-			// probability is strictly larger than 0.
-			std::vector<Type> x(maybeStates.getNumberOfSetBits(), Type(0.5));
-
-			// Map for x
-			Type *px = &(x[0]); // get the address storing the data for x
-			MapType vectorX(px, x.size()); // vectorX shares data 
-
-
-			// 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<double> b(maybeStates.getNumberOfSetBits());
-
-			Type *pb = &(b[0]); // get the address storing the data for b
-			MapType vectorB(pb, b.size()); // vectorB shares data 
-
-			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &x);
-
-			Eigen::BiCGSTAB<Eigen::SparseMatrix<Type, 1, int_fast32_t>> solver;
-			solver.compute(*eigenSubMatrix);
-			if(solver.info()!= Eigen::ComputationInfo::Success) {
-				// decomposition failed
-				LOG4CPLUS_ERROR(logger, "Decomposition of Submatrix failed!");
-			}
-
-			// Now do the actual solving.
-			LOG4CPLUS_INFO(logger, "Starting iterative solver.");
-			
-			solver.setTolerance(0.000001);
-			
-			vectorX = solver.solveWithGuess(vectorB, vectorX);
-
-			if(solver.info() == Eigen::ComputationInfo::InvalidInput) {
-				// solving failed
-				LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput");
-			} else if(solver.info() == Eigen::ComputationInfo::NoConvergence) {
-				// NoConvergence
-				throw storm::exceptions::NoConvergenceException("Solving of Submatrix with Eigen failed", solver.iterations(), solver.maxIterations());
-			} else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) {
-				// NumericalIssue
-				LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue");
-			} else if(solver.info() == Eigen::ComputationInfo::Success) {
-				// solving Success
-				LOG4CPLUS_INFO(logger, "Solving of Submatrix succeeded: Success");
-			} 
-
-			// Set values of resulting vector according to result.
-			storm::utility::setVectorValues<Type>(result, maybeStates, x);
-
-			// Delete temporary matrix.
-			delete eigenSubMatrix;
+	/*!
+	 * Solves the linear equation system Ax=b with the given parameters.
+	 *
+	 * @param A The matrix A specifying the coefficients of the linear equations.
+	 * @param x The vector x for which to solve the equations. The initial value of the elements of
+	 * this vector are used as the initial guess and might thus influence performance and convergence.
+	 * @param b The vector b specifying the values on the right-hand-sides of the equations.
+	 * @return The solution of the system of linear equations in form of the elements of the vector
+	 * x.
+	 */
+	virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>** vector, std::vector<Type>& b) const {
+		// Get the settings object to customize linear solving.
+		storm::settings::Settings* s = storm::settings::instance();
+
+		// Transform the submatric matrix to the eigen format to use its solvers
+		Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix<Type>(matrix);
+
+		Eigen::BiCGSTAB<Eigen::SparseMatrix<Type, 1, int_fast32_t>> solver;
+		solver.compute(*eigenMatrix);
+		if(solver.info()!= Eigen::ComputationInfo::Success) {
+			// decomposition failed
+			LOG4CPLUS_ERROR(logger, "Decomposition of matrix failed!");
+		}
+		solver.setMaxIterations(s->get<unsigned>("maxiter"));
+		solver.setTolerance(s->get<double>("precision"));
+
+		std::cout << matrix.toString(nullptr) << std::endl;
+		std::cout << **vector << std::endl;
+		std::cout << b << std::endl;
+
+		std::cout << *eigenMatrix << std::endl;
+
+		// Map for x
+		Type *px = &((**vector)[0]); // get the address storing the data for x
+		MapType vectorX(px, (*vector)->size()); // vectorX shares data
+
+		Type *pb = &(b[0]); // get the address storing the data for b
+		MapType vectorB(pb, b.size()); // vectorB shares data
+
+		vectorX = solver.solveWithGuess(vectorB, vectorX);
+
+		std::cout << **vector << std::endl;
+
+		if(solver.info() == Eigen::ComputationInfo::InvalidInput) {
+			// solving failed
+			LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput");
+		} else if(solver.info() == Eigen::ComputationInfo::NoConvergence) {
+			// NoConvergence
+ 			throw storm::exceptions::NoConvergenceException() << "Failed to converge within " << solver.iterations() << " out of a maximum of " << solver.maxIterations() << " iterations.";
+		} else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) {
+			// NumericalIssue
+			LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue");
+		} else if(solver.info() == Eigen::ComputationInfo::Success) {
+			// solving Success
+			LOG4CPLUS_INFO(logger, "Solving of Submatrix succeeded: Success");
 		}
 
-		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
-
-		return result;
+		delete eigenMatrix;
 	}
 };
 

src/modelchecker/GmmxxDtmcPrctlModelChecker.h

@@ -12,7 +12,6 @@
 
 #include "src/models/Dtmc.h"
 #include "src/modelchecker/DtmcPrctlModelChecker.h"
-#include "src/utility/GraphAnalyzer.h"
 #include "src/utility/Vector.h"
 #include "src/utility/ConstTemplates.h"
 #include "src/utility/Settings.h"
@@ -36,300 +35,15 @@ namespace modelChecker {
  * A model checking engine that makes use of the gmm++ backend.
  */
 template <class Type>
-class GmmxxDtmcPrctlModelChecker
-	: public DtmcPrctlModelChecker<Type> {
+class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
 
 public:
-	explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc)
-		: DtmcPrctlModelChecker<Type>(dtmc) {
+	explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) {
 		// Intentionally left empty.
 	}
 
-	virtual ~GmmxxDtmcPrctlModelChecker() { }
+	virtual ~GmmxxDtmcPrctlModelChecker() {
 
-	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const {
-		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
-		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
-		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
-
-		// Copy the matrix before we make any changes.
-		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
-
-		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
-		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
-
-		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(tmpMatrix);
-
-		// Create the vector with which to multiply.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-		storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
-
-		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
-		std::vector<Type>* swap = nullptr;
-		std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
-		for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
-			gmm::mult(*gmmxxMatrix, *result, *tmpResult);
-			swap = tmpResult;
-			tmpResult = result;
-			result = swap;
-		}
-		delete tmpResult;
-
-		// Delete intermediate results and return result.
-		delete gmmxxMatrix;
-		delete leftStates;
-		delete rightStates;
-		return result;
-	}
-
-	virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const {
-		// First, we need to compute the states that satisfy the sub-formula of the next-formula.
-		storm::storage::BitVector* nextStates = formula.getChild().check(*this);
-
-		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
-
-		// Create the vector with which to multiply and initialize it correctly.
-		std::vector<Type> x(this->getModel().getNumberOfStates());
-		storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne<Type>());
-
-		// Delete obsolete sub-result.
-		delete nextStates;
-
-		// Create resulting vector.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-
-		// Perform the actual computation, namely matrix-vector multiplication.
-		gmm::mult(*gmmxxMatrix, x, *result);
-
-		// Delete temporary matrix and return result.
-		delete gmmxxMatrix;
-		return result;
-	}
-
-	virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const {
-		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
-		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
-		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
-
-		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
-		// all states that have probability 0 and 1 of satisfying the until-formula.
-		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
-		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
-		storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
-
-		// Delete sub-results that are obsolete now.
-		delete leftStates;
-		delete rightStates;
-
-		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
-		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
-		storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
-		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
-
-		// Create resulting vector.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-
-		// Only try to solve system if there are states for which the probability is unknown.
-		uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits();
-		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
-			// system. That is, we go from x = A*x + b to (I-A)x = b.
-			submatrix->convertToEquationSystem();
-
-			// Transform the submatrix to the gmm++ format to use its solvers.
-			gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix);
-			delete submatrix;
-
-			// Initialize the x vector with 0.5 for each element. This is the initial guess for
-			// the iterative solvers. It should be safe as for all 'maybe' states we know that the
-			// probability is strictly larger than 0.
-			std::vector<Type> x(mayBeStatesSetBitCount, Type(0.5));
-
-			// 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<Type> b(mayBeStatesSetBitCount);
-			this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1, &b);
-
-			// Solve the corresponding system of linear equations.
-			this->solveLinearEquationSystem(*gmmxxMatrix, x, b);
-
-			// Set values of resulting vector according to result.
-			storm::utility::setVectorValues<Type>(result, maybeStates, x);
-
-			// 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.
-		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
-
-		return result;
-	}
-
-	virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const {
-		// Only compute the result if the model has a state-based reward model.
-		if (!this->getModel().hasStateRewards()) {
-			LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
-			throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula.";
-		}
-
-		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
-
-		// Initialize result to state rewards of the model.
-		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
-
-		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
-		std::vector<Type>* swap = nullptr;
-		std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
-		for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
-			gmm::mult(*gmmxxMatrix, *result, *tmpResult);
-			swap = tmpResult;
-			tmpResult = result;
-			result = swap;
-		}
-
-		// Delete temporary variables and return result.
-		delete tmpResult;
-		delete gmmxxMatrix;
-		return result;
-	}
-
-	virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const {
-		// Only compute the result if the model has at least one reward model.
-		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
-			LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
-			throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
-		}
-
-		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
-
-		// Compute the reward vector to add in each step based on the available reward models.
-		std::vector<Type>* totalRewardVector = nullptr;
-		if (this->getModel().hasTransitionRewards()) {
-			totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
-			if (this->getModel().hasStateRewards()) {
-				gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector);
-			}
-		} else {
-			totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector());
-		}
-
-		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
-
-		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
-		std::vector<Type>* swap = nullptr;
-		std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
-		for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
-			gmm::mult(*gmmxxMatrix, *result, *tmpResult);
-			swap = tmpResult;
-			tmpResult = result;
-			result = swap;
-
-			// Add the reward vector to the result.
-			gmm::add(*totalRewardVector, *result);
-		}
-
-		// Delete temporary variables and return result.
-		delete tmpResult;
-		delete gmmxxMatrix;
-		delete totalRewardVector;
-		return result;
-	}
-
-	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const {
-		// Only compute the result if the model has at least one reward model.
-		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
-			LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
-			throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
-		}
-
-		// Determine the states for which the target predicate holds.
-		storm::storage::BitVector* targetStates = formula.getChild().check(*this);
-
-		// 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);
-		storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates);
-		infinityStates.complement();
-
-		// 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) {
-			// 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
-			// system. That is, we go from x = A*x + b to (I-A)x = b.
-			submatrix->convertToEquationSystem();
-
-			// Transform the submatrix to the gmm++ format to use its solvers.
-			gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix);
-			delete submatrix;
-
-			// Initialize the x vector with 1 for each element. This is the initial guess for
-			// the iterative solvers.
-			std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
-
-			// Prepare the right-hand side of the equation system.
-			std::vector<Type>* b = new std::vector<Type>(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
-				// 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);
-				delete pointwiseProductRowSumVector;
-
-				if (this->getModel().hasStateRewards()) {
-					// If a state-based reward model is also available, we need to add this vector
-					// as well. 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.
-					std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStatesSetBitCount);
-					storm::utility::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector());
-					gmm::add(*subStateRewards, *b);
-					delete subStateRewards;
-				}
-			} else {
-				// If only a state-based reward model is  available, we take this vector as the
-				// 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::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector());
-			}
-
-			// Solve the corresponding system of linear equations.
-			this->solveLinearEquationSystem(*gmmxxMatrix, x, *b);
-
-			// Set values of resulting vector according to result.
-			storm::utility::setVectorValues<Type>(result, maybeStates, x);
-
-			// Delete temporary matrix and right-hand side.
-			delete gmmxxMatrix;
-			delete b;
-		}
-
-		// Set values of resulting vector that are known exactly.
-		storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
-
-		// Delete temporary storages and return result.
-		delete targetStates;
-		return result;
 	}
 
 	/*!
@@ -337,7 +51,7 @@ public:
 	 * @return The name of this module.
 	 */
 	static std::string getModuleName() {
-		return "gmm++det";
+		return "gmm++";
 	}
 
 	/*!
@@ -381,6 +95,37 @@ public:
 	}
 
 private:
+
+	virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand, uint_fast64_t repetitions = 1) const {
+		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+
+		// Now perform matrix-vector multiplication as long as we meet the bound.
+		std::vector<Type>* swap = nullptr;
+		std::vector<Type>* currentVector = &vector;
+		std::vector<Type>* tmpVector = new std::vector<Type>(this->getModel().getNumberOfStates());
+		for (uint_fast64_t i = 0; i < repetitions; ++i) {
+			gmm::mult(*gmmxxMatrix, *currentVector, *tmpVector);
+			swap = tmpVector;
+			tmpVector = currentVector;
+			currentVector = swap;
+
+			// If requested, add an offset to the current result vector.
+			if (summand != nullptr) {
+				gmm::add(*summand, *currentVector);
+			}
+		}
+
+		if (repetitions % 2 == 1) {
+			std::swap(vector, *currentVector);
+			delete currentVector;
+		} else {
+			delete tmpVector;
+		}
+
+		delete gmmxxMatrix;
+	}
+
 	/*!
 	 * Solves the linear equation system Ax=b with the given parameters.
 	 *
@@ -391,10 +136,13 @@ private:
 	 * @return The solution of the system of linear equations in form of the elements of the vector
 	 * x.
 	 */
-	void solveLinearEquationSystem(gmm::csr_matrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const {
+	virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type> const& b) const {
 		// Get the settings object to customize linear solving.
 		storm::settings::Settings* s = storm::settings::instance();
 
+		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
+		gmm::csr_matrix<Type>* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+
 		// Prepare an iteration object that determines the accuracy, maximum number of iterations
 		// and the like.
 		gmm::iteration iter(s->get<double>("precision"), 0, s->get<unsigned>("maxiter"));
@@ -415,13 +163,13 @@ private:
 		if (s->getString("lemethod") == "bicgstab") {
 			LOG4CPLUS_INFO(logger, "Using BiCGStab method.");
 			if (precond == "ilu") {
-				gmm::bicgstab(A, x, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(A), iter);
+				gmm::bicgstab(*A, vector, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(*A), iter);
 			} else if (precond == "diagonal") {
-				gmm::bicgstab(A, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(A), iter);
+				gmm::bicgstab(*A, vector, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*A), iter);
 			} else if (precond == "ildlt") {
-				gmm::bicgstab(A, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(A), iter);
+				gmm::bicgstab(*A, vector, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*A), iter);
 			} else if (precond == "none") {
-				gmm::bicgstab(A, x, b, gmm::identity_matrix(), iter);
+				gmm::bicgstab(*A, vector, b, gmm::identity_matrix(), iter);
 			}
 
 			// Check if the solver converged and issue a warning otherwise.
@@ -430,28 +178,16 @@ private:
 			} else {
 				LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
 			}
-		// FIXME: gmres has been disabled, because it triggers gmm++ compilation errors
-		/* } else if (s->getString("lemethod").compare("gmres") == 0) {
-			LOG4CPLUS_INFO(logger, "Using GMRES method.");
-			if (precond.compare("ilu")) {
-				gmm::gmres(A, x, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(A), s->get<unsigned>("restart"), iter);
-			} else if (precond == "diagonal") {
-				gmm::gmres(A, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(A), s->get<unsigned>("restart"), iter);
-			} else if (precond == "ildlt") {
-				gmm::gmres(A, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(A), s->get<unsigned>("restart"), iter);
-			} else if (precond == "none") {
-				gmm::gmres(A, x, b, gmm::identity_matrix(), s->get<unsigned>("restart"), iter);
-			} */
 		} else if (s->getString("lemethod") == "qmr") {
 			LOG4CPLUS_INFO(logger, "Using QMR method.");
 			if (precond == "ilu") {
-				gmm::qmr(A, x, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(A), iter);
+				gmm::qmr(*A, vector, b, gmm::ilu_precond<gmm::csr_matrix<Type>>(*A), iter);
 			} else if (precond == "diagonal") {
-				gmm::qmr(A, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(A), iter);
+				gmm::qmr(*A, vector, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*A), iter);
 			} else if (precond == "ildlt") {
-				gmm::qmr(A, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(A), iter);
+				gmm::qmr(*A, vector, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*A), iter);
 			} else if (precond == "none") {
-				gmm::qmr(A, x, b, gmm::identity_matrix(), iter);
+				gmm::qmr(*A, vector, b, gmm::identity_matrix(), iter);
 			}
 
 			// Check if the solver converged and issue a warning otherwise.
@@ -462,8 +198,10 @@ private:
 			}
 		} else if (s->getString("lemethod") == "jacobi") {
 			LOG4CPLUS_INFO(logger, "Using Jacobi method.");
-			solveLinearEquationSystemWithJacobi(A, x, b);
+			solveLinearEquationSystemWithJacobi(*A, vector, b);
 		}
+
+		delete A;
 	}
 
 	/*!

src/modelchecker/GmmxxMdpPrctlModelChecker.h

@@ -43,339 +43,33 @@ public:
 
 	virtual ~GmmxxMdpPrctlModelChecker() { }
 
-	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const {
-		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
-		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
-		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
-
-		// Copy the matrix before we make any changes.
-		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
-
+private:
+	virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand = nullptr, uint_fast64_t repetitions = 1) const {
 		// Get the starting row indices for the non-deterministic choices to reduce the resulting
 		// vector properly.
 		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, *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);
-
-		// Create the vector with which to multiply.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-		storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
 
 		// 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(), 0);
+		std::vector<Type> multiplyResult(matrix.getRowCount());
 
 		// 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);
+		for (uint_fast64_t i = 0; i < repetitions; ++i) {
+			gmm::mult(*gmmxxMatrix, vector, multiplyResult);
 			if (this->minimumOperatorStack.top()) {
-				storm::utility::reduceVectorMin(*multiplyResult, result, *nondeterministicChoiceIndices);
+				storm::utility::reduceVectorMin(multiplyResult, &vector, *nondeterministicChoiceIndices);
 			} else {
-				storm::utility::reduceVectorMax(*multiplyResult, result, *nondeterministicChoiceIndices);
+				storm::utility::reduceVectorMax(multiplyResult, &vector, *nondeterministicChoiceIndices);
 			}
 		}
-		delete multiplyResult;
 
 		// Delete intermediate results and return result.
 		delete gmmxxMatrix;
-		delete leftStates;
-		delete rightStates;
-		return result;
-	}
-
-	virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const {
-		// First, we need to compute the states that satisfy the sub-formula of the next-formula.
-		storm::storage::BitVector* nextStates = formula.getChild().check(*this);
-
-		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
-
-		// Create the vector with which to multiply and initialize it correctly.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-		storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne<Type>());
-
-		// Delete obsolete sub-result.
-		delete nextStates;
-
-		// Create resulting vector.
-		std::vector<Type>* temporaryResult = new std::vector<Type>(this->getModel().getTransitionMatrix()->getRowCount());
-
-		// Perform the actual computation, namely matrix-vector multiplication.
-		gmm::mult(*gmmxxMatrix, *result, *temporaryResult);
-
-		// Get the starting row indices for the non-deterministic choices to reduce the resulting
-		// vector properly.
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
-
-		if (this->minimumOperatorStack.top()) {
-			storm::utility::reduceVectorMin(*temporaryResult, result, *nondeterministicChoiceIndices);
-		} else {
-			storm::utility::reduceVectorMax(*temporaryResult, result, *nondeterministicChoiceIndices);
-		}
-
-		// Delete temporary matrix plus temporary result and return result.
-		delete gmmxxMatrix;
-		delete temporaryResult;
-		return result;
-	}
-
-	virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const {
-		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
-		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
-		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
-
-		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
-		// all states that have probability 0 and 1 of satisfying the until-formula.
-		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
-		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
-		if (this->minimumOperatorStack.top()) {
-			storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
-		} else {
-			storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
-		}
-
-		// Delete sub-results that are obsolete now.
-		delete leftStates;
-		delete rightStates;
-
-		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
-		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
-		storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
-		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
-
-		// Create resulting vector.
-		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
-
-		// Only try to solve system if there are states for which the probability is unknown.
-		uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
-		if (maybeStatesSetBitCount > 0) {
-			// First, we can eliminate the rows and columns from the original transition probability matrix for states
-			// whose probabilities are already known.
-			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
-
-			// Get the "new" nondeterministic choice indices for the submatrix.
-			std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
-
-			// Transform the submatrix to the gmm++ format to use its capabilities.
-			gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix);
-
-			// Create vector for results for maybe states.
-			std::vector<Type>* x = new std::vector<Type>(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<Type> b(submatrix->getRowCount());
-			this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, &b);
-			delete submatrix;
-
-			// Solve the corresponding system of equations.
-			this->solveEquationSystem(*gmmxxMatrix, x, b, *subNondeterministicChoiceIndices);
-
-			// Set values of resulting vector according to result.
-			storm::utility::setVectorValues<Type>(result, maybeStates, *x);
-
-			// Delete temporary matrix and vector.
-			delete gmmxxMatrix;
-			delete x;
-		}
-
-		// Set values of resulting vector that are known exactly.
-		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
-
-		return result;
-	}
-
-	virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const {
-		// Only compute the result if the model has a state-based reward model.
-		if (!this->getModel().hasStateRewards()) {
-			LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
-			throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula.";
-		}
-
-		// Get the starting row indices for the non-deterministic choices to reduce the resulting
-		// vector properly.
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
-
-		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
-
-		// Initialize result to state rewards of the model.
-		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
-
-		// 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(), 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 {
-				storm::utility::reduceVectorMax(*multiplyResult, result, *nondeterministicChoiceIndices);
-			}
-		}
-		delete multiplyResult;
-
-		// Delete temporary variables and return result.
-		delete gmmxxMatrix;
-		return result;
-	}
-
-	virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const {
-		// Only compute the result if the model has at least one reward model.
-		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
-			LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
-			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<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
-
-		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
-
-		// Compute the reward vector to add in each step based on the available reward models.
-		std::vector<Type>* totalRewardVector = nullptr;
-		if (this->getModel().hasTransitionRewards()) {
-			totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
-			if (this->getModel().hasStateRewards()) {
-				gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector);
-			}
-		} else {
-			totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector());
-		}
-
-		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
-
-		// 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(), 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 {
-				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 gmmxxMatrix;
-		delete totalRewardVector;
-		return result;
 	}
 
-	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const {
-		// Only compute the result if the model has at least one reward model.
-		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
-			LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
-			throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
-		}
-
-		// Determine the states for which the target predicate holds.
-		storm::storage::BitVector* targetStates = formula.getChild().check(*this);
-
-		// 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);
-		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();
-
-		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());
-
-		// Get the starting row indices for the non-deterministic choices to reduce the resulting
-		// vector properly.
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
-
-		// Check whether there are states for which we have to compute the result.
-		const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
-		if (maybeStatesSetBitCount > 0) {
-			// First, we can eliminate the rows and columns from the original transition probability matrix for states
-			// whose probabilities are already known.
-			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
-
-			// Get the "new" nondeterministic choice indices for the submatrix.
-			std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
-
-			// Transform the submatrix to the gmm++ format to use its capabilities.
-			gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix);
-
-			// Create vector for results for maybe states.
-			std::vector<Type>* x = new std::vector<Type>(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<Type> b(submatrix->getRowCount());
-			delete submatrix;
-
-			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
-				// 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, *nondeterministicChoiceIndices, *pointwiseProductRowSumVector);
-				delete pointwiseProductRowSumVector;
-
-				if (this->getModel().hasStateRewards()) {
-					// If a state-based reward model is also available, we need to add this vector
-					// as well. 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.
-					std::vector<Type>* subStateRewards = new std::vector<Type>(b.size());
-					storm::utility::selectVectorValuesRepeatedly(subStateRewards, maybeStates, *nondeterministicChoiceIndices, *this->getModel().getStateRewardVector());
-					gmm::add(*subStateRewards, b);
-					delete subStateRewards;
-				}
-			} else {
-				// If only a state-based reward model is  available, we take this vector as the
-				// 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::selectVectorValuesRepeatedly(&b, maybeStates, *nondeterministicChoiceIndices, *this->getModel().getStateRewardVector());
-			}
-
-			// Solve the corresponding system of equations.
-			this->solveEquationSystem(*gmmxxMatrix, x, b, *subNondeterministicChoiceIndices);
-
-			// 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.
-		storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
-
-		// Delete temporary storages and return result.
-		delete targetStates;
-		return result;
-	}
-
-private:
 	/*!
 	 * Solves the given equation system under the given parameters using the power method.
 	 *
@@ -386,7 +80,7 @@ private:
 	 * @return The solution of the system of linear equations in form of the elements of the vector
 	 * x.
 	 */
-	void solveEquationSystem(gmm::csr_matrix<Type> const& A, std::vector<Type>* x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const {
+	void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const {
 		// Get the settings object to customize solving.
 		storm::settings::Settings* s = storm::settings::instance();
 
@@ -395,43 +89,48 @@ private:
 		unsigned maxIterations = s->get<unsigned>("maxiter");
 		bool relative = s->get<bool>("relative");
 
+		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(matrix);
+
 		// Set up the environment for the power method.
-		std::vector<Type>* temporaryResult = new std::vector<Type>(b.size());
-		std::vector<Type>* newX = new std::vector<Type>(x->size());
+		std::vector<Type> multiplyResult(matrix.getRowCount());
+		std::vector<Type>* currentX = &x;
+		std::vector<Type>* newX = new std::vector<Type>(x.size());
 		std::vector<Type>* swap = nullptr;
-		bool converged = false;
 		uint_fast64_t iterations = 0;
+		bool converged = false;
 
 		// Proceed with the iterations as long as the method did not converge or reach the
 		// user-specified maximum number of iterations.
 		while (!converged && iterations < maxIterations) {
 			// Compute x' = A*x + b.
-			gmm::mult(A, *x, *temporaryResult);
-			gmm::add(b, *temporaryResult);
+			gmm::mult(*gmmxxMatrix, *currentX, multiplyResult);
+			gmm::add(b, multiplyResult);
 
 			// Reduce the vector x' by applying min/max for all non-deterministic choices.
 			if (this->minimumOperatorStack.top()) {
-				storm::utility::reduceVectorMin(*temporaryResult, newX, nondeterministicChoiceIndices);
+				storm::utility::reduceVectorMin(multiplyResult, newX, nondeterministicChoiceIndices);
 			} else {
-				storm::utility::reduceVectorMax(*temporaryResult, newX, nondeterministicChoiceIndices);
+				storm::utility::reduceVectorMax(multiplyResult, newX, nondeterministicChoiceIndices);
 			}
 
 			// Determine whether the method converged.
-			converged = storm::utility::equalModuloPrecision(*x, *newX, precision, relative);
+			converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative);
 
 			// Update environment variables.
-			swap = x;
-			x = newX;
+			swap = currentX;
+			currentX = newX;
 			newX = swap;
 			++iterations;
 		}
 
 		if (iterations % 2 == 1) {
-			delete x;
+			std::swap(x, *currentX);
+			delete currentX;
 		} else {
 			delete newX;
 		}
-		delete temporaryResult;
+		delete gmmxxMatrix;
 
 		// Check if the solver converged and issue a warning otherwise.
 		if (converged) {
@@ -440,22 +139,6 @@ private:
 			LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
 		}
 	}
-
-	std::shared_ptr<std::vector<uint_fast64_t>> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector constraint) const {
-		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
-		std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices(new std::vector<uint_fast64_t>(constraint.getNumberOfSetBits() + 1));
-		uint_fast64_t currentRowCount = 0;
-		uint_fast64_t currentIndexCount = 1;
-		(*subNondeterministicChoiceIndices)[0] = 0;
-		for (auto index : constraint) {
-			(*subNondeterministicChoiceIndices)[currentIndexCount] = currentRowCount + (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index];
-			currentRowCount += (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index];
-			++currentIndexCount;
-		}
-		(*subNondeterministicChoiceIndices)[constraint.getNumberOfSetBits()] = currentRowCount;
-
-		return subNondeterministicChoiceIndices;
-	}
 };
 
 } //namespace modelChecker

src/modelchecker/MdpPrctlModelChecker.h

@@ -189,7 +189,28 @@ public:
 	 * @param formula The Bounded Until path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const {
+		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
+		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
+		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
+
+		// Copy the matrix before we make any changes.
+		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
+
+		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
+		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *this->getModel().getNondeterministicChoiceIndices());
+
+		// Create the vector with which to multiply.
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+		storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
+
+		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound());
+
+		// Delete intermediate results and return result.
+		delete leftStates;
+		delete rightStates;
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with a Next operator node as root in its formula tree
@@ -197,7 +218,22 @@ public:
 	 * @param formula The Next path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const {
+		// First, we need to compute the states that satisfy the sub-formula of the next-formula.
+		storm::storage::BitVector* nextStates = formula.getChild().check(*this);
+
+		// Create the vector with which to multiply and initialize it correctly.
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+		storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne<Type>());
+
+		// Delete obsolete sub-result.
+		delete nextStates;
+
+		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result);
+
+		// Return result.
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with a Bounded Eventually operator node as root in its
@@ -246,7 +282,67 @@ public:
 	 * @param formula The Until path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const {
+		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
+		storm::storage::BitVector* leftStates = formula.getLeft().check(*this);
+		storm::storage::BitVector* rightStates = formula.getRight().check(*this);
+
+		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
+		// all states that have probability 0 and 1 of satisfying the until-formula.
+		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
+		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
+		if (this->minimumOperatorStack.top()) {
+			storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
+		} else {
+			storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
+		}
+
+		// Delete sub-results that are obsolete now.
+		delete leftStates;
+		delete rightStates;
+
+		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
+		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
+		storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
+		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+
+		// Create resulting vector.
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+
+		// Only try to solve system if there are states for which the probability is unknown.
+		uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
+		if (maybeStatesSetBitCount > 0) {
+			// First, we can eliminate the rows and columns from the original transition probability matrix for states
+			// whose probabilities are already known.
+			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
+
+			// Get the "new" nondeterministic choice indices for the submatrix.
+			std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
+
+			// Create vector for results for maybe states.
+			std::vector<Type> x(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<Type> b(submatrix->getRowCount());
+			this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, &b);
+
+			// Solve the corresponding system of equations.
+			this->solveEquationSystem(*submatrix, x, b, *subNondeterministicChoiceIndices);
+
+			// Set values of resulting vector according to result.
+			storm::utility::setVectorValues<Type>(result, maybeStates, x);
+
+			// Delete temporary matrix.
+			delete submatrix;
+		}
+
+		// Set values of resulting vector that are known exactly.
+		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
+
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with an Instantaneous Reward operator node as root in its
@@ -255,7 +351,21 @@ public:
 	 * @param formula The Instantaneous Reward formula to check
 	 * @returns for each state the reward that the instantaneous reward yields
 	 */
-	virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const {
+		// Only compute the result if the model has a state-based reward model.
+		if (!this->getModel().hasStateRewards()) {
+			LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
+			throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula.";
+		}
+
+		// Initialize result to state rewards of the model.
+		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+
+		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound());
+
+		// Return result.
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with a Cumulative Reward operator node as root in its
@@ -264,7 +374,32 @@ public:
 	 * @param formula The Cumulative Reward formula to check
 	 * @returns for each state the reward that the cumulative reward yields
 	 */
-	virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const {
+		// Only compute the result if the model has at least one reward model.
+		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
+			LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
+			throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
+		}
+
+		// Compute the reward vector to add in each step based on the available reward models.
+		std::vector<Type>* totalRewardVector = nullptr;
+		if (this->getModel().hasTransitionRewards()) {
+			totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
+			if (this->getModel().hasStateRewards()) {
+				gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector);
+			}
+		} else {
+			totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector());
+		}
+
+		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
+
+		this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound());
+
+		// Delete temporary variables and return result.
+		delete totalRewardVector;
+		return result;
+	}
 
 	/*!
 	 * The check method for a path formula with a Reachability Reward operator node as root in its
@@ -273,10 +408,118 @@ public:
 	 * @param formula The Reachbility Reward formula to check
 	 * @returns for each state the reward that the reachability reward yields
 	 */
-	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const = 0;
+	virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const {
+		// Only compute the result if the model has at least one reward model.
+		if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
+			LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula");
+			throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
+		}
+
+		// Determine the states for which the target predicate holds.
+		storm::storage::BitVector* targetStates = formula.getChild().check(*this);
+
+		// 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);
+		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();
+
+		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.
+		const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
+		if (maybeStatesSetBitCount > 0) {
+			// First, we can eliminate the rows and columns from the original transition probability matrix for states
+			// whose probabilities are already known.
+			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices());
+
+			// Get the "new" nondeterministic choice indices for the submatrix.
+			std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
+
+			// Create vector for results for maybe states.
+			std::vector<Type> x(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<Type> b(submatrix->getRowCount());
+
+			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
+				// 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, *this->getModel().getNondeterministicChoiceIndices(), *pointwiseProductRowSumVector);
+				delete pointwiseProductRowSumVector;
+
+				if (this->getModel().hasStateRewards()) {
+					// If a state-based reward model is also available, we need to add this vector
+					// as well. 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.
+					std::vector<Type>* subStateRewards = new std::vector<Type>(b.size());
+					storm::utility::selectVectorValuesRepeatedly(subStateRewards, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector());
+					gmm::add(*subStateRewards, b);
+					delete subStateRewards;
+				}
+			} else {
+				// If only a state-based reward model is  available, we take this vector as the
+				// 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::selectVectorValuesRepeatedly(&b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector());
+			}
+
+			// Solve the corresponding system of equations.
+			this->solveEquationSystem(*submatrix, x, b, *subNondeterministicChoiceIndices);
+
+			// Set values of resulting vector according to result.
+			storm::utility::setVectorValues<Type>(result, maybeStates, x);
+			delete submatrix;
+		}
+
+		// Set values of resulting vector that are known exactly.
+		storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero<Type>());
+		storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>());
+
+		// Delete temporary storages and return result.
+		delete targetStates;
+		return result;
+	}
 
 protected:
 	mutable std::stack<bool> minimumOperatorStack;
+
+private:
+	virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand = nullptr, uint_fast64_t repetitions = 1) const = 0;
+
+	virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const = 0;
+
+
+	std::shared_ptr<std::vector<uint_fast64_t>> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector constraint) const {
+		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
+		std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices(new std::vector<uint_fast64_t>(constraint.getNumberOfSetBits() + 1));
+		uint_fast64_t currentRowCount = 0;
+		uint_fast64_t currentIndexCount = 1;
+		(*subNondeterministicChoiceIndices)[0] = 0;
+		for (auto index : constraint) {
+			(*subNondeterministicChoiceIndices)[currentIndexCount] = currentRowCount + (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index];
+			currentRowCount += (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index];
+			++currentIndexCount;
+		}
+		(*subNondeterministicChoiceIndices)[constraint.getNumberOfSetBits()] = currentRowCount;
+
+		return subNondeterministicChoiceIndices;
+	}
 };
 
 } //namespace modelChecker

src/models/Dtmc.h

@@ -50,11 +50,10 @@ public:
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
 		}
 		if (this->getTransitionRewardMatrix() != nullptr) {
-			// FIXME: This is temporarily commented out, because the checking routine does not work properly.
-			//if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) {
-			//	LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
-			//	throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
-			//}
+			if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) {
+				LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
+				throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
+			}
 		}
 	}
 

src/parser/DeterministicModelParser.cpp

@@ -45,7 +45,9 @@ DeterministicModelParser::DeterministicModelParser(std::string const & transitio
 		this->stateRewards = srp.getStateRewards();
 	}
 	if (transitionRewardFile != "") {
-		storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, true);
+		RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(stateCount, stateCount, nullptr);
+		storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, rewardMatrixInfo);
+		delete rewardMatrixInfo;
 		this->transitionRewards = trp.getMatrix();
 	}
 	this->dtmc = nullptr;

src/parser/DeterministicSparseTransitionParser.cpp

@@ -44,12 +44,14 @@ namespace parser {
  *	@param buf Data to scan. Is expected to be some char array.
  *	@param maxnode Is set to highest id of all nodes.
  */
-uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode, bool rewardFile) {
+uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
+	bool isRewardMatrix = rewardMatrixInformation != nullptr;
+
 	uint_fast64_t nonZeroEntryCount = 0;
 	/*
 	 *	Check file header and extract number of transitions.
 	 */
-	if (!rewardFile) {
+	if (!isRewardMatrix) {
 		buf = strchr(buf, '\n') + 1;  // skip format hint
 	}
 
@@ -68,7 +70,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
             row = checked_strtol(buf, &buf);
             col = checked_strtol(buf, &buf);
 
-            if (!rewardFile) {
+            if (!isRewardMatrix) {
 				if (lastRow != row) {
 					if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
 						++nonZeroEntryCount;
@@ -109,7 +111,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
             buf = trimWhitespaces(buf);
     }
 
-    if (!rowHadDiagonalEntry && !rewardFile) {
+    if (!rowHadDiagonalEntry && !isRewardMatrix) {
     	++nonZeroEntryCount;
     }
 
@@ -126,13 +128,15 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
  *	@return a pointer to the created sparse matrix.
  */
 
-DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, bool rewardFile)
+DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation)
 	: matrix(nullptr) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
 	 */
 	setlocale(LC_NUMERIC, "C");
 
+	bool isRewardMatrix = rewardMatrixInformation != nullptr;
+
 	/*
 	 *	Open file.
 	 */
@@ -143,7 +147,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	 *	Perform first pass, i.e. count entries that are not zero.
 	 */
 	int_fast64_t maxStateId;
-	uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardFile);
+	uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardMatrixInformation);
 
 	LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros.");
 
@@ -164,10 +168,21 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	/*
 	 *	Read file header, extract number of states.
 	 */
-	if (!rewardFile) {
+	if (!isRewardMatrix) {
 		buf = strchr(buf, '\n') + 1;  // skip format hint
 	}
 
+	// If the matrix that is being parsed is a reward matrix, it should match the size of the
+	// transition matrix.
+	if (isRewardMatrix) {
+		if (maxStateId + 1 > rewardMatrixInformation->rowCount || maxStateId + 1 > rewardMatrixInformation->columnCount) {
+			LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix.");
+			throw storm::exceptions::WrongFileFormatException() << "Reward matrix has more rows or columns than transition matrix.";
+		} else {
+			maxStateId = rewardMatrixInformation->rowCount - 1;
+		}
+	}
+
 	/*
 	 *	Creating matrix here.
 	 *	The number of non-zero elements is computed by firstPass().
@@ -201,10 +216,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 
 		if (lastRow != row) {
 			if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
-				if (insertDiagonalEntriesIfMissing) {
+				if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
 					this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
 					LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
-				} else if (!rewardFile) {
+				} else if (!isRewardMatrix) {
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
 				}
 				// No increment for lastRow
@@ -212,11 +227,11 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 			}
 			for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
 				hadDeadlocks = true;
-				if (fixDeadlocks && !rewardFile) {
+				if (fixDeadlocks && !isRewardMatrix) {
 					this->matrix->addNextValue(skippedRow, skippedRow, storm::utility::constGetOne<double>());
 					rowHadDiagonalEntry = true;
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
-				} else if (!rewardFile) {
+				} else if (!isRewardMatrix) {
 					LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
 					// FIXME Why no exception at this point? This will break the App.
 				}
@@ -229,10 +244,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 			rowHadDiagonalEntry = true;
 		} else if (col > row && !rowHadDiagonalEntry) {
 			rowHadDiagonalEntry = true;
-			if (insertDiagonalEntriesIfMissing && !rewardFile) {
+			if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
 				this->matrix->addNextValue(row, row, storm::utility::constGetZero<double>());
 				LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
-			} else if (!rewardFile) {
+			} else if (!isRewardMatrix) {
 				LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
 			}
 		}
@@ -242,15 +257,15 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	}
 
 	if (!rowHadDiagonalEntry) {
-		if (insertDiagonalEntriesIfMissing && !rewardFile) {
+		if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
 			this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
 			LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
-		} else if (!rewardFile) {
+		} else if (!isRewardMatrix) {
 			LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
 		}
 	}
 
-	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
+	if (!fixDeadlocks && hadDeadlocks && !isRewardMatrix) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
 
 	/*
 	 *	Finalize Matrix.

src/parser/DeterministicSparseTransitionParser.h

@@ -17,7 +17,7 @@ namespace parser {
  */
 class DeterministicSparseTransitionParser : public Parser {
 	public:
-		DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, bool rewardFile = false);
+		DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
 		
 		std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
 			return this->matrix;
@@ -26,7 +26,7 @@ class DeterministicSparseTransitionParser : public Parser {
 	private:
 		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
 		
-		uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode, bool rewardFile);
+		uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
 	
 };
 		

src/parser/NondeterministicModelParser.cpp

@@ -38,7 +38,9 @@ NondeterministicModelParser::NondeterministicModelParser(std::string const & tra
 		this->stateRewards = srp.getStateRewards();
 	}
 	if (transitionRewardFile != "") {
-		storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, true, tp.getRowMapping());
+		RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(tp.getMatrix()->getRowCount(), tp.getMatrix()->getColumnCount(), tp.getRowMapping());
+		storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, rewardMatrixInfo);
+		delete rewardMatrixInfo;
 		this->transitionRewardMatrix = trp.getMatrix();
 	}
 

src/parser/NondeterministicSparseTransitionParser.cpp

@@ -49,11 +49,13 @@ namespace parser {
  *	@param maxnode Is set to highest id of all nodes.
  *	@return The number of non-zero elements.
  */
-uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices) {
+uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
+	bool isRewardFile = rewardMatrixInformation != nullptr;
+
 	/*
 	 *	Check file header and extract number of transitions.
 	 */
-	if (!rewardFile) {
+	if (!isRewardFile) {
 		buf = strchr(buf, '\n') + 1;  // skip format hint
 	}
 
@@ -80,17 +82,17 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
 			maxnode = source;
 		}
 
-		if (rewardFile) {
+		if (isRewardFile) {
 			// If we have switched the source state, we possibly need to insert the rows of the last
 			// last source state.
 			if (source != lastsource && lastsource != -1) {
-				choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
+				choices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
 			}
 
 			// If we skipped some states, we need to reserve empty rows for all their nondeterministic
 			// choices.
 			for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
-				choices += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
+				choices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
 			}
 
 			// If we advanced to the next state, but skipped some choices, we have to reserve rows
@@ -151,14 +153,14 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
 		buf = trimWhitespaces(buf);
 	}
 
-	if (rewardFile) {
+	if (isRewardFile) {
 		// If not all rows were filled for the last state, we need to insert them.
-		choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
+		choices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
 
 		// If we skipped some states, we need to reserve empty rows for all their nondeterministic
 		// choices.
-		for (uint_fast64_t i = lastsource + 1; i < nondeterministicChoiceIndices->size() - 1; ++i) {
-			choices += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
+		for (uint_fast64_t i = lastsource + 1; i < rewardMatrixInformation->nondeterministicChoiceIndices->size() - 1; ++i) {
+			choices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
 		}
 	}
 
@@ -175,13 +177,15 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
  *	@return a pointer to the created sparse matrix.
  */
 
-NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices)
+NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation)
 	: matrix(nullptr) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
 	 */
 	setlocale(LC_NUMERIC, "C");
 
+	bool isRewardFile = rewardMatrixInformation != nullptr;
+
 	/*
 	 *	Open file.
 	 */
@@ -193,7 +197,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	 */
 	int_fast64_t maxnode;
 	uint_fast64_t choices;
-	uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardFile, nondeterministicChoiceIndices);
+	uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardMatrixInformation);
 
 	/*
 	 *	If first pass returned zero, the file format was wrong.
@@ -212,10 +216,22 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	/*
 	 *	Skip file header.
 	 */
-	if (!rewardFile) {
+	if (!isRewardFile) {
 		buf = strchr(buf, '\n') + 1;  // skip format hint
 	}
 
+	if (isRewardFile) {
+		if (choices > rewardMatrixInformation->rowCount || maxnode + 1 > rewardMatrixInformation->columnCount) {
+			LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size.");
+			throw storm::exceptions::WrongFileFormatException() << "Reward matrix size exceeds transition matrix size.";
+		} else if (choices != rewardMatrixInformation->rowCount) {
+			LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count.");
+			throw storm::exceptions::WrongFileFormatException() << "Reward matrix row count does not match transition matrix row count.";
+		} else {
+			maxnode = rewardMatrixInformation->columnCount - 1;
+		}
+	}
+
 	/*
 	 *	Create and initialize matrix.
 	 *	The matrix should have as many columns as we have nodes and as many rows as we have choices.
@@ -253,17 +269,17 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 		source = checked_strtol(buf, &buf);
 		choice = checked_strtol(buf, &buf);
 
-		if (rewardFile) {
+		if (isRewardFile) {
 			// If we have switched the source state, we possibly need to insert the rows of the last
 			// last source state.
 			if (source != lastsource && lastsource != -1) {
-				curRow += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
+				curRow += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
 			}
 
 			// If we skipped some states, we need to reserve empty rows for all their nondeterministic
 			// choices.
 			for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
-				curRow += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
+				curRow += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
 			}
 
 			// If we advanced to the next state, but skipped some choices, we have to reserve rows
@@ -286,12 +302,12 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 			 */
 			for (int_fast64_t node = lastsource + 1; node < source; node++) {
 				hadDeadlocks = true;
-				if (!rewardFile && fixDeadlocks) {
+				if (fixDeadlocks) {
 					this->rowMapping->at(node) = curRow;
 					this->matrix->addNextValue(curRow, node, 1);
 					++curRow;
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
-				} else if (!rewardFile) {
+				} else {
 					LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
 				}
 			}
@@ -323,7 +339,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 
 	this->rowMapping->at(maxnode+1) = curRow + 1;
 
-	if (!fixDeadlocks && hadDeadlocks && !rewardFile) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
+	if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
 
 	/*
 	 * Finalize matrix.

src/parser/NondeterministicSparseTransitionParser.h

@@ -19,7 +19,7 @@ namespace parser {
  */
 class NondeterministicSparseTransitionParser : public Parser {
 	public:
-		NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile = false, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices = nullptr);
+		NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
 		
 		inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
 			return this->matrix;
@@ -33,7 +33,7 @@ class NondeterministicSparseTransitionParser : public Parser {
 		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
 		std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
 		
-		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices);
+		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
 	
 };
 		

src/parser/Parser.h

@@ -14,6 +14,8 @@
 #include <fcntl.h>
 #include <errno.h>
 #include <iostream>
+#include <memory>
+#include <vector>
 
 #include <boost/integer/integer_mask.hpp>
 #include "src/exceptions/FileIoException.h"
@@ -30,6 +32,21 @@ namespace storm {
  */
 namespace parser {
 	
+	struct RewardMatrixInformationStruct {
+		RewardMatrixInformationStruct() : rowCount(0), columnCount(0), nondeterministicChoiceIndices(nullptr) {
+			// Intentionally left empty.
+		}
+
+		RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices)
+		: rowCount(rowCount), columnCount(columnCount), nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
+			// Intentionally left empty.
+		}
+
+		uint_fast64_t rowCount;
+		uint_fast64_t columnCount;
+		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;
+	};
+
 	/*!
 	 *	@brief Opens a file and maps it to memory providing a char*
 	 *	containing the file content.

src/storage/BitVector.h

@@ -392,6 +392,40 @@ public:
 		return result;
 	}
 
+	/*!
+	 * Checks whether all bits that are set in the current bit vector are also set in the given bit
+	 * vector.
+	 * @param bv A reference to the bit vector whose bits are (possibly) a superset of the bits of
+	 * the current bit vector.
+	 * @returns True iff all bits that are set in the current bit vector are also set in the given bit
+	 * vector.
+	 */
+	bool isContainedIn(BitVector const& bv) const {
+		for (uint_fast64_t i = 0; i < this->bucketCount; ++i) {
+			if ((this->bucketArray[i] & bv.bucketArray[i]) != bv.bucketArray[i]) {
+				return false;
+			}
+		}
+		return true;
+	}
+
+	/*!
+	 * Checks whether none of the bits that are set in the current bit vector are also set in the
+	 * given bit vector.
+	 * @param bv A reference to the bit vector whose bits are (possibly) disjoint from the bits in
+	 * the current bit vector.
+	 * @returns True iff none of the bits that are set in the current bit vector are also set in the
+	 * given bit vector.
+	 */
+	bool isDisjointFrom(BitVector const& bv) const {
+		for (uint_fast64_t i = 0; i < this->bucketCount; ++i) {
+			if ((this->bucketArray[i] & bv.bucketArray[i]) != 0) {
+				return false;
+			}
+		}
+		return true;
+	}
+
 	/*!
 	 * Adds all indices of bits set to one to the provided list.
 	 * @param list The list to which to append the indices.

src/storage/SparseMatrix.h

@@ -865,16 +865,28 @@ public:
 	 *	@param matrix Matrix to check against.
 	 *	@return True iff this is a submatrix of matrix.
 	 */
-	bool isSubmatrixOf(SparseMatrix<T> const & matrix) const {
-		// FIXME: THIS DOES NOT IMPLEMENT WHAT IS PROMISED.
+	bool isSubmatrixOf(SparseMatrix<T> const& matrix) const {
 		if (this->getRowCount() != matrix.getRowCount()) return false;
 		if (this->getColumnCount() != matrix.getColumnCount()) return false;
 
+		/*
 		for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) {
 			for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem, ++elem2) {
 				if (columnIndications[elem] < matrix.columnIndications[elem2]) return false;
 			}
 		}
+		*/
+
+		for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) {
+			for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem) {
+				// Skip over all entries of the other matrix that are before the current entry in
+				// the current matrix.
+				while (elem2 < matrix.rowIndications[row + 1] && matrix.columnIndications[elem2] < columnIndications[elem]) {
+					++elem2;
+				}
+				if (!(elem2 < matrix.rowIndications[row + 1]) || columnIndications[elem] != matrix.columnIndications[elem2]) return false;
+			}
+		}
 		return true;
 	}
 

src/utility/ConstTemplates.h

@@ -18,6 +18,9 @@
 
 #include <limits>
 
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/storage/BitVector.h"
+
 namespace storm {
 
 namespace utility {

src/utility/Settings.h

@@ -70,6 +70,23 @@ namespace settings {
 			inline const bool isSet(std::string const & name) const {
 				return this->vm.count(name) > 0;
 			}
+			
+			/*!
+			 *	@brief	Set an option.
+			 */
+			inline void set(std::string const & name) {
+				bpo::variable_value val;
+				this->vm.insert( std::make_pair(name, val) );
+			}
+			
+			/*!
+			 *	@brief Set value for an option.
+			 */
+			template <typename T>
+			inline void set(std::string const & name, T const & value) {
+				bpo::variable_value val(value, false);
+				this->vm.insert( std::make_pair(name, val) );
+			}
 
 			/*!
 			 *	@brief	Register a new module.

test/functional/EigenDtmcPrctModelCheckerTest.cpp

@@ -0,0 +1,164 @@
+/*
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/utility/Settings.h"
+#include "src/modelchecker/EigenDtmcPrctlModelChecker.h"
+#include "src/parser/AutoParser.h"
+
+TEST(EigenDtmcPrctModelCheckerTest, Die) {
+	storm::settings::Settings* s = storm::settings::instance();
+	s->set("fix-deadlocks");
+	storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew");
+
+	ASSERT_EQ(parser.getType(), storm::models::DTMC);
+
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+
+	ASSERT_EQ(dtmc->getNumberOfStates(), 14);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28);
+
+	storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc);
+
+	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("one");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	std::vector<double>* result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("two");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("three");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
+
+	result = rewardFormula->check(mc);
+
+
+	ASSERT_LT(std::abs((*result)[1] - ((double)11/3)), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+}
+
+TEST(EigenDtmcPrctModelCheckerTest, Crowds) {
+	storm::settings::Settings* s = storm::settings::instance();
+	s->set("fix-deadlocks");
+	storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", "");
+
+	ASSERT_EQ(parser.getType(), storm::models::DTMC);
+
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+
+	ASSERT_EQ(dtmc->getNumberOfStates(), 8608);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 22461);
+
+	storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc);
+
+	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("observe0Greater1");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	std::vector<double>* result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 0.3328800375801578281), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("observeIGreater1");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 0.1522173670950556501), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("observeOnlyTrueSender");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 0.32153724292835045), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+}
+
+TEST(EigenDtmcPrctModelCheckerTest, SynchronousLeader) {
+	storm::settings::Settings* s = storm::settings::instance();
+	s->set("fix-deadlocks");
+	storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew");
+
+	ASSERT_EQ(parser.getType(), storm::models::DTMC);
+
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+
+	ASSERT_EQ(dtmc->getNumberOfStates(), 12401);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28895);
+
+	storm::modelChecker::EigenDtmcPrctlModelChecker<double> mc(*dtmc);
+
+	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	std::vector<double>* result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 1), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), apFormula, 20);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 0.9999965911265462636), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
+
+	result = rewardFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 1.0448979591835938496), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+}
+*/

test/functional/GmmxxDtmcPrctModelCheckerTest.cpp

@@ -0,0 +1,162 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/utility/Settings.h"
+#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
+#include "src/parser/AutoParser.h"
+
+TEST(GmmxxDtmcPrctModelCheckerTest, Die) {
+	storm::settings::Settings* s = storm::settings::instance();
+	s->set("fix-deadlocks");
+	storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew");
+
+	ASSERT_EQ(parser.getType(), storm::models::DTMC);
+
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+
+	ASSERT_EQ(dtmc->getNumberOfStates(), 14);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28);
+
+	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+
+	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("one");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	std::vector<double>* result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("two");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("three");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
+
+	result = rewardFormula->check(mc);
+
+
+	ASSERT_LT(std::abs((*result)[1] - ((double)11/3)), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+}
+
+TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
+	storm::settings::Settings* s = storm::settings::instance();
+	s->set("fix-deadlocks");
+	storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", "");
+
+	ASSERT_EQ(parser.getType(), storm::models::DTMC);
+
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+
+	ASSERT_EQ(dtmc->getNumberOfStates(), 8608);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 22461);
+
+	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+
+	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("observe0Greater1");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	std::vector<double>* result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 0.3328800375801578281), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("observeIGreater1");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 0.1522173670950556501), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("observeOnlyTrueSender");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 0.32153724292835045), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+}
+
+TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
+	storm::settings::Settings* s = storm::settings::instance();
+	s->set("fix-deadlocks");
+	storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew");
+
+	ASSERT_EQ(parser.getType(), storm::models::DTMC);
+
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+
+	ASSERT_EQ(dtmc->getNumberOfStates(), 12401);
+	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28895);
+
+	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+
+	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	std::vector<double>* result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 1), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), apFormula, 20);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 0.9999965911265462636), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);
+
+	result = rewardFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[1] - 1.0448979591835938496), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+}

test/functional/GmmxxMdpPrctModelCheckerTest.cpp

@@ -0,0 +1,248 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/utility/Settings.h"
+#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h"
+#include "src/parser/AutoParser.h"
+
+TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
+	storm::settings::Settings* s = storm::settings::instance();
+	storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew");
+
+	ASSERT_EQ(parser.getType(), storm::models::MDP);
+
+	std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+
+	ASSERT_EQ(mdp->getNumberOfStates(), 169);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 436);
+
+	storm::modelChecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+
+	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("two");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	std::vector<double>* result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("two");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("three");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("three");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("four");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("four");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("done");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+
+	result = rewardFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+
+	result = rewardFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+
+	storm::parser::AutoParser<double> stateRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.state.rew", "");
+
+	ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP);
+
+	std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
+
+	storm::modelChecker::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
+
+	apFormula = new storm::formula::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+
+	result = rewardFormula->check(stateRewardModelChecker);
+
+	ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+
+	result = rewardFormula->check(stateRewardModelChecker);
+
+	ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+
+	storm::parser::AutoParser<double> stateAndTransitionRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew");
+
+	ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP);
+
+	std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
+
+	storm::modelChecker::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
+
+	apFormula = new storm::formula::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+
+	result = rewardFormula->check(stateAndTransitionRewardModelChecker);
+
+	ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+
+	result = rewardFormula->check(stateAndTransitionRewardModelChecker);
+
+	ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+}
+
+TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
+	storm::settings::Settings* s = storm::settings::instance();
+	storm::parser::AutoParser<double> parser(STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.tra", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.trans.rew");
+
+	ASSERT_EQ(parser.getType(), storm::models::MDP);
+
+	std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+
+	ASSERT_EQ(mdp->getNumberOfStates(), 3172);
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 7144);
+
+	storm::modelChecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+
+	storm::formula::Ap<double>* apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	std::vector<double>* result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	eventuallyFormula = new storm::formula::Eventually<double>(apFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(apFormula, 25);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(apFormula, 25);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
+
+	result = probFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
+
+	delete probFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+
+	result = rewardFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+
+	apFormula = new storm::formula::Ap<double>("elected");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(apFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+
+	result = rewardFormula->check(mc);
+
+	ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision"));
+
+	delete rewardFormula;
+	delete result;
+}

test/parser/ParseMdpTest.cpp

@@ -13,9 +13,9 @@
 
 TEST(ParseMdpTest, parseAndOutput) {
 	storm::parser::NondeterministicModelParser* mdpParser = nullptr;
-	/*ASSERT_NO_THROW(*/mdpParser = new storm::parser::NondeterministicModelParser(
+	ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser(
 			STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra",
-			STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")/*)*/;
+			STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
 
 	std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
 	std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix();