Parser for labelling files including new data structure managing

different atomic propositions.
(Works now as node_array attribute of class Atomic_proposition is now
always instantiated with 0)

src/dtmc/atomic_proposition.h

@@ -12,6 +12,8 @@
 #include "src/exceptions/invalid_argument.h"
 #include "src/exceptions/out_of_range.h"
 
+
+
 namespace mrmc {
 
 namespace dtmc {
@@ -23,18 +25,39 @@ 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_count = nodeCount;
-		node_array = new uint_fast64_t[(int) std::ceil(nodeCount / 64)]();
+	   node_array = NULL;
+	   initialize(nodeCount);
 	}
 
 	~AtomicProposition() {
+	   if (node_array != NULL) {
 	      delete[] node_array;
 	   }
+	}
+
+	void initialize(uint_fast32_t nodeCount) {
+	   if (node_array == NULL) {
+	      node_count = nodeCount;
+	      node_array = new uint_fast64_t[(int) std::ceil(nodeCount / 64)]();
+	      if (node_array == NULL) {
+	         throw std::bad_alloc();
+	      }
+	   }
+
+	}
 
 	bool hasNodeLabel(uint_fast32_t nodeId) {
 		int bucket = static_cast<int>(std::floor(nodeId / 64));

src/dtmc/labelling.h

@@ -0,0 +1,85 @@
+/*
+ * labelling.h
+ *
+ *  Created on: 10.09.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef MRMC_DTMC_LABELLING_H_
+#define MRMC_DTMC_LABELLING_H_
+
+#include "atomic_proposition.h"
+
+#include "boost/unordered_map.hpp"
+
+#include <stdexcept>
+
+namespace mrmc {
+
+namespace dtmc {
+
+
+class labelling {
+   public:
+
+
+      labelling(const uint_fast32_t p_nodes) {
+         nodes = p_nodes;
+      }
+
+      virtual ~labelling() {
+         //deleting all the labelling vectors in the map.
+         boost::unordered_map<std::string, AtomicProposition*>::iterator it;
+         for (it = proposition_map.begin(); it != proposition_map.end(); ++it) {
+            if (it->second != NULL) {
+               delete (it->second);
+            }
+         }
+      }
+
+      void 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);
+      }
+
+      bool containsProposition(std::string proposition) {
+         return (proposition_map.count(proposition) != 0);
+      }
+
+
+      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 >= nodes) {
+            throw std::out_of_range("Node number out of range");
+         }
+         AtomicProposition* prop = (proposition_map[proposition]);
+         prop->addLabelToNode(node);
+      }
+
+      bool nodeHasProposition(std::string proposition, const uint_fast32_t node) {
+         return proposition_map[proposition]->hasNodeLabel(node);
+      }
+
+      uint_fast32_t getNumberOfPropositions() {
+         return proposition_map.size();
+      }
+
+      AtomicProposition* getProposition(std::string proposition) {
+         return (proposition_map[proposition]);
+      }
+
+   private:
+      uint_fast32_t nodes;
+      boost::unordered_map<std::string, AtomicProposition*> proposition_map;
+};
+
+} //namespace dtmc
+
+} //namespace mrmc
+
+#endif /* MRMC_DTMC_LABELLING_H_ */

src/parser/parser.h

@@ -0,0 +1,15 @@
+/*
+ * parser.h
+ *
+ *  Created on: 12.09.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef PARSER_H_
+#define PARSER_H_
+
+#include "boost/integer/integer_mask.hpp"
+
+const uint_fast32_t BUFFER_SIZE=1024;
+
+#endif /* PARSER_H_ */

src/parser/read_lab_file.cpp

@@ -0,0 +1,116 @@
+/*
+ * read_lab_file.cpp
+ *
+ *  Created on: 10.09.2012
+ *      Author: Thomas Heinemann
+ */
+
+#include "parser.h"
+
+#include "read_lab_file.h"
+
+#include "src/dtmc/labelling.h"
+
+#include "src/exceptions/wrong_file_format.h"
+#include "src/exceptions/file_IO_exception.h"
+
+#include <cstring>
+#include <cstdlib>
+#include <cstdio>
+
+
+namespace mrmc {
+
+namespace parser {
+
+
+/*!
+ * Reads a .lab file and puts the result in a labelling structure.
+ * @param node_count the number of states.
+ * @param filename   input .lab file's name.
+ * @return returns a pointer to a labelling object.
+ */
+mrmc::dtmc::labelling * 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.
+    * However, as only the result of its tokenization is used, this is not a problem.
+    *
+    * Thread-safety is ensured by using strtok_r instead of strtok.
+    */
+   FILE *P;
+   char s[BUFFER_SIZE];              //String buffer
+   char *saveptr = NULL;             //Buffer for strtok_r
+   char sep[] = " \n\t";             //Separators for the tokens
+
+   P = fopen(filename, "r");
+
+   if (P == NULL) {
+      throw mrmc::exceptions::file_IO_exception();
+   }
+
+   if (fgets(s, BUFFER_SIZE, P)) {
+      if (strcmp(s, "#DECLARATION\n")) {
+         fclose(P);
+         throw mrmc::exceptions::wrong_file_format();
+      }
+   }
+
+
+   mrmc::dtmc::labelling* result = new mrmc::dtmc::labelling(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);
+      }
+   } else {
+      fclose(P);
+      delete result;
+      throw mrmc::exceptions::wrong_file_format();
+   }
+
+   saveptr = NULL;                        //resetting save pointer for strtok_r
+
+   if (fgets(s, BUFFER_SIZE, P)) {
+      if (strcmp(s, "#END\n")) {
+         fclose(P);
+         delete result;
+         throw mrmc::exceptions::wrong_file_format();
+      }
+   }
+
+   while (fgets(s, BUFFER_SIZE, P)) {
+      char * token = NULL;
+      uint_fast32_t node = 0;
+      /* First token has to be a number identifying the node,
+       * hence it is treated differently from the other tokens.
+       */
+      token = strtok_r(s, sep, &saveptr);
+      if (sscanf(token, "%u", &node) == 0) {
+         fclose(P);
+         delete result;
+         throw mrmc::exceptions::wrong_file_format();
+      }
+      do {
+         token = strtok_r(NULL, sep, &saveptr);
+         if (token == NULL) {
+            break;
+         }
+         result->addLabelToNode(token, node);
+      } while (token != NULL);
+
+   }
+
+   fclose(P);
+
+   return result;
+
+}
+
+} //namespace parser
+
+} //namespace mrmc

src/parser/read_lab_file.h

@@ -0,0 +1,23 @@
+/*
+ * read_lab_file.h
+ *
+ *  Created on: 10.09.2012
+ *      Author: thomas
+ */
+
+#ifndef READ_LAB_FILE_H_
+#define READ_LAB_FILE_H_
+
+#include "src/dtmc/labelling.h"
+
+
+namespace mrmc {
+
+namespace parser {
+
+mrmc::dtmc::labelling * read_lab_file(int node_count, const char * filename);
+
+}
+}
+
+#endif /* READ_LAB_FILE_H_ */

src/parser/read_tra_file.cpp

@@ -9,6 +9,8 @@
  *      Author: Thomas Heinemann
  */
 
+#include "parser.h"
+
 #include "src/parser/read_tra_file.h"
 #include "src/exceptions/file_IO_exception.h"
 #include "src/exceptions/wrong_file_format.h"
@@ -43,11 +45,11 @@ static uint_fast32_t make_first_pass(FILE* p) {
       pantheios::log_ERROR("make_first_pass was called with NULL! (SHOULD NEVER HAPPEN)");
       throw exceptions::file_IO_exception ("make_first_pass: File not readable (this should be checked before calling this function!)");
    }
-   char s[1024];                 //String buffer
+   char s[BUFFER_SIZE];                 //String buffer
    uint_fast32_t rows=0, non_zero=0;
 
    //Reading No. of states
