Browse Source
Refactored the AutoParser.
Refactored the AutoParser.
- Devided the AutoParser.h into .h and .cpp
- The AutoParser now is a stateless class
|- This resulted in changes to the interface between the parsers and the rest of the project.
|- The main() now directly acquires a shared_ptr to an AbstractModel from the call of the AutoParser and keeps ownership of it.
|- Additionally, the division into .h and .cpp lead to a move of includes from the header to the source. This caused several tests to need some model header to be included.
|- Tests are still showing green (except those needing Gurobi, which I do not have).
Next up: Parser.h/.cpp, then comments and making things look nice.)
Former-commit-id: f59b7405e5
tempestpy_adaptions
masawei
11 years ago
13 changed files with 234 additions and 219 deletions
-
2src/counterexamples/PathBasedSubsystemGenerator.h
-
94src/parser/AutoParser.cpp
-
163src/parser/AutoParser.h
-
47src/storm.cpp
-
18test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
-
24test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
-
15test/functional/storage/MaximalEndComponentDecompositionTest.cpp
-
11test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
-
20test/performance/graph/GraphTest.cpp
-
14test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
-
14test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
-
11test/performance/storage/MaximalEndComponentDecompositionTest.cpp
-
20test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp
@ -0,0 +1,94 @@ |
|||
/*
|
|||
* AutoParser.cpp |
|||
* |
|||
* Created on: Jan 20, 2014 |
|||
* Author: Manuel S. Weiand |
|||
*/ |
|||
|
|||
#include "src/parser/AutoParser.h"
|
|||
|
|||
#include "src/parser/Parser.h"
|
|||
|
|||
#include "src/parser/DeterministicModelParser.h"
|
|||
#include "src/parser/NondeterministicModelParser.h"
|
|||
#include "src/parser/MarkovAutomatonParser.h"
|
|||
#include "src/exceptions/WrongFormatException.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
std::shared_ptr<storm::models::AbstractModel<double>> AutoParser::parseModel(std::string const & transitionSystemFile, |
|||
std::string const & labelingFile, |
|||
std::string const & stateRewardFile, |
|||
std::string const & transitionRewardFile) { |
|||
|
|||
// Find and parse the model type hint.
|
|||
storm::models::ModelType type = AutoParser::analyzeHint(transitionSystemFile); |
|||
|
|||
// In case the hint string is unknown or could not be found, throw an exception.
|
|||
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::WrongFormatException() << "Could not determine type of file " << transitionSystemFile; |
|||
} else { |
|||
LOG4CPLUS_INFO(logger, "Model type seems to be " << type); |
|||
} |
|||
|
|||
// Do the actual parsing.
|
|||
std::shared_ptr<storm::models::AbstractModel<double>> model; |
|||
switch (type) { |
|||
case storm::models::DTMC: { |
|||
model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::CTMC: { |
|||
model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::MDP: { |
|||
model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::CTMDP: { |
|||
model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::MA: { |
|||
model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); |
|||
break; |
|||
} |
|||
default: |
|||
LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type which cannot be parsed."); // Unknown
|
|||
} |
|||
|
|||
return model; |
|||
} |
|||
|
|||
storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) { |
|||
storm::models::ModelType hintType = storm::models::Unknown; |
|||
|
|||
// Find out the line endings used within the file.
|
|||
storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename); |
|||
|
|||
// Open the file.
|
|||
MappedFile file(filename.c_str()); |
|||
char* buf = file.data; |
|||
|
|||
// Find and read in the hint.
|
|||
char hint[128]; |
|||
// %20s => The input hint can be AT MOST 120 chars long.
|
|||
storm::parser::scanForModelHint(hint, sizeof(hint), buf, lineEndings); |
|||
|
|||
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); |
|||
|
|||
// Check if the hint value is known and store the appropriate enum value.
|
|||
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; |
|||
else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA; |
|||
|
|||
return hintType; |
|||
} |
|||
} |
|||
} |
|||
@ -1,140 +1,49 @@ |
|||
#ifndef STORM_PARSER_AUTOPARSER_H_ |
|||
#define STORM_PARSER_AUTOPARSER_H_ |
|||
|
|||
#include "src/parser/Parser.h" |
|||
#include "src/models/AbstractModel.h" |
|||
|
|||
#include "src/exceptions/WrongFormatException.h" |
|||
#include "src/models/AbstractModel.h" |
|||
#include "src/parser/DeterministicModelParser.h" |
|||
#include "src/parser/NondeterministicModelParser.h" |
|||
#include "src/parser/MarkovAutomatonParser.h" |
|||
|
|||
#include <memory> |
|||
#include <iostream> |
|||
#include <utility> |
|||
#include <string> |
|||
#include <cctype> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Checks the given files and parses the model within these files. |
|||
* |
|||
* This parser analyzes the format hint 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>(). |
|||
*/ |
|||
template<class T> |
|||
class AutoParser { |
|||
public: |
|||
AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|||
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "") : model(nullptr) { |
|||
storm::models::ModelType type = this->analyzeHint(transitionSystemFile); |
|||
|
|||
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::WrongFormatException() << "Could not determine type of file " << transitionSystemFile; |
|||
} else { |
|||
LOG4CPLUS_INFO(logger, "Model type seems to be " << type); |
|||
} |
|||
|
|||
// Do actual parsing |
|||
switch (type) { |
|||
case storm::models::DTMC: { |
|||
this->model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::CTMC: { |
|||
this->model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::MDP: { |
|||
this->model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::CTMDP: { |
|||
this->model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::MA: { |
|||
this->model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); |
|||
break; |
|||
} |
|||
default: ; // Unknown |
|||
} |
|||
|
|||
|
|||
if (!this->model) { |
|||
LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type. Model is still null."); |
|||
} |
|||
} |
|||
namespace parser { |
|||
|
|||
class AutoParser { |
|||
public: |
|||
|
|||
/*! |
|||
* Checks the given files and parses the model within these files. |
|||
* |
|||
* This parser analyzes the format hint 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, a shared pointer owning the resulting model is returned. |
|||
* The concrete model can be obtained using the as<Type>() member of the AbstractModel class. |
|||
* |
|||
* @param transitionsFilename The name of the file containing the transitions of the Markov automaton. |
|||
* @param labelingFilename The name of the file containing the labels for the states of the Markov automaton. |
|||
* @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton. |
|||
* @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton. |
|||
* @return A shared_ptr containing the resulting model. |
|||
*/ |
|||
static std::shared_ptr<storm::models::AbstractModel<double>> parseModel(std::string const & transitionSystemFile, |
|||
std::string const & labelingFile, |
|||
std::string const & stateRewardFile = "", |
|||
std::string const & transitionRewardFile = ""); |
|||
|
|||
/*! |
|||
* @brief Returns the type of model that was parsed. |
|||
*/ |
|||
storm::models::ModelType getType() { |
|||
if (this->model) { |
|||
return this->model->getType(); |
|||
} else { |
|||
return storm::models::Unknown; |
|||
} |
|||
} |
|||
private: |
|||
|
|||
/*! |
|||
* Opens the given file and parses the file format hint. |
|||
* |
|||
* @param filename The path and name of the file that is to be analysed. |
|||
* @return The type of the model as an enum value. |
|||
*/ |
|||
static storm::models::ModelType analyzeHint(const std::string& filename); |
|||
}; |
|||
|
|||
/*! |
|||
* @brief Returns the model with the given type. |
|||
*/ |
|||
template <typename Model> |
|||
std::shared_ptr<Model> getModel() { |
|||
return this->model->template as<Model>(); |
|||
} |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* @brief Open file and read file format hint. |
|||
*/ |
|||
storm::models::ModelType analyzeHint(const std::string& filename) { |
|||
storm::models::ModelType hintType = storm::models::Unknown; |
|||
|
|||
// Parse the File and check for the Line Endings |
|||
storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename); |
|||
|
|||
// Open file |
|||
MappedFile file(filename.c_str()); |
|||
char* buf = file.data; |
|||
|
|||
// parse hint |
|||
char hint[128]; |
|||
// %20s => The Input Hint can be AT MOST 120 chars long |
|||
storm::parser::scanForModelHint(hint, sizeof(hint), buf, lineEndings); |
|||
|
|||
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, "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; |
|||
else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA; |
|||
|
|||
return hintType; |
|||
} |
|||
|
|||
/*! |
|||
* @brief Pointer to a parser that has parsed the given transition system. |
|||
*/ |
|||
std::shared_ptr<storm::models::AbstractModel<T>> model; |
|||
}; |
|||
|
|||
} // namespace parser |
|||
|
|||
} // namespace parser |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_PARSER_AUTOPARSER_H_ */ |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue