diff --git a/src/parser/parser.h b/src/parser/parser.h index b36f8dc70..fcad8fa35 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -15,20 +15,47 @@ #include #include "src/exceptions/file_IO_exception.h" -namespace mrmc -{ -namespace parser -{ - +namespace mrmc { +namespace parser { + + /*! + * @brief Opens a file and maps it to memory providing a char* + * containing the file content. + * + * This class is a very simple interface to read files efficiently. + * The given file is opened and mapped to memory using mmap(). + * The public member data is a pointer to the actual file content. + * Using this method, the kernel will take care of all buffering. This is + * most probably much more efficient than doing this manually. + */ + class MappedFile { private: + /*! + * @brief file descriptor obtained by open(). + */ int file; + + /*! + * @brief stat information about the file. + */ struct stat st; public: - char* data; - + /*! + * @brief pointer to actual file content. + */ + char* data; + + /*! + * @brief Constructor of MappedFile. + * + * Will stat the given file, open it and map it to memory. + * If anything of this fails, an appropriate exception is raised + * and a log entry is written. + * @filename file to be opened + */ MappedFile(const char* filename) { if (stat(filename, &(this->st)) != 0) @@ -53,6 +80,11 @@ namespace parser } } + /*! + * @brief Destructor of MappedFile. + * + * Will unmap the data and close the file. + */ ~MappedFile() { munmap(this->data, this->st.st_size); @@ -60,5 +92,5 @@ namespace parser } }; -} -} \ No newline at end of file +} // namespace parser +} // namespace mrmc \ No newline at end of file diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp index 5fa97a0d3..f910e8dce 100644 --- a/src/parser/readLabFile.cpp +++ b/src/parser/readLabFile.cpp @@ -1,4 +1,4 @@ -/* +/*! * readLabFile.cpp * * Created on: 21.11.2012 @@ -28,76 +28,138 @@ #include namespace mrmc { - namespace parser { /*! - * Reads a .lab file and puts the result in a labeling structure. + * Reads a label 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 The pointer to the created labeling object. + * 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 The pointer to the created labeling object. */ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename) { + /* + * open file + */ MappedFile file(filename); - char* buf = file.data; - char sep[] = " \n\t"; - uint_fast32_t proposition_count = 0; - size_t cnt = 0; - do { - buf += cnt; - cnt = strcspn(buf, sep); - if (cnt > 0) { - if (strncmp(buf, "#DECLARATION", cnt) == 0) continue; - if (strncmp(buf, "#END", cnt) == 0) break; - proposition_count++; - } - else cnt = 1; - } while (cnt > 0); + /* + * first run: obtain number of propositions + */ + char separator[] = " \n\t"; + uint_fast32_t proposition_count = 0; + { + size_t cnt = 0; + do + { + buf += cnt; + cnt = strcspn(buf, separator); // position of next separator + if (cnt > 0) + { + /* + * next token is #DECLARATION: just skip it + * next token is #END: stop search + * otherwise increase proposition_count + */ + if (strncmp(buf, "#DECLARATION", cnt) == 0) continue; + if (strncmp(buf, "#END", cnt) == 0) break; + proposition_count++; + } + else cnt = 1; // next char is separator, one step forward + } while (cnt > 0); + } - printf("node count %d\n", node_count); + /* + * create labeling object with given node and proposition count + */ mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count); - char proposition[128]; + + /* + * second run: add propositions and node labels to labeling + * + * first thing to do: reset file pointer + */ buf = file.data; - cnt = 0; - do { - buf += cnt; - cnt = strcspn(buf, sep); - if (cnt > 0) { - if (strncmp(buf, "#DECLARATION", cnt) == 0) continue; - if (strncmp(buf, "#END", cnt) == 0) break; - strncpy(proposition, buf, cnt); - proposition[cnt] = '\0'; - result->addAtomicProposition(proposition); - } - else cnt = 1; - } while (cnt > 0); - buf += 4; + { + /* + * load propositions + */ + char proposition[128]; // buffer for proposition names + size_t cnt = 0; + do + { + buf += cnt; + cnt = strcspn(buf, separator); // position of next separator + if (cnt > 0) + { + /* + * next token is: #DECLARATION: just skip it + * next token is: #END: stop search + * otherwise: copy token to buffer, append trailing null byte and hand it to labeling + */ + if (strncmp(buf, "#DECLARATION", cnt) == 0) continue; + if (strncmp(buf, "#END", cnt) == 0) break; + strncpy(proposition, buf, cnt); + proposition[cnt] = '\0'; + result->addAtomicProposition(proposition); + } + else cnt = 1; // next char is separator, one step forward + } while (cnt > 0); + /* + * Right here, the buf pointer is still pointing to our last token, + * i.e. to #END. We want to skip this one... + */ + buf += 4; + } - uint_fast32_t node; - do { - node = strtol(buf, &buf, 10); - while (*buf != '\0') { - cnt = strcspn(buf, sep); - if (cnt == 0) buf++; - else break; - } - if (cnt > 0) { - strncpy(proposition, buf, cnt); - proposition[cnt] = '\0'; - result->addAtomicPropositionToState(proposition, node); - } - buf += cnt; - } while (cnt > 0); + { + /* + * now parse node label assignments + */ + uint_fast32_t node; + char proposition[128]; + size_t cnt; + do + { + node = strtol(buf, &buf, 10); // parse node number + while (*buf != '\0') // while not at end of file + { + cnt = strcspn(buf, separator); // position of next separator + if (cnt == 0) buf++; // next char is separator, one step forward + else break; + } + /* + * if cnt > 0, buf points to the next proposition + * otherwise, we have reached the end of the file + */ + if (cnt > 0) + { + /* + * copy proposition to buffer, add assignment to labeling + */ + strncpy(proposition, buf, cnt); + proposition[cnt] = '\0'; + result->addAtomicPropositionToState(proposition, node); + } + else if (node == 0) + { + /* + * If this is executed, we could read a number but there + * was no proposition after that. This strongly suggests a + * broken file, but it's not fatal... + */ + pantheios::log_WARNING("The label file ended on a node number. Is the file malformated?"); + } + buf += cnt; + } while (cnt > 0); + } return result; } } //namespace parser - } //namespace mrmc diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h index 4019864e0..e948a2ce3 100644 --- a/src/parser/readLabFile.h +++ b/src/parser/readLabFile.h @@ -1,19 +1,15 @@ -/* - * read_lab_file.h - * - */ - #pragma once #include "src/models/atomic_propositions_labeling.h" namespace mrmc { - namespace parser { +/*! + * @brief Load label file and return initialized AtomicPropositionsLabeling object. + */ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename); -} - -} +} // namespace parser +} // namespace mrmc diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp index 032ff0214..335699138 100644 --- a/src/parser/readTraFile.cpp +++ b/src/parser/readTraFile.cpp @@ -1,10 +1,8 @@ -/*! read_tra_file.cpp - * Provides functions for reading a *.tra file describing the transition - * system of a Markov chain (DTMC) and saving it into a corresponding - * matrix. +/*! + * readTraFile.cpp * - * Created on: 20.11.2012 - * Author: Gereon Kremer + * Created on: 20.11.2012 + * Author: Gereon Kremer */ #include "parser.h" @@ -30,9 +28,13 @@ #include namespace mrmc { - namespace parser{ +/*! + * Skips all whitespaces and returns new pointer. + * + * @todo should probably be replaced by strspn et.al. + */ char* skipWS(char* buf) { while(1) @@ -43,20 +45,25 @@ char* skipWS(char* buf) } /*! - * This method does the first pass through the .tra file and computes - * the number of non-zero elements that are not diagonal elements, - * which correspondents to the number of transitions that are not - * self-loops. - * (Diagonal elements are treated in a special way). + * @brief Perform first pass through the file and obtain number of + * non-zero cells and maximum node id. + * + * This method does the first pass through the .tra file and computes + * the number of non-zero elements that are not diagonal elements, + * which correspondents to the number of transitions that are not + * self-loops. + * (Diagonal elements are treated in a special way). + * It also calculates the maximum node id and stores it in maxnode. * - * @return The number of non-zero elements that are not on the diagonal - * @param buf Data to scan. Is expected to be some char array. + * @return The number of non-zero elements that are not on the diagonal + * @param buf Data to scan. Is expected to be some char array. + * @param maxnode Is set to highest id of all nodes. */ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode) { uint_fast32_t non_zero = 0; - /*! + /* * check file header and extract number of transitions */ if (strncmp(buf, "STATES ", 7) != 0) return 0; @@ -67,7 +74,7 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode) buf += 12; // skip "TRANSITIONS " if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0; - /*! + /* * check all transitions for non-zero diagonal entrys */ uint_fast32_t row, col; @@ -75,10 +82,20 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode) maxnode = 0; while (1) { + /* + * read row and column + */ row = strtol(buf, &buf, 10); - if (row > maxnode) maxnode = row; col = strtol(buf, &buf, 10); + /* + * check if one is larger than the current maximum id + */ + if (row > maxnode) maxnode = row; if (col > maxnode) maxnode = col; + /* + * read value. if value is zero, we have reached the end of the file. + * if row == col, we have a diagonal element which is treated seperately and this non_zero must be decreased. + */ val = strtod(buf, &buf); if (val == 0.0) break; if (row == col) non_zero--; @@ -89,44 +106,44 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode) -/*!Reads a .tra file and produces a sparse matrix representing the described Markov Chain. +/*! + * Reads a .tra file and produces a sparse matrix representing the described Markov Chain. * - * 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. + * 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 * readTraFile(const char * filename) { - /*! + /* * enforce locale where decimal point is '.' */ setlocale( LC_NUMERIC, "C" ); + /* + * open file + */ MappedFile file(filename); + char* buf = file.data; - /*! + /* * perform first pass, i.e. count entries that are not zero and not on the diagonal */ uint_fast32_t maxnode; uint_fast32_t non_zero = makeFirstPass(file.data, maxnode); - if (non_zero == 0) - { - /*! - * first pass returned zero, this means the file format was wrong - */ - throw mrmc::exceptions::wrong_file_format(); - return NULL; - } + /* + * if first pass returned zer, the file format was wrong + */ + if (non_zero == 0) throw mrmc::exceptions::wrong_file_format(); - /*! + /* * perform second pass * * from here on, we already know that the file header is correct */ - char* buf = file.data; sparse::StaticSparseMatrix *sp = NULL; - /*! + /* * read file header, extract number of states */ buf += 7; // skip "STATES " @@ -139,29 +156,27 @@ sparse::StaticSparseMatrix * readTraFile(const char * filename) { pantheios::integer(maxnode + 1), " maxnodes and ", pantheios::integer(non_zero), " Non-Zero-Elements"); - /*! + /* * Creating matrix * Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal * non-zero elements has to be specified (which is non_zero, computed by make_first_pass) */ sp = new sparse::StaticSparseMatrix(maxnode + 1); - if (sp == NULL) - { - /*! - * creating the matrix failed - */ - throw std::bad_alloc(); - return NULL; - } + if (sp == NULL) throw std::bad_alloc(); sp->initialize(non_zero); uint_fast64_t row, col; double val; - /*! + + /* * read all transitions from file */ while (1) { + /* + * read row, col and value. if value == 0.0, we have reached the + * end of the file. + */ row = strtol(buf, &buf, 10); col = strtol(buf, &buf, 10); val = strtod(buf, &buf); @@ -174,7 +189,7 @@ sparse::StaticSparseMatrix * readTraFile(const char * filename) { sp->addNextValue(row,col,val); } - /*! + /* * clean up */ pantheios::log_DEBUG("Finalizing Matrix"); @@ -183,5 +198,4 @@ sparse::StaticSparseMatrix * readTraFile(const char * filename) { } } //namespace parser - } //namespace mrmc diff --git a/src/parser/readTraFile.h b/src/parser/readTraFile.h index c4b025a64..629acde67 100644 --- a/src/parser/readTraFile.h +++ b/src/parser/readTraFile.h @@ -1,19 +1,16 @@ -/* - * read_tra_file.h - * - * Created on: 15.08.2012 - * Author: Thomas Heinemann - */ - #pragma once #include "src/sparse/static_sparse_matrix.h" namespace mrmc { - namespace parser { +namespace parser { - mrmc::sparse::StaticSparseMatrix * readTraFile(const char * filename); +/*! + * @brief Load transition system from file and return initialized + * StaticSparseMatrix object. + */ +mrmc::sparse::StaticSparseMatrix * readTraFile(const char * filename); - } -} +} // namespace parser +} // namespace mrmc