sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

more work on refactoring / rewriting parsers

tempestpy_adaptions
gereon 12 years ago
parent
e35b950eea
commit
2cf8f3baec
7 changed files with 220 additions and 273 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 123
      src/parser/readLabFile.cpp
  2. 19
      src/parser/readLabFile.h
  3. 91
      src/parser/readTraFile.cpp
  4. 19
      src/parser/readTraFile.h
  5. 181
      src/parser/read_lab_file.cpp
  6. 24
      src/parser/read_lab_file.h
  7. 20
      src/parser/read_tra_file.h

123
src/parser/readLabFile.cpp
View File

@ -0,0 +1,123 @@
/*
* readLabFile.cpp
*
* Created on: 21.11.2012
* Author: Gereon Kremer
*/
#include "parser.h"
#include "readLabFile.h"
#include "src/exceptions/wrong_file_format.h"
#include "src/exceptions/file_IO_exception.h"
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <clocale>
#include <iostream>
#include <errno.h>
#include <time.h>
#include <sys/stat.h>
#include <sys/mman.h>
#include <fcntl.h>
#include <locale.h>
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
namespace mrmc {
namespace parser {
/*!
* Reads a .lab file and puts the result in a labeling structure.
*
* Labelings created with this method have to be freed with the delete operator.
* @param node_count the number of states.
* @param filename input .lab file's name.
* @return The pointer to the created labeling object.
*/
mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename)
{
/*!
* open file and map to memory
*/
struct stat st;
int f = open(filename, O_RDONLY);
if ((f < 0) || (stat(filename, &st) != 0)) {
/*!
*
*/
pantheios::log_ERROR("File could not be opened.");
throw mrmc::exceptions::file_IO_exception();
return NULL;
}
char* data = (char*) mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE, f, 0);
if (data == (char*)-1)
{
pantheios::log_ERROR("File could not be mapped. Something went wrong with mmap.");
close(f);
throw mrmc::exceptions::file_IO_exception();
return NULL;
}
char* buf = data;
char sep[] = " \n\t";
uint_fast32_t proposition_count = 0;
size_t cnt = 0;
do {
buf += cnt;
cnt = strcspn(buf, sep);
if (cnt > 0) {
if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
if (strncmp(buf, "#END", cnt) == 0) break;
proposition_count++;
}
else cnt = 1;
} while (cnt > 0);
mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
char proposition[128];
buf = data;
cnt = 0;
do {
buf += cnt;
cnt = strcspn(buf, sep);
if (cnt > 0) {
if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
if (strncmp(buf, "#END", cnt) == 0) break;
strncpy(proposition, buf, cnt);
proposition[cnt] = '\0';
result->addAtomicProposition(proposition);
}
else cnt = 1;
} while (cnt > 0);
buf += 4;
uint_fast32_t node;
while (1) {
node = strtol(buf, &buf, 10);
while (*buf != '\0') {
cnt = strcspn(buf, sep);
if (cnt == 0) buf++;
else break;
}
strncpy(proposition, buf, cnt);
proposition[cnt] = '\0';
result->addAtomicPropositionToState(proposition, node);
buf += cnt;
}
munmap(data, st.st_size);
close(f);
return result;
}
} //namespace parser
} //namespace mrmc

19
src/parser/readLabFile.h
View File

@ -0,0 +1,19 @@
/*
* read_lab_file.h
*
*/
#pragma once
#include "src/models/atomic_propositions_labeling.h"
namespace mrmc {
namespace parser {
mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename);
}
}

91
src/parser/read_tra_file.cpp → src/parser/readTraFile.cpp
View File

