Browse Source

porting LabParser and TraParser from c-style API to class API

tempestpy_adaptions
gereon 12 years ago
parent
commit
f960e20e53
  1. 6
      src/mrmc.cpp
  2. 4
      src/parser/parser.cpp
  3. 24
      src/parser/parser.h
  4. 12
      src/parser/readLabFile.cpp
  5. 14
      src/parser/readLabFile.h
  6. 19
      src/parser/readTraFile.cpp
  7. 19
      src/parser/readTraFile.h
  8. 13
      src/utility/utility.cpp
  9. 15
      test/parser/read_lab_file_test.cpp
  10. 13
      test/parser/read_tra_file_test.cpp

6
src/mrmc.cpp

@ -91,9 +91,9 @@ int main(const int argc, const char* argv[]) {
LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console."); LOG4CPLUS_INFO(logger, "Enable verbose mode, log output gets printed to console.");
} }
mrmc::storage::SquareSparseMatrix<double>* probMatrix = mrmc::parser::readTraFile(s->getString("trafile").c_str());
mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::readLabFile(probMatrix->getRowCount(), s->getString("labfile").c_str());
mrmc::models::Dtmc<double> dtmc(probMatrix, labeling);
mrmc::parser::TraParser traparser(s->getString("trafile").c_str());
mrmc::parser::LabParser labparser(traparser.getMatrix()->getRowCount(), s->getString("labfile").c_str());
mrmc::models::Dtmc<double> dtmc(traparser.getMatrix(), labparser.getLabeling());
dtmc.printModelInformationToStream(std::cout); dtmc.printModelInformationToStream(std::cout);

4
src/parser/parser.cpp

@ -29,7 +29,7 @@ extern log4cplus::Logger logger;
* @param end New pointer will be written there * @param end New pointer will be written there
* @return Result of strtol() * @return Result of strtol()
*/ */
uint_fast64_t mrmc::parser::checked_strtol(const char* str, char** end)
uint_fast64_t mrmc::parser::Parser::checked_strtol(const char* str, char** end)
{ {
uint_fast64_t res = strtol(str, end, 10); uint_fast64_t res = strtol(str, end, 10);
if (str == *end) if (str == *end)
@ -47,7 +47,7 @@ uint_fast64_t mrmc::parser::checked_strtol(const char* str, char** end)
* @param buf String buffer * @param buf String buffer
* @return pointer to first non-whitespace character * @return pointer to first non-whitespace character
*/ */
char* mrmc::parser::skipWS(char* buf)
char* mrmc::parser::Parser::skipWS(char* buf)
{ {
while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++; while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++;
return buf; return buf;

24
src/parser/parser.h

@ -34,16 +34,6 @@ namespace mrmc {
*/ */
namespace parser { namespace parser {
/*!
* @brief Parses integer and checks, if something has been parsed.
*/
uint_fast64_t checked_strtol(const char* str, char** end);
/*!
* @brief Skips common whitespaces in a string.
*/
char* skipWS(char* buf);
/*! /*!
* @brief Opens a file and maps it to memory providing a char* * @brief Opens a file and maps it to memory providing a char*
* containing the file content. * containing the file content.
@ -110,6 +100,20 @@ namespace parser {
*/ */
~MappedFile(); ~MappedFile();
}; };
class Parser
{
protected:
/*!
* @brief Parses integer and checks, if something has been parsed.
*/
uint_fast64_t checked_strtol(const char* str, char** end);
/*!
* @brief Skips common whitespaces in a string.
*/
char* skipWS(char* buf);
};
} // namespace parser } // namespace parser
} // namespace mrmc } // namespace mrmc

12
src/parser/readLabFile.cpp

@ -45,7 +45,7 @@ namespace parser {
* @param filename input .lab file's name. * @param filename input .lab file's name.
* @return The pointer to the created labeling object. * @return The pointer to the created labeling object.
*/ */
mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename)
LabParser::LabParser(uint_fast64_t node_count, const char * filename)
{ {
/* /*
* open file * open file
@ -105,7 +105,7 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count,
/* /*
* create labeling object with given node and proposition count * create labeling object with given node and proposition count
*/ */
mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
this->labeling = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
/* /*
* second run: add propositions and node labels to labeling * second run: add propositions and node labels to labeling
@ -135,7 +135,7 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count,
if (strncmp(buf, "#END", cnt) == 0) break; if (strncmp(buf, "#END", cnt) == 0) break;
strncpy(proposition, buf, cnt); strncpy(proposition, buf, cnt);
proposition[cnt] = '\0'; proposition[cnt] = '\0';
result->addAtomicProposition(proposition);
this->labeling->addAtomicProposition(proposition);
} }
else cnt = 1; // next char is separator, one step forward else cnt = 1; // next char is separator, one step forward
} while (cnt > 0); } while (cnt > 0);
@ -178,19 +178,17 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count,
else else
{ {
/* /*
* copy proposition to buffer and add it to result
* copy proposition to buffer and add it to labeling
*/ */
strncpy(proposition, buf, cnt); strncpy(proposition, buf, cnt);
proposition[cnt] = '\0'; proposition[cnt] = '\0';
result->addAtomicPropositionToState(proposition, node);
this->labeling->addAtomicPropositionToState(proposition, node);
buf += cnt; buf += cnt;
} }
} }
buf = skipWS(buf); buf = skipWS(buf);
} }
} }
return result;
} }
} //namespace parser } //namespace parser

