Added logging for errors in labeling class. Corrected wrong labeling of MDP in examples. Extended test checking for first MDP example in main.

src/models/AtomicPropositionsLabeling.h

@@ -15,6 +15,11 @@
 #include <unordered_map>
 #include <set>
 
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+extern log4cplus::Logger logger;
+
 namespace storm {
 
 namespace models {
@@ -82,9 +87,11 @@ public:
 	 */
 	uint_fast64_t addAtomicProposition(std::string ap) {
 		if (nameToLabelingMap.count(ap) != 0) {
+			LOG4CPLUS_ERROR(logger, "Atomic Proposition already exists.");
 			throw storm::exceptions::OutOfRangeException("Atomic Proposition already exists.");
 		}
 		if (apsCurrent >= apCountMax) {
+			LOG4CPLUS_ERROR(logger, "Added more atomic propositions than previously declared.");
 			throw storm::exceptions::OutOfRangeException("Added more atomic propositions than"
 					"previously declared.");
 		}
@@ -110,9 +117,11 @@ public:
 	 */
 	void addAtomicPropositionToState(std::string ap, const uint_fast64_t state) {
 		if (nameToLabelingMap.count(ap) == 0) {
+			LOG4CPLUS_ERROR(logger, "Atomic Proposition '" << ap << "' unknown.");
 			throw storm::exceptions::OutOfRangeException() << "Atomic Proposition '" << ap << "' unknown.";
 		}
 		if (state >= stateCount) {
+			LOG4CPLUS_ERROR(logger, "State index out of range.");
 			throw storm::exceptions::OutOfRangeException("State index out of range.");
 		}
 		this->singleLabelings[nameToLabelingMap[ap]]->set(state, true);
@@ -125,6 +134,7 @@ public:
 	 */
 	std::set<std::string> getPropositionsForState(uint_fast64_t state) {
 		if (state >= stateCount) {
+			LOG4CPLUS_ERROR(logger, "State index out of range.");
 			throw storm::exceptions::OutOfRangeException("State index out of range.");
 		}
 		std::set<std::string> result;
@@ -165,6 +175,11 @@ public:
 	 * represents the labeling of the states with the given atomic proposition.
 	 */
 	storm::storage::BitVector* getAtomicProposition(std::string ap) {
+		if (!this->containsAtomicProposition(ap)) {
+			LOG4CPLUS_ERROR(logger, "The atomic proposition " << ap << " is invalid for the labeling of the model.");
+			throw storm::exceptions::InvalidArgumentException() << "The atomic proposition " << ap
+					<< " is invalid for the labeling of the model.";
+		}
 		return (this->singleLabelings[nameToLabelingMap[ap]]);
 	}
 

src/storm.cpp

@@ -205,8 +205,21 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
 	delete mc;
 }
 
-void testCheckingDice(storm::models::Mdp<double> mdp) {
+void testCheckingDice(storm::models::Mdp<double>& mdp) {
+	storm::storage::BitVector* targetStates = mdp.getLabeledStates(std::string("two"));
+	*targetStates |= *mdp.getLabeledStates(std::string("three"));
 
+	storm::storage::BitVector* trueStates = new storm::storage::BitVector(mdp.getNumberOfStates(), true);
+	storm::storage::BitVector* statesWithProbability0 = new storm::storage::BitVector(mdp.getNumberOfStates());
+	storm::storage::BitVector* statesWithProbability1 = new storm::storage::BitVector(mdp.getNumberOfStates());
+
+	storm::utility::GraphAnalyzer::performProb01Max(mdp, *trueStates, *targetStates, statesWithProbability0, statesWithProbability1);
+
+	std::cout << statesWithProbability0->toString() << std::endl << statesWithProbability1->toString() << std::endl;
+
+	delete statesWithProbability0;
+	delete statesWithProbability1;
+	delete trueStates;
 }
 
 /*!

src/utility/GraphAnalyzer.h

@@ -257,7 +257,7 @@ public:
 					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) {
+						for (auto colIt = transitionMatrix->beginConstColumnIterator(*rowIt); colIt != transitionMatrix->endConstColumnIterator(*rowIt); ++colIt) {
 							if (statesWithProbability0->get(*colIt)) {
 								hasAtLeastOneSuccessorWithProbabilityGreater0 = true;
 								break;