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 #include -#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 @@ -33,7 +34,6 @@ public: */ Dtmc(mrmc::sparse::StaticSparseMatrix* 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 &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) {