14
src/parser/readLabFile.h

@ -4,6 +4,7 @@
#include "src/models/AtomicPropositionsLabeling.h" #include "src/models/AtomicPropositionsLabeling.h"
#include "boost/integer/integer_mask.hpp" #include "boost/integer/integer_mask.hpp"
#include "src/parser/parser.h"
namespace mrmc { namespace mrmc {
namespace parser { namespace parser {
@ -11,7 +12,18 @@ namespace parser {
/*! /*!
* @brief Load label file and return initialized AtomicPropositionsLabeling object. * @brief Load label file and return initialized AtomicPropositionsLabeling object.
*/ */
mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename);
class LabParser : Parser
{
public:
LabParser(uint_fast64_t node_count, const char* filename);
mrmc::models::AtomicPropositionsLabeling* getLabeling()
{
return this->labeling;
}
private:
mrmc::models::AtomicPropositionsLabeling* labeling;
};
} // namespace parser } // namespace parser
} // namespace mrmc } // namespace mrmc

19
src/parser/readTraFile.cpp

@ -48,7 +48,7 @@ namespace parser{
* @param buf Data to scan. Is expected to be some char array. * @param buf Data to scan. Is expected to be some char array.
* @param maxnode Is set to highest id of all nodes. * @param maxnode Is set to highest id of all nodes.
*/ */
static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
uint_fast32_t TraParser::firstPass(char* buf, uint_fast32_t &maxnode)
{ {
uint_fast32_t non_zero = 0; uint_fast32_t non_zero = 0;
@ -117,7 +117,8 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
* @return a pointer to the created sparse matrix. * @return a pointer to the created sparse matrix.
*/ */
mrmc::storage::SquareSparseMatrix<double> * readTraFile(const char * filename) {
TraParser::TraParser(const char * filename)
{
/* /*
* enforce locale where decimal point is '.' * enforce locale where decimal point is '.'
*/ */
@ -133,7 +134,7 @@ mrmc::storage::SquareSparseMatrix<double> * readTraFile(const char * filename) {
* perform first pass, i.e. count entries that are not zero and not on the diagonal * perform first pass, i.e. count entries that are not zero and not on the diagonal
*/ */
uint_fast32_t maxnode; uint_fast32_t maxnode;
uint_fast32_t non_zero = makeFirstPass(file.data, maxnode);
uint_fast32_t non_zero = this->firstPass(file.data, maxnode);
/* /*
* if first pass returned zero, the file format was wrong * if first pass returned zero, the file format was wrong
*/ */
@ -148,7 +149,6 @@ mrmc::storage::SquareSparseMatrix<double> * readTraFile(const char * filename) {
* *
* from here on, we already know that the file header is correct * from here on, we already know that the file header is correct
*/ */
mrmc::storage::SquareSparseMatrix<double> *sp = NULL;
/* /*
* read file header, extract number of states * read file header, extract number of states
@ -165,13 +165,13 @@ mrmc::storage::SquareSparseMatrix<double> * readTraFile(const char * filename) {
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass) * non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
*/ */
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
sp = new mrmc::storage::SquareSparseMatrix<double>(maxnode + 1);
if (sp == NULL)
this->matrix = new mrmc::storage::SquareSparseMatrix<double>(maxnode + 1);
if (this->matrix == NULL)
{ {
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
throw std::bad_alloc(); throw std::bad_alloc();
} }
sp->initialize(non_zero);
this->matrix->initialize(non_zero);
uint_fast64_t row, col; uint_fast64_t row, col;
double val; double val;
@ -196,15 +196,14 @@ mrmc::storage::SquareSparseMatrix<double> * readTraFile(const char * filename) {
LOG4CPLUS_ERROR(logger, "Found transition probability of " << val << ", but we think probabilities should be from (0,1]."); LOG4CPLUS_ERROR(logger, "Found transition probability of " << val << ", but we think probabilities should be from (0,1].");
throw mrmc::exceptions::wrong_file_format(); throw mrmc::exceptions::wrong_file_format();
} }
sp->addNextValue(row,col,val);
this->matrix->addNextValue(row,col,val);
buf = skipWS(buf); buf = skipWS(buf);
} }
/* /*
* clean up * clean up
*/ */
sp->finalize();
return sp;
this->matrix->finalize();
} }
} //namespace parser } //namespace parser

19
src/parser/readTraFile.h

@ -3,6 +3,8 @@
#include "src/storage/SquareSparseMatrix.h" #include "src/storage/SquareSparseMatrix.h"
#include "src/parser/parser.h"
namespace mrmc { namespace mrmc {
namespace parser { namespace parser {
@ -10,7 +12,22 @@ namespace parser {
* @brief Load transition system from file and return initialized * @brief Load transition system from file and return initialized
* StaticSparseMatrix object. * StaticSparseMatrix object.
*/ */
mrmc::storage::SquareSparseMatrix<double> * readTraFile(const char * filename);
class TraParser : Parser
{
public:
TraParser(const char* filename);
mrmc::storage::SquareSparseMatrix<double>* getMatrix()
{
return this->matrix;
}
private:
mrmc::storage::SquareSparseMatrix<double>* matrix;
uint_fast32_t firstPass(char* buf, uint_fast32_t &maxnode);
};
} // namespace parser } // namespace parser
} // namespace mrmc } // namespace mrmc

13
src/utility/utility.cpp

@ -74,16 +74,13 @@ void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, const char* filename) {
} }
mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file) { mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file) {
mrmc::storage::SquareSparseMatrix<double>* transition_matrix =
mrmc::parser::readTraFile(tra_file);
uint_fast64_t node_count = transition_matrix->getRowCount();
mrmc::parser::TraParser tp(tra_file);
uint_fast64_t node_count = tp.getMatrix()->getRowCount();
mrmc::models::AtomicPropositionsLabeling* labeling =
mrmc::parser::readLabFile(node_count, lab_file);
mrmc::parser::LabParser lp(node_count, lab_file);
mrmc::models::Dtmc<double>* result =
new mrmc::models::Dtmc<double>(transition_matrix, labeling);
return result;
mrmc::models::Dtmc<double>* result = new mrmc::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling());
return result;
} }
} }

