Changed input format for non-deterministic models to PRISMs output format. Added min/max capability to probabilistic operator without bounds. Implemented Prob0E. Added a simple MDP model to example suite.

src/formula/ProbabilisticNoBoundOperator.h

@@ -51,7 +51,7 @@ public:
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticNoBoundOperator() : NoBoundOperator<T>(nullptr) {
+	ProbabilisticNoBoundOperator() : NoBoundOperator<T>(nullptr), optimalityOperator(false), minimumOperator(false) {
 		// Intentionally left empty
 	}
 
@@ -60,7 +60,18 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula),
+			optimalityOperator(false), minimumOperator(false) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : NoBoundOperator<T>(pathFormula),
+			optimalityOperator(true), minimumOperator(minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -68,11 +79,28 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const {
-		std::string result = "P = ? [";
+		std::string result = "P";
+		if (optimalityOperator) {
+			if (minimumOperator) {
+				result += "min";
+			} else {
+				result += "max";
+			}
+		}
+		result += "=? [";
 		result += this->getPathFormula().toString();
 		result += "]";
 		return result;
 	}
+
+private:
+	// A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator
+	// over a nondeterministic model.
+	bool optimalityOperator;
+
+	// In the case this operator is an optimizing operator, this flag indicates whether it is
+	// looking for the minimum or the maximum value.
+	bool minimumOperator;
 };
 
 } /* namespace formula */

src/parser/NondeterministicModelParser.cpp

@@ -5,7 +5,7 @@
  *      Author: Philipp Berger
  */
 
-#include "src/parser/NonDeterministicModelParser.h"
+#include "src/parser/NondeterministicModelParser.h"
 
 #include <string>
 #include <vector>

src/parser/NondeterministicSparseTransitionParser.cpp

@@ -70,14 +70,14 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
 	 *	Parse number of transitions.
 	 *	We will not actually use this value, but we will compare it to the
 	 *	number of transitions we count and issue a warning if this parsed
-	 *	vlaue is wrong.
+	 *	value is wrong.
 	 */
 	uint_fast64_t parsed_nonzero = strtol(buf, &buf, 10);
 
 	/*
 	 *	Read all transitions.
 	 */
-	int_fast64_t source, target;
+	int_fast64_t source, target, choice, lastchoice = -1;
 	int_fast64_t lastsource = -1;
 	uint_fast64_t nonzero = 0;
 	double val;
@@ -85,44 +85,47 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
 	maxnode = 0;
 	while (buf[0] != '\0') {
 		/*
-		 *	Read source node.
-		 *	Check if current source node is larger than current maximum node id.
-		 *	Increase number of choices.
-		 *	Check if we have skipped any source node, i.e. if any node has no
-		 *	outgoing transitions. If so, increase nonzero (and
-		 *	parsed_nonzero).
+		 *	Read source state and choice.
 		 */
 		source = checked_strtol(buf, &buf);
-		if (source > maxnode) maxnode = source;
-		choices++;
+
+		// Read the name of the nondeterministic choice.
+		choice = checked_strtol(buf, &buf);
+
+		// Check if we encountered a state index that is bigger than all previously seen.
+		if (source > maxnode) {
+			maxnode = source;
+		}
+
+		// If we have skipped some states, we need to reserve the space for the self-loop insertion
+		// in the second pass.
 		if (source > lastsource + 1) {
 			nonzero += source - lastsource - 1;
 			choices += source - lastsource - 1;
 			parsed_nonzero += source - lastsource - 1;
+		} else if (source != lastsource || choice != lastchoice) {
+			// If we have switched the source state or the nondeterministic choice, we need to
+			// reserve one row more.
+			++choices;
 		}
-		lastsource = source;
-		buf = trimWhitespaces(buf);  // Skip to name of choice
-		buf += strcspn(buf, " \t\n\r");  // Skip name of choice.
 
-		/*
-		 *	Read all targets for this choice.
-		 */
-		buf = trimWhitespaces(buf);
-		while (buf[0] == '*') {
-			buf++;
-			/*
-			 *	Read target node and transition value.
-			 *	Check if current target node is larger than current maximum node id.
-			 *	Check if the transition value is a valid probability.
-			 */
+		// Read target and check if we encountered a state index that is bigger than all previously
+		// seen.
 		target = checked_strtol(buf, &buf);
-			if (target > maxnode) maxnode = target;
+		if (target > maxnode) {
+			maxnode = target;
+		}
+
+		// Read value and check whether it's positive.
 		val = checked_strtod(buf, &buf);
 		if ((val < 0.0) || (val > 1.0)) {
 			LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
 			return 0;
 		}
 
+		lastchoice = choice;
+		lastsource = source;
+
 		/*
 		 *	Increase number of non-zero values.
 		 */
@@ -133,7 +136,6 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
 		 */
 		buf = trimWhitespaces(buf);
 	}
-	}
 
 	/*
 	 *	Check if the number of transitions given in the file is correct.
@@ -219,9 +221,8 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	/*
 	 *	Parse file content.
 	 */
