From c279c693e55acc71265298ac0bea881c0810b3cd Mon Sep 17 00:00:00 2001 From: masawei Date: Wed, 8 Jan 2014 00:06:04 +0100 Subject: [PATCH] Refactored NondeterministicModelParser.h/.cpp -Mostly restruturing and tidying up. Next up: Refatoring AtomicPropositionLabelingParser.h/.cpp Former-commit-id: c26abad85032afa07e5105812c73992fc3cf4b27 --- src/parser/AutoParser.h | 4 +- src/parser/DeterministicModelParser.cpp | 10 +- src/parser/DeterministicModelParser.h | 8 +- src/parser/NondeterministicModelParser.cpp | 113 +++++++++++---------- src/parser/NondeterministicModelParser.h | 96 +++++++++-------- test/functional/parser/ParseMdpTest.cpp | 2 +- 6 files changed, 125 insertions(+), 108 deletions(-) diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index cec1fad66..59082a135 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -56,11 +56,11 @@ class AutoParser { break; } case storm::models::MDP: { - this->model.reset(new storm::models::Mdp(std::move(NondeterministicModelParserAsMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + this->model.reset(new storm::models::Mdp(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); break; } case storm::models::CTMDP: { - this->model.reset(new storm::models::Ctmdp(std::move(NondeterministicModelParserAsCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + this->model.reset(new storm::models::Ctmdp(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); break; } case storm::models::MA: { diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index c7411b14f..3f25b9c0c 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -26,16 +26,16 @@ 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) */ -DeterministicModelParser::ResultContainer DeterministicModelParser::parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { +DeterministicModelParser::Result 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))); uint_fast64_t stateCount = resultTransitionSystem.getColumnCount(); uint_fast64_t rowCount = resultTransitionSystem.getRowCount(); - storm::models::AtomicPropositionsLabeling resultLabeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); + storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); - DeterministicModelParser::ResultContainer result(std::move(resultTransitionSystem), std::move(resultLabeling)); + DeterministicModelParser::Result result(std::move(resultTransitionSystem), std::move(labeling)); // Only parse state rewards of a file is given. if (stateRewardFile != "") { @@ -58,7 +58,7 @@ DeterministicModelParser::ResultContainer DeterministicModelParser::parseDetermi */ 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))); + DeterministicModelParser::Result 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>>()); } @@ -69,7 +69,7 @@ storm::models::Dtmc DeterministicModelParser::parseDtmc(std::string cons */ 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))); + DeterministicModelParser::Result 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 c6b64b6c1..3fc840c5e 100644 --- a/src/parser/DeterministicModelParser.h +++ b/src/parser/DeterministicModelParser.h @@ -35,13 +35,13 @@ public: /*! * @brief A struct containing the parsed components of a deterministic model. */ - struct ResultContainer { + struct Result { - ResultContainer(storm::storage::SparseMatrix& transitionSystem, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { + Result(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)) { + Result(storm::storage::SparseMatrix&& transitionSystem, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) { // Intentionally left empty. } @@ -80,7 +80,7 @@ private: /*! * @brief Call sub-parsers on the given files and fill the container with the results. */ - static ResultContainer parseDeterministicModel(std::string const & transitionSystemFile, + static Result parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 5f6e13360..fd2e85912 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -15,63 +15,64 @@ #include "src/parser/SparseStateRewardParser.h" namespace storm { -namespace parser { + namespace parser { -/*! - * Parses a transition file and a labeling file and produces an intermediate Result Container - * Note that the labeling file may have at most as many nodes as the transition file! - * - * @param transitionSystemFile String containing the location of the transition file (....tra) - * @param labelingFile String containing the location of the labeling file (....lab) - * @param stateRewardFile String containing the location of the state reward file (...srew) - * @param transitionRewardFile String containing the location of the transition reward file (...trew) - */ -NondeterministicModelParserResultContainer parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile, std::string const & transitionRewardFile) { - - NondeterministicSparseTransitionParser::Result transitionParserResult(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile))); - storm::storage::SparseMatrix transitions(std::move(transitionParserResult.transitionMatrix)); - - uint_fast64_t stateCount = transitions.getColumnCount(); - uint_fast64_t rowCount = transitions.getRowCount(); - - storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); - - NondeterministicModelParserResultContainer result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling)); - - if (stateRewardFile != "") { - result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile)); - } - - if (transitionRewardFile != "") { - RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, &result.rowMapping); - result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo).transitionMatrix); - } - return result; -} - -/*! - * Uses the Function parseNondeterministicModel internally to parse the given input files. - * @note This is a Short-Hand for Constructing a Mdp directly from the data returned by @parseNondeterministicModel - * @return A Mdp Model - */ -storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile, std::string const & transitionRewardFile) { - NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); -} - -/*! - * Uses the Function parseNondeterministicModel internally to parse the given input files. - * @note This is a Short-Hand for Constructing a Ctmdp directly from the data returned by @parseNondeterministicModel - * @return A Ctmdp Model - */ -storm::models::Ctmdp NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile, std::string const & transitionRewardFile) { - NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); -} + /*! + * Parses a transition file and a labeling file and produces an intermediate Result Container + * Note that the labeling file may have at most as many nodes as the transition file! + * + * @param transitionSystemFile String containing the location of the transition file (....tra) + * @param labelingFile String containing the location of the labeling file (....lab) + * @param stateRewardFile String containing the location of the state reward file (...srew) + * @param transitionRewardFile String containing the location of the transition reward file (...trew) + */ + NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) { + + NondeterministicSparseTransitionParser::Result transitionParserResult(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile))); + storm::storage::SparseMatrix transitions(std::move(transitionParserResult.transitionMatrix)); + + uint_fast64_t stateCount = transitions.getColumnCount(); + uint_fast64_t rowCount = transitions.getRowCount(); + + storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); + + Result result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling)); + + // 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, &result.rowMapping); + result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo).transitionMatrix); + } + return result; + } + + /*! + * Uses the Function parseNondeterministicModel internally to parse the given input files. + * @note This is a Short-Hand for Constructing a Mdp directly from the data returned by @parseNondeterministicModel + * @return A Mdp Model + */ + storm::models::Mdp NondeterministicModelParser::parseMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { + + Result parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + } + + /*! + * Uses the Function parseNondeterministicModel internally to parse the given input files. + * @note This is a Short-Hand for Constructing a Ctmdp directly from the data returned by @parseNondeterministicModel + * @return A Ctmdp Model + */ + storm::models::Ctmdp NondeterministicModelParser::parseCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { -} /* namespace parser */ + Result parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + } + } /* namespace parser */ } /* namespace storm */ diff --git a/src/parser/NondeterministicModelParser.h b/src/parser/NondeterministicModelParser.h index 449a9b162..6719a4585 100644 --- a/src/parser/NondeterministicModelParser.h +++ b/src/parser/NondeterministicModelParser.h @@ -13,52 +13,68 @@ #include "src/models/Ctmdp.h" namespace storm { + namespace parser { -namespace parser { + class NondeterministicModelParser { -/*! - * @brief Load label and transition file and return initialized mdp object - * - * @note This class creates a new Mdp object that can - * be accessed via getMdp(). However, it will not delete this object! - * - * @note The labeling representation in the file may use at most as much nodes as are specified in the mdp. - */ + public: -storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); -storm::models::Ctmdp NondeterministicModelParserAsCtmdp(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 five return values of the NondeterministicModelParser + */ + struct Result { + Result(storm::storage::SparseMatrix& transitionSystem, std::vector& rowMapping, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling), rowMapping(rowMapping) { + // Intentionally left empty. + } -/*! - * @brief This Class acts as a container much like std::pair for the five return values of the NondeterministicModelParser - */ -template -class NondeterministicModelParserResultContainer { -public: - storm::storage::SparseMatrix transitionSystem; - storm::models::AtomicPropositionsLabeling labeling; - std::vector rowMapping; - boost::optional> stateRewards; - boost::optional> transitionRewards; - NondeterministicModelParserResultContainer(storm::storage::SparseMatrix& transitionSystem, std::vector& rowMapping, storm::models::AtomicPropositionsLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling), rowMapping(rowMapping) { } - NondeterministicModelParserResultContainer(storm::storage::SparseMatrix&& transitionSystem, std::vector&& rowMapping, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)), rowMapping(std::move(rowMapping)) { } - - NondeterministicModelParserResultContainer(const NondeterministicModelParserResultContainer & other) : transitionSystem(other.transitionSystem), - labeling(other.labeling), rowMapping(other.rowMapping), stateRewards(other.stateRewards), transitionRewards(other.transitionRewards) {} - NondeterministicModelParserResultContainer(NondeterministicModelParserResultContainer && other) : transitionSystem(std::move(other.transitionSystem)), - labeling(std::move(other.labeling)), rowMapping(std::move(other.rowMapping)), stateRewards(std::move(other.stateRewards)), transitionRewards(std::move(other.transitionRewards)) {} -private: - NondeterministicModelParserResultContainer() {} -}; - - -NondeterministicModelParserResultContainer parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - -} /* namespace parser */ + Result(storm::storage::SparseMatrix&& transitionSystem, std::vector&& rowMapping, storm::models::AtomicPropositionsLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)), rowMapping(std::move(rowMapping)) { + // Intentionally left empty. + } + + // A matrix representing the transitions of the model + storm::storage::SparseMatrix transitionSystem; + + // The labels of each state. + storm::models::AtomicPropositionsLabeling labeling; + + // A mapping from rows of the matrix to states of the model. + // This resolves the nondeterministic choices inside the transition system. + std::vector rowMapping; + + // Optional rewards for each state. + boost::optional> stateRewards; + + // Optional rewards for each transition. + boost::optional> transitionRewards; + }; + + /*! + * @brief Load label and transition file and return initialized Mdp object + * + * @note This class creates a new Mdp object that can + * be accessed via getMdp(). However, it will not delete this object! + * + * @note The labeling representation in the file may use at most as much nodes as are specified in the mdp. + */ + static storm::models::Mdp parseMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + + + /*! + * + */ + static storm::models::Ctmdp parseCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + + private: + + /*! + * + */ + static Result parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + + }; + } /* namespace parser */ } /* namespace storm */ #endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */ diff --git a/test/functional/parser/ParseMdpTest.cpp b/test/functional/parser/ParseMdpTest.cpp index 58673269d..ff447488d 100644 --- a/test/functional/parser/ParseMdpTest.cpp +++ b/test/functional/parser/ParseMdpTest.cpp @@ -11,7 +11,7 @@ #include "src/parser/NondeterministicModelParser.h" TEST(ParseMdpTest, parseAndOutput) { - storm::models::Mdp mdp = storm::parser::NondeterministicModelParserAsMdp( + storm::models::Mdp mdp = storm::parser::NondeterministicModelParser::parseMdp( STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"); storm::storage::SparseMatrix const& matrix = mdp.getTransitionMatrix();