From 4bd59b86491eb6cc69df90fb950a25b0b6726661 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 14 Dec 2015 16:44:53 +0100 Subject: [PATCH] Small formatting changes Former-commit-id: 08eb57a9b0df7ff4f84ca2a4ead102a7ac71eef5 --- src/parser/DFTGalileoParser.cpp | 38 ++++++++++++++++++++------------- src/parser/DFTGalileoParser.h | 4 ---- src/storage/dft/DFT.cpp | 2 +- src/storage/dft/DFT.h | 4 ---- src/storage/dft/DFTBuilder.cpp | 29 +++++++++++-------------- src/storage/dft/DFTBuilder.h | 4 +--- src/storage/dft/DFTUnit.h | 2 ++ src/storm-dyftee.cpp | 12 ++++++++++- 8 files changed, 50 insertions(+), 45 deletions(-) diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 79e969260..a93e84e92 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -24,6 +24,9 @@ namespace storm { if(firstQuots == std::string::npos) { return name; + } else if (secondQuots ==std::string::npos) { + std::cerr << "No ending quotation mark found in " << name <(tokens[1].substr(3)), childNames); + success = mBuilder.addVotElement(name, boost::lexical_cast(tokens[1].substr(3)), childNames); } else if(tokens[1] == "pand") { - mBuilder.addPandElement(name, childNames); + success = mBuilder.addPandElement(name, childNames); } else if(tokens[1] == "wsp" || tokens[1] == "csp") { - mBuilder.addSpareElement(name, childNames); + success = mBuilder.addSpareElement(name, childNames); } else if(boost::starts_with(tokens[1], "lambda=")) { - mBuilder.addBasicElement(name, boost::lexical_cast(tokens[1].substr(7)), boost::lexical_cast(tokens[2].substr(5))); + success = mBuilder.addBasicElement(name, boost::lexical_cast(tokens[1].substr(7)), boost::lexical_cast(tokens[2].substr(5))); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " + tokens[1] + " not recognized."); + success = false; } } - + if (generalSuccess) { + generalSuccess = success; + } } if(!mBuilder.setTopLevel(toplevelId)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } file.close(); - return true; + return generalSuccess; } - } } \ No newline at end of file diff --git a/src/parser/DFTGalileoParser.h b/src/parser/DFTGalileoParser.h index 3dc6f11eb..9d0cc0096 100644 --- a/src/parser/DFTGalileoParser.h +++ b/src/parser/DFTGalileoParser.h @@ -6,8 +6,6 @@ #include - - namespace storm { namespace parser { class DFTGalileoParser { @@ -23,7 +21,5 @@ namespace storm { } } - - #endif /* DFTGALILEOPARSER_H */ diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 551c7ad2a..8dee2a0b6 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -75,7 +75,7 @@ namespace storm { } void DFT::printSpareModules(std::ostream& os) const { - std::cout << "[" << mElements[mTopLevelIndex] << "] {"; + std::cout << "[" << mElements[mTopLevelIndex]->id() << "] {"; std::vector::const_iterator it = mTopModule.begin(); assert(it != mTopModule.end()); os << mElements[(*it)]->name(); diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 1f8939fd7..fbf035f44 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -16,7 +16,6 @@ namespace storm { namespace storage { - struct DFTElementSort { bool operator()(std::shared_ptr const& a, std::shared_ptr const& b) const { if (a->rank() == 0 && b->rank() == 0) { @@ -29,8 +28,6 @@ namespace storm { class DFT { - - private: std::vector> mElements; size_t mNrOfBEs; @@ -44,7 +41,6 @@ namespace storm { std::vector mIdToFailureIndex; std::map mUsageIndex; - public: DFT(std::vector> const& elements, std::shared_ptr const& tle); diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index f6364a523..b8e2c54a2 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -10,7 +10,6 @@ namespace storm { namespace storage { - DFT DFTBuilder::build() { for(auto& elem : mChildNames) { @@ -23,8 +22,6 @@ namespace storm { // Sort elements topologically - - // compute rank for (auto& elem : mElements) { computeRank(elem.second); @@ -48,23 +45,22 @@ namespace storm { if(elem->rank() == -1) { if(elem->nrChildren() == 0) { elem->setRank(0); - return 0; - } - std::shared_ptr gate = std::static_pointer_cast(elem); - unsigned maxrnk = 0; - unsigned newrnk = 0; + } else { + std::shared_ptr gate = std::static_pointer_cast(elem); + unsigned maxrnk = 0; + unsigned newrnk = 0; - for(std::shared_ptr const& child : gate->children()) { - newrnk = computeRank(child); - if(newrnk > maxrnk) { - maxrnk = newrnk; + for (std::shared_ptr const &child : gate->children()) { + newrnk = computeRank(child); + if (newrnk > maxrnk) { + maxrnk = newrnk; + } } + elem->setRank(maxrnk + 1); } - elem->setRank(maxrnk+1); - return maxrnk + 1; - } else { - return elem->rank(); } + + return elem->rank(); } bool DFTBuilder::addStandardGate(std::string const& name, std::vector const& children, DFTElementTypes tp) { @@ -109,7 +105,6 @@ namespace storm { } visited[n] = topoSortColour::BLACK; L.push_back(n); - } } diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index e29a8aa02..68e64b1dc 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -43,8 +43,6 @@ namespace storm { return addStandardGate(name, children, DFTElementTypes::SPARE); } - - bool addVotElement(std::string const& name, unsigned threshold, std::vector const& children) { assert(children.size() > 0); if(mElements.count(name) != 0) { @@ -103,8 +101,8 @@ namespace storm { enum class topoSortColour {WHITE, BLACK, GREY}; void topoVisit(std::shared_ptr const& n, std::map, topoSortColour>& visited, std::vector>& L); - std::vector> topoSort(); + std::vector> topoSort(); }; } diff --git a/src/storage/dft/DFTUnit.h b/src/storage/dft/DFTUnit.h index 18319b70c..5e179f091 100644 --- a/src/storage/dft/DFTUnit.h +++ b/src/storage/dft/DFTUnit.h @@ -1,6 +1,8 @@ #ifndef DFTUNIT_H #define DFTUNIT_H +#include "../BitVector.h" + namespace storm { namespace storage { class DFT; diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 07e2624ee..e491cbe2b 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -11,12 +11,22 @@ int main(int argc, char** argv) { std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl; } storm::utility::setUp(); - + + std::cout << "Parsing DFT file..." << std::endl; storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(argv[1]); + + std::cout << "Built data structure" << std::endl; dft.printElements(); dft.printSpareModules(); + + std::cout << "Building CTMC..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft); builder.buildCtmc(); + std::cout << "Built CTMC" << std::endl; + + //std::cout << "Model checking..." << std::endl; + //TODO check CTMC + //std::cout << "Checked model" << std::endl; }