From 4ae86c76f91a1b526076944a6c14f15cf3127629 Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 16 Dec 2015 16:53:33 +0100 Subject: [PATCH] Output uses logger now Former-commit-id: bb5061ccd41a7c5a7e83f67fa5323e4f138df50c --- src/builder/ExplicitDFTModelBuilder.cpp | 19 ++++--- src/parser/DFTGalileoParser.cpp | 15 +++--- src/storage/dft/DFT.cpp | 53 ++++++++++--------- src/storage/dft/DFT.h | 27 +++------- src/storage/dft/DFTBuilder.cpp | 6 --- src/storage/dft/DFTElements.h | 40 +++++++------- src/storage/dft/DFTState.cpp | 3 +- src/storage/dft/DFTState.h | 14 ++--- .../dft/DFTStateSpaceGenerationQueues.h | 2 +- src/storm-dyftee.cpp | 12 +++-- 10 files changed, 90 insertions(+), 101 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 788c5a0fa..bf23c5d4f 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -17,12 +17,11 @@ namespace storm { // Begin model generation exploreStates(stateQueue, transitionMatrixBuilder); - //std::cout << "Generated " << mStates.size() << " states" << std::endl; + STORM_LOG_DEBUG("Generated " << mStates.size() << " states"); // Build CTMC transitionMatrix = transitionMatrixBuilder.build(); - //std::cout << "TransitionMatrix: " << std::endl; - //std::cout << transitionMatrix << std::endl; + STORM_LOG_DEBUG("TransitionMatrix: " << std::endl << transitionMatrix); // TODO Matthias: build CTMC } @@ -44,7 +43,7 @@ namespace storm { // Let BE fail while (smallest < state.nrFailableBEs()) { - //std::cout << "exploring from: " << mDft.getStateString(state) << std::endl; + STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state)); storm::storage::DFTState newState(state); std::pair>, bool> nextBE = newState.letNextBEFail(smallest++); @@ -53,7 +52,7 @@ namespace storm { break; } - //std::cout << "with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]" << std::endl; + STORM_LOG_TRACE("with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]"); storm::storage::DFTStateSpaceGenerationQueues queues; @@ -85,22 +84,22 @@ namespace storm { auto itInsert = mStates.insert(newState); assert(itInsert.second); it = itInsert.first; - //std::cout << "New state " << mDft.getStateString(newState) << std::endl; + STORM_LOG_TRACE("New state " << mDft.getStateString(newState)); // Recursive call if (!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) { stateQueue.push(newState); } else { if (mDft.hasFailed(newState)) { - //std::cout << "Failed " << mDft.getStateString(newState) << std::endl; + STORM_LOG_TRACE("Failed " << mDft.getStateString(newState)); } else { assert(mDft.isFailsafe(newState)); - //std::cout << "Failsafe" << mDft.getStateString(newState) << std::endl; + STORM_LOG_TRACE("Failsafe" << mDft.getStateString(newState)); } } } else { // State already exists - //std::cout << "State " << mDft.getStateString(*it) << " already exists" << std::endl; + STORM_LOG_TRACE("State " << mDft.getStateString(*it) << " already exists"); } // Set transition @@ -114,7 +113,7 @@ namespace storm { { ValueType rate = it->second / sum; transitionMatrixBuilder.addNextValue(state.getId(), it->first, rate); - //std::cout << "Added transition from " << state.getId() << " to " << it->first << " with " << rate << std::endl; + STORM_LOG_TRACE("Added transition from " << state.getId() << " to " << it->first << " with " << rate); } } // end while queue diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index a93e84e92..a710e81d3 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -12,7 +12,10 @@ namespace storm { namespace parser { storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename) { if(readFile(filename)) { - return 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; } else { throw storm::exceptions::FileIoException(); } @@ -24,9 +27,8 @@ namespace storm { if(firstQuots == std::string::npos) { return name; - } else if (secondQuots ==std::string::npos) { - std::cerr << "No ending quotation mark found in " << name <print(os); - os << std::endl; + stream << "[" << elem->id() << "]" << elem->toString() << std::endl; } + return stream.str(); } - - - void DFT::printInfo(std::ostream& os) const { - os << "Top level index: " << mTopLevelIndex << std::endl << "Nr BEs" << mNrOfBEs << std::endl; + std::string DFT::getInfoString() const { + std::stringstream stream; + stream << "Top level index: " << mTopLevelIndex << ", Nr BEs" << mNrOfBEs; + return stream.str(); } - void DFT::printSpareModules(std::ostream& os) const { - std::cout << "[" << mElements[mTopLevelIndex]->id() << "] {"; + std::string DFT::getSpareModulesString() const { + std::stringstream stream; + stream << "[" << mElements[mTopLevelIndex]->id() << "] {"; std::vector::const_iterator it = mTopModule.begin(); assert(it != mTopModule.end()); - os << mElements[(*it)]->name(); + stream << mElements[(*it)]->name(); ++it; while(it != mTopModule.end()) { - os << ", " << mElements[(*it)]->name(); + stream << ", " << mElements[(*it)]->name(); ++it; } - os << "}" << std::endl; + stream << "}" << std::endl; for(auto const& spareModule : mSpareModules) { - std::cout << "[" << mElements[spareModule.first]->name() << "] = {"; - os.flush(); + stream << "[" << mElements[spareModule.first]->name() << "] = {"; std::vector::const_iterator it = spareModule.second.begin(); assert(it != spareModule.second.end()); - os << mElements[(*it)]->name(); + stream << mElements[(*it)]->name(); ++it; while(it != spareModule.second.end()) { - os << ", " << mElements[(*it)]->name(); - os.flush(); + stream << ", " << mElements[(*it)]->name(); ++it; } - os << "}" << std::endl; + stream << "}" << std::endl; } + return stream.str(); } - void DFT::printElementsWithState(DFTState const& state, std::ostream& os) const{ + std::string DFT::getElementsWithStateString(DFTState const& state) const{ + std::stringstream stream; for (auto const& elem : mElements) { - os << "[" << elem->id() << "]"; - elem->print(os); - os << "\t** " << state.getElementState(elem->id()); + stream << "[" << elem->id() << "]"; + stream << elem->toString(); + stream << "\t** " << state.getElementState(elem->id()); if(elem->isSpareGate()) { if(state.isActiveSpare(elem->id())) { - os << " actively"; + stream << " actively"; } - os << " using " << state.uses(elem->id()); + stream << " using " << state.uses(elem->id()); } - std::cout << std::endl; + stream << std::endl; } + return stream.str(); } std::string DFT::getStateString(DFTState const& state) const{ diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index 64a9ccdc4..df97df476 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -11,6 +11,7 @@ #include #include "../../utility/math.h" +#include "src/utility/macros.h" #include namespace storm { @@ -143,15 +144,14 @@ namespace storm { bool isFailsafe(DFTState const& state) const { return state.isFailsafe(mTopLevelIndex); } - - void printElements(std::ostream& os = std::cout) const; - - void printInfo(std::ostream& os = std::cout) const; - - void printSpareModules(std::ostream& os = std::cout) const; - - void printElementsWithState(DFTState const& state, std::ostream& os = std::cout) const; + std::string getElementsString() const; + + std::string getInfoString() const; + + std::string getSpareModulesString() const; + + std::string getElementsWithStateString(DFTState const& state) const; std::string getStateString(DFTState const& state) const; @@ -163,18 +163,7 @@ namespace storm { return true; } - - - }; - - - - - - - - } } diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index d1d6f320f..10d96b6d0 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -34,13 +34,7 @@ namespace storm { for(std::shared_ptr e : elems) { e->setId(id++); } - for(auto& e : elems) { - std::cout << "[" << e->id() << "] "; - e->print(); - std::cout << std::endl; - } return DFT(elems, mElements[topLevelIdentifier]); - } unsigned DFTBuilder::computeRank(std::shared_ptr const& elem) { diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 9479293d2..e7a97e66c 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -96,8 +96,8 @@ namespace storm { virtual void extendSpareModule(std::set& elementsInModule) const; virtual size_t nrChildren() const = 0; - virtual void print(std::ostream& = std::cout) const = 0; - + virtual std::string toString() const = 0; + virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; virtual std::vector independentUnit() const = 0; @@ -187,16 +187,18 @@ namespace storm { - virtual void print(std::ostream& os = std::cout) const override { - os << "{" << name() << "} " << typestring() << "( "; + virtual std::string toString() const override { + std::stringstream stream; + stream << "{" << name() << "} " << typestring() << "( "; std::vector>::const_iterator it = mChildren.begin(); - os << (*it)->name(); + stream << (*it)->name(); ++it; while(it != mChildren.end()) { - os << ", " << (*it)->name(); + stream << ", " << (*it)->name(); ++it; } - os << ")"; + stream << ")"; + return stream.str(); } virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { @@ -287,8 +289,10 @@ namespace storm { return mPassiveFailureRate; } - void print(std::ostream& os = std::cout) const { - os << *this; + std::string toString() const { + std::stringstream stream; + stream << *this; + return stream.str(); } bool isBasicElement() const { @@ -372,8 +376,7 @@ namespace storm { }; inline std::ostream& operator<<(std::ostream& os, DFTAnd const& gate) { - gate.print(os); - return os; + return os << gate.toString(); } @@ -411,8 +414,7 @@ namespace storm { }; inline std::ostream& operator<<(std::ostream& os, DFTOr const& gate) { - gate.print(os); - return os; + return os << gate.toString(); } class DFTSeqAnd : public DFTGate { @@ -463,8 +465,7 @@ namespace storm { }; inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) { - gate.print(os); - return os; + return os << gate.toString(); } class DFTPand : public DFTGate { @@ -510,8 +511,7 @@ namespace storm { }; inline std::ostream& operator<<(std::ostream& os, DFTPand const& gate) { - gate.print(os); - return os; + return os << gate.toString(); } class DFTPor : public DFTGate { @@ -534,8 +534,7 @@ namespace storm { }; inline std::ostream& operator<<(std::ostream& os, DFTPor const& gate) { - gate.print(os); - return os; + return os << gate.toString(); } class DFTVot : public DFTGate { @@ -594,8 +593,7 @@ namespace storm { }; inline std::ostream& operator<<(std::ostream& os, DFTVot const& gate) { - gate.print(os); - return os; + return os << gate.toString(); } class DFTSpare : public DFTGate { diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index e7756cbbd..599de5525 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -69,8 +69,7 @@ namespace storm { std::pair>, bool> DFTState::letNextBEFail(size_t index) { assert(index < mIsCurrentlyFailableBE.size()); - //std::cout << "currently failable: "; - //printCurrentlyFailable(); + STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString()); std::pair>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false); mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index); setFailed(res.first->id()); diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 67eec6598..2085ba010 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -4,7 +4,7 @@ #include "../BitVector.h" #include "DFTElementState.h" -#include +#include namespace storm { namespace storage { @@ -111,18 +111,20 @@ namespace storm { std::pair>, bool> letNextBEFail(size_t smallestIndex = 0); - void printCurrentlyFailable(std::ostream& os = std::cout) { + std::string getCurrentlyFailableString() { + std::stringstream stream; auto it = mIsCurrentlyFailableBE.begin(); - os << "{"; + stream << "{"; if(it != mIsCurrentlyFailableBE.end()) { - os << *it; + stream << *it; } ++it; while(it != mIsCurrentlyFailableBE.end()) { - os << ", " << *it; + stream << ", " << *it; ++it; } - os << "}" << std::endl; + stream << "}"; + return stream.str(); } friend bool operator==(DFTState const& a, DFTState const& b) { diff --git a/src/storage/dft/DFTStateSpaceGenerationQueues.h b/src/storage/dft/DFTStateSpaceGenerationQueues.h index f748e8232..ec0879d52 100644 --- a/src/storage/dft/DFTStateSpaceGenerationQueues.h +++ b/src/storage/dft/DFTStateSpaceGenerationQueues.h @@ -31,7 +31,7 @@ namespace storm { } std::shared_ptr nextFailurePropagation() { - std::shared_ptr next= failurePropagation.top(); + std::shared_ptr next = failurePropagation.top(); failurePropagation.pop(); return next; } diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 75f329ccb..bd34cdeea 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -10,22 +10,24 @@ int main(int argc, char** argv) { if(argc != 2) { std::cout << "Storm-DyFTeE should be called with a filename as argument." << std::endl; } + storm::utility::setUp(); + log4cplus::LogLevel level = log4cplus::TRACE_LOG_LEVEL; + logger.setLogLevel(level); + logger.getAppender("mainConsoleAppender")->setThreshold(level); 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; + std::cout << "Model checking..." << std::endl; + //TODO Matthias: check CTMC + std::cout << "Checked model" << std::endl; }