From 7b37023f791145b2ad2e9978d2c958c714834831 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 15 Dec 2015 11:48:11 +0100 Subject: [PATCH] Some refactoring Former-commit-id: c5954a71a2b035a195f3cb2b1161a803a00dd744 --- src/builder/ExplicitDFTModelBuilder.cpp | 72 +++++++++++++++++++ src/builder/ExplicitDFTModelBuilder.h | 91 +++++-------------------- src/storage/dft/DFT.cpp | 15 +++- src/storage/dft/DFT.h | 4 +- src/storage/dft/DFTState.cpp | 21 ++++-- src/storage/dft/DFTState.h | 14 +++- src/storm-dyftee.cpp | 2 +- 7 files changed, 134 insertions(+), 85 deletions(-) create mode 100644 src/builder/ExplicitDFTModelBuilder.cpp diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp new file mode 100644 index 000000000..8683dd57e --- /dev/null +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -0,0 +1,72 @@ +#include "src/builder/ExplicitDFTModelBuilder.h" + +namespace storm { + namespace builder { + + void ExplicitDFTModelBuilder::exploreStateSuccessors(storm::storage::DFTState const &state) { + size_t smallest = 0; + + while(smallest < state.nrFailableBEs()) { + //std::cout << "exploring from: " << mDft.getStateString(state) << std::endl; + + storm::storage::DFTState newState(state); + std::pair>, bool> nextBE = newState.letNextBEFail(smallest++); + if(nextBE.first == nullptr) { + //std::cout << "break" << std::endl; + break; + + } + //std::cout << "with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]" << std::endl; + + storm::storage::DFTStateSpaceGenerationQueues queues; + + for(std::shared_ptr parent : nextBE.first->parents()) { + if(newState.isOperational(parent->id())) { + queues.propagateFailure(parent); + } + } + + while(!queues.failurePropagationDone()) { + std::shared_ptr next = queues.nextFailurePropagation(); + next->checkFails(newState, queues); + } + + while(!queues.failsafePropagationDone()) { + std::shared_ptr next = queues.nextFailsafePropagation(); + next->checkFailsafe(newState, queues); + } + + while(!queues.dontCarePropagationDone()) { + std::shared_ptr next = queues.nextDontCarePropagation(); + next->checkDontCareAnymore(newState, queues); + } + + auto it = mStates.find(newState); + if (it == mStates.end()) { + // New state + newState.setId(newIndex++); + mStates.insert(newState); + //std::cout << "New state " << mDft.getStateString(newState) << std::endl; + + // Recursive call + if(!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) { + exploreStateSuccessors(newState); + } else { + if (mDft.hasFailed(newState)) { + //std::cout << "Failed " << mDft.getStateString(newState) << std::endl; + } else { + assert(mDft.isFailsafe(newState)); + //std::cout << "Failsafe" << mDft.getStateString(newState) << std::endl; + } + } + } else { + // State already exists + //std::cout << "State " << mDft.getStateString(*it) << " already exists" << std::endl; + } + } + } + + } // namespace builder +} // namespace storm + + diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h index e8c169976..7009c4896 100644 --- a/src/builder/ExplicitDFTModelBuilder.h +++ b/src/builder/ExplicitDFTModelBuilder.h @@ -3,91 +3,34 @@ #include "../storage/dft/DFT.h" +#include + namespace storm { namespace builder { class ExplicitDFTModelBuilder { - storm::storage::DFT const& mDft; - std::unordered_map mStateIndices; + storm::storage::DFT const &mDft; + std::unordered_set mStates; size_t newIndex = 0; //std::stack> mStack; - - public: - ExplicitDFTModelBuilder(storm::storage::DFT const& dft) : mDft(dft) - { - - } - - - void exploreStateSuccessors(storm::storage::DFTState const& state) { - size_t smallest = 0; - - while(smallest < state.nrFailableBEs()) { - //std::cout << "exploring from :" << std::endl; - //mDft.printElementsWithState(state); - //std::cout << "***************" << std::endl; - storm::storage::DFTState newState(state); - std::pair>, bool> nextBE = newState.letNextBEFail(smallest++); - if(nextBE.first == nullptr) { - //std::cout << "break" << std::endl; - break; - - } - //std::cout << "with the failure of: " << nextBE.first->name() << std::endl; - - storm::storage::DFTStateSpaceGenerationQueues queues; - for(std::shared_ptr parent : nextBE.first->parents()) { - if(newState.isOperational(parent->id())) { - queues.propagateFailure(parent); - } - } - - - while(!queues.failurePropagationDone()) { - std::shared_ptr next = queues.nextFailurePropagation(); - next->checkFails(newState, queues); - } - - while(!queues.failsafePropagationDone()) { - std::shared_ptr next = queues.nextFailsafePropagation(); - next->checkFailsafe(newState, queues); - } - - while(!queues.dontCarePropagationDone()) { - std::shared_ptr next = queues.nextDontCarePropagation(); - next->checkDontCareAnymore(newState, queues); - } - - - - if(!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) { - auto it = mStateIndices.find(newState); - if(it == mStateIndices.end()) { - exploreStateSuccessors(newState); - mStateIndices.insert(std::make_pair(newState, newIndex++)); - if(newIndex % 16384 == 0) std::cout << newIndex << std::endl; - } - - } - else { - //std::cout << "done." << std::endl; - } + public: + ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) { - - - } } - - void buildCtmc() { - storm::storage::DFTState state(mDft); + + void buildCTMC() { + // Construct starting start + storm::storage::DFTState state(mDft, newIndex++); + mStates.insert(state); + // Begin model generation exploreStateSuccessors(state); - std::cout << mStateIndices.size() << std::endl; + std::cout << "Generated " << mStates.size() << " states" << std::endl; } - + + private: + void exploreStateSuccessors(storm::storage::DFTState const &state); }; } } - -#endif /* EXPLICITDFTMODELBUILDER_H */ - +#endif /* EXPLICITDFTMODELBUILDER_H */ \ No newline at end of file diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp index 8dee2a0b6..faed81efd 100644 --- a/src/storage/dft/DFT.cpp +++ b/src/storage/dft/DFT.cpp @@ -114,9 +114,22 @@ namespace storm { os << " using " << state.uses(elem->id()); } std::cout << std::endl; + } + } - + std::string DFT::getStateString(DFTState const& state) const{ + std::stringstream stream; + stream << "(" << state.getId() << ") "; + for (auto const& elem : mElements) { + stream << state.getElementStateInt(elem->id()); + /*if(elem->isSpareGate()) { + if(state.isActiveSpare(elem->id())) { + os << " actively"; + } + os << " using " << state.uses(elem->id()); + }*/ } + return stream.str(); } } } diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h index fbf035f44..64a9ccdc4 100644 --- a/src/storage/dft/DFT.h +++ b/src/storage/dft/DFT.h @@ -151,7 +151,9 @@ namespace storm { void printSpareModules(std::ostream& os = std::cout) const; - void printElementsWithState(DFTState const& state, std::ostream& os = std::cout) const; + void printElementsWithState(DFTState const& state, std::ostream& os = std::cout) const; + + std::string getStateString(DFTState const& state) const; private: bool elementIndicesCorrect() const { diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 5536b05a6..01534342b 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -5,7 +5,7 @@ namespace storm { namespace storage { - DFTState::DFTState(DFT const& dft) : mStatus(dft.stateSize()), mDft(dft) { + DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mDft(dft), mId(id) { mInactiveSpares = dft.getSpareIndices(); dft.initializeUses(*this); dft.initializeActivation(*this); @@ -15,7 +15,19 @@ namespace storm { } DFTElementState DFTState::getElementState(size_t id) const { - return static_cast(mStatus.getAsInt(mDft.failureIndex(id), 2)); + return static_cast(getElementStateInt(id)); + } + + int DFTState::getElementStateInt(size_t id) const { + return mStatus.getAsInt(mDft.failureIndex(id), 2); + } + + size_t DFTState::getId() const { + return mId; + } + + void DFTState::setId(size_t id) { + mId = id; } bool DFTState::isOperational(size_t id) const { @@ -58,7 +70,7 @@ namespace storm { { assert(index < mIsCurrentlyFailableBE.size()); //std::cout << "currently failable: "; - //printCurrentlyFailable(std::cout); + //printCurrentlyFailable(); std::pair>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false); mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index); setFailed(res.first->id()); @@ -98,8 +110,6 @@ namespace storm { } - - void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) { mStatus.setFromInt(usageIndex, mDft.usageInfoBits(), child); mUsedRepresentants.push_back(child); @@ -121,5 +131,6 @@ namespace storm { } return false; } + } } diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 719d49e37..67eec6598 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -4,6 +4,7 @@ #include "../BitVector.h" #include "DFTElementState.h" +#include namespace storm { namespace storage { @@ -18,6 +19,7 @@ namespace storm { friend struct std::hash; private: storm::storage::BitVector mStatus; + size_t mId; std::vector mInactiveSpares; std::vector mIsCurrentlyFailableBE; std::vector mUsedRepresentants; @@ -25,9 +27,15 @@ namespace storm { const DFT& mDft; public: - DFTState(DFT const& dft); + DFTState(DFT const& dft, size_t id); DFTElementState getElementState(size_t id) const; + + int getElementStateInt(size_t id) const; + + size_t getId() const; + + void setId(size_t id); bool isOperational(size_t id) const; @@ -103,7 +111,7 @@ namespace storm { std::pair>, bool> letNextBEFail(size_t smallestIndex = 0); - void printCurrentlyFailable(std::ostream& os) { + void printCurrentlyFailable(std::ostream& os = std::cout) { auto it = mIsCurrentlyFailableBE.begin(); os << "{"; if(it != mIsCurrentlyFailableBE.end()) { @@ -116,7 +124,7 @@ namespace storm { } os << "}" << std::endl; } - + friend bool operator==(DFTState const& a, DFTState const& b) { return a.mStatus == b.mStatus; } diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index e491cbe2b..b86781460 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -22,7 +22,7 @@ int main(int argc, char** argv) { std::cout << "Building CTMC..." << std::endl; storm::builder::ExplicitDFTModelBuilder builder(dft); - builder.buildCtmc(); + builder.buildCTMC(); std::cout << "Built CTMC" << std::endl; //std::cout << "Model checking..." << std::endl;