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

Refactored AtomicPropositionLabelingParser. 

- Not much to do here.
- Mostly comment corrections and code restructuring.

Next up: Parser.h/.cpp and the AutoParser.


Former-commit-id: 22d67dadb8
main
masawei 12 years ago
parent
c279c693e5
commit
46e783c981
7 changed files with 162 additions and 186 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. 295
      src/parser/AtomicPropositionLabelingParser.cpp
  2. 31
      src/parser/AtomicPropositionLabelingParser.h
  3. 2
      src/parser/DeterministicModelParser.cpp
  4. 6
      src/parser/DeterministicSparseTransitionParser.h
  5. 2
      src/parser/MarkovAutomatonParser.cpp
  6. 2
      src/parser/NondeterministicModelParser.cpp
  7. 10
      test/functional/parser/ReadLabFileTest.cpp

295
src/parser/AtomicPropositionLabelingParser.cpp
View File

@ -6,193 +6,164 @@
*/
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/parser/Parser.h"
#include <errno.h>
#include <time.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <locale.h>
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <string>
#include <clocale>
#include <iostream>
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/FileIoException.h"
#include "src/utility/OsDetection.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace parser {
namespace parser {
storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t node_count, std::string const & filename) {
/*!
* 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.
*/
storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const & filename) {
/*
* Open file.
*/
if (!storm::parser::fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
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[5];// = " \r\n\t";
storm::parser::getMatchingSeparatorString(separator, sizeof(separator), lineEndings);
bool foundDecl = false, foundEnd = false;
uint_fast32_t proposition_count = 0;
{
size_t cnt = 0;
/*
* Iterate over tokens until we hit #END or 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;
} else if (strncmp(buf, "#END", cnt) == 0) {
foundEnd = true;
break;
// Open the given file.
if (!storm::parser::fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
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 pass: Count the number of propositions.
// Convert the line endings into a string containing all whitespace characters, that separate words in the file.
char separator[5];
storm::parser::getMatchingSeparatorString(separator, sizeof(separator), lineEndings);
bool foundDecl = false, foundEnd = false;
uint_fast32_t proposition_count = 0;
size_t cnt = 0;
// Iterate over tokens until we hit #END or the end of the file.
while(buf[0] != '\0') {
// Move the buffer pointer to the separator.
buf += cnt;
// Get the number of characters until the next separator.
cnt = strcspn(buf, separator);
if (cnt > 0) {
// If the next token is #DECLARATION: Just skip it.
// If the next token is #END: Stop the search.
// Otherwise increase proposition_count.
if (strncmp(buf, "#DECLARATION", cnt) == 0) {
foundDecl = true;
continue;
} else if (strncmp(buf, "#END", cnt) == 0) {
foundEnd = true;
break;
}
proposition_count++;
} else {
// If the next character is a separator, skip it.
buf++;
}
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)) {
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted.");
if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token.");
if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token.");
throw storm::exceptions::WrongFormatException();
}
}
/*
* create labeling object with given node and proposition count
*/
storm::models::AtomicPropositionsLabeling labeling(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 >= sizeof(proposition)) {
/*
* if token is longer than our buffer, the following strncpy code might get risky...
*/
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found.");
// If #DECLARATION or #END have not been found, the file format is wrong.
if (!(foundDecl && foundEnd)) {
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted.");
if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token.");
if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token.");
throw storm::exceptions::WrongFormatException();
} else 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';
labeling.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_fast64_t node;
char proposition[128];
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] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) {
// Create labeling object with given node and proposition count.
storm::models::AtomicPropositionsLabeling labeling(node_count, proposition_count);
// Second pass: Add propositions and node labels to labeling.
// First thing to do: Reset the file pointer.
buf = file.data;
// Prepare a buffer for proposition names.
char proposition[128];
cnt = 0;
// Parse proposition names.
// As we already checked the file header, we know that #DECLARATION and #END are tokens in the character stream.
while(buf[0] != '\0') {
// Move the buffer pointer to the separator.
buf += cnt;
// The number of characters until the next separator.
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' || buf[0] == '\r') break;
buf++;
} else {
/*
* copy proposition to buffer and add it to labeling
*/
if (cnt >= sizeof(proposition)) {
// if token is longer than our buffer, the following strncpy code might get risky...
LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found.");
throw storm::exceptions::WrongFormatException();
} else if (cnt > 0) {
// If the next token is #DECLARATION: Just skip it.
if (strncmp(buf, "#DECLARATION", cnt) == 0) continue;
// If the next token is #END: Stop the search.
if (strncmp(buf, "#END", cnt) == 0) break;
// Otherwise copy the token to the buffer, append a trailing null byte and hand it to labeling.
strncpy(proposition, buf, cnt);
proposition[cnt] = '\0';
labeling.addAtomicPropositionToState(proposition, node);
buf += cnt;
labeling.addAtomicProposition(proposition);
} else {
// The next character is a separator, thus move one step forward.
buf++;
}
}
buf = storm::parser::trimWhitespaces(buf);
// At this point, the pointer buf is still pointing to our last token, i.e. to #END.
// We want to skip it.
buf += 4;
uint_fast64_t node;
cnt = 0;
// Now parse the assignments of labels to nodes.
while (buf[0] != '\0') {
// Parse the node number and iterate over its labels (atomic propositions).
// Stop at the end of the line.
node = checked_strtol(buf, &buf);
while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) {
cnt = strcspn(buf, separator);
if (cnt == 0) {
// The next character is a separator.
// If it is a line separator, we continue with next node.
// Otherwise, we skip it and try again.
if (buf[0] == '\n' || buf[0] == '\r') break;
buf++;
} else {
// Copy the label to the buffer, null terminate it and add it to labeling.
strncpy(proposition, buf, cnt);
proposition[cnt] = '\0';
labeling.addAtomicPropositionToState(proposition, node);
buf += cnt;
}
}
buf = trimWhitespaces(buf);
}
return labeling;
}
}
return labeling;
}
} // namespace parser
} // namespace parser
} // namespace storm

