Browse Source

Lab and Tra parser pass test cases

Some more fixing, error handling and restructuring.
Both parsers now pass all test cases.
tempestpy_adaptions
gereon 12 years ago
parent
commit
bb1dae23fc
  1. 35
      src/parser/parser.h
  2. 89
      src/parser/readLabFile.cpp
  3. 2
      src/parser/readLabFile.h
  4. 42
      src/parser/readTraFile.cpp

35
src/parser/parser.h

@ -18,13 +18,46 @@
#include <sys/stat.h> #include <sys/stat.h>
#include <fcntl.h> #include <fcntl.h>
#include <errno.h> #include <errno.h>
#include <iostream>
#include <pantheios/pantheios.hpp> #include <pantheios/pantheios.hpp>
#include "src/exceptions/file_IO_exception.h" #include "src/exceptions/file_IO_exception.h"
#include "src/exceptions/wrong_file_format.h"
namespace mrmc { namespace mrmc {
namespace parser { namespace parser {
/*!
* @brief Parses integer and checks, if something has been parsed.
*
* Calls strtol() internally and checks if the new pointer is different
* from the original one, i.e. if str != *end. If they are the same, a
* mrmc::exceptions::wrong_file_format will be thrown.
* @param str String to parse
* @param end New pointer will be written there
* @return Result of strtol()
*/
inline uint_fast64_t checked_strtol(const char* str, char** end)
{
uint_fast64_t res = strtol(str, end, 10);
if (str == *end) throw mrmc::exceptions::wrong_file_format();
return res;
}
/*!
* @brief Skips common whitespaces in a string.
*
* Skips spaces, tabs, newlines and carriage returns. Returns pointer
* to first char that is not a whitespace.
* @param buf String buffer
* @return pointer to first non-whitespace character
*/
inline char* skipWS(char* buf)
{
while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++;
return 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.
@ -79,7 +112,7 @@ namespace parser {
* Will stat the given file, open it and map it to memory. * Will stat the given file, open it and map it to memory.
* If anything of this fails, an appropriate exception is raised * If anything of this fails, an appropriate exception is raised
* and a log entry is written. * and a log entry is written.
* @filename file to be opened
* @param filename file to be opened
*/ */
MappedFile(const char* filename) MappedFile(const char* filename)
{ {

89
src/parser/readLabFile.cpp

@ -43,7 +43,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(int node_count, const char * filename)
mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename)
{ {
/* /*
* open file * open file
@ -55,10 +55,14 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
* first run: obtain number of propositions * first run: obtain number of propositions
*/ */
char separator[] = " \n\t"; char separator[] = " \n\t";
bool foundDecl = false, foundEnd = false;
uint_fast32_t proposition_count = 0; uint_fast32_t proposition_count = 0;
{ {
size_t cnt = 0; size_t cnt = 0;
do
/*
* iterate over tokens while not at end of file
*/
while(buf[0] != '\0')
{ {
buf += cnt; buf += cnt;
cnt = strcspn(buf, separator); // position of next separator cnt = strcspn(buf, separator); // position of next separator
@ -69,12 +73,25 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
* next token is #END: stop search * next token is #END: stop search
* otherwise increase proposition_count * otherwise increase proposition_count
*/ */
if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
if (strncmp(buf, "#END", cnt) == 0) break;
if (strncmp(buf, "#DECLARATION", cnt) == 0)
{
foundDecl = true;
continue;
}
if (strncmp(buf, "#END", cnt) == 0)
{
foundEnd = true;
break;
}
proposition_count++; proposition_count++;
} }
else cnt = 1; // next char is separator, one step forward
} while (cnt > 0);
else buf++; // next char is separator, one step forward
}
/*
* If #DECLARATION or #END were not found, the file format is wrong
*/
if (! (foundDecl && foundEnd)) throw mrmc::exceptions::wrong_file_format();
} }
/* /*
@ -91,6 +108,7 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
{ {
/* /*
* load propositions * load propositions
* As we already checked the file format, we can be a bit sloppy here...
*/ */
char proposition[128]; // buffer for proposition names char proposition[128]; // buffer for proposition names
size_t cnt = 0; size_t cnt = 0;
@ -126,40 +144,43 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha
*/ */
uint_fast32_t node; uint_fast32_t node;
char proposition[128]; char proposition[128];
char* tmp;
size_t cnt; size_t cnt;
do
/*
* iterate over nodes
*/
while (buf[0] != '\0')
{ {
node = strtol(buf, &buf, 10); // parse node number
while (*buf != '\0') // while not at end of file
{
cnt = strcspn(buf, separator); // position of next separator
if (cnt == 0) buf++; // next char is separator, one step forward
else break;
}
/* /*
* if cnt > 0, buf points to the next proposition
* otherwise, we have reached the end of the file
* parse node number, then iterate over propositions
*/ */
if (cnt > 0)
{
/*
* copy proposition to buffer, add assignment to labeling
*/
strncpy(proposition, buf, cnt);
proposition[cnt] = '\0';
result->addAtomicPropositionToState(proposition, node);
}
else if (node == 0)
node = checked_strtol(buf, &buf);
while (buf[0] != '\n')
{ {
/*
* If this is executed, we could read a number but there
* was no proposition after that. This strongly suggests a
* broken file, but it's not fatal...
*/
pantheios::log_WARNING("The label file ended on a node number. Is the file malformated?");
cnt = strcspn(buf, separator);
if (cnt == 0)
{
/*
* next char is a separator
* if it's a newline, we continue with next node
* otherwise we skip it and try again
*/
if (buf[0] == '\n') break;
buf++;
}
else
{
/*
* copy proposition to buffer and add it to result
*/
strncpy(proposition, buf, cnt);
proposition[cnt] = '\0';
result->addAtomicPropositionToState(proposition, node);
buf += cnt;
}
} }
buf += cnt;
} while (cnt > 0);
buf = skipWS(buf);
}
} }
return result; return result;

2
src/parser/readLabFile.h

@ -10,7 +10,7 @@ namespace parser {
/*! /*!
* @brief Load label file and return initialized AtomicPropositionsLabeling object. * @brief Load label file and return initialized AtomicPropositionsLabeling object.
*/ */
mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename);
mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename);
} // namespace parser } // namespace parser
} // namespace mrmc } // namespace mrmc

42
src/parser/readTraFile.cpp

@ -33,20 +33,6 @@
namespace mrmc { namespace mrmc {
namespace parser{ namespace parser{
/*!
* Skips all whitespaces and returns new pointer.
*
* @todo should probably be replaced by strspn et.al.
*/
char* skipWS(char* buf)
{
while(1)
{
if ((buf[0] != ' ') && (buf[0] != '\t') && (buf[0] != '\n') && (buf[0] != '\r')) return buf;
buf++;
}
}
/*! /*!
* @brief Perform first pass through the file and obtain number of * @brief Perform first pass through the file and obtain number of
* non-zero cells and maximum node id. * non-zero cells and maximum node id.
@ -83,13 +69,13 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
uint_fast32_t row, col; uint_fast32_t row, col;
double val; double val;
maxnode = 0; maxnode = 0;
while (1)
while (buf[0] != '\0')
{ {
/* /*
* read row and column * read row and column
*/ */
row = strtol(buf, &buf, 10);
col = strtol(buf, &buf, 10);
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
/* /*
* check if one is larger than the current maximum id * check if one is larger than the current maximum id
*/ */
@ -102,6 +88,7 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
val = strtod(buf, &buf); val = strtod(buf, &buf);
if (val == 0.0) break; if (val == 0.0) break;
if (row == col) non_zero--; if (row == col) non_zero--;
buf = skipWS(buf);
} }
return non_zero; return non_zero;
@ -150,10 +137,10 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
* read file header, extract number of states * read file header, extract number of states
*/ */
buf += 7; // skip "STATES " buf += 7; // skip "STATES "
strtol(buf, &buf, 10);
checked_strtol(buf, &buf);
buf = skipWS(buf); buf = skipWS(buf);
buf += 12; // skip "TRANSITIONS " buf += 12; // skip "TRANSITIONS "
strtol(buf, &buf, 10);
checked_strtol(buf, &buf);
pantheios::log_DEBUG("Creating matrix with ", pantheios::log_DEBUG("Creating matrix with ",
pantheios::integer(maxnode + 1), " maxnodes and ", pantheios::integer(maxnode + 1), " maxnodes and ",
@ -177,19 +164,16 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
while (buf[0] != '\0') while (buf[0] != '\0')
{ {
/* /*
* read row, col and value. if value == 0.0, we have reached the
* end of the file.
* read row, col and value.
*/ */
row = strtol(buf, &buf, 10);
if ((buf[0] != ' ') && (buf[0] != '\t')) throw mrmc::exceptions::wrong_file_format();
col = strtol(buf, &buf, 10);
if ((buf[0] != ' ') && (buf[0] != '\t')) throw mrmc::exceptions::wrong_file_format();
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
val = strtod(buf, &buf); val = strtod(buf, &buf);
if ((buf[0] != '\n') && (buf[0] != '\r')) throw mrmc::exceptions::wrong_file_format();
if (val == 0.0) break;
/*
* only values in (0, 1] are meaningful
*/
if ((val <= 0.0) || (val > 1.0)) throw mrmc::exceptions::wrong_file_format();
pantheios::log_DEBUG("Write value ", pantheios::log_DEBUG("Write value ",
pantheios::real(val), pantheios::real(val),
" to position ", " to position ",

Loading…
Cancel
Save