Browse Source

first working version of AutoParser

tempestpy_adaptions
gereon 12 years ago
parent
commit
4dbbb1486b
  1. 77
      src/parser/AutoParser.cpp
  2. 25
      src/parser/AutoParser.h
  3. 2
      src/parser/DeterministicSparseTransitionParser.cpp

77
src/parser/AutoParser.cpp

@ -6,48 +6,24 @@
//#include "NonDeterministicSparseTransitionParser.h"
#include <string>
#include <cctype>
namespace storm {
namespace parser {
AutoParser::AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
std::string const & stateRewardFile, std::string const & transitionRewardFile)
{
: model(nullptr) {
storm::models::ModelType name = this->analyzeFilename(transitionSystemFile);
std::pair<storm::models::ModelType,storm::models::ModelType> content = this->analyzeContent(transitionSystemFile);
storm::models::ModelType hint = content.first, transitions = content.second;
storm::models::ModelType type = this->analyzeHint(transitionSystemFile);
storm::models::ModelType type = storm::models::Unknown;
if (hint == storm::models::Unknown) {
if (name == transitions) type = name;
else {
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ". Filename suggests " << name << " but transitions look like " << transitions); LOG4CPLUS_ERROR(logger, "Please fix your file and try again.");
throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile;
}
} else {
if ((hint == name) && (name == transitions)) type = name;
else if (hint == name) {
LOG4CPLUS_WARN(logger, "Transition format in file " << transitionSystemFile << " of type " << name << " look like " << transitions << " transitions.");
LOG4CPLUS_WARN(logger, "We will use the parser for " << name << " and hope for the best!");
type = name;
}
else if (hint == transitions) {
LOG4CPLUS_WARN(logger, "File extension of " << transitionSystemFile << " suggests type " << name << " but the content seems to be " << hint);
LOG4CPLUS_WARN(logger, "We will use the parser for " << hint << " and hope for the best!");
type = hint;
}
else if (name == transitions) {
LOG4CPLUS_WARN(logger, "File " << transitionSystemFile << " contains a hint that it is " << hint << " but filename and transition pattern suggests " << name);
LOG4CPLUS_WARN(logger, "We will use the parser for " << name << " and hope for the best!");
type = name;
}
else {
LOG4CPLUS_WARN(logger, "File " << transitionSystemFile << " contains a hint that it is " << hint << " but filename suggests " << name << " and transition pattern suggests " << transitions);
LOG4CPLUS_WARN(logger, "We will stick to the hint, use the parser for " << hint << " and hope for the best!");
type = hint;
}
if (type == storm::models::Unknown) {
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile;
}
else {
LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
}
// Do actual parsing
@ -65,26 +41,13 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con
break;
default: ; // Unknown
}
}
storm::models::ModelType AutoParser::analyzeFilename(const std::string& filename) {
storm::models::ModelType type = storm::models::Unknown;
// find file extension
std::string::size_type extpos = filename.rfind(".");
if (extpos == std::string::npos) return storm::models::Unknown;
else extpos++;
// check file extension
if (filename.substr(extpos) == "dtmc") type = storm::models::DTMC;
else if (filename.substr(extpos) == "mdp") type = storm::models::MDP;
return type;
if (! this->model) std::cout << "model is still null" << std::endl;
}
std::pair<storm::models::ModelType,storm::models::ModelType> AutoParser::analyzeContent(const std::string& filename) {
storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) {
storm::models::ModelType hintType = storm::models::Unknown, transType = storm::models::Unknown;
storm::models::ModelType hintType = storm::models::Unknown;
// Open file
MappedFile file(filename.c_str());
char* buf = file.data;
@ -92,18 +55,16 @@ std::pair<storm::models::ModelType,storm::models::ModelType> AutoParser::analyze
// parse hint
char hint[128];
sscanf(buf, "%s\n", hint);
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
// check hint
if (strncmp(hint, "dtmc", sizeof(hint)) == 0) hintType = storm::models::DTMC;
else if (strncmp(hint, "mdp", sizeof(hint)) == 0) hintType = storm::models::MDP;
if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
// check transition format
// todo.
return std::pair<storm::models::ModelType,storm::models::ModelType>(hintType, transType);
return hintType;
}
} //namespace parser
} //namespace storm

25
src/parser/AutoParser.h

@ -14,17 +14,9 @@ namespace parser {
/*!
* @brief Checks the given files and parses the model within these files.
*
* This parser analyzes the filename, an optional format hint (in the first
* line of the transition file) and the transitions within the file.
*
* If all three (or two, if the hint is not given) are consistent, it will
* call the appropriate parser.
* If two guesses are the same but the third one contradicts, it will issue
* a warning to the user and call the (hopefully) appropriate parser.
* If all guesses differ, but a format hint is given, it will issue a
* warning to the user and use the format hint to determine the correct
* parser.
* Otherwise, it will issue an error.
* This parser analyzes the format hitn in the first line of the transition
* file. If this is a valid format, it will use the parser for this format,
* otherwise it will throw an exception.
*
* When the files are parsed successfully, the parsed ModelType and Model
* can be obtained via getType() and getModel<ModelClass>().
@ -38,7 +30,8 @@ class AutoParser : Parser {
* @brief Returns the type of model that was parsed.
*/
storm::models::ModelType getType() {
return this->model->getType();
if (this->model) return this->model->getType();
else return storm::models::Unknown;
}
/*!
@ -51,11 +44,13 @@ class AutoParser : Parser {
private:
storm::models::ModelType analyzeFilename(const std::string& filename);
std::pair<storm::models::ModelType, storm::models::ModelType> analyzeContent(const std::string& filename);
/*!
* @brief Open file and read file format hint.
*/
storm::models::ModelType analyzeHint(const std::string& filename);
/*!
* @brief Pointer to a parser that has parsed the given transition system.
* @brief Pointer to a parser that has parsed the given transition system.
*/
std::shared_ptr<storm::models::AbstractModel> model;
};

2
src/parser/DeterministicSparseTransitionParser.cpp

@ -49,6 +49,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas
/*
* check file header and extract number of transitions
*/
buf = strchr(buf, '\n') + 1; // skip format hint
if (strncmp(buf, "STATES ", 7) != 0) {
LOG4CPLUS_ERROR(logger, "Expected \"STATES\" but got \"" << std::string(buf, 0, 16) << "\".");
return 0;
@ -142,6 +143,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
/*
* read file header, extract number of states
*/
buf = strchr(buf, '\n') + 1; // skip format hint
buf += 7; // skip "STATES "
checked_strtol(buf, &buf);
buf = trimWhitespaces(buf);

Loading…
Cancel
Save