Added capability to compute model size in bytes and corresponding functions in several classes. Added model info output to DTMC class. Added atomic proposition information output to atomic propositions labeling class.

src/models/atomic_propositions_labeling.h

@@ -8,6 +8,11 @@
 #ifndef MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_
 #define MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_
 
+#include <pantheios/pantheios.hpp>
+#include <pantheios/inserters/integer.hpp>
+
+#include <iostream>
+
 #include "single_atomic_proposition_labeling.h"
 
 #define USE_STD_UNORDERED_MAP
@@ -143,7 +148,7 @@ public:
 	/*! Returns the number of propositions managed by this object (which was set in the initialization)
 	 * @return The number of propositions.
 	 */
-	uint_fast32_t getNumberOfPropositions() {
+	uint_fast32_t getNumberOfAtomicPropositions() {
 		return proposition_count;
 	}
 
@@ -153,10 +158,30 @@ public:
 	 * @param proposition The name of the proposition.
 	 * @return A pointer to the atomic_proposition object of the proposition.
 	 */
-	SingleAtomicPropositionLabeling* getProposition(std::string proposition) {
+	SingleAtomicPropositionLabeling* getAtomicProposition(std::string proposition) {
 		return (propositions[proposition_map[proposition]]);
 	}
 
+   /*!
+    * Returns the size of the labeling in memory measured in bytes.
+    * @return The size of the labeling in memory measured in bytes.
+    */
+	uint_fast64_t getSizeInMemory() {
+		uint_fast64_t size = sizeof(*this);
+		for (uint_fast32_t i = 0; i < proposition_count; i++) {
+			size += propositions[i]->getSizeInMemory(); // count sizes of bit vectors
+		}
+		return size;
+	}
+
+	void printAtomicPropositionsInformation() {
+		std::cout << "Atomic Propositions: \t" << this->getNumberOfAtomicPropositions() << std::endl;
+		for(auto ap : this->proposition_map) {
+			std::cout << "\t * " << ap.first << " -> " << propositions[ap.second]->getNumberOfLabeledStates();
+			std::cout << " state(s)" << std::endl;
+		}
+	}
+
 private:
 	uint_fast32_t node_count, proposition_count, propositions_current;
 	MAP<std::string, uint_fast32_t> proposition_map;

src/models/dtmc.h

@@ -11,6 +11,8 @@
 #include <pantheios/pantheios.hpp>
 #include <pantheios/inserters/integer.hpp>
 
+#include <iostream>
+
 #include "atomic_propositions_labeling.h"
 #include "src/sparse/static_sparse_matrix.h"
 
@@ -73,10 +75,13 @@ public:
 
 	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 << "Model type: \t\tDTMC" << std::endl;
+		std::cout << "States: \t\t" << this->getStateSpaceSize() << std::endl;
+		std::cout << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
+		this->state_labeling->printAtomicPropositionsInformation();
+		std::cout << "Size in memory: \t" << (this->probability_matrix->getSizeInMemory() +
+											this->state_labeling->getSizeInMemory() +
+											sizeof(*this))/1024 << " kbytes" << std::endl;
 		std::cout << "------------------------------------------------------- " << std::endl;
 	}
 

src/models/single_atomic_proposition_labeling.h

@@ -44,6 +44,18 @@ class SingleAtomicPropositionLabeling {
 		nodes.set(nodeId, true);
 	}
 	
+	uint_fast64_t getNumberOfLabeledStates() {
+		return nodes.getNumberOfSetBits();
+	}
+
+	/*!
+	 * Returns the size of the single atomic proposition labeling in memory measured in bytes.
+	 * @return The size of the single atomic proposition labeling in memory measured in bytes.
+	 */
+	uint_fast64_t getSizeInMemory() {
+		return sizeof(*this) + nodes.getSizeInMemory();
+	}
+
  private:
 	/*! BitVector containing the boolean bits for each node */
 	mrmc::vector::BitVector nodes;

src/sparse/static_sparse_matrix.h

@@ -488,6 +488,18 @@ class StaticSparseMatrix {
       fclose(P);
    }
 
+   /*!
+    * Returns the size of the matrix in memory measured in bytes.
+    * @return The size of the matrix in memory measured in bytes.
+    */
+   uint_fast64_t getSizeInMemory() {
+	   uint_fast64_t size = sizeof(*this);
+	   size += sizeof(T) * non_zero_entry_count; // add value_storage size
+	   size += sizeof(T) * (row_count + 1); // add diagonal_storage size
+	   size += sizeof(uint_fast64_t) * non_zero_entry_count; // add column_indications size
+	   size += sizeof(uint_fast64_t) * (row_count + 1); // add row_indications size
+	   return size;
+   }
 
  private:
 	uint_fast64_t current_size;

src/vector/bitvector.h

@@ -137,6 +137,36 @@ class BitVector {
 
 		return result;
 	}
+
+	/*!
+	 * Returns the number of bits that are set (to one) in this bit vector.
+	 * @return The number of bits that are set (to one) in this bit vector.
+	 */
+	uint_fast64_t getNumberOfSetBits() {
+		uint_fast64_t set_bits = 0;
+		for (uint_fast64_t i = 0; i < bucket_count; i++) {
+#ifdef __GNUG__ // check if we are using g++ and use built-in function if available
+			set_bits += __builtin_popcount (this->bucket_array[i]);
+#else
+			uint_fast32_t cnt;
+			uint_fast64_t bitset = this->bucket_array[i];
+			for (cnt = 0; bitset; cnt++) {
+				bitset &= bitset - 1;
+			}
+			set_bits += cnt;
+#endif
+		}
+		return set_bits;
+	}
+
+	/*!
+	 * Returns the size of the bit vector in memory measured in bytes.
+	 * @return The size of the bit vector in memory measured in bytes.
+	 */
+	uint_fast64_t getSizeInMemory() {
+		return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count;
+	}
+
  private:
 	uint_fast64_t bucket_count;