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

@@ -26,6 +26,9 @@
 
 #include <stdexcept>
 
+#include <pantheios/pantheios.hpp>
+#include <pantheios/inserters/integer.hpp>
+
 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<std::string, AtomicProposition*>::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<std::string, AtomicProposition*> proposition_map;
-      //AtomicProposition** propositions;
-      //boost::unordered_map<std::string, AtomicProposition*> proposition_map;
+      uint_fast32_t node_count, proposition_count, propositions_current;
+      MAP<std::string, uint_fast32_t> proposition_map;
+      AtomicProposition** propositions;
 };
 
 } //namespace dtmc

src/parser/read_lab_file.cpp

@@ -16,6 +16,9 @@
 #include <cstdlib>
 #include <cstdio>
 
+#include <pantheios/pantheios.hpp>
+#include <pantheios/inserters/integer.hpp>
+
 
 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,32 +51,77 @@ 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)) {
+   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();
+      }
+   } while (need_next_iteration);
+
+   uint_fast32_t proposition_count = 0;
    char * proposition;
-      for (proposition = strtok_r(s, sep, &saveptr);
+   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);
    }
-   } else {
-      fclose(P);
-      delete result;
-      throw mrmc::exceptions::wrong_file_format();
-   }
+
+
 
    saveptr = NULL;                        //resetting save pointer for strtok_r
 
@@ -77,6 +129,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
       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 {

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);
 }
+