您最多选择25个主题 主题必须以字母或数字开头,可以包含连字符 (-),并且长度不得超过35个字符

140 行
4.8 KiB

  1. #ifndef STORM_PARSER_AUTOPARSER_H_
  2. #define STORM_PARSER_AUTOPARSER_H_
  3. #include "src/parser/Parser.h"
  4. #include "src/models/AbstractModel.h"
  5. #include "src/exceptions/WrongFormatException.h"
  6. #include "src/models/AbstractModel.h"
  7. #include "src/parser/DeterministicModelParser.h"
  8. #include "src/parser/NondeterministicModelParser.h"
  9. #include "src/parser/MarkovAutomatonParser.h"
  10. #include <memory>
  11. #include <iostream>
  12. #include <utility>
  13. #include <string>
  14. #include <cctype>
  15. namespace storm {
  16. namespace parser {
  17. /*!
  18. * @brief Checks the given files and parses the model within these files.
  19. *
  20. * This parser analyzes the format hint in the first line of the transition
  21. * file. If this is a valid format, it will use the parser for this format,
  22. * otherwise it will throw an exception.
  23. *
  24. * When the files are parsed successfully, the parsed ModelType and Model
  25. * can be obtained via getType() and getModel<ModelClass>().
  26. */
  27. template<class T>
  28. class AutoParser {
  29. public:
  30. AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
  31. std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "") : model(nullptr) {
  32. storm::models::ModelType type = this->analyzeHint(transitionSystemFile);
  33. if (type == storm::models::Unknown) {
  34. LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
  35. LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
  36. throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionSystemFile;
  37. } else {
  38. LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
  39. }
  40. // Do actual parsing
  41. switch (type) {
  42. case storm::models::DTMC: {
  43. this->model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParserAsDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
  44. break;
  45. }
  46. case storm::models::CTMC: {
  47. this->model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParserAsCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
  48. break;
  49. }
  50. case storm::models::MDP: {
  51. this->model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParserAsMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
  52. break;
  53. }
  54. case storm::models::CTMDP: {
  55. this->model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParserAsCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
  56. break;
  57. }
  58. case storm::models::MA: {
  59. this->model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
  60. break;
  61. }
  62. default: ; // Unknown
  63. }
  64. if (!this->model) {
  65. LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type. Model is still null.");
  66. }
  67. }
  68. /*!
  69. * @brief Returns the type of model that was parsed.
  70. */
  71. storm::models::ModelType getType() {
  72. if (this->model) {
  73. return this->model->getType();
  74. } else {
  75. return storm::models::Unknown;
  76. }
  77. }
  78. /*!
  79. * @brief Returns the model with the given type.
  80. */
  81. template <typename Model>
  82. std::shared_ptr<Model> getModel() {
  83. return this->model->template as<Model>();
  84. }
  85. private:
  86. /*!
  87. * @brief Open file and read file format hint.
  88. */
  89. storm::models::ModelType analyzeHint(const std::string& filename) {
  90. storm::models::ModelType hintType = storm::models::Unknown;
  91. // Parse the File and check for the Line Endings
  92. storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename);
  93. // Open file
  94. MappedFile file(filename.c_str());
  95. char* buf = file.data;
  96. // parse hint
  97. char hint[128];
  98. // %20s => The Input Hint can be AT MOST 120 chars long
  99. storm::parser::scanForModelHint(hint, sizeof(hint), buf, lineEndings);
  100. for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
  101. // check hint
  102. if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
  103. else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
  104. else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
  105. else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
  106. else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA;
  107. return hintType;
  108. }
  109. /*!
  110. * @brief Pointer to a parser that has parsed the given transition system.
  111. */
  112. std::shared_ptr<storm::models::AbstractModel<T>> model;
  113. };
  114. } // namespace parser
  115. } // namespace storm
  116. #endif /* STORM_PARSER_AUTOPARSER_H_ */