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

minor cleanups, added documentation.

tempestpy_adaptions
gereon 12 years ago
parent
ea8504a84e
commit
ad0c802fcc
5 changed files with 229 additions and 128 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. 50
      src/parser/parser.h
  2. 168
      src/parser/readLabFile.cpp
  3. 14
      src/parser/readLabFile.h
  4. 106
      src/parser/readTraFile.cpp
  5. 19
      src/parser/readTraFile.h

50
src/parser/parser.h
View File

@ -15,20 +15,47 @@
#include <pantheios/pantheios.hpp>
#include "src/exceptions/file_IO_exception.h"
namespace mrmc
{
namespace parser
{
namespace mrmc {
namespace parser {
/*!
* @brief Opens a file and maps it to memory providing a char*
* containing the file content.
*
* This class is a very simple interface to read files efficiently.
* The given file is opened and mapped to memory using mmap().
* The public member data is a pointer to the actual file content.
* Using this method, the kernel will take care of all buffering. This is
* most probably much more efficient than doing this manually.
*/
class MappedFile
{
private:
/*!
* @brief file descriptor obtained by open().
*/
int file;
/*!
* @brief stat information about the file.
*/
struct stat st;
public:
char* data;
/*!
* @brief pointer to actual file content.
*/
char* data;
/*!
* @brief Constructor of MappedFile.
*
* Will stat the given file, open it and map it to memory.
* If anything of this fails, an appropriate exception is raised
* and a log entry is written.
* @filename file to be opened
*/
MappedFile(const char* filename)
{
if (stat(filename, &(this->st)) != 0)
@ -53,6 +80,11 @@ namespace parser
}
}
/*!
* @brief Destructor of MappedFile.
*
* Will unmap the data and close the file.
*/
~MappedFile()
{
munmap(this->data, this->st.st_size);
@ -60,5 +92,5 @@ namespace parser
}
};
}
}
} // namespace parser
} // namespace mrmc

168
src/parser/readLabFile.cpp
View File

@ -1,4 +1,4 @@
/*
/*!
* readLabFile.cpp
*
* Created on: 21.11.2012
@ -28,76 +28,138 @@
#include <pantheios/inserters/integer.hpp>
namespace mrmc {
namespace parser {
/*!
* Reads a .lab file and puts the result in a labeling structure.
* Reads a label 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.
* 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
*/
MappedFile file(filename);
char* buf = file.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);
/*
* first run: obtain number of propositions
*/
char separator[] = " \n\t";
uint_fast32_t proposition_count = 0;
{
size_t cnt = 0;
do
{
buf += cnt;
cnt = strcspn(buf, separator); // position of next separator
if (cnt > 0)
{
/*
* next token is #DECLARATION: just skip it
* next token is #END: stop search
* otherwise increase proposition_count
*/
if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
if (strncmp(buf, "#END", cnt) == 0) break;
proposition_count++;
}
else cnt = 1; // next char is separator, one step forward
} while (cnt > 0);
}
printf("node count %d\n", node_count);
/*
* create labeling object with given node and proposition count
*/
mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
char proposition[128];
/*
* second run: add propositions and node labels to labeling
*
* first thing to do: reset file pointer
*/
buf = file.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;
{
/*
* load propositions
*/
char proposition[128]; // buffer for proposition names
size_t cnt = 0;
do
{
buf += cnt;
cnt = strcspn(buf, separator); // position of next separator
if (cnt > 0)
{
/*
* next token is: #DECLARATION: just skip it
* next token is: #END: stop search
* otherwise: copy token to buffer, append trailing null byte and hand it to labeling
*/
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; // next char is separator, one step forward
} while (cnt > 0);
/*
* Right here, the buf pointer is still pointing to our last token,
* i.e. to #END. We want to skip this one...
*/
buf += 4;
}
uint_fast32_t node;
do {
node = strtol(buf, &buf, 10);
while (*buf != '\0') {
cnt = strcspn(buf, sep);
if (cnt == 0) buf++;
else break;
}
if (cnt > 0) {
strncpy(proposition, buf, cnt);
proposition[cnt] = '\0';
result->addAtomicPropositionToState(proposition, node);
}
buf += cnt;
} while (cnt > 0);
{
/*
* now parse node label assignments
*/
uint_fast32_t node;
char proposition[128];
size_t cnt;
do
{
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
*/
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)
{
/*
* 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?");
}
buf += cnt;
} while (cnt > 0);
}
return result;
}
} //namespace parser
} //namespace mrmc

14
src/parser/readLabFile.h
View File

@ -1,19 +1,15 @@
/*
* read_lab_file.h
*
*/
#pragma once
#include "src/models/atomic_propositions_labeling.h"
namespace mrmc {
namespace parser {
/*!
* @brief Load label file and return initialized AtomicPropositionsLabeling object.
*/
mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename);
}
}
} // namespace parser
} // namespace mrmc

106
src/parser/readTraFile.cpp
View File