-   if (fgets(s, 1024, p) != NULL) {
+   if (fgets(s, BUFFER_SIZE, p) != NULL) {
       if (sscanf( s, "STATES %d", &rows) == 0) {
          pantheios::log_WARNING(pantheios::integer(rows));
          (void)fclose(p);
@@ -56,7 +58,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
    }
 
    //Reading No. of transitions
-   if (fgets(s, 1024, p) != NULL) {
+   if (fgets(s, BUFFER_SIZE, p) != NULL) {
       if (sscanf( s, "TRANSITIONS %d", &non_zero) == 0) {
          (void)fclose(p);
          throw mrmc::exceptions::wrong_file_format();
@@ -65,7 +67,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
 
    //Reading transitions (one per line)
    //And increase number of transitions
-   while (NULL != fgets( s, 1024, p ))
+   while (NULL != fgets( s, BUFFER_SIZE, p ))
    {
       uint_fast32_t row=0, col=0;
       double val=0.0;
@@ -90,7 +92,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
 
 sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
    FILE *p = NULL;
-   char s[1024];
+   char s[BUFFER_SIZE];
    uint_fast32_t rows, non_zero;
    sparse::StaticSparseMatrix<double> *sp = NULL;
 
@@ -105,7 +107,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
    rewind(p);
 
    //Reading No. of states
-   if (fgets(s, 1024, p) != NULL) {
+   if (fgets(s, BUFFER_SIZE, p) != NULL) {
       if (sscanf( s, "STATES %d", &rows) == 0) {
          pantheios::log_WARNING(pantheios::integer(rows));
          (void)fclose(p);
@@ -117,7 +119,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
     * Note that the result is not used in this function as make_first_pass()
     * computes the relevant number (non_zero)
     */
-   if (fgets(s, 1024, p) != NULL) {
+   if (fgets(s, BUFFER_SIZE, p) != NULL) {
       uint_fast32_t nnz=0;
       if (sscanf( s, "TRANSITIONS %d", &nnz) == 0) {
          (void)fclose(p);
@@ -140,7 +142,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
       }
 
    //Reading transitions (one per line) and saving the results in the matrix
-   while (NULL != fgets( s, 1024, p ))
+   while (NULL != fgets( s, BUFFER_SIZE, p ))
    {
       uint_fast32_t row=0, col=0;
       double val = 0.0;

test/parser/read_lab_file_test.cpp

@@ -0,0 +1,77 @@
+/*
+ * read_lab_file_test.cpp
+ *
+ *  Created on: 12.09.2012
+ *      Author: Thomas Heinemann
+ */
+
+#include "gtest/gtest.h"
+#include "src/dtmc/labelling.h"
+#include "src/parser/read_lab_file.h"
+#include "src/exceptions/file_IO_exception.h"
+#include "src/exceptions/wrong_file_format.h"
+
+TEST(ReadLabFileTest, NonExistingFileTest) {
+   //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
+   ASSERT_THROW(mrmc::parser::read_lab_file(0,"nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
+}
+
+TEST(ReadLabFileTest, ParseTest) {
+   //This test is based on a testcase from the original MRMC.
+   mrmc::dtmc::labelling* labelling;
+
+   //Parsing the file
+   ASSERT_NO_THROW(labelling = 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));
+
+   //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));
+
+   //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));
+
+   //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;
+}

test/parser/read_tra_file_test.cpp

@@ -23,7 +23,7 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
 TEST(ReadTraFileTest, ParseFileTest1) {
    pantheios::log_INFORMATIONAL("Started ParseFileTest1");
    mrmc::sparse::StaticSparseMatrix<double> *result;
-   ASSERT_NO_THROW(result = mrmc::parser::read_tra_file("test/parser/csl_general_input_01.tra"));
+   ASSERT_NO_THROW(result = mrmc::parser::read_tra_file("test/parser/tra_files/csl_general_input_01.tra"));
 
    double val = 0;
    ASSERT_TRUE(result->getValue(1,1,&val));
@@ -65,17 +65,17 @@ TEST(ReadTraFileTest, ParseFileTest1) {
 TEST(ReadTraFileTest, WrongFormatTestHeader1) {
    pantheios::log_INFORMATIONAL("Started WrongFormatTestHeader1");
 
-   ASSERT_THROW(mrmc::parser::read_tra_file("test/parser/wrong_format_header1.tra"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::read_tra_file("test/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::wrong_file_format);
 }
 
 TEST(ReadTraFileTest, WrongFormatTestHeader2) {
    pantheios::log_INFORMATIONAL("Started WrongFormatTestHeader2");
 
-   ASSERT_THROW(mrmc::parser::read_tra_file("test/parser/wrong_format_header2.tra"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::read_tra_file("test/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::wrong_file_format);
 }
 
 TEST(ReadTraFileTest, WrongFormatTestTransition) {
    pantheios::log_INFORMATIONAL("Started WrongFormatTestTransition");
 
-   ASSERT_THROW(mrmc::parser::read_tra_file("test/parser/wrong_format_transition.tra"), mrmc::exceptions::wrong_file_format);
+   ASSERT_THROW(mrmc::parser::read_tra_file("test/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::wrong_file_format);
 }