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

Added multi plattform new-line handling for parsers 

Former-commit-id: f7df0996a7
main
PBerger 12 years ago
parent
d596f126b2
commit
2fc666892d
6 changed files with 128 additions and 19 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. 35
      src/parser/AtomicPropositionLabelingParser.cpp
  2. 38
      src/parser/DeterministicSparseTransitionParser.cpp
  3. 2
      src/parser/DeterministicSparseTransitionParser.h
  4. 59
      src/parser/NondeterministicSparseTransitionParser.cpp
  5. 11
      src/parser/Parser.cpp
  6. 2
      src/parser/Parser.h

35
src/parser/AtomicPropositionLabelingParser.cpp
View File

@ -49,13 +49,42 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f
throw storm::exceptions::FileIoException() << "The supplied Labeling input file \"" << filename << "\" does not exist or is not readable by this process.";
}
/*
* Find out about the used line endings.
*/
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true);
MappedFile file(filename.c_str());
char* buf = file.data;
/*
* First run: obtain number of propositions.
*/
char separator[] = " \r\n\t";
char separator[5];// = " \r\n\t";
switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN:
separator[0] = ' ';
separator[1] = '\n';
separator[2] = '\t';
separator[3] = '\0';
separator[4] = '\0';
break;
case SupportedLineEndingsEnum::SlashR:
separator[0] = ' ';
separator[1] = '\r';
separator[2] = '\t';
separator[3] = '\0';
separator[4] = '\0';
break;
case SupportedLineEndingsEnum::SlashRN:
separator[0] = ' ';
separator[1] = '\r';
separator[2] = '\n';
separator[3] = '\t';
separator[4] = '\0';
break;
}
bool foundDecl = false, foundEnd = false;
uint_fast32_t proposition_count = 0;
{
@ -160,7 +189,7 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f
* parse node number, then iterate over propositions
*/
node = checked_strtol(buf, &buf);
while ((buf[0] != '\n') && (buf[0] != '\0')) {
while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) {
cnt = strcspn(buf, separator);
if (cnt == 0) {
/*
@ -168,7 +197,7 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f
* if it's a newline, we continue with next node
* otherwise we skip it and try again
*/
if (buf[0] == '\n') break;
if (buf[0] == '\n' || buf[0] == '\r') break;
buf++;
} else {
/*

38
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -44,15 +44,27 @@ namespace parser {
* @param buf Data to scan. Is expected to be some char array.
* @param maxnode Is set to highest id of all nodes.
*/
uint_fast64_t firstPass(char* buf, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
bool isRewardMatrix = rewardMatrixInformation != nullptr;
uint_fast64_t nonZeroEntryCount = 0;
/*
* Check file header and extract number of transitions.
*/
if (!isRewardMatrix) {
buf = strchr(buf, '\n') + 1; // skip format hint
// skip format hint
switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN:
buf = strchr(buf, '\n') + 1;
break;
case SupportedLineEndingsEnum::SlashR:
buf = strchr(buf, '\r') + 1;
break;
case SupportedLineEndingsEnum::SlashRN:
buf = strchr(buf, '\r') + 2;
break;
}
}
/*
@ -129,7 +141,7 @@ uint_fast64_t firstPass(char* buf, uint_fast64_t& maxnode, RewardMatrixInformati
* @return a pointer to the created sparse matrix.
*/
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) {
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::string const& filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) {
/*
* Enforce locale where decimal point is '.'.
*/
@ -142,6 +154,11 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process.";
}
/*
* Find out about the used line endings.
*/
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true);
/*
* Open file.
*/
@ -152,7 +169,7 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
* Perform first pass, i.e. count entries that are not zero.
*/
uint_fast64_t maxStateId;
uint_fast64_t nonZeroEntryCount = firstPass(file.data, maxStateId, rewardMatrixInformation);
uint_fast64_t nonZeroEntryCount = firstPass(file.data, lineEndings, maxStateId, rewardMatrixInformation);
LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros.");
@ -174,7 +191,18 @@ storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::st
* Read file header, extract number of states.
*/
if (!isRewardMatrix) {
buf = strchr(buf, '\n') + 1; // skip format hint
// skip format hint
switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN:
buf = strchr(buf, '\n') + 1;
break;
case SupportedLineEndingsEnum::SlashR:
buf = strchr(buf, '\r') + 1;
break;
case SupportedLineEndingsEnum::SlashRN:
buf = strchr(buf, '\r') + 2;
break;
}
}
// If the matrix that is being parsed is a reward matrix, it should match the size of the