@ -3,15 +3,13 @@
* system of a Markov chain (DTMC) and saving it into a corresponding
* matrix.
*
* Reuses code from the file "read_tra_file.c" from the old MRMC project.
*
* Created on: 20.11.2012
* Author: Gereon Kremer
*/
#include "parser.h"
#include "src/parser/read_tra_file.h"
#include "src/parser/readTraFile.h"
#include "src/exceptions/file_IO_exception.h"
#include "src/exceptions/wrong_file_format.h"
#include "boost/integer/integer_mask.hpp"
@ -44,25 +42,22 @@ char* skipWS(char* buf)
}
}
// Disable C4996 - This function or variable may be unsafe.
#pragma warning(disable:4996)
/*!
* This method does the first pass through the .tra file and computes
* the number of non-zero elements that are not diagonal elements,
* which correspondents to the number of transitions that are not
* self-loops.
* (Diagonal elements are treated in a special way).
*
* @return The number of non-zero elements that are not on the diagonal
* @param buf Data to scan. Is expected to be some char array.
*/
static uint_fast32_t make_first_pass(char* buf)
* This method does the first pass through the .tra file and computes
* the number of non-zero elements that are not diagonal elements,
* which correspondents to the number of transitions that are not
* self-loops.
* (Diagonal elements are treated in a special way).
*
* @return The number of non-zero elements that are not on the diagonal
* @param buf Data to scan. Is expected to be some char array.
*/
static uint_fast32_t makeFirstPass(char* buf)
{
uint_fast32_t non_zero = 0;
/*
check file header and extract number of transitions
/*!
* check file header and extract number of transitions
*/
if (strncmp(buf, "STATES ", 7) != 0) return 0;
buf += 7; // skip "STATES "
@ -72,8 +67,8 @@ static uint_fast32_t make_first_pass(char* buf)
buf += 12; // skip "TRANSITIONS "
if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
/*
check all transitions for non-zero diagonal entrys
/*!
* check all transitions for non-zero diagonal entrys
*/
unsigned int row, col;
double val;
@ -98,17 +93,21 @@ static uint_fast32_t make_first_pass(char* buf)
* @return a pointer to the created sparse matrix.
*/
sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
if (setlocale( LC_NUMERIC, "de_DE" ) == 0)
{
fprintf(stderr, "could not set locale\n");
}
/*
open file and map to memory
sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
/*!
* enforce locale where decimal point is '.'
*/
setlocale( LC_NUMERIC, "C" );
/*!
* open file and map to memory
*/
struct stat st;
int f = open(filename, O_RDONLY);
if((f < 0) || (stat(filename, &st) != 0)) {
/*!
* stat() or open() failed
*/
pantheios::log_ERROR("File ", filename, " was not readable (Does it exist?)");
throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)");
return NULL;
@ -116,35 +115,41 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
char *data = (char*)mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, f, 0);
if (data == (char*)-1)
{
/*!
* mmap() failed
*/
pantheios::log_ERROR("Could not map the file to memory. Something went wrong with mmap.");
throw exceptions::file_IO_exception("mrmc::read_tra_file: Error mapping file to memory");
close(f);
return NULL;
}
/*
perform first pass
/*!
* perform first pass, i.e. count entries that are not zero and not on the diagonal
*/
uint_fast32_t non_zero = make_first_pass(data);
uint_fast32_t non_zero = makeFirstPass(data);
if (non_zero == 0)
{
/*!
* first pass returned zero, this means the file format was wrong
*/
close(f);
munmap(data, st.st_size);
throw mrmc::exceptions::wrong_file_format();
return NULL;
}
/*
perform second pass
from here on, we already know that the file header is correct
/*!
* perform second pass
*
* from here on, we already know that the file header is correct
*/
char* buf = data;
uint_fast32_t rows;
sparse::StaticSparseMatrix<double> *sp = NULL;
/*
read file header, extract number of states
/*!
* read file header, extract number of states
*/
buf += 7; // skip "STATES "
rows = strtol(buf, &buf, 10);
@ -156,13 +161,17 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
pantheios::integer(rows), " rows and ",
pantheios::integer(non_zero), " Non-Zero-Elements");
/* Creating matrix
/*!
* Creating matrix
* Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
*/
sp = new sparse::StaticSparseMatrix<double>(rows);
if (sp == NULL)
{
/*!
* creating the matrix failed
*/
close(f);
munmap(data, st.st_size);
throw std::bad_alloc();
@ -172,8 +181,8 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
uint_fast64_t row, col;
double val;
/*
read all transitions from file
/*!
* read all transitions from file
*/
while (1)
{
@ -189,7 +198,9 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
sp->addNextValue(row,col,val);
}
// clean up
/*!
* clean up
*/
close(f);
munmap(data, st.st_size);

19
src/parser/readTraFile.h
View File

@ -0,0 +1,19 @@
/*
* read_tra_file.h
*
* Created on: 15.08.2012
* Author: Thomas Heinemann
*/
#pragma once
#include "src/sparse/static_sparse_matrix.h"
namespace mrmc {
namespace parser {
mrmc::sparse::StaticSparseMatrix<double> * readTraFile(const char * filename);
}
}

181
src/parser/read_lab_file.cpp
View File

@ -1,181 +0,0 @@
/*
* read_lab_file.cpp
*
* Created on: 10.09.2012
* Author: Thomas Heinemann
*/
#include "parser.h"
#include "read_lab_file.h"
#include "src/exceptions/wrong_file_format.h"
#include "src/exceptions/file_IO_exception.h"
#include <cstring>
#include <cstdlib>
#include <cstdio>
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
#ifdef WIN32
# define STRTOK_FUNC strtok_s
#else
# define STRTOK_FUNC strtok_r
#endif
// Disable C4996 - This function or variable may be unsafe.
#pragma warning(disable:4996)
namespace mrmc {
namespace parser {
/*!
* Reads a .lab file and puts the result in a labeling structure.
*
* Labelings created with this method have to be freed with the delete operator.
* @param node_count the number of states.
* @param filename input .lab file's name.
* @return The pointer to the created labeling object.
*/
mrmc::models::AtomicPropositionsLabeling * 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;
//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. (fixed by Philipp. Or?)
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) {
pantheios::log_ERROR("File could not be opened.");
throw mrmc::exceptions::file_IO_exception();
return NULL;
}
if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#DECLARATION\n")) {
fclose(P);
pantheios::log_ERROR("Wrong declaration section (\"#DECLARATION\" missing).");
throw mrmc::exceptions::wrong_file_format();
return NULL;
}
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();
delete[] decl_buffer;
return NULL;
}
} while (need_next_iteration);
uint_fast32_t proposition_count = 0;
char * proposition;
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::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
//Here, all propositions are to be declared...
for (proposition = STRTOK_FUNC(decl_buffer, sep, &saveptr);
proposition != NULL;
proposition = STRTOK_FUNC(NULL, sep, &saveptr)) {
result -> addAtomicProposition(proposition);
}
// Free decl_buffer
delete[] decl_buffer;
saveptr = NULL; //resetting save pointer for strtok_r
if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#END\n")) {
fclose(P);
delete result;
pantheios::log_ERROR("Wrong declaration section (\"#END\" missing).");
throw mrmc::exceptions::wrong_file_format();
return NULL;
}
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_FUNC(s, sep, &saveptr);
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();
return NULL;
}
do {
token = STRTOK_FUNC(NULL, sep, &saveptr);
if (token == NULL) {
break;
}
result->addAtomicPropositionToState(token, node);
} while (token != NULL);
}
fclose(P);
return result;
}
} //namespace parser
} //namespace mrmc

24
src/parser/read_lab_file.h
View File

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

20
src/parser/read_tra_file.h
View File

@ -1,20 +0,0 @@
/*
* read_tra_file.h
*
* Created on: 15.08.2012
* Author: Thomas Heinemann
*/
#ifndef READ_TRA_FILE_H_
#define READ_TRA_FILE_H_
#include "src/sparse/static_sparse_matrix.h"
namespace mrmc{
namespace parser {
mrmc::sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename);
}
}
#endif /* READ_TRA_FILE_H_ */
Write Preview
Loading…
Cancel
Save