Browse Source
Merge branch 'parser'
Merge branch 'parser'
Conflicts: CMakeLists.txt src/mrmc-cpp.cpp src/parser/read_lab_file.cpp src/parser/read_lab_file.h src/parser/read_tra_file.cpp src/parser/read_tra_file.h src/utility/utility.cpp test/parser/read_lab_file_test.cpp test/parser/read_tra_file_test.cpptempestpy_adaptions
gereon
12 years ago
19 changed files with 1050 additions and 487 deletions
-
111resources/3rdparty/gtest-1.6.0/Makefile.in
-
201resources/3rdparty/gtest-1.6.0/aclocal.m4
-
4src/formula/BoundedUntil.h
-
128src/parser/parser.cpp
-
97src/parser/parser.h
-
190src/parser/readLabFile.cpp
-
19src/parser/readLabFile.h
-
123src/parser/readPrctlFile.cpp
-
17src/parser/readPrctlFile.h
-
195src/parser/readTraFile.cpp
-
18src/parser/readTraFile.h
-
177src/parser/read_lab_file.cpp
-
24src/parser/read_lab_file.h
-
161src/parser/read_tra_file.cpp
-
20src/parser/read_tra_file.h
-
11src/utility/osDetection.h
-
17src/utility/utility.cpp
-
12test/parser/read_lab_file_test.cpp
-
12test/parser/read_tra_file_test.cpp
@ -0,0 +1,128 @@ |
|||
#include "src/parser/parser.h"
|
|||
|
|||
#if defined LINUX || defined MACOSX
|
|||
#include <sys/mman.h>
|
|||
#elif defined WINDOWS
|
|||
#endif
|
|||
|
|||
#include <sys/stat.h>
|
|||
#include <fcntl.h>
|
|||
#include <errno.h>
|
|||
#include <iostream>
|
|||
|
|||
#include <pantheios/pantheios.hpp>
|
|||
#include "src/exceptions/file_IO_exception.h"
|
|||
#include "src/exceptions/wrong_file_format.h"
|
|||
|
|||
/*!
|
|||
* 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() |
|||
*/ |
|||
uint_fast64_t mrmc::parser::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; |
|||
} |
|||
|
|||
/*!
|
|||
* 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 |
|||
*/ |
|||
char* mrmc::parser::skipWS(char* buf) |
|||
{ |
|||
while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++; |
|||
return buf; |
|||
} |
|||
|
|||
/*!
|
|||
* 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. |
|||
* @param filename file to be opened |
|||
*/ |
|||
mrmc::parser::MappedFile::MappedFile(const char* filename) |
|||
{ |
|||
#if defined LINUX || defined MACOSX
|
|||
/*
|
|||
* Do file mapping for reasonable systems. |
|||
* stat64(), open(), mmap() |
|||
*/ |
|||
if (stat64(filename, &(this->st)) != 0) |
|||
{ |
|||
pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?"); |
|||
throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()"); |
|||
} |
|||
this->file = open(filename, O_RDONLY); |
|||
|
|||
if (this->file < 0) |
|||
{ |
|||
pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?"); |
|||
throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in open()"); |
|||
} |
|||
|
|||
this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE|MAP_DENYWRITE, this->file, 0); |
|||
if (this->data == (char*)-1) |
|||
{ |
|||
close(this->file); |
|||
pantheios::log_ERROR("Could not mmap ", filename, "."); |
|||
throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in mmap()"); |
|||
} |
|||
this->dataend = this->data + this->st.st_size; |
|||
#elif defined WINDOWS
|
|||
/*
|
|||
* Do file mapping for windows. |
|||
* _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile() |
|||
*/ |
|||
if (_stat64(filename, &(this->st)) != 0) |
|||
{ |
|||
pantheios::log_ERROR("Could not stat ", filename, ". Does it exist? Is it readable?"); |
|||
throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in stat()"); |
|||
} |
|||
|
|||
this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL); |
|||
if (this->file == INVALID_HANDLE_VALUE) |
|||
{ |
|||
pantheios::log_ERROR("Could not open ", filename, ". Does it exist? Is it readable?"); |
|||
throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFile()"); |
|||
} |
|||
|
|||
this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL); |
|||
if (this->mapping == NULL) |
|||
{ |
|||
CloseHandle(this->file); |
|||
pantheios::log_ERROR("Could not create file mapping for ", filename, "."); |
|||
throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in CreateFileMapping()"); |
|||
} |
|||
|
|||
this->data = static_cast<char*>(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size)); |
|||
if (this->data == NULL) |
|||
{ |
|||
CloseHandle(this->mapping); |
|||
CloseHandle(this->file); |
|||
pantheios::log_ERROR("Could not create file map view for ", filename, "."); |
|||
throw exceptions::file_IO_exception("mrmc::parser::MappedFile Error in MapViewOfFile()"); |
|||
} |
|||
this->dataend = this->data + this->st.st_size; |
|||
#endif
|
|||
} |
|||
|
|||
/*!
|
|||
* Will unmap the data and close the file. |
|||
*/ |
|||
mrmc::parser::MappedFile::~MappedFile() |
|||
{ |
|||
#if defined LINUX || defined MACOSX
|
|||
munmap(this->data, this->st.st_size); |
|||
close(this->file); |
|||
#elif defined WINDOWS
|
|||
CloseHandle(this->mapping); |
|||
CloseHandle(this->file); |
|||
#endif
|
|||
} |
|||
@ -1,15 +1,102 @@ |
|||
/* |
|||
* parser.h |
|||
* |
|||
* Created on: 12.09.2012 |
|||
* Author: Thomas Heinemann |
|||
* Created on: 21.11.2012 |
|||
* Author: Gereon Kremer |
|||
*/ |
|||
|
|||
#ifndef PARSER_H_ |
|||
#define PARSER_H_ |
|||
|
|||
#include "boost/integer/integer_mask.hpp" |
|||
#include "src/utility/osDetection.h" |
|||
|
|||
const uint_fast32_t BUFFER_SIZE=1024; |
|||
#if defined LINUX || defined MACOSX |
|||
#include <sys/mman.h> |
|||
#elif defined WINDOWS |
|||
#endif |
|||
|
|||
#endif /* PARSER_H_ */ |
|||
#include <sys/stat.h> |
|||
#include <fcntl.h> |
|||
#include <errno.h> |
|||
#include <iostream> |
|||
|
|||
#include <pantheios/pantheios.hpp> |
|||
#include "src/exceptions/file_IO_exception.h" |
|||
#include "src/exceptions/wrong_file_format.h" |
|||
|
|||
namespace mrmc { |
|||
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* |
|||
* 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. |
|||
*/ |
|||
|
|||
#if !defined LINUX && !defined MACOSX && !defined WINDOWS |
|||
#error Platform not supported |
|||
#endif |
|||
|
|||
class MappedFile |
|||
{ |
|||
private: |
|||
/*! |
|||
* @brief file descriptor obtained by open(). |
|||
*/ |
|||
#if defined LINUX || defined MACOSX |
|||
int file; |
|||
#elif defined WINDOWS |
|||
HANDLE file; |
|||
HANDLE mapping; |
|||
#endif |
|||
|
|||
/*! |
|||
* @brief stat information about the file. |
|||
*/ |
|||
#if defined LINUX || defined MACOSX |
|||
struct stat64 st; |
|||
#elif defined WINDOWS |
|||
struct __stat64 st; |
|||
#endif |
|||
|
|||
public: |
|||
/*! |
|||
* @brief pointer to actual file content. |
|||
*/ |
|||
char* data; |
|||
|
|||
/*! |
|||
* @brief pointer to end of file content. |
|||
*/ |
|||
char* dataend; |
|||
|
|||
/*! |
|||
* @brief Constructor of MappedFile. |
|||
*/ |
|||
MappedFile(const char* filename); |
|||
|
|||
/*! |
|||
* @brief Destructor of MappedFile. |
|||
*/ |
|||
~MappedFile(); |
|||
}; |
|||
|
|||
} // namespace parser |
|||
} // namespace mrmc |
|||
|
|||
#endif /* PARSER_H_ */ |
|||
@ -0,0 +1,190 @@ |
|||
/*!
|
|||
* 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>
|
|||
#if defined LINUX || defined MACOSX
|
|||
#include <sys/mman.h>
|
|||
#elif defined WINDOWS
|
|||
#define strncpy strncpy_s
|
|||
#endif
|
|||
#include <fcntl.h>
|
|||
#include <locale.h>
|
|||
|
|||
#include <pantheios/pantheios.hpp>
|
|||
#include <pantheios/inserters/integer.hpp>
|
|||
|
|||
namespace mrmc { |
|||
namespace parser { |
|||
|
|||
|
|||
/*!
|
|||
* 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. |
|||
*/ |
|||
mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename) |
|||
{ |
|||
/*
|
|||
* open file |
|||
*/ |
|||
MappedFile file(filename); |
|||
char* buf = file.data; |
|||
|
|||
/*
|
|||
* first run: obtain number of propositions |
|||
*/ |
|||
char separator[] = " \n\t"; |
|||
bool foundDecl = false, foundEnd = false; |
|||
uint_fast32_t proposition_count = 0; |
|||
{ |
|||
size_t cnt = 0; |
|||
/*
|
|||
* iterate over tokens while not at end of file |
|||
*/ |
|||
while(buf[0] != '\0') |
|||
{ |
|||
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) |
|||
{ |
|||
foundDecl = true; |
|||
continue; |
|||
} |
|||
if (strncmp(buf, "#END", cnt) == 0) |
|||
{ |
|||
foundEnd = true; |
|||
break; |
|||
} |
|||
proposition_count++; |
|||
} |
|||
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(); |
|||
} |
|||
|
|||
/*
|
|||
* create labeling object with given node and proposition count |
|||
*/ |
|||
mrmc::models::AtomicPropositionsLabeling* result = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count); |
|||
|
|||
/*
|
|||
* second run: add propositions and node labels to labeling |
|||
* |
|||
* first thing to do: reset file pointer |
|||
*/ |
|||
buf = file.data; |
|||
{ |
|||
/*
|
|||
* load propositions |
|||
* As we already checked the file format, we can be a bit sloppy here... |
|||
*/ |
|||
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; |
|||
} |
|||
|
|||
{ |
|||
/*
|
|||
* now parse node label assignments |
|||
*/ |
|||
uint_fast32_t node; |
|||
char proposition[128]; |
|||
char* tmp; |
|||
size_t cnt; |
|||
/*
|
|||
* iterate over nodes |
|||
*/ |
|||
while (buf[0] != '\0') |
|||
{ |
|||
/*
|
|||
* parse node number, then iterate over propositions |
|||
*/ |
|||
node = checked_strtol(buf, &buf); |
|||
while (buf[0] != '\n') |
|||
{ |
|||
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 = skipWS(buf); |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
} //namespace parser
|
|||
} //namespace mrmc
|
|||
@ -0,0 +1,19 @@ |
|||
#ifndef READLABFILE_H_ |
|||
#define READLABFILE_H_ |
|||
|
|||
#include "src/models/atomic_propositions_labeling.h" |
|||
#include "boost/integer/integer_mask.hpp" |
|||
|
|||
|
|||
namespace mrmc { |
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Load label file and return initialized AtomicPropositionsLabeling object. |
|||
*/ |
|||
mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename); |
|||
|
|||
} // namespace parser |
|||
} // namespace mrmc |
|||
|
|||
#endif /* READLABFILE_H_ */ |
|||
@ -0,0 +1,123 @@ |
|||
#include "src/parser/readPrctlFile.h"
|
|||
|
|||
#include "src/parser/parser.h"
|
|||
|
|||
#include <iostream>
|
|||
|
|||
#include <map>
|
|||
//#include <pair>
|
|||
|
|||
#include <boost/spirit/include/classic_core.hpp>
|
|||
#include <boost/spirit/include/qi_grammar.hpp>
|
|||
#include <boost/spirit/include/qi_rule.hpp>
|
|||
#include <boost/spirit/include/qi.hpp>
|
|||
#include <boost/spirit/include/phoenix_operator.hpp>
|
|||
#include <boost/spirit/include/qi_char_class.hpp>
|
|||
|
|||
#include <boost/bind.hpp>
|
|||
|
|||
namespace bs = boost::spirit; |
|||
|
|||
namespace |
|||
{ |
|||
using namespace bs; |
|||
using namespace bs::qi; |
|||
using namespace bs::standard; |
|||
|
|||
struct PRCTLParser : public grammar< char const* > |
|||
{ |
|||
typedef rule< char const* > rule_none; |
|||
typedef rule< char const*, double() > rule_double; |
|||
typedef rule< char const*, std::string() > rule_string; |
|||
|
|||
/*!
|
|||
* @brief Generic Nonterminals. |
|||
*/ |
|||
rule_none ws; |
|||
rule_string variable; |
|||
rule_double value; |
|||
|
|||
/*!
|
|||
* @brief Nonterminals for file header. |
|||
*/ |
|||
rule< char const* > varDef; |
|||
rule_none type; |
|||
|
|||
/*!
|
|||
* @brief Nonterminals for formula. |
|||
*/ |
|||
rule_none formula, opP; |
|||
|
|||
/*!
|
|||
* @brief Nonterminals for high-level file structure. |
|||
*/ |
|||
rule_none file, header; |
|||
|
|||
/*!
|
|||
* @brief Variable assignments. |
|||
*/ |
|||
std::map<std::string, double> variables; |
|||
|
|||
/*!
|
|||
* @brief Resulting formula. |
|||
*/ |
|||
mrmc::formula::PCTLFormula* result; |
|||
|
|||
struct dump |
|||
{ |
|||
void print(double const& i, std::string& s) |
|||
{ |
|||
std::cout << s << " = " << i << std::endl; |
|||
} |
|||
void operator()(double const& a, unused_type, unused_type) const |
|||
{ |
|||
std::cout << a << std::endl; |
|||
} |
|||
void operator()(std::string const& a, unused_type, unused_type) const |
|||
{ |
|||
std::cout << a << std::endl; |
|||
} |
|||
void operator()(utree const& a, unused_type, unused_type) const |
|||
{ |
|||
std::cout << &a << std::endl; |
|||
} |
|||
}; |
|||
|
|||
PRCTLParser() : PRCTLParser::base_type(file, "PRCTL parser") |
|||
{ |
|||
variable %= alnum; |
|||
ws = *( space ); |
|||
value %= ( double_ | int_ ); // double_ must be *before* int_
|
|||
type = string("int") | string("double"); |
|||
varDef = |
|||
string("const") >> ws >> |
|||
type >> ws >> |
|||
variable >> ws >> |
|||
string("=") >> ws >> |
|||
value >> ws >> |
|||
string(";"); |
|||
|
|||
header = +( varDef >> ws ); |
|||
|
|||
file = header; |
|||
} |
|||
|
|||
|
|||
}; |
|||
} |
|||
|
|||
mrmc::formula::PCTLFormula* mrmc::parser::readPrctlFile(const char* filename) |
|||
{ |
|||
PRCTLParser p; |
|||
mrmc::parser::MappedFile file(filename); |
|||
|
|||
char* data = file.data; |
|||
if (bs::qi::parse< char const* >(data, file.dataend, p)) |
|||
{ |
|||
std::cout << "File was parsed" << std::endl; |
|||
std::string rest(data, file.dataend); |
|||
std::cout << "Rest: " << rest << std::endl; |
|||
return p.result; |
|||
} |
|||
else return NULL; |
|||
} |
|||
@ -0,0 +1,17 @@ |
|||
#ifndef READPRCTLFILE_H_ |
|||
#define READPRCTLFILE_H_ |
|||
|
|||
#include "src/formula/PCTLformula.h" |
|||
|
|||
namespace mrmc { |
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Load PRCTL file |
|||
*/ |
|||
mrmc::formula::PCTLFormula* readPrctlFile(const char * filename); |
|||
|
|||
} // namespace parser |
|||
} // namespace mrmc |
|||
|
|||
#endif /* READPRCTLFILE_H_ */ |
|||
@ -0,0 +1,195 @@ |
|||
/*!
|
|||
* readTraFile.cpp |
|||
* |
|||
* Created on: 20.11.2012 |
|||
* Author: Gereon Kremer |
|||
*/ |
|||
|
|||
#include "parser.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"
|
|||
#include <cstdlib>
|
|||
#include <cstdio>
|
|||
#include <cstring>
|
|||
#include <clocale>
|
|||
#include <iostream>
|
|||
#include <errno.h>
|
|||
#include <time.h>
|
|||
#include <sys/stat.h>
|
|||
#if defined LINUX || defined MACOSX
|
|||
#include <sys/mman.h>
|
|||
#elif defined WINDOWS
|
|||
#endif
|
|||
#include <fcntl.h>
|
|||
#include <locale.h>
|
|||
|
|||
#include <pantheios/pantheios.hpp>
|
|||
#include <pantheios/inserters/integer.hpp>
|
|||
#include <pantheios/inserters/real.hpp>
|
|||
|
|||
namespace mrmc { |
|||
namespace parser{ |
|||
|
|||
/*!
|
|||
* @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. |
|||
* @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; |
|||
buf += 7; // skip "STATES "
|
|||
if (strtol(buf, &buf, 10) == 0) return 0; |
|||
buf = skipWS(buf); |
|||
if (strncmp(buf, "TRANSITIONS ", 12) != 0) return 0; |
|||
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; |
|||
double val; |
|||
maxnode = 0; |
|||
while (buf[0] != '\0') |
|||
{ |
|||
/*
|
|||
* read row and column |
|||
*/ |
|||
row = checked_strtol(buf, &buf); |
|||
col = checked_strtol(buf, &buf); |
|||
/*
|
|||
* 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--; |
|||
buf = skipWS(buf); |
|||
} |
|||
|
|||
return non_zero; |
|||
} |
|||
|
|||
|
|||
|
|||
/*!
|
|||
* 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. |
|||
*/ |
|||
|
|||
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 first pass returned zero, 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 |
|||
*/ |
|||
sparse::StaticSparseMatrix<double> *sp = NULL; |
|||
|
|||
/*
|
|||
* read file header, extract number of states |
|||
*/ |
|||
buf += 7; // skip "STATES "
|
|||
checked_strtol(buf, &buf); |
|||
buf = skipWS(buf); |
|||
buf += 12; // skip "TRANSITIONS "
|
|||
checked_strtol(buf, &buf); |
|||
|
|||
pantheios::log_DEBUG("Creating matrix with ", |
|||
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) throw std::bad_alloc(); |
|||
sp->initialize(non_zero); |
|||
|
|||
uint_fast64_t row, col; |
|||
double val; |
|||
|
|||
/*
|
|||
* read all transitions from file |
|||
*/ |
|||
while (buf[0] != '\0') |
|||
{ |
|||
/*
|
|||
* read row, col and value. |
|||
*/ |
|||
row = checked_strtol(buf, &buf); |
|||
col = checked_strtol(buf, &buf); |
|||
val = strtod(buf, &buf); |
|||
|
|||
/*
|
|||
* 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::real(val), |
|||
" to position ", |
|||
pantheios::integer(row), " x ", |
|||
pantheios::integer(col)); |
|||
sp->addNextValue(row,col,val); |
|||
buf = skipWS(buf); |
|||
} |
|||
|
|||
/*
|
|||
* clean up |
|||
*/ |
|||
pantheios::log_DEBUG("Finalizing Matrix"); |
|||
sp->finalize(); |
|||
return sp; |
|||
} |
|||
|
|||
} //namespace parser
|
|||
} //namespace mrmc
|
|||
@ -0,0 +1,18 @@ |
|||
#ifndef READTRAFILE_H_ |
|||
#define READTRAFILE_H_ |
|||
|
|||
#include "src/sparse/static_sparse_matrix.h" |
|||
|
|||
namespace mrmc { |
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Load transition system from file and return initialized |
|||
* StaticSparseMatrix object. |
|||
*/ |
|||
mrmc::sparse::StaticSparseMatrix<double> * readTraFile(const char * filename); |
|||
|
|||
} // namespace parser |
|||
} // namespace mrmc |
|||
|
|||
#endif /* READTRAFILE_H_ */ |
|||
@ -1,177 +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 <iostream>
|
|||
|
|||
#ifdef WIN32
|
|||
# define STRTOK_FUNC strtok_s
|
|||
#else
|
|||
# define STRTOK_FUNC strtok_r
|
|||
#endif
|
|||
|
|||
// Only disable the warning if we are not using GCC, because
|
|||
// GCC does not know this pragma and raises a warning
|
|||
#ifndef __GNUG__
|
|||
// Disable C4996 - This function or variable may be unsafe.
|
|||
#pragma warning(disable:4996)
|
|||
#endif
|
|||
|
|||
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) { |
|||
throw mrmc::exceptions::file_IO_exception(); |
|||
return NULL; |
|||
} |
|||
|
|||
if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#DECLARATION\n")) { |
|||
fclose(P); |
|||
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 { |
|||
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; |
|||
throw mrmc::exceptions::wrong_file_format(); |
|||
return NULL; |
|||
} |
|||
|
|||
while (fgets(s, BUFFER_SIZE, P)) { |
|||
char * token = NULL; |
|||
unsigned int 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; |
|||
throw mrmc::exceptions::wrong_file_format(); |
|||
return NULL; |
|||
} |
|||
do { |
|||
token = STRTOK_FUNC(NULL, sep, &saveptr); |
|||
if (token == NULL) { |
|||
break; |
|||
} |
|||
result->addAtomicPropositionToState(token, static_cast<uint_fast64_t>(node)); |
|||
} while (token != NULL); |
|||
} |
|||
|
|||
fclose(P); |
|||
return result; |
|||
} |
|||
|
|||
} //namespace parser
|
|||
|
|||
} //namespace mrmc
|
|||
@ -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/AtomicPropositionsLabeling.h" |
|||
|
|||
|
|||
namespace mrmc { |
|||
|
|||
namespace parser { |
|||
|
|||
mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const char * filename); |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* READ_LAB_FILE_H_ */ |
|||
@ -1,161 +0,0 @@ |
|||
/*! 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. |
|||
* |
|||
* Reuses code from the file "read_tra_file.c" from the old MRMC project. |
|||
* |
|||
* Created on: 15.08.2012 |
|||
* 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"
|
|||
#include "boost/integer/integer_mask.hpp"
|
|||
#include <cstdlib>
|
|||
#include <cstdio>
|
|||
|
|||
namespace mrmc { |
|||
|
|||
namespace parser{ |
|||
|
|||
// Only disable the warning if we are not using GCC, because
|
|||
// GCC does not know this pragma and raises a warning
|
|||
#ifndef __GNUG__
|
|||
// Disable C4996 - This function or variable may be unsafe.
|
|||
#pragma warning(disable:4996)
|
|||
#endif
|
|||
|
|||
/*!
|
|||
* 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 p File stream to scan. Is expected to be opened, a NULL pointer will |
|||
* be rejected! |
|||
*/ |
|||
static uint_fast32_t make_first_pass(FILE* p) { |
|||
if(p==NULL) { |
|||
throw exceptions::file_IO_exception ("make_first_pass: File not readable (this should be checked before calling this function!)"); |
|||
} |
|||
char s[BUFFER_SIZE]; //String buffer
|
|||
int rows=0, non_zero=0; |
|||
|
|||
//Reading No. of states
|
|||
if (fgets(s, BUFFER_SIZE, p) != NULL) { |
|||
if (sscanf( s, "STATES %d", &rows) == 0) { |
|||
(void)fclose(p); |
|||
throw mrmc::exceptions::wrong_file_format(); |
|||
} |
|||
} |
|||
|
|||
//Reading No. of transitions
|
|||
if (fgets(s, BUFFER_SIZE, p) != NULL) { |
|||
if (sscanf( s, "TRANSITIONS %d", &non_zero) == 0) { |
|||
(void)fclose(p); |
|||
throw mrmc::exceptions::wrong_file_format(); |
|||
} |
|||
} |
|||
|
|||
//Reading transitions (one per line)
|
|||
//And increase number of transitions
|
|||
while (NULL != fgets( s, BUFFER_SIZE, p )) |
|||
{ |
|||
int row=0, col=0; |
|||
double val=0.0; |
|||
if (sscanf( s, "%d%d%lf", &row, &col, &val ) != 3) { |
|||
(void)fclose(p); |
|||
throw mrmc::exceptions::wrong_file_format(); |
|||
} |
|||
//Diagonal elements are not counted into the result!
|
|||
if(row == col) { |
|||
--non_zero; |
|||
} |
|||
} |
|||
return static_cast<uint_fast64_t>(non_zero); |
|||
} |
|||
|
|||
|
|||
|
|||
/*!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. |
|||
*/ |
|||
|
|||
storage::SquareSparseMatrix<double> * read_tra_file(const char * filename) { |
|||
FILE *p = NULL; |
|||
char s[BUFFER_SIZE]; |
|||
uint_fast64_t non_zero = 0; |
|||
int rows = 0; |
|||
storage::SquareSparseMatrix<double> *sp = NULL; |
|||
|
|||
p = fopen(filename, "r"); |
|||
if(p == NULL) { |
|||
throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)"); |
|||
return NULL; |
|||
} |
|||
non_zero = make_first_pass(p); |
|||
|
|||
//Set file reader back to the beginning
|
|||
rewind(p); |
|||
|
|||
//Reading No. of states
|
|||
if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "STATES %d", &rows) == 0)) { |
|||
(void)fclose(p); |
|||
throw mrmc::exceptions::wrong_file_format(); |
|||
return NULL; |
|||
} |
|||
|
|||
/* Reading No. of transitions
|
|||
* Note that the result is not used in this function as make_first_pass() |
|||
* computes the relevant number (non_zero) |
|||
*/ |
|||
int nnz = 0; |
|||
if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "TRANSITIONS %d", &nnz) == 0)) { |
|||
(void)fclose(p); |
|||
throw mrmc::exceptions::wrong_file_format(); |
|||
return NULL; |
|||
} |
|||
|
|||
/* 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 storage::SquareSparseMatrix<double>(static_cast<uint_fast64_t>(rows) + 1); |
|||
if ( NULL == sp ) { |
|||
throw std::bad_alloc(); |
|||
return NULL; |
|||
} |
|||
sp->initialize(non_zero); |
|||
|
|||
//Reading transitions (one per line) and saving the results in the matrix
|
|||
while (NULL != fgets(s, BUFFER_SIZE, p )) { |
|||
int row=0, col=0; |
|||
double val = 0.0; |
|||
if (sscanf(s, "%d%d%lf", &row, &col, &val) != 3) { |
|||
(void)fclose(p); |
|||
throw mrmc::exceptions::wrong_file_format(); |
|||
// Delete Matrix to free allocated memory
|
|||
delete sp; |
|||
return NULL; |
|||
} |
|||
sp->addNextValue(static_cast<uint_fast64_t>(row),static_cast<uint_fast64_t>(col),static_cast<uint_fast64_t>(val)); |
|||
} |
|||
|
|||
(void)fclose(p); |
|||
|
|||
sp->finalize(); |
|||
return sp; |
|||
} |
|||
|
|||
} //namespace parser
|
|||
|
|||
} //namespace mrmc
|
|||
@ -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/storage/SquareSparseMatrix.h" |
|||
namespace mrmc{ |
|||
namespace parser { |
|||
|
|||
mrmc::storage::SquareSparseMatrix<double> * read_tra_file(const char * filename); |
|||
|
|||
} |
|||
} |
|||
|
|||
|
|||
#endif /* READ_TRA_FILE_H_ */ |
|||
@ -0,0 +1,11 @@ |
|||
#pragma once |
|||
|
|||
#if defined __linux__ || defined __linux |
|||
#define LINUX |
|||
#elif defined TARGET_OS_MAC || defined __apple__ |
|||
#define MACOSX |
|||
#elif defined _WIN32 || defined _WIN64 |
|||
#define WINDOWS |
|||
#else |
|||
#error Could not detect Operating System |
|||
#endif |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue