From a0e07c202200144d0c71c13231d48d4de0bc48bf Mon Sep 17 00:00:00 2001 From: Thomas Heinemann Date: Thu, 13 Sep 2012 15:06:11 +0200 Subject: [PATCH] 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 | 31 +++++++- src/dtmc/labelling.h | 85 +++++++++++++++++++++ src/parser/parser.h | 15 ++++ src/parser/read_lab_file.cpp | 116 +++++++++++++++++++++++++++++ src/parser/read_lab_file.h | 23 ++++++ src/parser/read_tra_file.cpp | 18 +++-- test/parser/read_lab_file_test.cpp | 77 +++++++++++++++++++ test/parser/read_tra_file_test.cpp | 8 +- 8 files changed, 357 insertions(+), 16 deletions(-) create mode 100644 src/dtmc/labelling.h create mode 100644 src/parser/parser.h create mode 100644 src/parser/read_lab_file.cpp create mode 100644 src/parser/read_lab_file.h create mode 100644 test/parser/read_lab_file_test.cpp diff --git a/src/dtmc/atomic_proposition.h b/src/dtmc/atomic_proposition.h index 50f12fda3..19acc9e16 100644 --- a/src/dtmc/atomic_proposition.h +++ b/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 { @@ -22,18 +24,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() { - delete[] node_array; + 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) { diff --git a/src/dtmc/labelling.h b/src/dtmc/labelling.h new file mode 100644 index 000000000..742b44e46 --- /dev/null +++ b/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 + +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::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 proposition_map; +}; + +} //namespace dtmc + +} //namespace mrmc + +#endif /* MRMC_DTMC_LABELLING_H_ */ diff --git a/src/parser/parser.h b/src/parser/parser.h new file mode 100644 index 000000000..2ebefdb9d --- /dev/null +++ b/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_ */ diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp new file mode 100644 index 000000000..27da49622 --- /dev/null +++ b/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 +#include +#include + + +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 diff --git a/src/parser/read_lab_file.h b/src/parser/read_lab_file.h new file mode 100644 index 000000000..f4a2d0077 --- /dev/null +++ b/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_ */ diff --git a/src/parser/read_tra_file.cpp b/src/parser/read_tra_file.cpp index 4fec19a43..6056db8cf 100644 --- a/src/parser/read_tra_file.cpp +++ b/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 * read_tra_file(const char * filename) { FILE *p = NULL; - char s[1024]; + char s[BUFFER_SIZE]; uint_fast32_t rows, non_zero; sparse::StaticSparseMatrix *sp = NULL; @@ -105,7 +107,7 @@ sparse::StaticSparseMatrix * 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 * 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 * 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; diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/read_lab_file_test.cpp new file mode 100644 index 000000000..e7fa6bcb9 --- /dev/null +++ b/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; +} diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/read_tra_file_test.cpp index 39b501bca..ddf83b4ce 100644 --- a/test/parser/read_tra_file_test.cpp +++ b/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 *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); }