diff --git a/src/models/atomic_proposition.h b/src/models/atomic_proposition.h deleted file mode 100644 index 8afc6dd92..000000000 --- a/src/models/atomic_proposition.h +++ /dev/null @@ -1,62 +0,0 @@ -#ifndef MRMC_DTMC_ATOMIC_PROPOSITION_H_ -#define MRMC_DTMC_ATOMIC_PROPOSITION_H_ - -#include -#include -#include "boost/integer/integer_mask.hpp" - -#include -#include - -#include "src/vector/bitvector.h" - - -namespace mrmc { - -namespace models { - -//! An atomic proposition for DTMCs with a constant number of nodes -/*! - A dense vector representing a single atomic proposition for all nodes of a DTMC. - */ -class AtomicProposition { - public: - - //! Constructor - /*! - \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) { - return nodes.get(nodeId); - } - - void addLabelToNode(uint_fast32_t nodeId) { - nodes.set(nodeId, true); - } - - private: - /*! BitVector containing the boolean bits for each node */ - mrmc::vector::BitVector nodes; -}; - -} // namespace models - -} // namespace mrmc - -#endif // MRMC_DTMC_ATOMIC_PROPOSITION_H_ diff --git a/src/models/atomic_propositions_labeling.h b/src/models/atomic_propositions_labeling.h new file mode 100644 index 000000000..5faed98a5 --- /dev/null +++ b/src/models/atomic_propositions_labeling.h @@ -0,0 +1,169 @@ +/* + * labeling.h + * + * Created on: 10.09.2012 + * Author: Thomas Heinemann + */ + +#ifndef MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ +#define MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ + +#include "single_atomic_proposition_labeling.h" + +#define USE_STD_UNORDERED_MAP + +/* Map types: By default, the boost hash map is used. + * If the macro USE_STD_MAP is defined, the default C++ class (std::map) + * is used instead. + */ +#ifdef USE_STD_MAP +# include +# define MAP std::map +#else +# ifdef USE_STD_UNORDERED_MAP +# include +# define MAP std::unordered_map +# else +# include "boost/unordered_map.hpp" +# define MAP boost::unordered_map +# endif +#endif + +#include + +#include +#include + +namespace mrmc { + +namespace models { + +/*! + * This class manages the labeling of the state space with a fixed number of + * atomic propositions. + */ +class AtomicPropositionsLabeling { + +public: + + /*! Constructor creating an object of class labeling. + * @param nodeCount The number of nodes; necessary for class AtomicProposition. + * @param propositionCount The number of atomic propositions. + */ + AtomicPropositionsLabeling(const uint_fast32_t nodeCount, + const uint_fast32_t propositionCount) { + node_count = nodeCount; + proposition_count = propositionCount; + propositions_current = 0; + propositions = new SingleAtomicPropositionLabeling*[proposition_count]; + for (uint_fast32_t i = 0; i < proposition_count; ++i) { + propositions[i] = new SingleAtomicPropositionLabeling(node_count); + } + } + + //! Copy Constructor + /*! Copy Constructor. Performs a deep copy of this Labeling object. + * + */ + AtomicPropositionsLabeling(const AtomicPropositionsLabeling& atomic_propositions_labeling) : + node_count(atomic_propositions_labeling.node_count), proposition_count( + atomic_propositions_labeling.proposition_count), propositions_current( + atomic_propositions_labeling.propositions_current), proposition_map( + atomic_propositions_labeling.proposition_map) { + propositions = new SingleAtomicPropositionLabeling*[proposition_count]; + for (uint_fast32_t i = 0; i < proposition_count; ++i) { + propositions[i] = new SingleAtomicPropositionLabeling( + *atomic_propositions_labeling.propositions[i]); + } + } + + virtual ~AtomicPropositionsLabeling() { + //deleting all the labeling vectors in the map. + MAP::iterator it; + for (uint_fast32_t i = 0; i < proposition_count; ++i) { + delete propositions[i]; + propositions[i] = NULL; + } + delete[] propositions; + propositions = NULL; + } + + /*! Registers the name of a proposition. + * Will throw an error if more propositions are added than were initialized, + * or if a proposition is registered twice. + * @param proposition The name of the proposition to add. + * @return The index of the new proposition. + */ + uint_fast32_t addProposition(std::string proposition) { + if (proposition_map.count(proposition) != 0) { + throw std::out_of_range("Proposition does already exist."); + } + if (propositions_current >= proposition_count) { + throw std::out_of_range("Added more propositions than initialized for"); + } + proposition_map[proposition] = propositions_current; + + uint_fast32_t returnValue = propositions_current++; + //pantheios::log_INFO("returning ", pantheios::integer(returnValue), " for position "); + return returnValue; + } + + /*! Checks whether the name of a proposition is already registered with the labeling. + * @return True if the proposition was added to the labeling, false otherwise. + */ + bool containsProposition(std::string proposition) { + return (proposition_map.count(proposition) != 0); + } + + /*! Labels a node with an atomic proposition. + * @param proposition The name of the proposition + * @param node The index of the node to label + */ + void addLabelToNode(std::string proposition, const uint_fast32_t node) { + //TODO (Thomas Heinemann): Differentiate exceptions? + if (proposition_map.count(proposition) == 0) { + throw std::out_of_range("Proposition does not exist."); + } + if (node >= node_count) { + throw std::out_of_range("Node number out of range"); + } + propositions[proposition_map[proposition]]->addLabelToNode(node); + } + + /*! Checks whether a node is labeled with a proposition. + * @param proposition The name of the proposition + * @param node The index of the node + * @return True if the node is labeled with the proposition, false otherwise. + */ + bool nodeHasProposition(std::string proposition, const uint_fast32_t node) { + return propositions[proposition_map[proposition]]->hasNodeLabel(node); + } + + /*! Returns the number of propositions managed by this object (which was set in the initialization) + * @return The number of propositions. + */ + uint_fast32_t getNumberOfPropositions() { + return proposition_count; + } + + /*! This function provides direct access to an atomic_proposition class object + * by its string identifier. This object manages the nodes that are labeled with the + * respective atomic proposition. + * @param proposition The name of the proposition. + * @return A pointer to the atomic_proposition object of the proposition. + */ + SingleAtomicPropositionLabeling* getProposition(std::string proposition) { + return (propositions[proposition_map[proposition]]); + } + +private: + uint_fast32_t node_count, proposition_count, propositions_current; + MAP proposition_map; + SingleAtomicPropositionLabeling** propositions; +}; + +} //namespace models + +} //namespace mrmc + +#endif /* MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ */ diff --git a/src/models/dtmc.h b/src/models/dtmc.h index d337951e1..1aff5e23a 100644 --- a/src/models/dtmc.h +++ b/src/models/dtmc.h @@ -8,6 +8,9 @@ #ifndef DTMC_H_ #define DTMC_H_ +#include +#include + #include "labeling.h" #include "src/sparse/static_sparse_matrix.h" @@ -18,33 +21,63 @@ namespace models { /*! This class represents a discrete-time Markov chain (DTMC) whose states are * labeled with atomic propositions. */ +template class Dtmc { public: //! Constructor /*! + * Constructs a DTMC object from the given transition probability matrix and the given labeling of the states. \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) { + 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; } //! Copy Constructor /*! - Copy Constructor. Creates an exact copy of the source DTMC. Modification of either DTMC does not affect the other. + Copy Constructor. Performs a deep copy of the given DTMC. @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) { + Dtmc(const Dtmc &dtmc) : probability_matrix(dtmc.probability_matrix), state_labeling(dtmc.state_labeling) { // intentionally left empty } + /*! + * Returns the state space size of the DTMC. + * @return The size of the state space of the DTMC. + */ + uint_fast64_t getStateSpaceSize() { + return this->probability_matrix->getRowCount(); + } + + /*! + * Returns the number of (non-zero) transitions of the DTMC. + * @return The number of (non-zero) transitions of the DTMC. + */ + uint_fast64_t getNumberOfTransitions() { + return this->probability_matrix->getNonZeroEntryCount(); + } + + /*! + * Returns a pointer to the matrix representing the transition probability function. + * @return A pointer to the matrix representing the transition probability function. + */ + mrmc::sparse::StaticSparseMatrix* getTransitionProbabilityMatrix() { + return this->probability_matrix; + } + private: - mrmc::sparse::StaticSparseMatrix* probability_matrix; - mrmc::models::Labeling* state_labeling; + /*! A matrix representing the transition probability function of the DTMC. */ + mrmc::sparse::StaticSparseMatrix* probability_matrix; + + /*! The labeling of the states of the DTMC. */ + mrmc::models::AtomicPropositionsLabeling* state_labeling; }; diff --git a/src/models/labeling.h b/src/models/labeling.h deleted file mode 100644 index cc5296a9b..000000000 --- a/src/models/labeling.h +++ /dev/null @@ -1,164 +0,0 @@ -/* - * labeling.h - * - * Created on: 10.09.2012 - * Author: Thomas Heinemann - */ - -#ifndef MRMC_DTMC_LABELING_H_ -#define MRMC_DTMC_LABELING_H_ - -#include "atomic_proposition.h" - - -#define USE_STD_UNORDERED_MAP - -/* Map types: By default, the boost hash map is used. - * If the macro USE_STD_MAP is defined, the default C++ class (std::map) - * is used instead. - */ -#ifdef USE_STD_MAP -# include -# define MAP std::map -#else -# ifdef USE_STD_UNORDERED_MAP -# include -# define MAP std::unordered_map -# else -# include "boost/unordered_map.hpp" -# define MAP boost::unordered_map -# endif -#endif - -#include - -#include -#include - -namespace mrmc { - -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 { - public: - - - /*! Constructor creating an object of 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, - const uint_fast32_t propositionCount) { - node_count = nodeCount; - proposition_count = propositionCount; - propositions_current = 0; - propositions = new AtomicProposition*[proposition_count]; - for (uint_fast32_t i = 0; i < proposition_count; ++i) { - propositions[i] = new AtomicProposition(node_count); - } - } - - //! 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) { - delete propositions[i]; - propositions[i] = NULL; - } - delete[] propositions; - propositions = NULL; - } - - /*! Registers the name of a proposition. - * Will throw an error if more propositions are added than were initialized, - * or if a proposition is registered twice. - * @param proposition The name of the proposition to add. - * @return The index of the new proposition. - */ - uint_fast32_t addProposition(std::string proposition) { - if (proposition_map.count(proposition) != 0) { - throw std::out_of_range("Proposition does already exist."); - } - if (propositions_current >= proposition_count) { - throw std::out_of_range("Added more propositions than initialized for"); - } - proposition_map[proposition] = propositions_current; - - uint_fast32_t returnValue = propositions_current++; - //pantheios::log_INFO("returning ", pantheios::integer(returnValue), " for position "); - return returnValue; - } - - /*! Checks whether the name of a proposition is already registered with the labeling. - * @return True if the proposition was added to the labeling, false otherwise. - */ - bool containsProposition(std::string proposition) { - return (proposition_map.count(proposition) != 0); - } - - /*! Labels a node with an atomic proposition. - * @param proposition The name of the proposition - * @param node The index of the node to label - */ - void addLabelToNode(std::string proposition, const uint_fast32_t node) { - //TODO (Thomas Heinemann): Differentiate exceptions? - if (proposition_map.count(proposition) == 0) { - throw std::out_of_range("Proposition does not exist."); - } - if (node >= node_count) { - throw std::out_of_range("Node number out of range"); - } - propositions[proposition_map[proposition]]->addLabelToNode(node); - } - - /*! Checks whether a node is labeled with a proposition. - * @param proposition The name of the proposition - * @param node The index of the node - * @return True if the node is labeled with the proposition, false otherwise. - */ - bool nodeHasProposition(std::string proposition, const uint_fast32_t node) { - return propositions[proposition_map[proposition]]->hasNodeLabel(node); - } - - /*! Returns the number of propositions managed by this object (which was set in the initialization) - * @return The number of propositions. - */ - uint_fast32_t getNumberOfPropositions() { - return proposition_count; - } - - /*! This function provides direct access to an atomic_proposition class object - * by its string identifier. This object manages the nodes that are labeled with the - * respective atomic proposition. - * @param proposition The name of the proposition. - * @return A pointer to the atomic_proposition object of the proposition. - */ - AtomicProposition* getProposition(std::string proposition) { - return (propositions[proposition_map[proposition]]); - } - - private: - uint_fast32_t node_count, proposition_count, propositions_current; - MAP proposition_map; - AtomicProposition** propositions; -}; - -} //namespace models - -} //namespace mrmc - -#endif /* MRMC_DTMC_LABELING_H_ */ diff --git a/src/models/single_atomic_proposition_labeling.h b/src/models/single_atomic_proposition_labeling.h new file mode 100644 index 000000000..bd4ee1f9a --- /dev/null +++ b/src/models/single_atomic_proposition_labeling.h @@ -0,0 +1,56 @@ +#ifndef MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_ +#define MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_ + +#include "src/vector/bitvector.h" + +namespace mrmc { + +namespace models { + +/*! + * This class represents the labeling of a state space with a single atomic proposition. + * Internally, this is done by keeping a dense bit vector such that the i-th bit + * in the vector is set to true if and only if the i-th state satisfies the + * atomic proposition + */ +class SingleAtomicPropositionLabeling { + public: + + //! Constructor + /*! + \param nodeCount Amount of nodes that the DTMC has to label + */ + SingleAtomicPropositionLabeling(uint_fast32_t nodeCount) : nodes(nodeCount) { + // intentionally left empty + } + + //! Copy Constructor + /*! + * Copy constructor. Performs a deep copy of this AtomicProposition object. + */ + SingleAtomicPropositionLabeling(const SingleAtomicPropositionLabeling& single_atomic_proposition_labeling) : nodes(single_atomic_proposition_labeling.nodes) { + // intentionally left empty + } + + ~SingleAtomicPropositionLabeling() { + // intentionally left empty + } + + bool hasNodeLabel(uint_fast32_t nodeId) { + return nodes.get(nodeId); + } + + void addLabelToNode(uint_fast32_t nodeId) { + nodes.set(nodeId, true); + } + + private: + /*! BitVector containing the boolean bits for each node */ + mrmc::vector::BitVector nodes; +}; + +} // namespace models + +} // namespace mrmc + +#endif // MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_ diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp index e11162021..45aa31929 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::models::Labeling * read_lab_file(int node_count, const char * filename) +mrmc::models::AtomicPropositionsLabeling * 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::models::Labeling * read_lab_file(int node_count, const char * filename) pos++; } - mrmc::models::Labeling* result = new mrmc::models::Labeling(node_count, proposition_count); + mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(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 df032675a..ddbb7f82a 100644 --- a/src/parser/read_lab_file.h +++ b/src/parser/read_lab_file.h @@ -8,16 +8,17 @@ #ifndef READ_LAB_FILE_H_ #define READ_LAB_FILE_H_ -#include "src/models/labeling.h" +#include "src/models/atomic_propositions_labeling.h" namespace mrmc { namespace parser { -mrmc::models::Labeling * read_lab_file(int node_count, const char * filename); +mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const char * filename); } + } #endif /* READ_LAB_FILE_H_ */ diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/read_lab_file_test.cpp index 6bacc5395..789f853cf 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/models/labeling.h" +#include "src/models/atomic_propositions_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::models::Labeling* labeling = NULL; + mrmc::models::AtomicPropositionsLabeling* 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"));