From 7ceb1ed9b2b219f33a3c5e4b794e05d9253f0185 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 14 Feb 2013 15:29:50 +0100
Subject: [PATCH] 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 +++++++++++++++
 src/storm.cpp                           | 15 ++++++++++++++-
 src/utility/GraphAnalyzer.h             |  2 +-
 3 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h
index 66b5c879f..2689ad6ea 100644
--- a/src/models/AtomicPropositionsLabeling.h
+++ b/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]]);
 	}
 
diff --git a/src/storm.cpp b/src/storm.cpp
index a8e839595..77e58fd52 100644
--- a/src/storm.cpp
+++ b/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;
 }
 
 /*!
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
index a05e3705d..9806077a2 100644
--- a/src/utility/GraphAnalyzer.h
+++ b/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;