From 65763c29f15898bd5b33d215cb6e2ef5d9edd82a Mon Sep 17 00:00:00 2001 From: Thomas Heinemann Date: Mon, 17 Sep 2012 14:40:28 +0200 Subject: [PATCH] Restructured labeling class (map does not directly point to the Atomic_proposition objects any longer) Adapted labeling parser to work with declaration lines longer than BUFFER_SIZE bytes. With credits to Philipp :-) --- src/dtmc/labeling.h | 50 +++++++++++------ src/parser/read_lab_file.cpp | 78 ++++++++++++++++++++++----- test/parser/read_lab_file_test.cpp | 87 +++++++++++++++--------------- 3 files changed, 143 insertions(+), 72 deletions(-) diff --git a/src/dtmc/labeling.h b/src/dtmc/labeling.h index f236bfaa4..56db09aeb 100644 --- a/src/dtmc/labeling.h +++ b/src/dtmc/labeling.h @@ -26,6 +26,9 @@ #include +#include +#include + namespace mrmc { namespace dtmc { @@ -35,25 +38,40 @@ class labeling { public: - labeling(const uint_fast32_t p_nodes) { - nodes = p_nodes; + 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 (int i = 0; i < proposition_count; ++i) { + propositions[i] = new AtomicProposition(node_count); + } } virtual ~labeling() { //deleting all the labeling vectors in the map. MAP::iterator it; - for (it = proposition_map.begin(); it != proposition_map.end(); ++it) { - if (it->second != NULL) { - delete (it->second); - } + for (int i = 0; i < proposition_count; ++i) { + delete propositions[i]; + propositions[i] = NULL; } + delete[] propositions; + propositions = NULL; } - void addProposition(std::string proposition) { + uint_fast32_t addProposition(std::string proposition) { if (proposition_map.count(proposition) != 0) { throw std::out_of_range("Proposition does already exist."); } - proposition_map[proposition] = new AtomicProposition(nodes); + 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; } bool containsProposition(std::string proposition) { @@ -66,15 +84,14 @@ class labeling { if (proposition_map.count(proposition) == 0) { throw std::out_of_range("Proposition does not exist."); } - if (node >= nodes) { + if (node >= node_count) { throw std::out_of_range("Node number out of range"); } - AtomicProposition* prop = (proposition_map[proposition]); - prop->addLabelToNode(node); + propositions[proposition_map[proposition]]->addLabelToNode(node); } bool nodeHasProposition(std::string proposition, const uint_fast32_t node) { - return proposition_map[proposition]->hasNodeLabel(node); + return propositions[proposition_map[proposition]]->hasNodeLabel(node); } uint_fast32_t getNumberOfPropositions() { @@ -82,14 +99,13 @@ class labeling { } AtomicProposition* getProposition(std::string proposition) { - return (proposition_map[proposition]); + return (propositions[proposition_map[proposition]]); } private: - uint_fast32_t nodes; - MAP proposition_map; - //AtomicProposition** propositions; - //boost::unordered_map proposition_map; + uint_fast32_t node_count, proposition_count, propositions_current; + MAP proposition_map; + AtomicProposition** propositions; }; } //namespace dtmc diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp index 3a8c7244d..85547d7ad 100644 --- a/src/parser/read_lab_file.cpp +++ b/src/parser/read_lab_file.cpp @@ -16,6 +16,9 @@ #include #include +#include +#include + namespace mrmc { @@ -37,6 +40,10 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename) * Thread-safety is ensured by using strtok_r instead of strtok. */ FILE *P; + + //TODO (Thomas Heinemann): handle files with lines that are longer than BUFFER_SIZE + //TODO (Thomas Heinemann): Throw errors if fgets return NULL in the declaration. + char s[BUFFER_SIZE]; //String buffer char *saveptr = NULL; //Buffer for strtok_r char sep[] = " \n\t"; //Separators for the tokens @@ -44,39 +51,85 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename) P = fopen(filename, "r"); if (P == NULL) { + pantheios::log_ERROR("File could not be opened."); throw mrmc::exceptions::file_IO_exception(); } if (fgets(s, BUFFER_SIZE, P)) { if (strcmp(s, "#DECLARATION\n")) { fclose(P); + pantheios::log_ERROR("Wrong declaration section (\"#DECLARATION\" missing)."); throw mrmc::exceptions::wrong_file_format(); } } - mrmc::dtmc::labeling* result = new mrmc::dtmc::labeling(node_count); - //Here, all propositions are to be declared... - if (fgets(s, BUFFER_SIZE, P)) { - char * proposition; - for (proposition = strtok_r(s, sep, &saveptr); - proposition != NULL; - proposition = strtok_r(NULL, sep, &saveptr)) { - result -> addProposition(proposition); + uint_fast32_t buffer_size_count = 1; + uint_fast32_t buffer_start = 0; + char* decl_buffer = new char[buffer_size_count*BUFFER_SIZE]; + bool need_next_iteration = true; + + do { + decl_buffer[buffer_size_count*BUFFER_SIZE - 1] = '\xff'; + if (fgets(decl_buffer + buffer_start, buffer_size_count*BUFFER_SIZE - buffer_start, P)) { + if ((decl_buffer[buffer_size_count*BUFFER_SIZE - 1] != '\xff') && + (decl_buffer[buffer_size_count*BUFFER_SIZE - 2] != '\n')) { + //fgets changed the last bit -> read string has maximum length + //AND line is longer than size of decl_buffer + char* temp_buffer = decl_buffer; + decl_buffer = NULL; + + buffer_size_count++; + decl_buffer = new char[buffer_size_count*BUFFER_SIZE]; + + buffer_start = (buffer_size_count - 1) * BUFFER_SIZE; + + memcpy(decl_buffer, temp_buffer, buffer_start - 1); + delete[] temp_buffer; + } else { + need_next_iteration = false; + } + } else { + pantheios::log_ERROR("EOF in the declaration section"); + throw mrmc::exceptions::wrong_file_format(); } - } else { - fclose(P); - delete result; - throw mrmc::exceptions::wrong_file_format(); + } while (need_next_iteration); + + uint_fast32_t proposition_count = 0; + char * proposition; + int pos = 0; + + if (decl_buffer[pos] != ' ' && decl_buffer[pos] != '\t' && decl_buffer[pos] != '\0') { + proposition_count++; + } + + while (decl_buffer[pos] != '\0') { + if ((decl_buffer[pos] == ' ' || decl_buffer[pos] == '\t') && + (decl_buffer[pos + 1] != ' ' && decl_buffer[pos + 1] != '\t' && decl_buffer[pos + 1] != '\0')) { + proposition_count++; + } + pos++; } + mrmc::dtmc::labeling* result = new mrmc::dtmc::labeling(node_count, proposition_count); + + //Here, all propositions are to be declared... + for (proposition = strtok_r(decl_buffer, sep, &saveptr); + proposition != NULL; + proposition = strtok_r(NULL, sep, &saveptr)) { + result -> addProposition(proposition); + } + + + saveptr = NULL; //resetting save pointer for strtok_r if (fgets(s, BUFFER_SIZE, P)) { if (strcmp(s, "#END\n")) { fclose(P); delete result; + pantheios::log_ERROR("Wrong declaration section (\"#END\" missing)."); throw mrmc::exceptions::wrong_file_format(); } } @@ -91,6 +144,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename) if (sscanf(token, "%u", &node) == 0) { fclose(P); delete result; + pantheios::log_ERROR("Line assigning propositions does not start with a node number."); throw mrmc::exceptions::wrong_file_format(); } do { diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/read_lab_file_test.cpp index bee571f4a..9a614355e 100644 --- a/test/parser/read_lab_file_test.cpp +++ b/test/parser/read_lab_file_test.cpp @@ -18,62 +18,62 @@ TEST(ReadLabFileTest, NonExistingFileTest) { TEST(ReadLabFileTest, ParseTest) { //This test is based on a test case from the original MRMC. - mrmc::dtmc::labeling* labelling; + mrmc::dtmc::labeling* labeling; //Parsing the file - ASSERT_NO_THROW(labelling = mrmc::parser::read_lab_file(12,"test/parser/lab_files/pctl_general_input_01.lab")); + ASSERT_NO_THROW(labeling = mrmc::parser::read_lab_file(12,"test/parser/lab_files/pctl_general_input_01.lab")); //Checking whether all propositions are in the labelling char phi[] = "phi", psi[] = "psi", smth[] = "smth"; - ASSERT_TRUE(labelling->containsProposition(phi)); - ASSERT_TRUE(labelling->containsProposition(psi)); - ASSERT_TRUE(labelling->containsProposition(smth)); + ASSERT_TRUE(labeling->containsProposition(phi)); + ASSERT_TRUE(labeling->containsProposition(psi)); + ASSERT_TRUE(labeling->containsProposition(smth)); //Testing whether all and only the correct nodes are labeled with "phi" - ASSERT_TRUE(labelling->nodeHasProposition(phi,1)); - ASSERT_TRUE(labelling->nodeHasProposition(phi,2)); - ASSERT_TRUE(labelling->nodeHasProposition(phi,3)); - ASSERT_TRUE(labelling->nodeHasProposition(phi,5)); - ASSERT_TRUE(labelling->nodeHasProposition(phi,7)); - ASSERT_TRUE(labelling->nodeHasProposition(phi,9)); - ASSERT_TRUE(labelling->nodeHasProposition(phi,10)); - ASSERT_TRUE(labelling->nodeHasProposition(phi,11)); - - ASSERT_FALSE(labelling->nodeHasProposition(phi,4)); - ASSERT_FALSE(labelling->nodeHasProposition(phi,6)); + ASSERT_TRUE(labeling->nodeHasProposition(phi,1)); + ASSERT_TRUE(labeling->nodeHasProposition(phi,2)); + ASSERT_TRUE(labeling->nodeHasProposition(phi,3)); + ASSERT_TRUE(labeling->nodeHasProposition(phi,5)); + ASSERT_TRUE(labeling->nodeHasProposition(phi,7)); + ASSERT_TRUE(labeling->nodeHasProposition(phi,9)); + ASSERT_TRUE(labeling->nodeHasProposition(phi,10)); + ASSERT_TRUE(labeling->nodeHasProposition(phi,11)); + + ASSERT_FALSE(labeling->nodeHasProposition(phi,4)); + ASSERT_FALSE(labeling->nodeHasProposition(phi,6)); //Testing whether all and only the correct nodes are labeled with "psi" - ASSERT_TRUE(labelling->nodeHasProposition(psi,6)); - ASSERT_TRUE(labelling->nodeHasProposition(psi,7)); - ASSERT_TRUE(labelling->nodeHasProposition(psi,8)); - - ASSERT_FALSE(labelling->nodeHasProposition(psi,1)); - ASSERT_FALSE(labelling->nodeHasProposition(psi,2)); - ASSERT_FALSE(labelling->nodeHasProposition(psi,3)); - ASSERT_FALSE(labelling->nodeHasProposition(psi,4)); - ASSERT_FALSE(labelling->nodeHasProposition(psi,5)); - ASSERT_FALSE(labelling->nodeHasProposition(psi,9)); - ASSERT_FALSE(labelling->nodeHasProposition(psi,10)); - ASSERT_FALSE(labelling->nodeHasProposition(psi,11)); + ASSERT_TRUE(labeling->nodeHasProposition(psi,6)); + ASSERT_TRUE(labeling->nodeHasProposition(psi,7)); + ASSERT_TRUE(labeling->nodeHasProposition(psi,8)); + + ASSERT_FALSE(labeling->nodeHasProposition(psi,1)); + ASSERT_FALSE(labeling->nodeHasProposition(psi,2)); + ASSERT_FALSE(labeling->nodeHasProposition(psi,3)); + ASSERT_FALSE(labeling->nodeHasProposition(psi,4)); + ASSERT_FALSE(labeling->nodeHasProposition(psi,5)); + ASSERT_FALSE(labeling->nodeHasProposition(psi,9)); + ASSERT_FALSE(labeling->nodeHasProposition(psi,10)); + ASSERT_FALSE(labeling->nodeHasProposition(psi,11)); //Testing whether all and only the correct nodes are labeled with "smth" - ASSERT_TRUE(labelling->nodeHasProposition(smth,4)); - ASSERT_TRUE(labelling->nodeHasProposition(smth,5)); - - ASSERT_FALSE(labelling->nodeHasProposition(smth,1)); - ASSERT_FALSE(labelling->nodeHasProposition(smth,2)); - ASSERT_FALSE(labelling->nodeHasProposition(smth,3)); - ASSERT_FALSE(labelling->nodeHasProposition(smth,6)); - ASSERT_FALSE(labelling->nodeHasProposition(smth,7)); - ASSERT_FALSE(labelling->nodeHasProposition(smth,8)); - ASSERT_FALSE(labelling->nodeHasProposition(smth,9)); - ASSERT_FALSE(labelling->nodeHasProposition(smth,10)); - ASSERT_FALSE(labelling->nodeHasProposition(smth,11)); - - //Deleting the labelling - delete labelling; + ASSERT_TRUE(labeling->nodeHasProposition(smth,4)); + ASSERT_TRUE(labeling->nodeHasProposition(smth,5)); + + ASSERT_FALSE(labeling->nodeHasProposition(smth,1)); + ASSERT_FALSE(labeling->nodeHasProposition(smth,2)); + ASSERT_FALSE(labeling->nodeHasProposition(smth,3)); + ASSERT_FALSE(labeling->nodeHasProposition(smth,6)); + ASSERT_FALSE(labeling->nodeHasProposition(smth,7)); + ASSERT_FALSE(labeling->nodeHasProposition(smth,8)); + ASSERT_FALSE(labeling->nodeHasProposition(smth,9)); + ASSERT_FALSE(labeling->nodeHasProposition(smth,10)); + ASSERT_FALSE(labeling->nodeHasProposition(smth,11)); + + //Deleting the labeling + delete labeling; } TEST(ReadLabFileTest, WrongHeaderTest1) { @@ -87,3 +87,4 @@ TEST(ReadLabFileTest, WrongHeaderTest2) { TEST(ReadLabFileTest, WrongPropositionTest) { ASSERT_THROW(mrmc::parser::read_lab_file(3,"test/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::wrong_file_format); } +