31
src/parser/AtomicPropositionLabelingParser.h
View File

@ -1,23 +1,28 @@
#ifndef STORM_PARSER_LABPARSER_H_
#define STORM_PARSER_LABPARSER_H_
#ifndef STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_
#define STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_
#include "src/models/AtomicPropositionsLabeling.h"
#include <cstdint>
#include "src/parser/Parser.h"
namespace storm {
namespace parser {
#include <memory>
class AtomicPropositionLabelingParser {
namespace storm {
namespace parser {
public:
/*
* Reads a label file and puts the result in an AtomicPropositionsLabeling object.
*
* @param node_count The number of states of the model to be labeled.
* @param filename The path and name of the labeling (.lab) file.
* @return The parsed labeling as an AtomicPropositionsLabeling object.
*/
static storm::models::AtomicPropositionsLabeling parseAtomicPropositionLabeling(uint_fast64_t node_count, std::string const &filename);
/*!
* @brief Load label file and return initialized AtomicPropositionsLabeling object.
*
*/
storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename);
};
} // namespace parser
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_LABPARSER_H_ */
#endif /* STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_ */

2
src/parser/DeterministicModelParser.cpp
View File

@ -33,7 +33,7 @@ DeterministicModelParser::Result DeterministicModelParser::parseDeterministicMod
uint_fast64_t stateCount = resultTransitionSystem.getColumnCount();
uint_fast64_t rowCount = resultTransitionSystem.getRowCount();
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile)));
DeterministicModelParser::Result result(std::move(resultTransitionSystem), std::move(labeling));

6
src/parser/DeterministicSparseTransitionParser.h
View File

@ -1,5 +1,5 @@
#ifndef STORM_PARSER_TRAPARSER_H_
#define STORM_PARSER_TRAPARSER_H_
#ifndef STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_
#define STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_
#include "src/storage/SparseMatrix.h"
#include "src/parser/Parser.h"
@ -82,4 +82,4 @@ private:
} // namespace storm
#endif /* STORM_PARSER_TRAPARSER_H_ */
#endif /* STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ */

2
src/parser/MarkovAutomatonParser.cpp
View File

@ -16,7 +16,7 @@ storm::models::MarkovAutomaton<double> MarkovAutomatonParser::parseMarkovAutomat
storm::storage::SparseMatrix<double> transitionMatrix(transitionResult.transitionMatrixBuilder.build(0,0));
// Parse the state labeling.
storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser(transitionMatrix.getColumnCount(), labelingFilename));
storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename));
// If given, parse the state rewards file.
boost::optional<std::vector<double>> stateRewards;

2
src/parser/NondeterministicModelParser.cpp
View File

@ -35,7 +35,7 @@ namespace storm {
uint_fast64_t stateCount = transitions.getColumnCount();
uint_fast64_t rowCount = transitions.getRowCount();
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile)));
storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile)));
Result result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling));

10
test/functional/parser/ReadLabFileTest.cpp
View File

@ -16,14 +16,14 @@
TEST(ReadLabFileTest, NonExistingFileTest) {
// No matter what happens, please do NOT create a file with the name "nonExistingFile.not"!
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(0,STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(0,STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
}
TEST(ReadLabFileTest, ParseTest) {
// This test is based on a test case from the original MRMC.
// Parsing the file
storm::models::AtomicPropositionsLabeling labeling = storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab");
storm::models::AtomicPropositionsLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab");
// Checking whether all propositions are in the labelling
@ -79,14 +79,14 @@ TEST(ReadLabFileTest, ParseTest) {
}
TEST(ReadLabFileTest, WrongHeaderTest1) {
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException);
}
TEST(ReadLabFileTest, WrongHeaderTest2) {
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException);
}
TEST(ReadLabFileTest, WrongPropositionTest) {
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException);
}
Write Preview
Loading…
Cancel
Save