diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 5d22c39e9..f11366e8b 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -6,48 +6,24 @@ //#include "NonDeterministicSparseTransitionParser.h" #include +#include 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 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 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 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; - - - // check transition format - // todo. - - return std::pair(hintType, transType); + 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; + + return hintType; } } //namespace parser - } //namespace storm diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index 51f4e1d6a..d609f10dc 100644 --- a/src/parser/AutoParser.h +++ b/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(). @@ -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 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 model; }; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index a970cfec4..6247fda29 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/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);