From 4343b5b98001bfb8c5d88903db4d0c8aed33e8d2 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 17 Dec 2015 11:55:29 +0100 Subject: [PATCH] Refactored some classes into templates Former-commit-id: b495cf93d44619444463b18c189f988a80bf3a55 --- src/builder/ExplicitDFTModelBuilder.cpp | 3 +-- src/parser/DFTGalileoParser.cpp | 21 ++++++++++++---- src/parser/DFTGalileoParser.h | 10 +++++--- src/storage/dft/DFT.h | 4 ++- src/storage/dft/DFTBuilder.cpp | 33 ++++++++++++++++--------- src/storage/dft/DFTBuilder.h | 7 +++--- src/storage/dft/DFTState.cpp | 4 +-- src/storage/dft/DFTState.h | 3 ++- src/storm-dyftee.cpp | 2 +- 9 files changed, 57 insertions(+), 30 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index bb4204918..6dff245c5 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -165,8 +165,7 @@ namespace storm { } // Explicitly instantiate the class. - template - class ExplicitDFTModelBuilder, uint32_t>; + template class ExplicitDFTModelBuilder, uint32_t>; #ifdef STORM_HAVE_CARL template class ExplicitDFTModelBuilder, uint32_t>; diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index a710e81d3..0bce51685 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -10,7 +10,9 @@ namespace storm { namespace parser { - storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename) { + + template + storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename) { if(readFile(filename)) { storm::storage::DFT dft = mBuilder.build(); STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString()); @@ -20,8 +22,9 @@ namespace storm { throw storm::exceptions::FileIoException(); } } - - std::string stripQuotsFromName(std::string const& name) { + + template + std::string DFTGalileoParser::stripQuotsFromName(std::string const& name) { size_t firstQuots = name.find("\""); size_t secondQuots = name.find("\"", firstQuots+1); @@ -33,8 +36,9 @@ namespace storm { return name.substr(firstQuots+1,secondQuots-1); } } - - bool DFTGalileoParser::readFile(const std::string& filename) { + + template + bool DFTGalileoParser::readFile(const std::string& filename) { // constants std::string topleveltoken = "toplevel"; std::string toplevelId; @@ -108,6 +112,13 @@ namespace storm { file.close(); return generalSuccess; } + + // Explicitly instantiate the class. + template class DFTGalileoParser; + +#ifdef STORM_HAVE_CARL + template class DFTGalileoParser; +#endif } } \ No newline at end of file diff --git a/src/parser/DFTGalileoParser.h b/src/parser/DFTGalileoParser.h index 9d0cc0096..d0f95383e 100644 --- a/src/parser/DFTGalileoParser.h +++ b/src/parser/DFTGalileoParser.h @@ -8,16 +8,18 @@ namespace storm { namespace parser { + + template class DFTGalileoParser { - storm::storage::DFTBuilder mBuilder; + storm::storage::DFTBuilder mBuilder; public: storm::storage::DFT parseDFT(std::string const& filename); private: bool readFile(std::string const& filename); - - - }; + + std::string stripQuotsFromName(std::string const& name); + }; } } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 69a407461..3878198bd 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -131,12 +131,14 @@ namespace storm { assert(index < nrElements()); return mElements[index]; } - + + // TODO Matthias: template std::shared_ptr> getBasicElement(size_t index) const { assert(mElements[index]->isBasicElement()); return std::static_pointer_cast>(mElements[index]); } + // TODO Matthias: template std::vector>> getBasicElements() const { std::vector>> elements; for (std::shared_ptr elem : mElements) { diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index 10d96b6d0..bb51852ee 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -12,8 +12,9 @@ namespace storm { namespace storage { - - DFT DFTBuilder::build() { + + template + DFT DFTBuilder::build() { for(auto& elem : mChildNames) { for(auto const& child : elem.second) { std::shared_ptr gate = std::static_pointer_cast(elem.first); @@ -36,8 +37,9 @@ namespace storm { } return DFT(elems, mElements[topLevelIdentifier]); } - - unsigned DFTBuilder::computeRank(std::shared_ptr const& elem) { + + template + unsigned DFTBuilder::computeRank(std::shared_ptr const& elem) { if(elem->rank() == -1) { if(elem->nrChildren() == 0) { elem->setRank(0); @@ -58,8 +60,9 @@ namespace storm { return elem->rank(); } - - bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementTypes tp) { + + template + bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementTypes tp) { assert(children.size() > 0); if(mElements.count(name) != 0) { // Element with that name already exists. @@ -97,9 +100,9 @@ namespace storm { mChildNames[element] = children; return true; } - - - void DFTBuilder::topoVisit(std::shared_ptr const& n, std::map, topoSortColour>& visited, std::vector>& L) { + + template + void DFTBuilder::topoVisit(std::shared_ptr const& n, std::map, topoSortColour>& visited, std::vector>& L) { if(visited[n] == topoSortColour::GREY) { throw storm::exceptions::WrongFormatException("DFT is cyclic"); } else if(visited[n] == topoSortColour::WHITE) { @@ -114,7 +117,8 @@ namespace storm { } } - std::vector> DFTBuilder::topoSort() { + template + std::vector> DFTBuilder::topoSort() { std::map, topoSortColour> visited; for(auto const& e : mElements) { visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); @@ -126,7 +130,14 @@ namespace storm { } //std::reverse(L.begin(), L.end()); return L; - } + } + + // Explicitly instantiate the class. + template class DFTBuilder; + +#ifdef STORM_HAVE_CARL + template class DFTBuilder; +#endif } } diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 68e64b1dc..a78d62224 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -10,7 +10,8 @@ namespace storm { namespace storage { class DFT; - + + template class DFTBuilder { std::size_t mNextId = 0; @@ -69,7 +70,7 @@ namespace storm { return true; } - bool addBasicElement(std::string const& name, double failureRate, double dormancyFactor) { + bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor) { if(failureRate <= 0.0) { std::cerr << "Failure rate must be positive." << std::endl; return false; @@ -80,7 +81,7 @@ namespace storm { return false; } - mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor); + mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor); return true; } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 599de5525..201f32810 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -65,8 +65,8 @@ namespace storm { } } - - std::pair>, bool> DFTState::letNextBEFail(size_t index) + // TODO Matthias: template + std::pair>, bool> DFTState::letNextBEFail(size_t index) { assert(index < mIsCurrentlyFailableBE.size()); STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 788162ce3..d2964e152 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -105,7 +105,8 @@ namespace storm { size_t nrFailableBEs() const { return mIsCurrentlyFailableBE.size(); } - + + // TODO Matthias: template std::pair>, bool> letNextBEFail(size_t smallestIndex = 0); std::string getCurrentlyFailableString() { diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index d24d2ad08..2c85edcf6 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -19,7 +19,7 @@ int main(int argc, char** argv) { logger.getAppender("mainConsoleAppender")->setThreshold(level); std::cout << "Parsing DFT file..." << std::endl; - storm::parser::DFTGalileoParser parser; + storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(argv[1]); std::cout << "Built data structure" << std::endl;