From c2669ccec49747a95a6fd04766381f16c5d2f684 Mon Sep 17 00:00:00 2001 From: gereon Date: Sun, 20 Jan 2013 20:54:14 +0100 Subject: [PATCH] "Creating" DeterministicModelParser this new parser is actually the old DtmcParser. It can now also create Ctmc models... --- src/parser/AutoParser.cpp | 9 ++- ...arser.cpp => DeterministicModelParser.cpp} | 26 +++++---- src/parser/DeterministicModelParser.h | 56 +++++++++++++++++++ src/parser/DtmcParser.h | 40 ------------- test/parser/ParseDtmcTest.cpp | 6 +- 5 files changed, 80 insertions(+), 57 deletions(-) rename src/parser/{DtmcParser.cpp => DeterministicModelParser.cpp} (70%) create mode 100644 src/parser/DeterministicModelParser.h delete mode 100644 src/parser/DtmcParser.h diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 6aaab5693..110831ff6 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -5,7 +5,7 @@ #include "src/exceptions/WrongFileFormatException.h" #include "src/models/AbstractModel.h" -#include "src/parser/DtmcParser.h" +#include "src/parser/DeterministicModelParser.h" #include "src/parser/MdpParser.h" namespace storm { @@ -27,12 +27,15 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con // Do actual parsing switch (type) { case storm::models::DTMC: { - DtmcParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); this->model = parser.getDtmc(); break; } - case storm::models::CTMC: + case storm::models::CTMC: { + DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser.getCtmc(); break; + } case storm::models::MDP: { MdpParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); this->model = parser.getMdp(); diff --git a/src/parser/DtmcParser.cpp b/src/parser/DeterministicModelParser.cpp similarity index 70% rename from src/parser/DtmcParser.cpp rename to src/parser/DeterministicModelParser.cpp index 3aee7b46a..2372cde3e 100644 --- a/src/parser/DtmcParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -1,11 +1,11 @@ /* - * DtmcParser.cpp + * DeterministicModelParser.cpp * * Created on: 19.12.2012 * Author: thomas */ -#include "src/parser/DtmcParser.h" +#include "src/parser/DeterministicModelParser.h" #include #include @@ -27,25 +27,29 @@ 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) */ -DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, +DeterministicModelParser::DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile); - uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); - - std::shared_ptr> stateRewards = nullptr; - std::shared_ptr> transitionRewards = nullptr; + this->transitionSystem = tp.getMatrix(); + + uint_fast64_t stateCount = this->transitionSystem->getRowCount(); storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); + this->labeling = lp.getLabeling(); + + this->stateRewards = nullptr; + this->transitionRewards = nullptr; + if (stateRewardFile != "") { storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); - stateRewards = srp.getStateRewards(); + this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile); - transitionRewards = trp.getMatrix(); + this->transitionRewards = trp.getMatrix(); } - - this->dtmc = std::shared_ptr>(new storm::models::Dtmc(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); + this->dtmc = nullptr; + this->ctmc = nullptr; } } /* namespace parser */ diff --git a/src/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h new file mode 100644 index 000000000..99ce3856f --- /dev/null +++ b/src/parser/DeterministicModelParser.h @@ -0,0 +1,56 @@ +/* + * DtmcParser.h + * + * Created on: 19.12.2012 + * Author: thomas + */ + +#ifndef STORM_PARSER_DETERMINISTICMODELPARSER_H_ +#define STORM_PARSER_DETERMINISTICMODELPARSER_H_ + +#include "src/parser/Parser.h" +#include "src/models/Dtmc.h" +#include "src/models/Ctmc.h" + +namespace storm { +namespace parser { + +/*! + * @brief Load label and transition file and return initialized dtmc or ctmc object. + * + * @Note This class creates a new Dtmc or Ctmc object that can + * be accessed via getDtmc() or getCtmc(). 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 transition system. + */ +class DeterministicModelParser: public storm::parser::Parser { + public: + DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + + std::shared_ptr> getDtmc() { + if (this->dtmc == nullptr) { + this->dtmc = std::shared_ptr>(new storm::models::Dtmc(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards)); + } + return this->dtmc; + } + std::shared_ptr> getCtmc() { + if (this->ctmc == nullptr) { + this->ctmc = std::shared_ptr>(new storm::models::Ctmc(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards)); + } + return this->ctmc; + } + + private: + std::shared_ptr> transitionSystem; + std::shared_ptr labeling; + std::shared_ptr> stateRewards; + std::shared_ptr> transitionRewards; + + std::shared_ptr> dtmc; + std::shared_ptr> ctmc; +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */ diff --git a/src/parser/DtmcParser.h b/src/parser/DtmcParser.h deleted file mode 100644 index b1f746bb5..000000000 --- a/src/parser/DtmcParser.h +++ /dev/null @@ -1,40 +0,0 @@ -/* - * DtmcParser.h - * - * Created on: 19.12.2012 - * Author: thomas - */ - -#ifndef STORM_PARSER_DTMCPARSER_H_ -#define STORM_PARSER_DTMCPARSER_H_ - -#include "src/parser/Parser.h" -#include "src/models/Dtmc.h" - -namespace storm { -namespace parser { - -/*! - * @brief Load label and transition file and return initialized dtmc object - * - * @Note This class creates a new Dtmc object that can - * be accessed via getDtmc(). 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 dtmc. - */ -class DtmcParser: public storm::parser::Parser { -public: - DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - - std::shared_ptr> getDtmc() { - return this->dtmc; - } - -private: - std::shared_ptr> dtmc; -}; - -} /* namespace parser */ -} /* namespace storm */ -#endif /* STORM_PARSER_DTMCPARSER_H_ */ diff --git a/test/parser/ParseDtmcTest.cpp b/test/parser/ParseDtmcTest.cpp index be1dd1595..f5bd8f163 100644 --- a/test/parser/ParseDtmcTest.cpp +++ b/test/parser/ParseDtmcTest.cpp @@ -8,12 +8,12 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/parser/DtmcParser.h" +#include "src/parser/DeterministicModelParser.h" #include "src/utility/IoUtility.h" TEST(ParseDtmcTest, parseAndOutput) { - storm::parser::DtmcParser* dtmcParser; - ASSERT_NO_THROW(dtmcParser = new storm::parser::DtmcParser( + storm::parser::DeterministicModelParser* dtmcParser; + ASSERT_NO_THROW(dtmcParser = new storm::parser::DeterministicModelParser( STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));