From 7737205149708a764bfe4194078b83376b79713b Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 17 Dec 2015 12:16:34 +0100 Subject: [PATCH] More refactoring with templates Former-commit-id: 6b614ed7f306010c1a3d63ecc5a3d527693fee30 --- src/builder/ExplicitDFTModelBuilder.h | 4 ++-- src/parser/DFTGalileoParser.cpp | 19 +++++++++++++---- src/parser/DFTGalileoParser.h | 2 +- src/storage/dft/DFT.cpp | 30 ++++++++++++++++++++------- src/storage/dft/DFT.h | 15 +++++++------- src/storage/dft/DFTBuilder.cpp | 4 ++-- src/storage/dft/DFTBuilder.h | 3 ++- src/storage/dft/DFTState.cpp | 5 +++-- src/storage/dft/DFTState.h | 9 +++++--- src/storm-dyftee.cpp | 10 +++++---- 10 files changed, 66 insertions(+), 35 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index f5920bb52..de3a94293 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -35,12 +35,12 @@ namespace storm { boost::optional>> choiceLabeling; }; - storm::storage::DFT const &mDft; + storm::storage::DFT const &mDft; std::unordered_set mStates; size_t newIndex = 0; public: - ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) { + ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) { } diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 0bce51685..e3368bbe3 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -4,6 +4,7 @@ #include #include #include +#include #include "../exceptions/FileIoException.h" #include "../exceptions/NotSupportedException.h" #include "src/utility/macros.h" @@ -12,9 +13,9 @@ namespace storm { namespace parser { template - storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename) { + storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename) { if(readFile(filename)) { - storm::storage::DFT dft = mBuilder.build(); + storm::storage::DFT dft = mBuilder.build(); STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString()); STORM_LOG_DEBUG("Spare Modules:" << std::endl << dft.getSpareModulesString()); return dft; @@ -95,8 +96,18 @@ namespace storm { } else if(tokens[1] == "wsp" || tokens[1] == "csp") { success = mBuilder.addSpareElement(name, childNames); } else if(boost::starts_with(tokens[1], "lambda=")) { - //TODO Matthias: Use ValueType instead of fixed double - success = mBuilder.addBasicElement(name, boost::lexical_cast(tokens[1].substr(7)), boost::lexical_cast(tokens[2].substr(5))); + ValueType failureRate = 0; + ValueType dormancyFactor = 0; + if (std::is_same::value) { + failureRate = boost::lexical_cast(tokens[1].substr(7)); + dormancyFactor = boost::lexical_cast(tokens[2].substr(5)); + } else { + // TODO Matthias: Parse RationalFunction + failureRate; + dormancyFactor; + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Parsing into rational function not supported."); + } + success = mBuilder.addBasicElement(name, failureRate, dormancyFactor); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " + tokens[1] + " not recognized."); success = false; diff --git a/src/parser/DFTGalileoParser.h b/src/parser/DFTGalileoParser.h index d0f95383e..4f7da1566 100644 --- a/src/parser/DFTGalileoParser.h +++ b/src/parser/DFTGalileoParser.h @@ -13,7 +13,7 @@ namespace storm { class DFTGalileoParser { storm::storage::DFTBuilder mBuilder; public: - storm::storage::DFT parseDFT(std::string const& filename); + storm::storage::DFT parseDFT(std::string const& filename); private: bool readFile(std::string const& filename); diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index c7801681b..719c59e26 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -2,8 +2,9 @@ namespace storm { namespace storage { - - DFT::DFT(std::vector> const& elements, std::shared_ptr const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0) + + template + DFT::DFT(std::vector> const& elements, std::shared_ptr const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0) { assert(elementIndicesCorrect()); @@ -60,8 +61,9 @@ namespace storm { mTopLevelIndex = tle->id(); } - - std::string DFT::getElementsString() const { + + template + std::string DFT::getElementsString() const { std::stringstream stream; for (auto const& elem : mElements) { stream << "[" << elem->id() << "]" << elem->toString() << std::endl; @@ -69,13 +71,15 @@ namespace storm { return stream.str(); } - std::string DFT::getInfoString() const { + template + std::string DFT::getInfoString() const { std::stringstream stream; stream << "Top level index: " << mTopLevelIndex << ", Nr BEs" << mNrOfBEs; return stream.str(); } - std::string DFT::getSpareModulesString() const { + template + std::string DFT::getSpareModulesString() const { std::stringstream stream; stream << "[" << mElements[mTopLevelIndex]->id() << "] {"; std::vector::const_iterator it = mTopModule.begin(); @@ -103,7 +107,8 @@ namespace storm { return stream.str(); } - std::string DFT::getElementsWithStateString(DFTState const& state) const{ + template + std::string DFT::getElementsWithStateString(DFTState const& state) const{ std::stringstream stream; for (auto const& elem : mElements) { stream << "[" << elem->id() << "]"; @@ -120,7 +125,8 @@ namespace storm { return stream.str(); } - std::string DFT::getStateString(DFTState const& state) const{ + template + std::string DFT::getStateString(DFTState const& state) const{ std::stringstream stream; stream << "(" << state.getId() << ") "; for (auto const& elem : mElements) { @@ -134,5 +140,13 @@ namespace storm { } return stream.str(); } + + // Explicitly instantiate the class. + template class DFT; + +#ifdef STORM_HAVE_CARL + template class DFT; +#endif + } } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 3878198bd..068ea4ef1 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -26,7 +26,8 @@ namespace storm { } } }; - + + template class DFT { private: @@ -132,18 +133,16 @@ namespace storm { return mElements[index]; } - // TODO Matthias: template - std::shared_ptr> getBasicElement(size_t index) const { + std::shared_ptr> getBasicElement(size_t index) const { assert(mElements[index]->isBasicElement()); - return std::static_pointer_cast>(mElements[index]); + return std::static_pointer_cast>(mElements[index]); } - // TODO Matthias: template - std::vector>> getBasicElements() const { - std::vector>> elements; + std::vector>> getBasicElements() const { + std::vector>> elements; for (std::shared_ptr elem : mElements) { if (elem->isBasicElement()) { - elements.push_back(std::static_pointer_cast>(elem)); + elements.push_back(std::static_pointer_cast>(elem)); } } return elements; diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index bb51852ee..ee7676449 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -14,7 +14,7 @@ namespace storm { namespace storage { template - DFT DFTBuilder::build() { + DFT DFTBuilder::build() { for(auto& elem : mChildNames) { for(auto const& child : elem.second) { std::shared_ptr gate = std::static_pointer_cast(elem.first); @@ -35,7 +35,7 @@ namespace storm { for(std::shared_ptr e : elems) { e->setId(id++); } - return DFT(elems, mElements[topLevelIdentifier]); + return DFT(elems, mElements[topLevelIdentifier]); } template diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index a78d62224..f129afc0b 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -9,6 +9,7 @@ namespace storm { namespace storage { + template class DFT; template @@ -90,7 +91,7 @@ namespace storm { return mElements.count(tle) > 0; } - DFT build(); + DFT build(); private: diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 201f32810..87838b9a2 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -4,8 +4,9 @@ namespace storm { namespace storage { - - DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) { + + // TODO Matthias: template + DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mId(id), mDft(dft) { mInactiveSpares = dft.getSpareIndices(); dft.initializeUses(*this); dft.initializeActivation(*this); diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index d2964e152..1e8f8cb01 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -8,7 +8,8 @@ namespace storm { namespace storage { - + + template class DFT; template class DFTBE; @@ -23,10 +24,12 @@ namespace storm { std::vector mIsCurrentlyFailableBE; std::vector mUsedRepresentants; bool mValid = true; - const DFT& mDft; + // TODO Matthias: template + const DFT& mDft; public: - DFTState(DFT const& dft, size_t id); + // TODO Matthias: template + DFTState(DFT const& dft, size_t id); DFTElementState getElementState(size_t id) const; diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 2c85edcf6..7040db9ad 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -5,6 +5,8 @@ #include "modelchecker/results/CheckResult.h" #include "utility/storm.h" +#define VALUE_TYPE double + /* * Entry point for the DyFTeE backend. */ @@ -19,14 +21,14 @@ int main(int argc, char** argv) { logger.getAppender("mainConsoleAppender")->setThreshold(level); std::cout << "Parsing DFT file..." << std::endl; - storm::parser::DFTGalileoParser parser; - storm::storage::DFT dft = parser.parseDFT(argv[1]); + storm::parser::DFTGalileoParser parser; + storm::storage::DFT dft = parser.parseDFT(argv[1]); std::cout << "Built data structure" << std::endl; std::cout << "Building CTMC..." << std::endl; - storm::builder::ExplicitDFTModelBuilder builder(dft); - std::shared_ptr> model = builder.buildCTMC(); + storm::builder::ExplicitDFTModelBuilder builder(dft); + std::shared_ptr> model = builder.buildCTMC(); std::cout << "Built CTMC" << std::endl; std::cout << "Model checking..." << std::endl;