Browse Source

A thousand things.

- More tests.
- Changed SparseStateRewardParser to a static class
- Added comments here and there
- Some reformatting.
- Fixed some warnings.
- Eliminated some unnecessary includes.
- ...


Former-commit-id: efe1c96fee
main
masawei 12 years ago
parent
commit
f8566e9dc2
  1. 2
      src/parser/DeterministicModelParser.cpp
  2. 4
      src/parser/MarkovAutomatonParser.cpp
  3. 3
      src/parser/MarkovAutomatonParser.h
  4. 4
      src/parser/MarkovAutomatonSparseTransitionParser.cpp
  5. 6
      src/parser/MarkovAutomatonSparseTransitionParser.h
  6. 2
      src/parser/NondeterministicModelParser.cpp
  7. 78
      src/parser/Parser.cpp
  8. 1
      src/parser/Parser.h
  9. 20
      src/parser/SparseStateRewardParser.cpp
  10. 13
      src/parser/SparseStateRewardParser.h
  11. 39
      test/functional/parser/MarkovAutomatonParserTest.cpp

2
src/parser/DeterministicModelParser.cpp

@ -39,7 +39,7 @@ DeterministicModelParserResultContainer<double> parseDeterministicModel(std::str
DeterministicModelParserResultContainer<double> result(std::move(resultTransitionSystem), std::move(resultLabeling));
if (stateRewardFile != "") {
result.stateRewards.reset(storm::parser::SparseStateRewardParser(stateCount, stateRewardFile));
result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile));
}
if (transitionRewardFile != "") {
RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(rowCount, stateCount, nullptr);

4
src/parser/MarkovAutomatonParser.cpp

@ -3,6 +3,7 @@
#include "SparseStateRewardParser.h"
namespace storm {
namespace parser {
storm::models::MarkovAutomaton<double> MarkovAutomatonParser::parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) {
@ -11,7 +12,7 @@ namespace storm {
boost::optional<std::vector<double>> stateRewards;
if (stateRewardFilename != "") {
stateRewards.reset(storm::parser::SparseStateRewardParser(transitionResult.transitionMatrix.getColumnCount(), stateRewardFilename));
stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionResult.transitionMatrix.getColumnCount(), stateRewardFilename));
}
if (transitionRewardFilename != "") {
@ -25,4 +26,5 @@ namespace storm {
}
} // namespace parser
} // namespace storm

3
src/parser/MarkovAutomatonParser.h

@ -5,6 +5,7 @@
#include "src/parser/MarkovAutomatonSparseTransitionParser.h"
namespace storm {
namespace parser {
/*!
@ -23,7 +24,9 @@ namespace storm {
*/
static storm::models::MarkovAutomaton<double> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename);
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_MARKOVAUTOMATONPARSER_H_ */

4
src/parser/MarkovAutomatonSparseTransitionParser.cpp

@ -3,6 +3,7 @@
#include "src/settings/Settings.h"
namespace storm {
namespace parser {
MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings) {
@ -192,7 +193,6 @@ namespace storm {
buf = forwardToNextLine(buf, lineEndings);
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
bool hasSuccessorState = false;
bool encounteredNewDistribution = false;
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
@ -205,8 +205,6 @@ namespace storm {
// we may legally stop reading here.
encounteredEOF = true;
} else if (buf[0] == '*') {
// We need to record that we found at least one successor state for the current choice.
hasSuccessorState = true;
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf = skipWord(buf);

6
src/parser/MarkovAutomatonSparseTransitionParser.h

@ -6,6 +6,7 @@
#include "Parser.h"
namespace storm {
namespace parser {
/*
@ -39,6 +40,10 @@ namespace storm {
*/
struct ResultType {
/*
* Creates a new instance of the struct using the result of the first pass to correctly initialize the container.
* @param firstPassResult A reference to the result of the first pass.
*/
ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) {
transitionMatrix.initialize(firstPassResult.numberOfNonzeroEntries);
// Intentionally left empty.
@ -90,6 +95,7 @@ namespace storm {
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_MARKOVAUTOMATONSPARSETRANSITIONPARSER_H_ */

2
src/parser/NondeterministicModelParser.cpp

@ -40,7 +40,7 @@ NondeterministicModelParserResultContainer<double> parseNondeterministicModel(st
NondeterministicModelParserResultContainer<double> result(std::move(resultTransitionSystem), std::move(nondeterministicSparseTransitionParserResult.second), std::move(resultLabeling));
if (stateRewardFile != "") {
result.stateRewards.reset(storm::parser::SparseStateRewardParser(stateCount, stateRewardFile));
result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile));
}
if (transitionRewardFile != "") {
RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(rowCount, stateCount, &result.rowMapping);

78
src/parser/Parser.cpp

@ -13,6 +13,10 @@
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace parser {
/*!
* 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
@ -21,7 +25,7 @@ extern log4cplus::Logger logger;
* @param end New pointer will be written there
* @return Result of strtol()
*/
uint_fast64_t storm::parser::checked_strtol(const char* str, char** end) {
uint_fast64_t checked_strtol(const char* str, char** end) {
uint_fast64_t res = strtol(str, end, 10);
if (str == *end) {
LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number.");
@ -39,7 +43,7 @@ uint_fast64_t storm::parser::checked_strtol(const char* str, char** end) {
* @param end New pointer will be written there
* @return Result of strtod()
*/
double storm::parser::checked_strtod(const char* str, char** end) {
double checked_strtod(const char* str, char** end) {
double res = strtod(str, end);
if (str == *end) {
LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number.");
@ -53,7 +57,7 @@ double storm::parser::checked_strtod(const char* str, char** end) {
* @brief Tests whether the given file exists and is readable.
* @return True iff the file exists and is readable.
*/
bool storm::parser::fileExistsAndIsReadable(const char* fileName) {
bool fileExistsAndIsReadable(const char* fileName) {
std::ifstream fin(fileName);
bool returnValue = !fin.fail();
return returnValue;
@ -62,8 +66,10 @@ bool storm::parser::fileExistsAndIsReadable(const char* fileName) {
/*!
* Skips all numbers, letters and special characters.
* Returns a pointer to the first char that is a whitespace.
* @param buf The string buffer to operate on.
* @return A pointer to the first whitespace character.
*/
char* storm::parser::skipWord(char* buf){
char* skipWord(char* buf){
while((*buf != ' ') && (*buf != '\t') && (*buf != '\n') && (*buf != '\r')) buf++;
return buf;
}
@ -71,10 +77,10 @@ char* storm::parser::skipWord(char* buf){
/*!
* Skips spaces, tabs, newlines and carriage returns. Returns a pointer
* to first char that is not a whitespace.
* @param buf String buffer
* @return pointer to first non-whitespace character
* @param buf The string buffer to operate on.
* @return A pointer to the first non-whitespace character.
*/
char* storm::parser::trimWhitespaces(char* buf) {
char* trimWhitespaces(char* buf) {
while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++;
return buf;
}
@ -82,7 +88,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, bool throwOnUnsupported) {
SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported) {
MappedFile fileMap(fileName.c_str());
char* buf = nullptr;
char* const bufferEnd = fileMap.dataend;
@ -91,11 +97,11 @@ storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::
if (*buf == '\r') {
// check for following \n
if (((buf + sizeof(char)) < bufferEnd) && (*(buf + sizeof(char)) == '\n')) {
return storm::parser::SupportedLineEndingsEnum::SlashRN;
return SupportedLineEndingsEnum::SlashRN;
}
return storm::parser::SupportedLineEndingsEnum::SlashR;
return SupportedLineEndingsEnum::SlashR;
} else if (*buf == '\n') {
return storm::parser::SupportedLineEndingsEnum::SlashN;
return SupportedLineEndingsEnum::SlashN;
}
}
@ -105,25 +111,25 @@ storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::
}
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;
return SupportedLineEndingsEnum::Unsupported;
}
/*!
* @brief Encapsulates the usage of function @strchr to forward to the next line
*/
char* storm::parser::forwardToNextLine(char* buffer, storm::parser::SupportedLineEndingsEnum lineEndings) {
char* forwardToNextLine(char* buffer, SupportedLineEndingsEnum lineEndings) {
switch (lineEndings) {
case storm::parser::SupportedLineEndingsEnum::SlashN:
case SupportedLineEndingsEnum::SlashN:
return strchr(buffer, '\n') + 1;
break;
case storm::parser::SupportedLineEndingsEnum::SlashR:
case SupportedLineEndingsEnum::SlashR:
return strchr(buffer, '\r') + 1;
break;
case storm::parser::SupportedLineEndingsEnum::SlashRN:
case SupportedLineEndingsEnum::SlashRN:
return strchr(buffer, '\r') + 2;
break;
default:
case storm::parser::SupportedLineEndingsEnum::Unsupported:
case SupportedLineEndingsEnum::Unsupported:
// This Line will never be reached as the Parser would have thrown already.
throw;
break;
@ -136,26 +142,26 @@ char* storm::parser::forwardToNextLine(char* buffer, storm::parser::SupportedLin
* @param targetBuffer The Target for the hint, must be at least 64 bytes long
* @param buffer The Source Buffer from which the Model Hint will be read
*/
void storm::parser::scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, storm::parser::SupportedLineEndingsEnum lineEndings) {
void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, SupportedLineEndingsEnum lineEndings) {
if (targetBufferSize <= 4) {
throw;
}
switch (lineEndings) {
case storm::parser::SupportedLineEndingsEnum::SlashN:
case SupportedLineEndingsEnum::SlashN:
#ifdef WINDOWS
sscanf_s(buffer, "%60s\n", targetBuffer, targetBufferSize);
#else
sscanf(buffer, "%60s\n", targetBuffer);
#endif
break;
case storm::parser::SupportedLineEndingsEnum::SlashR:
case SupportedLineEndingsEnum::SlashR:
#ifdef WINDOWS
sscanf_s(buffer, "%60s\r", targetBuffer, sizeof(targetBufferSize));
#else
sscanf(buffer, "%60s\r", targetBuffer);
#endif
break;
case storm::parser::SupportedLineEndingsEnum::SlashRN:
case SupportedLineEndingsEnum::SlashRN:
#ifdef WINDOWS
sscanf_s(buffer, "%60s\r\n", targetBuffer, sizeof(targetBufferSize));
#else
@ -163,7 +169,7 @@ void storm::parser::scanForModelHint(char* targetBuffer, uint_fast64_t targetBuf
#endif
break;
default:
case storm::parser::SupportedLineEndingsEnum::Unsupported:
case SupportedLineEndingsEnum::Unsupported:
// This Line will never be reached as the Parser would have thrown already.
throw;
break;
@ -173,9 +179,9 @@ void storm::parser::scanForModelHint(char* targetBuffer, uint_fast64_t targetBuf
/*!
* @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0
*/
void storm::parser::getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, storm::parser::SupportedLineEndingsEnum lineEndings) {
void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, SupportedLineEndingsEnum lineEndings) {
if (targetBufferSize < 5) {
LOG4CPLUS_ERROR(logger, "storm::parser::getMatchingSeparatorString: The passed Target Buffer is too small.");
LOG4CPLUS_ERROR(logger, "getMatchingSeparatorString: The passed Target Buffer is too small.");
throw;
}
switch (lineEndings) {
@ -209,7 +215,7 @@ void storm::parser::getMatchingSeparatorString(char* targetBuffer, uint_fast64_t
default:
case SupportedLineEndingsEnum::Unsupported:
// This Line will never be reached as the Parser would have thrown already.
LOG4CPLUS_ERROR(logger, "storm::parser::getMatchingSeparatorString: The passed lineEndings were Unsupported. Check your input file.");
LOG4CPLUS_ERROR(logger, "getMatchingSeparatorString: The passed lineEndings were Unsupported. Check your input file.");
throw;
break;
}
@ -221,7 +227,7 @@ void storm::parser::getMatchingSeparatorString(char* targetBuffer, uint_fast64_t
* and a log entry is written.
* @param filename file to be opened
*/
storm::parser::MappedFile::MappedFile(const char* filename) {
MappedFile::MappedFile(const char* filename) {
#if defined LINUX || defined MACOSX
/*
* Do file mapping for reasonable systems.
@ -233,20 +239,20 @@ storm::parser::MappedFile::MappedFile(const char* filename) {
if (stat64(filename, &(this->st)) != 0) {
#endif
LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException() << "storm::parser::MappedFile Error in stat(): Probably, this file does not exist.";
throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist.";
}
this->file = open(filename, O_RDONLY);
if (this->file < 0) {
LOG4CPLUS_ERROR(logger, "Error in open(" << filename << "): Probably, we may not read this file.");
throw exceptions::FileIoException() << "storm::parser::MappedFile Error in open(): Probably, we may not read this file.";
throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file.";
}
this->data = reinterpret_cast<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
if (this->data == reinterpret_cast<char*>(-1)) {
close(this->file);
LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno));
throw exceptions::FileIoException() << "storm::parser::MappedFile Error in mmap(): " << std::strerror(errno);
throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno);
}
this->dataend = this->data + this->st.st_size;
#elif defined WINDOWS
@ -256,20 +262,20 @@ storm::parser::MappedFile::MappedFile(const char* filename) {
*/
if (_stat64(filename, &(this->st)) != 0) {
LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException("storm::parser::MappedFile Error in stat(): Probably, this file does not exist.");
throw exceptions::FileIoException("MappedFile Error in stat(): Probably, this file does not exist.");
}
this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
if (this->file == INVALID_HANDLE_VALUE) {
LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << "): Probably, we may not read this file.");
throw exceptions::FileIoException("storm::parser::MappedFile Error in CreateFileA(): Probably, we may not read this file.");
throw exceptions::FileIoException("MappedFile Error in CreateFileA(): Probably, we may not read this file.");
}
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);
LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ").");
throw exceptions::FileIoException("storm::parser::MappedFile Error in CreateFileMappingA().");
throw exceptions::FileIoException("MappedFile Error in CreateFileMappingA().");
}
this->data = static_cast<char*>(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size));
@ -277,7 +283,7 @@ storm::parser::MappedFile::MappedFile(const char* filename) {
CloseHandle(this->mapping);
CloseHandle(this->file);
LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ").");
throw exceptions::FileIoException("storm::parser::MappedFile Error in MapViewOfFile().");
throw exceptions::FileIoException("MappedFile Error in MapViewOfFile().");
}
this->dataend = this->data + this->st.st_size;
#endif
@ -286,7 +292,7 @@ storm::parser::MappedFile::MappedFile(const char* filename) {
/*!
* Will unmap the data and close the file.
*/
storm::parser::MappedFile::~MappedFile() {
MappedFile::~MappedFile() {
#if defined LINUX || defined MACOSX
munmap(this->data, this->st.st_size);
close(this->file);
@ -295,3 +301,7 @@ storm::parser::MappedFile::~MappedFile() {
CloseHandle(this->file);
#endif
}
} // namespace parser
} // namespace storm

1
src/parser/Parser.h

@ -174,6 +174,7 @@ namespace parser {
void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, storm::parser::SupportedLineEndingsEnum lineEndings);
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_PARSER_H_ */

20
src/parser/SparseStateRewardParser.cpp

@ -7,29 +7,18 @@
#include "src/parser/SparseStateRewardParser.h"
#include <errno.h>
#include <time.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <locale.h>
#include <iostream>
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <string>
#include <vector>
#include <clocale>
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/FileIoException.h"
#include "src/utility/OsDetection.h"
#include "src/parser/Parser.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace parser {
namespace parser {
/*!
* Reads a state reward file and puts the result in a state reward vector.
@ -38,7 +27,7 @@ namespace parser {
* @param filename The filename of the state reward file.
* @return The created state reward vector.
*/
std::vector<double> SparseStateRewardParser(uint_fast64_t stateCount, std::string const & filename) {
std::vector<double> SparseStateRewardParser::parseSparseStateReward(uint_fast64_t stateCount, std::string const & filename) {
// Open file.
if (!fileExistsAndIsReadable(filename.c_str())) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
@ -51,7 +40,6 @@ std::vector<double> SparseStateRewardParser(uint_fast64_t stateCount, std::strin
// Create state reward vector with given state count.
std::vector<double> stateRewards(stateCount);
{
// Now parse state reward assignments.
uint_fast64_t state;
double reward;
@ -70,9 +58,9 @@ std::vector<double> SparseStateRewardParser(uint_fast64_t stateCount, std::strin
buf = trimWhitespaces(buf);
}
}
return stateRewards;
}
} // namespace parser
} // namespace storm

13
src/parser/SparseStateRewardParser.h

@ -2,18 +2,25 @@
#define STORM_PARSER_SPARSESTATEREWARDPARSER_H_
#include <cstdint>
#include "src/parser/Parser.h"
#include <memory>
#include <vector>
#include <string>
namespace storm {
namespace parser {
/*!
* A class providing the functionality to parse a the state rewards of a model.
*/
class SparseStateRewardParser {
public:
/*!
* @brief Load state reward file and return vector of state rewards.
*/
std::vector<double> SparseStateRewardParser(uint_fast64_t stateCount, std::string const &filename);
static std::vector<double> parseSparseStateReward(uint_fast64_t stateCount, std::string const &filename);
};
} // namespace parser

39
test/functional/parser/MarkovAutomatonParserTest.cpp

@ -9,8 +9,13 @@
#include "storm-config.h"
#include "src/settings/Settings.h"
#include <cmath>
#include <vector>
#include "src/parser/MarkovAutomatonSparseTransitionParser.h"
#include "src/parser/SparseStateRewardParser.h"
#include "src/parser/Parser.h"
#include "src/parser/MarkovAutomatonParser.h"
#define STATE_COUNT 6
#define CHOICE_COUNT 7
@ -176,3 +181,37 @@ TEST(MarkovAutomatonSparseTransitionParserTest, DeadlockTest) {
storm::settings::Settings::getInstance()->set("fixDeadlocks");
}
}*/
double round(double val, int precision)
{
std::stringstream s;
s << std::setprecision(precision) << std::setiosflags(std::ios_base::fixed) << val;
s >> val;
return val;
}
TEST(SparseStateRewardParserTest, BasicParseTest) {
// Get the parsing result.
std::vector<double> result = storm::parser::SparseStateRewardParser::parseSparseStateReward(100, STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/state_reward_parser_basic.state.rew");
// Now test if the correct value were parsed.
for(int i = 0; i < 100; i++) {
ASSERT_EQ(std::round(result[i]) , std::round(2*i + 15/13*i*i - 1.5/(i+0.1) + 15.7));
}
}
TEST(MarkovAutomatonParserTest, BasicParseTest) {
// Get the parsing result.
storm::models::MarkovAutomaton<double> result = storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/ma_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/ma_general_input_01.lab", STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/ma_general_input_01.state.rew", "");
// Test sizes and counts.
ASSERT_EQ(result.getNumberOfStates(), STATE_COUNT);
ASSERT_EQ(result.getNumberOfChoices(), CHOICE_COUNT);
ASSERT_EQ(result.getNumberOfTransitions(), 12);
// Test
std::vector<double> rates = result.getExitRates();
ASSERT_EQ(rates[0], 2);
}
Loading…
Cancel
Save