From 0ec2369459772bea1d78edfbdd8eacac5de7950f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 14 Nov 2012 15:27:27 +0100
Subject: [PATCH] Added support for 1-based indices for atomic proposition
 labeling. Fixed some whitespace typos.

---
 src/models/atomic_propositions_labeling.h       |  3 ++-
 src/models/dtmc.h                               | 17 +++++++++++++----
 src/models/single_atomic_proposition_labeling.h |  2 +-
 3 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/models/atomic_propositions_labeling.h b/src/models/atomic_propositions_labeling.h
index 5faed98a5..c3f6467c3 100644
--- a/src/models/atomic_propositions_labeling.h
+++ b/src/models/atomic_propositions_labeling.h
@@ -52,7 +52,8 @@ public:
 	 */
 	AtomicPropositionsLabeling(const uint_fast32_t nodeCount,
 			const uint_fast32_t propositionCount) {
-		node_count = nodeCount;
+		// add one for 1-bound indices
+		node_count = nodeCount + 1;
 		proposition_count = propositionCount;
 		propositions_current = 0;
 		propositions = new SingleAtomicPropositionLabeling*[proposition_count];
diff --git a/src/models/dtmc.h b/src/models/dtmc.h
index 1aff5e23a..7a95433cd 100644
--- a/src/models/dtmc.h
+++ b/src/models/dtmc.h
@@ -11,14 +11,15 @@
 #include <pantheios/pantheios.hpp>
 #include <pantheios/inserters/integer.hpp>
 
-#include "labeling.h"
+#include "atomic_propositions_labeling.h"
 #include "src/sparse/static_sparse_matrix.h"
 
 namespace mrmc {
 
 namespace models {
 
-/*! This class represents a discrete-time Markov chain (DTMC) whose states are
+/*!
+ * This class represents a discrete-time Markov chain (DTMC) whose states are
  * labeled with atomic propositions.
  */
 template <class T>
@@ -33,7 +34,6 @@ public:
 	*/
 	Dtmc(mrmc::sparse::StaticSparseMatrix<T>* probability_matrix,
 			mrmc::models::AtomicPropositionsLabeling* state_labeling) {
-		pantheios::log_DEBUG("Creating a DTMC ");
 		this->probability_matrix = probability_matrix;
 		this->state_labeling = state_labeling;
 	}
@@ -44,7 +44,7 @@ public:
 		@param dtmc A reference to the DTMC that is to be copied.
 	 */
 	Dtmc(const Dtmc<T> &dtmc) : probability_matrix(dtmc.probability_matrix), state_labeling(dtmc.state_labeling) {
-		// intentionally left empty
+		pantheios::log_DEBUG("Copy constructor of DTMC invoked.");
 	}
 
 	/*!
@@ -71,6 +71,15 @@ public:
 		return this->probability_matrix;
 	}
 
+	void printModelInformation() {
+		std::cout << "------------------------------------------------------- " << std::endl;
+		std::cout << "Model type: DTMC" << std::endl;
+		std::cout << "States: " << this->getStateSpaceSize() << std::endl;
+		std::cout << "Transitions: " << this->getNumberOfTransitions() << std::endl;
+		std::cout << "Size in memory: " << sizeof(this->probability_matrix) + sizeof(this->state_labeling) << std::endl;
+		std::cout << "------------------------------------------------------- " << std::endl;
+	}
+
 private:
 
 	/*! A matrix representing the transition probability function of the DTMC. */
diff --git a/src/models/single_atomic_proposition_labeling.h b/src/models/single_atomic_proposition_labeling.h
index bd4ee1f9a..ec1a3f20f 100644
--- a/src/models/single_atomic_proposition_labeling.h
+++ b/src/models/single_atomic_proposition_labeling.h
@@ -17,7 +17,7 @@ class SingleAtomicPropositionLabeling {
  public:
 
 	//! Constructor
-	 /*!
+	/*!
 		\param nodeCount Amount of nodes that the DTMC has to label
 	 */
 	SingleAtomicPropositionLabeling(uint_fast32_t nodeCount) : nodes(nodeCount) {