diff --git a/CMakeLists.txt b/CMakeLists.txt index 164afef61..76df18c29 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -7,9 +7,13 @@ set (MRMC_CPP_VERSION_MAJOR 1) set (MRMC_CPP_VERSION_MINOR 0) #Configurations for GCC -if(CMAKE_COMPILER_IS_GNUCC) +if(CMAKE_COMPILER_IS_GNUCC) + + #Using C++11 + set (CMAKE_CXX_FLAGS "-std=c++0x") + #Debug symbols - set (CMAKE_CXX_FLAGS "-g") + set (CMAKE_CXX_FLAGS_DEBUG "-g") endif() # configure a header file to pass some of the CMake settings diff --git a/src/dtmc/atomic_proposition.h b/src/dtmc/atomic_proposition.h index 7b8e75690..001a92a4b 100644 --- a/src/dtmc/atomic_proposition.h +++ b/src/dtmc/atomic_proposition.h @@ -25,21 +25,19 @@ namespace dtmc { class AtomicProposition { public: - /*! Default Constructor - * Creates an uninitialized object - * Useful for array construction, afterwards, the initialize function has to be called. - */ - AtomicProposition() { - - } - //! Constructor /*! \param nodeCount Amount of nodes that the DTMC has to label */ AtomicProposition(uint_fast32_t nodeCount) { node_array = NULL; - initialize(nodeCount); + if (node_array == NULL) { + node_count = nodeCount; + int n = (int) std::ceil(nodeCount / 64.0); + node_array = new uint_fast64_t[n]; + //Initialization with 0 is crucial! + memset(node_array, 0, n*sizeof(uint_fast64_t)); + } } ~AtomicProposition() { @@ -48,17 +46,6 @@ class AtomicProposition { } } - void initialize(uint_fast32_t nodeCount) { - if (node_array == NULL) { - node_count = nodeCount; - int n = (int) std::ceil(nodeCount / 64.0); - node_array = new uint_fast64_t[n]; - //Initialization with 0 is crucial! - memset(node_array, 0, n*sizeof(uint_fast64_t)); - } - - } - bool hasNodeLabel(uint_fast32_t nodeId) { int bucket = static_cast(std::floor(nodeId / 64)); int bucket_place = nodeId % 64; diff --git a/src/dtmc/labeling.h b/src/dtmc/labeling.h index 76311ce53..740f0eaaf 100644 --- a/src/dtmc/labeling.h +++ b/src/dtmc/labeling.h @@ -11,17 +11,23 @@ #include "atomic_proposition.h" +#define USE_STD_UNORDERED_MAP /* Map types: By default, the boost hash map is used. - * When the macro DEFAULT_MAP is defined, the default C++ class (std::map) + * If the macro USE_STD_MAP is defined, the default C++ class (std::map) * is used instead. */ -#ifdef DEFAULT_MAP -#include -#define MAP std::map +#ifdef USE_STD_MAP +# include +# define MAP std::map #else -#include "boost/unordered_map.hpp" -#define MAP boost::unordered_map +# 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 @@ -33,11 +39,17 @@ namespace mrmc { namespace dtmc { - +/*! 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; @@ -60,6 +72,12 @@ class labeling { 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."); @@ -74,11 +92,17 @@ class labeling { 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) { @@ -90,14 +114,28 @@ class labeling { 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]]); } diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp index 0d89b3935..ebda11d3b 100644 --- a/src/parser/read_lab_file.cpp +++ b/src/parser/read_lab_file.cpp @@ -32,10 +32,12 @@ namespace parser { /*! - * Reads a .lab file and puts the result in a labelling structure. + * Reads a .lab file and puts the result in a labeling structure. + * + * Labelings created with this method have to be freed with the delete operator. * @param node_count the number of states. * @param filename input .lab file's name. - * @return returns a pointer to a labelling object. + * @return The pointer to the created labeling object. */ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename) { diff --git a/src/parser/read_tra_file.cpp b/src/parser/read_tra_file.cpp index 6056db8cf..8c2d12a95 100644 --- a/src/parser/read_tra_file.cpp +++ b/src/parser/read_tra_file.cpp @@ -86,8 +86,10 @@ static uint_fast32_t make_first_pass(FILE* p) { /*!Reads a .tra file and produces a sparse matrix representing the described Markov Chain. - * @param *filename input .tra file's name. - * @return a pointer to a sparse matrix. + * + * Matrices created with this method have to be freed with the delete operator. + * @param filename input .tra file's name. + * @return a pointer to the created sparse matrix. */ sparse::StaticSparseMatrix * read_tra_file(const char * filename) {