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;