From 44fbef62bdff06559ae5b58e99db3fe126f1f9e1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Nov 2012 16:57:19 +0100 Subject: [PATCH] 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 | 29 ++++++++++++++++-- src/models/dtmc.h | 13 +++++--- .../single_atomic_proposition_labeling.h | 12 ++++++++ src/sparse/static_sparse_matrix.h | 12 ++++++++ src/vector/bitvector.h | 30 +++++++++++++++++++ 5 files changed, 90 insertions(+), 6 deletions(-) diff --git a/src/models/atomic_propositions_labeling.h b/src/models/atomic_propositions_labeling.h index c3f6467c3..78dfe9f5e 100644 --- a/src/models/atomic_propositions_labeling.h +++ b/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 +#include + +#include + #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 proposition_map; diff --git a/src/models/dtmc.h b/src/models/dtmc.h index 7a95433cd..46a715cdc 100644 --- a/src/models/dtmc.h +++ b/src/models/dtmc.h @@ -11,6 +11,8 @@ #include #include +#include + #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; } diff --git a/src/models/single_atomic_proposition_labeling.h b/src/models/single_atomic_proposition_labeling.h index ec1a3f20f..ebd384727 100644 --- a/src/models/single_atomic_proposition_labeling.h +++ b/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; diff --git a/src/sparse/static_sparse_matrix.h b/src/sparse/static_sparse_matrix.h index 7efdebb68..fdb73b814 100644 --- a/src/sparse/static_sparse_matrix.h +++ b/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; diff --git a/src/vector/bitvector.h b/src/vector/bitvector.h index e3c05c59a..74fd0abf1 100644 --- a/src/vector/bitvector.h +++ b/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;