Browse Source

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
parent
commit
15d13bc06d
  1. 2
      src/counterexamples/PathBasedSubsystemGenerator.h
  2. 94
      src/parser/AutoParser.cpp
  3. 163
      src/parser/AutoParser.h
  4. 47
      src/storm.cpp
  5. 18
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  6. 24
      test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  7. 15
      test/functional/storage/MaximalEndComponentDecompositionTest.cpp
  8. 11
      test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
  9. 20
      test/performance/graph/GraphTest.cpp
  10. 14
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  11. 14
      test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  12. 11
      test/performance/storage/MaximalEndComponentDecompositionTest.cpp
  13. 20
      test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp

2
src/counterexamples/PathBasedSubsystemGenerator.h

@ -507,7 +507,7 @@ public:
/*!
*
*/
static storm::models::Dtmc<T> computeCriticalSubsystem(storm::models::Dtmc<T>& model, storm::property::prctl::AbstractStateFormula<T> const& stateFormula) {
static storm::models::Dtmc<T> computeCriticalSubsystem(storm::models::Dtmc<T> & model, storm::property::prctl::AbstractStateFormula<T> const& stateFormula) {
//-------------------------------------------------------------
// 1. Strip and handle formulas

94
src/parser/AutoParser.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;
}
}
}

163
src/parser/AutoParser.h

@ -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 sp/tempestpy - tempestpy - Gitea: Git with a cup of tea
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

19 lines
608 B

  1. # Minimal makefile for Sphinx documentation
  2. #
  3. # You can set these variables from the command line.
  4. SPHINXOPTS =
  5. SPHINXBUILD = sphinx-build
  6. SPHINXPROJ = stormpy
  7. SOURCEDIR = source
  8. BUILDDIR = build
  9. # Put it first so that "make" without argument is like "make help".
  10. help:
  11. @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
  12. .PHONY: help Makefile
  13. # Catch-all target: route all unknown targets to Sphinx using the new
  14. # "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS).
  15. %: Makefile
  16. @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
0