sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

modified AutoParser to reflect changes in the model type system.

tempestpy_adaptions
gereon 12 years ago
parent
b4862360ba
commit
4dc780ef77
2 changed files with 63 additions and 77 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 79
      src/parser/AutoParser.cpp
  2. 61
      src/parser/AutoParser.h

79
src/parser/AutoParser.cpp
View File

@ -2,82 +2,89 @@
#include "src/exceptions/WrongFileFormatException.h" #include "src/exceptions/WrongFileFormatException.h"
#include "DeterministicSparseTransitionParser.h"
#include "NonDeterministicSparseTransitionParser.h"
#include "src/parser/DtmcParser.h"
//#include "NonDeterministicSparseTransitionParser.h"
#include <string> #include <string>
namespace storm { namespace storm {
namespace parser { 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<ModelType,ModelType> content = this->analyzeContent(filename);
ModelType hint = content.first, transitions = content.second;
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;
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 { 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 { } else {
if ((hint == name) && (name == transitions)) this->type = name;
if ((hint == name) && (name == transitions)) type = name;
else if (hint == 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!"); LOG4CPLUS_WARN(logger, "We will use the parser for " << name << " and hope for the best!");
this->type = name;
type = name;
} }
else if (hint == transitions) { 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!"); LOG4CPLUS_WARN(logger, "We will use the parser for " << hint << " and hope for the best!");
this->type = hint;
type = hint;
} }
else if (name == transitions) { 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!"); LOG4CPLUS_WARN(logger, "We will use the parser for " << name << " and hope for the best!");
this->type = name;
type = name;
} }
else { 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!"); 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 // 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; break;
case NDTMC:
this->parser = new NonDeterministicSparseTransitionParser(filename);
case storm::models::CTMDP:
break; break;
default: ; // Unknown 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 // find file extension
std::string::size_type extpos = filename.rfind("."); 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++; else extpos++;
// check file extension // 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; return type;
} }
std::pair<ModelType,ModelType> AutoParser::analyzeContent(const std::string& filename) {
std::pair<storm::models::ModelType,storm::models::ModelType> AutoParser::analyzeContent(const std::string& filename) {
ModelType hintType = Unknown, transType = Unknown;
storm::models::ModelType hintType = storm::models::Unknown, transType = storm::models::Unknown;
// Open file // Open file
MappedFile file(filename.c_str()); MappedFile file(filename.c_str());
char* buf = file.data; char* buf = file.data;
@ -87,14 +94,14 @@ std::pair<ModelType,ModelType> AutoParser::analyzeContent(const std::string& fil
sscanf(buf, "%s\n", hint); sscanf(buf, "%s\n", hint);
// check 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 // check transition format
// todo. // todo.
return std::pair<ModelType,ModelType>(hintType, transType);
return std::pair<storm::models::ModelType,storm::models::ModelType>(hintType, transType);
} }
} //namespace parser } //namespace parser

61
src/parser/AutoParser.h
View File

@ -1,10 +1,8 @@
#ifndef STORM_PARSER_AUTOPARSER_H_ #ifndef STORM_PARSER_AUTOPARSER_H_
#define 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/parser/Parser.h"
#include "src/models/AbstractModel.h"
#include <memory> #include <memory>
#include <iostream> #include <iostream>
@ -14,28 +12,10 @@ namespace storm {
namespace parser { 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 * 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 * If all three (or two, if the hint is not given) are consistent, it will
* call the appropriate parser. * 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 * warning to the user and use the format hint to determine the correct
* parser. * parser.
* Otherwise, it will issue an error. * Otherwise, it will issue an error.
*
* When the files are parsed successfully, the parsed ModelType and Model
* can be obtained via getType() and getModel<ModelClass>().
*/ */
class AutoParser : Parser { class AutoParser : Parser {
public: 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 <typename T>
T* getParser() {
return dynamic_cast<T*>( this->parser );
/*!
* @brief Returns the model with the given type.
*/
template <typename Model>
std::shared_ptr<Model> getModel() {
return this->model->as<Model>();
} }
~AutoParser() {
delete this->parser;
}
private: private:
ModelType analyzeFilename(const std::string& filename);
std::pair<ModelType,ModelType> analyzeContent(const std::string& filename);
/*!
* @brief Type of the transition system.
*/
ModelType type;
storm::models::ModelType analyzeFilename(const std::string& filename);
std::pair<storm::models::ModelType, storm::models::ModelType> analyzeContent(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.
*/ */
Parser* parser;
std::shared_ptr<storm::models::AbstractModel> model;
}; };
} // namespace parser } // namespace parser

Write Preview
Loading…
Cancel
Save