diff --git a/src/dtmc/atomic_proposition.h b/src/models/atomic_proposition.h similarity index 74% rename from src/dtmc/atomic_proposition.h rename to src/models/atomic_proposition.h index 5beb41227..8afc6dd92 100644 --- a/src/dtmc/atomic_proposition.h +++ b/src/models/atomic_proposition.h @@ -13,7 +13,7 @@ namespace mrmc { -namespace dtmc { +namespace models { //! An atomic proposition for DTMCs with a constant number of nodes /*! @@ -27,11 +27,19 @@ class AtomicProposition { \param nodeCount Amount of nodes that the DTMC has to label */ AtomicProposition(uint_fast32_t nodeCount) : nodes(nodeCount) { - // + // intentionally left empty + } + + //! Copy Constructor + /*! + * Copy constructor. Performs a deep copy of this AtomicProposition object. + */ + AtomicProposition(const AtomicProposition& atomic_proposition) : nodes(atomic_proposition.nodes) { + // intentionally left empty } ~AtomicProposition() { - // + // intentionally left empty } bool hasNodeLabel(uint_fast32_t nodeId) { @@ -47,7 +55,7 @@ class AtomicProposition { mrmc::vector::BitVector nodes; }; -} // namespace dtmc +} // namespace models } // namespace mrmc diff --git a/src/models/dtmc.h b/src/models/dtmc.h new file mode 100644 index 000000000..516f43b3b --- /dev/null +++ b/src/models/dtmc.h @@ -0,0 +1,57 @@ +/* + * dtmc.h + * + * Created on: 14.11.2012 + * Author: Christian Dehnert + */ + +#ifndef DTMC_H_ +#define DTMC_H_ + +#include "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 + * labeled with atomic propositions. + */ +class Dtmc { + +public: + + //! Constructor + /*! + \param probability_matrix The transition probability function of the DTMC given by a matrix. + \param state_labeling The labeling that assigns a set of atomic propositions to each state. + */ + Dtmc(mrmc::sparse::StaticSparseMatrix* probability_matrix, + mrmc::models::Labeling* state_labeling) { + this->probability_matrix = probability_matrix; + this->state_labeling = state_labeling; + } + + //! Copy Constructor + /*! + Copy Constructor. Creates an exact copy of the source DTMC. Modification of either DTMC does not affect the other. + @param dtmc A reference to the matrix that should be copied from + */ + Dtmc(const Dtmc &dtmc) : probability_matrix(dtmc.probability_matrix), state_labeling(dtmc.state_labeling) { + // intentionally left empty + } + + +private: + + mrmc::sparse::StaticSparseMatrix* probability_matrix; + mrmc::models::Labeling* state_labeling; + +}; + +} //namespace models + +} //namespace mrmc + +#endif /* DTMC_H_ */ diff --git a/src/dtmc/labeling.h b/src/models/labeling.h similarity index 88% rename from src/dtmc/labeling.h rename to src/models/labeling.h index 5cbb6ddcf..cc5296a9b 100644 --- a/src/dtmc/labeling.h +++ b/src/models/labeling.h @@ -37,12 +37,12 @@ namespace mrmc { -namespace dtmc { +namespace models { /*! This class manages the objects of class atomic_proposition. Access is possible with the * string identifiers which are used in the input. */ -class labeling { +class Labeling { public: @@ -50,7 +50,7 @@ class labeling { * @param nodeCount The number of nodes; necessary for class AtomicProposition. * @param propositionCount The number of atomic propositions. */ - labeling(const uint_fast32_t nodeCount, + Labeling(const uint_fast32_t nodeCount, const uint_fast32_t propositionCount) { node_count = nodeCount; proposition_count = propositionCount; @@ -61,7 +61,18 @@ class labeling { } } - virtual ~labeling() { + //! Copy Constructor + /*! Copy Constructor. Performs a deep copy of this Labeling object. + * + */ + Labeling(const Labeling& labeling) : node_count(labeling.node_count), proposition_count(labeling.proposition_count), propositions_current(labeling.propositions_current), proposition_map(labeling.proposition_map) { + propositions = new AtomicProposition*[proposition_count]; + for (uint_fast32_t i = 0; i < proposition_count; ++i) { + propositions[i] = new AtomicProposition(*labeling.propositions[i]); + } + } + + virtual ~Labeling() { //deleting all the labeling vectors in the map. MAP::iterator it; for (uint_fast32_t i = 0; i < proposition_count; ++i) { @@ -146,7 +157,7 @@ class labeling { AtomicProposition** propositions; }; -} //namespace dtmc +} //namespace models } //namespace mrmc diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp index d631cb215..e11162021 100644 --- a/src/parser/read_lab_file.cpp +++ b/src/parser/read_lab_file.cpp @@ -42,7 +42,7 @@ namespace parser { * @param filename input .lab file's name. * @return The pointer to the created labeling object. */ -mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename) +mrmc::models::Labeling * read_lab_file(int node_count, const char * filename) { /* Note that this function uses strtok_r on char-array s. * This function will modify this string. @@ -125,7 +125,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename) pos++; } - mrmc::dtmc::labeling* result = new mrmc::dtmc::labeling(node_count, proposition_count); + mrmc::models::Labeling* result = new mrmc::models::Labeling(node_count, proposition_count); //Here, all propositions are to be declared... for (proposition = STRTOK_FUNC(decl_buffer, sep, &saveptr); diff --git a/src/parser/read_lab_file.h b/src/parser/read_lab_file.h index f51595af4..df032675a 100644 --- a/src/parser/read_lab_file.h +++ b/src/parser/read_lab_file.h @@ -8,14 +8,14 @@ #ifndef READ_LAB_FILE_H_ #define READ_LAB_FILE_H_ -#include "src/dtmc/labeling.h" +#include "src/models/labeling.h" namespace mrmc { namespace parser { -mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename); +mrmc::models::Labeling * read_lab_file(int node_count, const char * filename); } } diff --git a/src/vector/bitvector.h b/src/vector/bitvector.h index ec50d2870..e3c05c59a 100644 --- a/src/vector/bitvector.h +++ b/src/vector/bitvector.h @@ -26,7 +26,7 @@ class BitVector { public: //! Constructor /*! - \param initial_length The initial size of the boolean Array. Can be changed later on via @resize() + \param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize() */ BitVector(uint_fast64_t initial_length) { bucket_count = initial_length / 64; @@ -43,8 +43,8 @@ class BitVector { //! Copy Constructor /*! - Copy Constructor. Creates an exact copy of the source sparse matrix ssm. Modification of either matrix does not affect the other. - @param ssm A reference to the matrix that should be copied from + Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other. + @param bv A reference to the bit vector that should be copied from */ BitVector(const BitVector &bv) : bucket_count(bv.bucket_count) { diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/read_lab_file_test.cpp index afaae3111..6bacc5395 100644 --- a/test/parser/read_lab_file_test.cpp +++ b/test/parser/read_lab_file_test.cpp @@ -7,7 +7,7 @@ #include "gtest/gtest.h" #include "MRMCConfig.h" -#include "src/dtmc/labeling.h" +#include "src/models/labeling.h" #include "src/parser/read_lab_file.h" #include "src/exceptions/file_IO_exception.h" #include "src/exceptions/wrong_file_format.h" @@ -19,7 +19,7 @@ TEST(ReadLabFileTest, NonExistingFileTest) { TEST(ReadLabFileTest, ParseTest) { //This test is based on a test case from the original MRMC. - mrmc::dtmc::labeling* labeling = NULL; + mrmc::models::Labeling* labeling = NULL; //Parsing the file ASSERT_NO_THROW(labeling = mrmc::parser::read_lab_file(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));