@ -1,10 +1,8 @@
/*! read_tra_file.cpp
* Provides functions for reading a *.tra file describing the transition
* system of a Markov chain (DTMC) and saving it into a corresponding
* matrix.
/*!
* readTraFile.cpp
*
* Created on: 20.11.2012
* Author: Gereon Kremer
* Created on: 20.11.2012
* Author: Gereon Kremer
*/
#include "parser.h"
@ -30,9 +28,13 @@
#include <pantheios/inserters/real.hpp>
namespace mrmc {
namespace parser{
/*!
* Skips all whitespaces and returns new pointer.
*
* @todo should probably be replaced by strspn et.al.
*/
char* skipWS(char* buf)
{
while(1)
@ -43,20 +45,25 @@ char* skipWS(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).
* @brief Perform first pass through the file and obtain number of
* non-zero cells and maximum node id.
*
* 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).
* It also calculates the maximum node id and stores it in maxnode.
*
* @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.
* @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.
* @param maxnode Is set to highest id of all nodes.
*/
static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
{
uint_fast32_t non_zero = 0;
/*!
/*
* check file header and extract number of transitions
*/
if (strncmp(buf, "STATES ", 7) != 0) return 0;
@ -67,7 +74,7 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
buf += 12; // skip "TRANSITIONS "
if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
/*!
/*
* check all transitions for non-zero diagonal entrys
*/
uint_fast32_t row, col;
@ -75,10 +82,20 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
maxnode = 0;
while (1)
{
/*
* read row and column
*/
row = strtol(buf, &buf, 10);
if (row > maxnode) maxnode = row;
col = strtol(buf, &buf, 10);
/*
* check if one is larger than the current maximum id
*/
if (row > maxnode) maxnode = row;
if (col > maxnode) maxnode = col;
/*
* read value. if value is zero, we have reached the end of the file.
* if row == col, we have a diagonal element which is treated seperately and this non_zero must be decreased.
*/
val = strtod(buf, &buf);
if (val == 0.0) break;
if (row == col) non_zero--;
@ -89,44 +106,44 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode)
/*!Reads a .tra file and produces a sparse matrix representing the described Markov Chain.
/*!
* Reads a .tra file and produces a sparse matrix representing the described Markov Chain.
*
* Matrices created with this method have to be freed with the delete operator.
* @param filename input .tra file's name.
* @return a pointer to the created sparse matrix.
* Matrices created with this method have to be freed with the delete operator.
* @param filename input .tra file's name.
* @return a pointer to the created sparse matrix.
*/
sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
/*!
/*
* enforce locale where decimal point is '.'
*/
setlocale( LC_NUMERIC, "C" );
/*
* open file
*/
MappedFile file(filename);
char* buf = file.data;
/*!
/*
* perform first pass, i.e. count entries that are not zero and not on the diagonal
*/
uint_fast32_t maxnode;
uint_fast32_t non_zero = makeFirstPass(file.data, maxnode);
if (non_zero == 0)
{
/*!
* first pass returned zero, this means the file format was wrong
*/
throw mrmc::exceptions::wrong_file_format();
return NULL;
}
/*
* if first pass returned zer, the file format was wrong
*/
if (non_zero == 0) throw mrmc::exceptions::wrong_file_format();
/*!
/*
* perform second pass
*
* from here on, we already know that the file header is correct
*/
char* buf = file.data;
sparse::StaticSparseMatrix<double> *sp = NULL;
/*!
/*
* read file header, extract number of states
*/
buf += 7; // skip "STATES "
@ -139,29 +156,27 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
pantheios::integer(maxnode + 1), " maxnodes and ",
pantheios::integer(non_zero), " Non-Zero-Elements");
/*!
/*
* 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>(maxnode + 1);
if (sp == NULL)
{
/*!
* creating the matrix failed
*/
throw std::bad_alloc();
return NULL;
}
if (sp == NULL) throw std::bad_alloc();
sp->initialize(non_zero);
uint_fast64_t row, col;
double val;
/*!
/*
* read all transitions from file
*/
while (1)
{
/*
* read row, col and value. if value == 0.0, we have reached the
* end of the file.
*/
row = strtol(buf, &buf, 10);
col = strtol(buf, &buf, 10);
val = strtod(buf, &buf);
@ -174,7 +189,7 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
sp->addNextValue(row,col,val);
}
/*!
/*
* clean up
*/
pantheios::log_DEBUG("Finalizing Matrix");
@ -183,5 +198,4 @@ sparse::StaticSparseMatrix<double> * readTraFile(const char * filename) {
}
} //namespace parser
} //namespace mrmc

19
src/parser/readTraFile.h
View File

@ -1,19 +1,16 @@
/*
* 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 {
namespace parser {
mrmc::sparse::StaticSparseMatrix<double> * readTraFile(const char * filename);
/*!
* @brief Load transition system from file and return initialized
* StaticSparseMatrix object.
*/
mrmc::sparse::StaticSparseMatrix<double> * readTraFile(const char * filename);
}
}
} // namespace parser
} // namespace mrmc
Write Preview
Loading…
Cancel
Save