15
test/parser/read_lab_file_test.cpp

@ -14,15 +14,17 @@
TEST(ReadLabFileTest, NonExistingFileTest) { TEST(ReadLabFileTest, NonExistingFileTest) {
//No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
ASSERT_THROW(mrmc::parser::readLabFile(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
ASSERT_THROW(mrmc::parser::LabParser(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
} }
TEST(ReadLabFileTest, ParseTest) { TEST(ReadLabFileTest, ParseTest) {
//This test is based on a test case from the original MRMC. //This test is based on a test case from the original MRMC.
mrmc::models::AtomicPropositionsLabeling* labeling = NULL; mrmc::models::AtomicPropositionsLabeling* labeling = NULL;
mrmc::parser::LabParser* parser;
//Parsing the file //Parsing the file
ASSERT_NO_THROW(labeling = mrmc::parser::readLabFile(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
ASSERT_NO_THROW(parser = new mrmc::parser::LabParser(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
labeling = parser->getLabeling();
//Checking whether all propositions are in the labelling //Checking whether all propositions are in the labelling
@ -76,20 +78,21 @@ TEST(ReadLabFileTest, ParseTest) {
//Deleting the labeling //Deleting the labeling
delete labeling; delete labeling;
delete parser;
} else { } else {
FAIL(); FAIL();
} }
} }
TEST(ReadLabFileTest, WrongHeaderTest1) { TEST(ReadLabFileTest, WrongHeaderTest1) {
ASSERT_THROW(mrmc::parser::readLabFile(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::wrong_file_format);
ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::wrong_file_format);
} }
TEST(ReadLabFileTest, WrongHeaderTest2) { TEST(ReadLabFileTest, WrongHeaderTest2) {
ASSERT_THROW(mrmc::parser::readLabFile(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::wrong_file_format);
ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::wrong_file_format);
} }
TEST(ReadLabFileTest, WrongPropositionTest) { TEST(ReadLabFileTest, WrongPropositionTest) {
ASSERT_THROW(mrmc::parser::readLabFile(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::wrong_file_format);
ASSERT_THROW(mrmc::parser::LabParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::wrong_file_format);
} }

13
test/parser/read_tra_file_test.cpp

@ -14,14 +14,16 @@
TEST(ReadTraFileTest, NonExistingFileTest) { TEST(ReadTraFileTest, NonExistingFileTest) {
//No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
ASSERT_THROW(mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
} }
/* The following test case is based on one of the original MRMC test cases /* The following test case is based on one of the original MRMC test cases
*/ */
TEST(ReadTraFileTest, ParseFileTest1) { TEST(ReadTraFileTest, ParseFileTest1) {
mrmc::storage::SquareSparseMatrix<double> *result = NULL; mrmc::storage::SquareSparseMatrix<double> *result = NULL;
ASSERT_NO_THROW(result = mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
mrmc::parser::TraParser* parser;
ASSERT_NO_THROW(parser = new mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
result = parser->getMatrix();
if (result != NULL) { if (result != NULL) {
double val = 0; double val = 0;
@ -62,19 +64,20 @@ TEST(ReadTraFileTest, ParseFileTest1) {
// FIXME: adapt this test case to the new dot-output routines // FIXME: adapt this test case to the new dot-output routines
/* result->toDOTFile("output.dot"); */ /* result->toDOTFile("output.dot"); */
delete result; delete result;
delete parser;
} else { } else {
FAIL(); FAIL();
} }
} }
TEST(ReadTraFileTest, WrongFormatTestHeader1) { TEST(ReadTraFileTest, WrongFormatTestHeader1) {
ASSERT_THROW(mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::wrong_file_format);
ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::wrong_file_format);
} }
TEST(ReadTraFileTest, WrongFormatTestHeader2) { TEST(ReadTraFileTest, WrongFormatTestHeader2) {
ASSERT_THROW(mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::wrong_file_format);
ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::wrong_file_format);
} }
TEST(ReadTraFileTest, WrongFormatTestTransition) { TEST(ReadTraFileTest, WrongFormatTestTransition) {
ASSERT_THROW(mrmc::parser::readTraFile(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::wrong_file_format);
ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::wrong_file_format);
} }
Loading…
Cancel
Save