From 1f71bb5240bcd252bc6f54bb9bba7777caa94490 Mon Sep 17 00:00:00 2001 From: masawei Date: Fri, 20 Dec 2013 16:35:23 +0100 Subject: [PATCH] Refactored the DeterministicModelParser. Former-commit-id: 7227d25499a85308abb06f282a8531c0d21d0adb --- .gitignore | 3 + src/parser/AutoParser.h | 4 +- src/parser/DeterministicModelParser.cpp | 28 +++--- src/parser/DeterministicModelParser.h | 85 +++++++++++++------ .../DeterministicSparseTransitionParser.cpp | 9 +- .../DeterministicSparseTransitionParser.h | 4 - src/parser/MarkovAutomatonParser.cpp | 1 + .../MarkovAutomatonSparseTransitionParser.cpp | 9 +- src/parser/Parser.cpp | 3 + src/parser/Parser.h | 9 -- test/functional/parser/CslParserTest.cpp | 1 + test/functional/parser/LtlParserTest.cpp | 1 + test/functional/parser/PrctlParserTest.cpp | 1 + 13 files changed, 92 insertions(+), 66 deletions(-) diff --git a/.gitignore b/.gitignore index 47ad40437..9abd6bea7 100644 --- a/.gitignore +++ b/.gitignore @@ -39,3 +39,6 @@ build//CMakeLists.txt /*.vcxproj /*.filters /*.sln +#Temp texteditor files +*.orig +*.*~ diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index 32baaae40..cec1fad66 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -48,11 +48,11 @@ class AutoParser { // Do actual parsing switch (type) { case storm::models::DTMC: { - this->model.reset(new storm::models::Dtmc(std::move(DeterministicModelParserAsDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + this->model.reset(new storm::models::Dtmc(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); break; } case storm::models::CTMC: { - this->model.reset(new storm::models::Ctmc(std::move(DeterministicModelParserAsCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + this->model.reset(new storm::models::Ctmc(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); break; } case storm::models::MDP: { diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 44e484bc0..555b2485e 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -26,8 +26,7 @@ namespace parser { * @param stateRewardFile String containing the location of the state reward file (...srew) * @param transitionRewardFile String containing the location of the transition reward file (...trew) */ -DeterministicModelParserResultContainer parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile, std::string const & transitionRewardFile) { +DeterministicModelParser::ResultContainer DeterministicModelParser::parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { storm::storage::SparseMatrix resultTransitionSystem(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile))); @@ -36,11 +35,14 @@ DeterministicModelParserResultContainer parseDeterministicModel(std::str storm::models::AtomicPropositionsLabeling resultLabeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); - DeterministicModelParserResultContainer result(std::move(resultTransitionSystem), std::move(resultLabeling)); + DeterministicModelParser::ResultContainer result(std::move(resultTransitionSystem), std::move(resultLabeling)); + // Only parse state rewards of a file is given. if (stateRewardFile != "") { result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile)); } + + // Only parse transition rewards of a file is given. if (transitionRewardFile != "") { RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, nullptr); result.transitionRewards.reset(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo))); @@ -50,24 +52,24 @@ DeterministicModelParserResultContainer parseDeterministicModel(std::str } /*! - * Uses the Function parseDeterministicModel internally to parse the given input files. - * @note This is a Short-Hand for Constructing a Dtmc directly from the data returned by @parseDeterministicModel + * Uses the parseDeterministicModel function internally to parse the given input files. + * @note This is a short-hand for constructing a Dtmc directly from the data returned by @parseDeterministicModel * @return A Dtmc Model */ -storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile, std::string const & transitionRewardFile) { - DeterministicModelParserResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); +storm::models::Dtmc DeterministicModelParser::parseDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { + + DeterministicModelParser::ResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); return storm::models::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } /*! - * Uses the Function parseDeterministicModel internally to parse the given input files. - * @note This is a Short-Hand for Constructing a Ctmc directly from the data returned by @parseDeterministicModel + * Uses the parseDeterministicModel function internally to parse the given input files. + * @note This is a short-hand for constructing a Ctmc directly from the data returned by @parseDeterministicModel * @return A Ctmc Model */ -storm::models::Ctmc DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile, std::string const & transitionRewardFile) { - DeterministicModelParserResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); +storm::models::Ctmc DeterministicModelParser::parseCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { + + DeterministicModelParser::ResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); return storm::models::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } diff --git a/src/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h index 273c64c49..c6b64b6c1 100644 --- a/src/parser/DeterministicModelParser.h +++ b/src/parser/DeterministicModelParser.h @@ -18,44 +18,77 @@ namespace storm { namespace parser { /*! - * @brief Load label and transition file and returns an initialized dtmc or ctmc object. + * @brief Loads a deterministic model (Dtmc or Ctmc) from files. + * + * Given the file paths of the files holding the transitions, the atomic propositions and optionally the state- and transition rewards + * it loads the files, parses them and returns the desired model. * * @note This class creates a new Dtmc or Ctmc object * * @note The labeling representation in the file may use at most as much nodes as are specified in the transition system. */ +class DeterministicModelParser { -storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); -storm::models::Ctmc DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - -/*! - * @brief This Class acts as a container much like std::pair for the four return values of the DeterministicModelParser - */ -template -class DeterministicModelParserResultContainer { public: - storm::storage::SparseMatrix transitionSystem; - storm::models::AtomicPropositionsLabeling labeling; - boost::optional> stateRewards; - boost::optional> transitionRewards; - DeterministicModelParserResultContainer(storm::storage::SparseMatrix& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { } - DeterministicModelParserResultContainer(storm::storage::SparseMatrix&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) { } - - DeterministicModelParserResultContainer(const DeterministicModelParserResultContainer & other) : transitionSystem(other.transitionSystem), - labeling(other.labeling), stateRewards(other.stateRewards), transitionRewards(other.transitionRewards) {} - DeterministicModelParserResultContainer(DeterministicModelParserResultContainer && other) : transitionSystem(std::move(other.transitionSystem)), - labeling(std::move(other.labeling)), stateRewards(std::move(other.stateRewards)), transitionRewards(std::move(other.transitionRewards)) {} + + /*! + * @brief A struct containing the parsed components of a deterministic model. + */ + struct ResultContainer { + + ResultContainer(storm::storage::SparseMatrix& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { + // Intentionally left empty. + } + + ResultContainer(storm::storage::SparseMatrix&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) { + // Intentionally left empty. + } + + // A matrix representing the transitions of the model + storm::storage::SparseMatrix transitionSystem; + + // The labels of each state. + storm::models::AtomicPropositionsLabeling labeling; + + // Optional rewards for each state. + boost::optional> stateRewards; + + // Optional rewards for each transition. + boost::optional> transitionRewards; + }; + + + /*! + * @brief Parse a Dtmc. + */ + static storm::models::Dtmc parseDtmc(std::string const & transitionSystemFile, + std::string const & labelingFile, + std::string const & stateRewardFile = "", + std::string const & transitionRewardFile = ""); + + /*! + * @brief Parse a Ctmc. + */ + static storm::models::Ctmc parseCtmc(std::string const & transitionSystemFile, + std::string const & labelingFile, + std::string const & stateRewardFile = "", + std::string const & transitionRewardFile = ""); + private: - DeterministicModelParserResultContainer() {} -}; + /*! + * @brief Call sub-parsers on the given files and fill the container with the results. + */ + static ResultContainer parseDeterministicModel(std::string const & transitionSystemFile, + std::string const & labelingFile, + std::string const & stateRewardFile = "", + std::string const & transitionRewardFile = ""); -DeterministicModelParserResultContainer parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); +}; } /* namespace parser */ + } /* namespace storm */ + #endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */ diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 76cd49af5..683042353 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -7,22 +7,15 @@ #include "src/parser/DeterministicSparseTransitionParser.h" -#include -#include -#include -#include -#include - -#include #include #include +#include #include #include #include #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" -#include #include "src/settings/Settings.h" #include "log4cplus/logger.h" diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 7fcd62a1f..c44583b97 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -2,11 +2,7 @@ #define STORM_PARSER_TRAPARSER_H_ #include "src/storage/SparseMatrix.h" - #include "src/parser/Parser.h" -#include "src/utility/OsDetection.h" - -#include namespace storm { diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index 8b74a896b..b8df6390a 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -1,6 +1,7 @@ #include "MarkovAutomatonParser.h" #include "AtomicPropositionLabelingParser.h" #include "SparseStateRewardParser.h" +#include "src/exceptions/WrongFormatException.h" namespace storm { diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index ce89951d9..7d3336ae8 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -1,6 +1,7 @@ #include "MarkovAutomatonSparseTransitionParser.h" #include "src/settings/Settings.h" +#include "src/exceptions/WrongFormatException.h" namespace storm { @@ -18,8 +19,8 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran } // Now read the transitions. - int_fast64_t source, target = -1; - int_fast64_t lastsource = -1; + uint_fast64_t source, target = 0; + uint_fast64_t lastsource = 0; bool encounteredEOF = false; bool stateHasMarkovianChoice = false; bool stateHasProbabilisticChoice = false; @@ -150,8 +151,8 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio buf = storm::parser::forwardToNextLine(buf, lineEndings); // Now read the transitions. - int_fast64_t source, target = -1; - int_fast64_t lastsource = -1; + uint_fast64_t source, target = 0; + uint_fast64_t lastsource = 0; bool encounteredEOF = false; uint_fast64_t currentChoice = 0; while (buf[0] != '\0' && !encounteredEOF) { diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp index 67b2772d7..6fb26ef4b 100644 --- a/src/parser/Parser.cpp +++ b/src/parser/Parser.cpp @@ -1,10 +1,13 @@ #include "src/parser/Parser.h" +#include #include +#include #include #include #include +#include #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" #include "src/utility/OsDetection.h" diff --git a/src/parser/Parser.h b/src/parser/Parser.h index 3fee43b98..e7fcf4dab 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -11,18 +11,9 @@ #include "src/utility/OsDetection.h" #include -#include -#include -#include -#include -#include #include #include -#include -#include "src/exceptions/FileIoException.h" -#include "src/exceptions/WrongFormatException.h" - namespace storm { /*! diff --git a/test/functional/parser/CslParserTest.cpp b/test/functional/parser/CslParserTest.cpp index fb758e951..4e4a67af9 100644 --- a/test/functional/parser/CslParserTest.cpp +++ b/test/functional/parser/CslParserTest.cpp @@ -8,6 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/CslParser.h" +#include "src/exceptions/WrongFormatException.h" TEST(CslParserTest, parseApOnlyTest) { std::string formula = "ap"; diff --git a/test/functional/parser/LtlParserTest.cpp b/test/functional/parser/LtlParserTest.cpp index 00df82ff9..1da53769d 100644 --- a/test/functional/parser/LtlParserTest.cpp +++ b/test/functional/parser/LtlParserTest.cpp @@ -8,6 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/LtlParser.h" +#include "src/exceptions/WrongFormatException.h" TEST(LtlParserTest, parseApOnlyTest) { std::string formula = "ap"; diff --git a/test/functional/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp index 923b5f941..c51cf3164 100644 --- a/test/functional/parser/PrctlParserTest.cpp +++ b/test/functional/parser/PrctlParserTest.cpp @@ -9,6 +9,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/PrctlParser.h" +#include "src/exceptions/WrongFormatException.h" TEST(PrctlParserTest, parseApOnlyTest) { std::string ap = "ap";