diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 31c71953c..5d22c39e9 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -2,82 +2,89 @@ #include "src/exceptions/WrongFileFormatException.h" -#include "DeterministicSparseTransitionParser.h" -#include "NonDeterministicSparseTransitionParser.h" +#include "src/parser/DtmcParser.h" +//#include "NonDeterministicSparseTransitionParser.h" #include namespace storm { namespace parser { -AutoParser::AutoParser(const std::string& filename) - : type(Unknown) { +AutoParser::AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) + { - ModelType name = this->analyzeFilename(filename); - std::pair content = this->analyzeContent(filename); - ModelType hint = content.first, transitions = content.second; + storm::models::ModelType name = this->analyzeFilename(transitionSystemFile); + std::pair content = this->analyzeContent(transitionSystemFile); + storm::models::ModelType hint = content.first, transitions = content.second; - if (hint == Unknown) { - if (name == transitions) this->type = name; + 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 " << filename << ". 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 " << filename; + 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)) this->type = name; + if ((hint == name) && (name == transitions)) type = name; else if (hint == name) { - LOG4CPLUS_WARN(logger, "Transition format in file " << filename << " of type " << name << " look like " << transitions << " transitions."); + 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!"); - this->type = name; + type = name; } else if (hint == transitions) { - LOG4CPLUS_WARN(logger, "File extension of " << filename << " suggests type " << name << " but the content seems to be " << hint); + 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!"); - this->type = hint; + type = hint; } else if (name == transitions) { - LOG4CPLUS_WARN(logger, "File " << filename << " contains a hint that it is " << hint << " but filename and transition pattern suggests " << name); + 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!"); - this->type = name; + type = name; } else { - LOG4CPLUS_WARN(logger, "File " << filename << " contains a hint that it is " << hint << " but filename suggests " << name << " and transition pattern suggests " << transitions); + 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!"); - this->type = hint; + type = hint; } } // Do actual parsing - switch (this->type) { - case DTMC: - this->parser = new DeterministicSparseTransitionParser(filename); + switch (type) { + case storm::models::DTMC: { + DtmcParser* parser = new DtmcParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser->getDtmc(); + break; + } + case storm::models::CTMC: + break; + case storm::models::MDP: break; - case NDTMC: - this->parser = new NonDeterministicSparseTransitionParser(filename); + case storm::models::CTMDP: break; default: ; // Unknown } } -ModelType AutoParser::analyzeFilename(const std::string& filename) { - ModelType type = 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 Unknown; + if (extpos == std::string::npos) return storm::models::Unknown; else extpos++; // check file extension - if (filename.substr(extpos) == "dtmc") type = DTMC; - else if (filename.substr(extpos) == "ndtmc") type = NDTMC; + if (filename.substr(extpos) == "dtmc") type = storm::models::DTMC; + else if (filename.substr(extpos) == "mdp") type = storm::models::MDP; return type; } -std::pair AutoParser::analyzeContent(const std::string& filename) { +std::pair AutoParser::analyzeContent(const std::string& filename) { - ModelType hintType = Unknown, transType = Unknown; + storm::models::ModelType hintType = storm::models::Unknown, transType = storm::models::Unknown; // Open file MappedFile file(filename.c_str()); char* buf = file.data; @@ -87,14 +94,14 @@ std::pair AutoParser::analyzeContent(const std::string& fil sscanf(buf, "%s\n", hint); // check hint - if (strncmp(hint, "dtmc", sizeof(hint)) == 0) hintType = DTMC; - else if (strncmp(hint, "ndtmc", sizeof(hint)) == 0) hintType = NDTMC; + 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); + return std::pair(hintType, transType); } } //namespace parser diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index f1452520b..51f4e1d6a 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -1,10 +1,8 @@ #ifndef STORM_PARSER_AUTOPARSER_H_ #define STORM_PARSER_AUTOPARSER_H_ -#include "src/models/AtomicPropositionsLabeling.h" -#include "boost/integer/integer_mask.hpp" - #include "src/parser/Parser.h" +#include "src/models/AbstractModel.h" #include #include @@ -14,28 +12,10 @@ namespace storm { namespace parser { /*! - * @brief Enumeration of all supported types of models. - */ -enum ModelType { - Unknown, DTMC, NDTMC -}; - -std::ostream& operator<<(std::ostream& os, const ModelType type) -{ - switch (type) { - case Unknown: os << "Unknown"; break; - case DTMC: os << "DTMC"; break; - case NDTMC: os << "NDTMC"; break; - default: os << "Invalid ModelType"; - } - return os; -} - -/*! - * @brief Checks the given file and tries to call the correct 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 file) and the transitions within the file. + * 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. @@ -45,40 +25,39 @@ std::ostream& operator<<(std::ostream& os, const ModelType type) * warning to the user and use the format hint to determine the correct * parser. * Otherwise, it will issue an error. + * + * When the files are parsed successfully, the parsed ModelType and Model + * can be obtained via getType() and getModel(). */ class AutoParser : Parser { public: - AutoParser(const std::string& filename); + AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); /*! - * @brief Returns the type of transition system that was detected. + * @brief Returns the type of model that was parsed. */ - ModelType getModelType() { - return this->type; + storm::models::ModelType getType() { + return this->model->getType(); } - template - T* getParser() { - return dynamic_cast( this->parser ); + /*! + * @brief Returns the model with the given type. + */ + template + std::shared_ptr getModel() { + return this->model->as(); } - ~AutoParser() { - delete this->parser; - } private: - ModelType analyzeFilename(const std::string& filename); - std::pair analyzeContent(const std::string& filename); - - /*! - * @brief Type of the transition system. - */ - ModelType type; + storm::models::ModelType analyzeFilename(const std::string& filename); + std::pair analyzeContent(const std::string& filename); /*! * @brief Pointer to a parser that has parsed the given transition system. */ - Parser* parser; + std::shared_ptr model; }; } // namespace parser