2
src/parser/DeterministicSparseTransitionParser.h
View File

@ -15,7 +15,7 @@ namespace parser {
* @brief Load a deterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
*/
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::string const& filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
} // namespace parser
} // namespace storm

59
src/parser/NondeterministicSparseTransitionParser.cpp
View File

@ -49,14 +49,25 @@ namespace parser {
* @param maxnode Is set to highest id of all nodes.
* @return The number of non-zero elements.
*/
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
bool isRewardFile = rewardMatrixInformation != nullptr;
/*
* Check file header and extract number of transitions.
*/
if (!isRewardFile) {
buf = strchr(buf, '\n') + 1; // skip format hint
// skip format hint
switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN:
buf = strchr(buf, '\n') + 1;
break;
case SupportedLineEndingsEnum::SlashR:
buf = strchr(buf, '\r') + 1;
break;
case SupportedLineEndingsEnum::SlashRN:
buf = strchr(buf, '\r') + 2;
break;
}
}
/*
@ -149,7 +160,17 @@ uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode
/*
* Proceed to beginning of next line.
*/
buf += strcspn(buf, " \t\n\r");
switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN:
buf += strcspn(buf, " \t\n");
break;
case SupportedLineEndingsEnum::SlashR:
buf += strcspn(buf, " \t\r");
break;
case SupportedLineEndingsEnum::SlashRN:
buf += strcspn(buf, " \t\r\n");
break;
}
buf = trimWhitespaces(buf);
}
@ -190,6 +211,11 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
bool isRewardFile = rewardMatrixInformation != nullptr;
/*
* Find out about the used line endings.
*/
SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true);
/*
* Open file.
*/
@ -201,7 +227,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
*/
int_fast64_t maxnode;
uint_fast64_t choices;
uint_fast64_t nonzero = firstPass(file.data, choices, maxnode, rewardMatrixInformation);
uint_fast64_t nonzero = firstPass(file.data, lineEndings, choices, maxnode, rewardMatrixInformation);
/*
* If first pass returned zero, the file format was wrong.
@ -221,7 +247,18 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
* Skip file header.
*/
if (!isRewardFile) {
buf = strchr(buf, '\n') + 1; // skip format hint
// skip format hint
switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN:
buf = strchr(buf, '\n') + 1;
break;
case SupportedLineEndingsEnum::SlashR:
buf = strchr(buf, '\r') + 1;
break;
case SupportedLineEndingsEnum::SlashRN:
buf = strchr(buf, '\r') + 2;
break;
}
}
if (isRewardFile) {
@ -338,7 +375,17 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
if (buf[0] == ' ') {
++buf;
}
buf += strcspn(buf, " \t\n\r");
switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN:
buf += strcspn(buf, " \t\n");
break;
case SupportedLineEndingsEnum::SlashR:
buf += strcspn(buf, " \t\r");
break;
case SupportedLineEndingsEnum::SlashRN:
buf += strcspn(buf, " \t\r\n");
break;
}
buf = trimWhitespaces(buf);
}

11
src/parser/Parser.cpp
View File

@ -72,9 +72,7 @@ char* storm::parser::trimWhitespaces(char* buf) {
/*!
* @briefs Analyzes the given file and tries to find out the used file endings.
*/
storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::string const& fileName) {
storm::parser::SupportedLineEndingsEnum result = storm::parser::SupportedLineEndingsEnum::Unsupported;
storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported) {
MappedFile fileMap(fileName.c_str());
char* buf = nullptr;
char* const bufferEnd = fileMap.dataend;
@ -91,6 +89,13 @@ storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::
return storm::parser::SupportedLineEndingsEnum::SlashN;
}
}
if (throwOnUnsupported) {
LOG4CPLUS_ERROR(logger, "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n");
throw storm::exceptions::WrongFormatException() << "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n";
}
LOG4CPLUS_WARN(logger, "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n");
return storm::parser::SupportedLineEndingsEnum::Unsupported;
}

2
src/parser/Parser.h
View File

@ -148,7 +148,7 @@ namespace parser {
/*!
* @briefs Analyzes the given file and tries to find out the used line endings.
*/
storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName);
storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported = false);
} // namespace parser
} // namespace storm

Write Preview
Loading…
Cancel
Save