-	int_fast64_t source, target, lastsource = -1;
-	uint_fast64_t curRow = 0;
-	std::string choice;
+	int_fast64_t source, target, lastsource = -1, choice, lastchoice = -1;
+	uint_fast64_t curRow = -1;
 	double val;
 	bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks");
 	bool hadDeadlocks = false;
@@ -231,11 +232,16 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	 */
 	while (buf[0] != '\0') {
 		/*
-		 *	Read source node and choice name.
+		 *	Read source state and choice.
 		 */
 		source = checked_strtol(buf, &buf);
-		buf = trimWhitespaces(buf);  // Skip to name of choice
-		choice = std::string(buf, strcspn(buf, " \t\n\r"));
+		choice = checked_strtol(buf, &buf);
+
+		// Increase line count if we have either finished reading the transitions of a certain state
+		// or we have finished reading one nondeterministic choice of a state.
+		if ((source != lastsource || choice != lastchoice)) {
+			++curRow;
+		}
 
 		/*
 		 *	Check if we have skipped any source node, i.e. if any node has no
@@ -247,7 +253,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 			if (fixDeadlocks) {
 				this->rowMapping->at(node) = curRow;
 				this->matrix->addNextValue(curRow, node, 1);
-				curRow++;
+				++curRow;
 				LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
 			} else {
 				LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
@@ -259,34 +265,20 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 			 */
 			this->rowMapping->at(source) = curRow;
 		}
-		lastsource = source;
 
-		/*
-		 *	Skip name of choice.
-		 */
-		buf += strcspn(buf, " \t\n\r");
-
-		/*
-		 *	Read all targets for this choice.
-		 */
-		buf = trimWhitespaces(buf);
-		while (buf[0] == '*') {
-			buf++;
-			/*
-			 *	Read target node and transition value.
-			 *	Put it into the matrix.
-			 */
+		// Read target and value and write it to the matrix.
 		target = checked_strtol(buf, &buf);
 		val = checked_strtod(buf, &buf);
 		this->matrix->addNextValue(curRow, target, val);
 
+		lastsource = source;
+		lastchoice = choice;
+
 		/*
 		 *	Proceed to beginning of next line in file and next row in matrix.
 		 */
 		buf = trimWhitespaces(buf);
 	}
-		curRow++;
-	}
 
 	this->rowMapping->at(maxnode+1) = curRow;
 

src/storm.cpp

@@ -205,6 +205,10 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
 	delete mc;
 }
 
+void testCheckingDice(storm::models::Mdp<double> mdp) {
+
+}
+
 /*!
  * Simple testing procedure.
  */
@@ -220,7 +224,14 @@ void testChecking() {
 		// testCheckingCrowds(*dtmc);
 		// testCheckingSynchronousLeader(*dtmc, 4);
 	}
-	else std::cout << "Input is not DTMC" << std::endl;
+	else if (parser.getType() == storm::models::MDP) {
+		std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+		mdp->printModelInformationToStream(std::cout);
+
+		// testCheckingDice(*mdp);
+	} else {
+		std::cout << "Input is neither a DTMC nor an MDP." << std::endl;
+	}
 }
 
 /*!

src/utility/GraphAnalyzer.h

@@ -224,7 +224,62 @@ public:
 
 	template <class T>
 	static void performProb0E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+		// Check for valid parameter.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
 
+		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix();
+		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices();
+
+		// Get the backwards transition relation from the model to ease the search.
+		storm::models::GraphTransitions<T> backwardTransitions(transitionMatrix, nondeterministicChoiceIndices, false);
+
+		// Add all psi states as the already satisfy the condition.
+		*statesWithProbability0 |= psiStates;
+
+		// Initialize the stack used for the DFS with the states
+		std::vector<uint_fast64_t> stack;
+		stack.reserve(model.getNumberOfStates());
+		psiStates.getList(stack);
+
+		// Perform the actual DFS.
+		while(!stack.empty()) {
+			uint_fast64_t currentState = stack.back();
+			stack.pop_back();
+
+			for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
+				if (phiStates.get(*it) && !statesWithProbability0->get(*it)) {
+
+					// Check whether the predecessor has at least one successor in the current state
+					// set for every nondeterministic choice.
+					bool addToStatesWithProbability0 = true;
+					for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) {
+						bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false;
+						for (auto colIt = transitionMatrix->beginConstColumnIterator(*rowIt); colIt != transitionMatrix->endConstColumnIterator(); ++colIt) {
+							if (statesWithProbability0->get(*colIt)) {
+								hasAtLeastOneSuccessorWithProbabilityGreater0 = true;
+								break;
+							}
+						}
+						if (!hasAtLeastOneSuccessorWithProbabilityGreater0) {
+							addToStatesWithProbability0 = false;
+							break;
+						}
+					}
+
+					// If we need to add the state, then actually add it and perform further search
+					// from the state.
+					if (addToStatesWithProbability0) {
+						statesWithProbability0->set(*it, true);
+						stack.push_back(*it);
+					}
+				}
+			}
+		}
+
+		statesWithProbability0->complement();
 	}
 
 	template <class T>