From a42703a49a47229cc5668e70a9b90b60a028d9a9 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 15 Dec 2016 01:27:03 +0100 Subject: [PATCH] towards support for n-ary pdeps --- src/storm-dft/storage/dft/DFTBuilder.cpp | 32 ++++++++++++------ src/storm-dft/storage/dft/DFTBuilder.h | 33 ++++++++++++------- .../storage/dft/elements/DFTDependency.h | 19 ++++------- 3 files changed, 50 insertions(+), 34 deletions(-) diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 7953bf498..ed35b176d 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -50,17 +50,29 @@ namespace storm { } } - // Initialize dependencies - for (auto& dependency : mDependencies) { - DFTGatePointer triggerEvent = std::static_pointer_cast>(mElements[dependency->nameTrigger()]); - STORM_LOG_ASSERT(mElements[dependency->nameDependent()]->isBasicElement(), "Dependent element is not BE."); - std::shared_ptr> dependentEvent = std::static_pointer_cast>(mElements[dependency->nameDependent()]); - dependency->initialize(triggerEvent, dependentEvent); - triggerEvent->addOutgoingDependency(dependency); - dependentEvent->addIngoingDependency(dependency); + for(auto& elem : mDependencyChildNames) { + bool first = true; + std::vector>> dependencies; + for(auto const& childName : elem.second) { + auto itFind = mElements.find(childName); + STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found"); + DFTElementPointer childElement = itFind->second; + if (!first) { + dependencies.push_back(std::static_pointer_cast>(childElement)); + } else { + elem.first->setTriggerElement(std::static_pointer_cast>(childElement)); + childElement->addOutgoingDependency(elem.first); + } + first = false; + } + if (binaryDependencies) { + assert(dependencies.size() == 1); + } + assert(binaryDependencies); + elem.first->setDependentEvent(dependencies[0]); + dependencies[0]->addIngoingDependency(elem.first); } - - + // Sort elements topologically // compute rank diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 4109272b7..9f216720c 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -31,6 +31,7 @@ namespace storm { std::unordered_map mElements; std::unordered_map> mChildNames; std::unordered_map> mRestrictionChildNames; + std::unordered_map> mDependencyChildNames; std::vector mDependencies; std::vector mRestrictions; std::unordered_map mLayoutInfo; @@ -101,7 +102,7 @@ namespace storm { //TODO Matthias: collect constraints for SMT solving //0 <= probability <= 1 - if (!storm::utility::isOne(probability) && children.size() > 2) { + if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) { // Introduce additional element for first capturing the proabilistic dependency std::string nameAdditional = name + "_additional"; addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero()); @@ -114,17 +115,25 @@ namespace storm { return true; } else { // Add dependencies - for (size_t i = 1; i < children.size(); ++i) { - std::string nameDep = name + "_" + std::to_string(i); - if(mElements.count(nameDep) != 0) { - // Element with that name already exists. - STORM_LOG_ERROR("Element with name: " << nameDep << " already exists."); - return false; + if(binaryDependencies) { + for (size_t i = 1; i < children.size(); ++i) { + std::string nameDep = name + "_" + std::to_string(i); + if (mElements.count(nameDep) != 0) { + // Element with that name already exists. + STORM_LOG_ERROR("Element with name: " << nameDep << " already exists."); + return false; + } + STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, + "PDep with multiple children supported."); + DFTDependencyPointer element = std::make_shared>(mNextId++, + nameDep, + probability); + mElements[element->name()] = element; + mDependencyChildNames[element] = {trigger, children[i]}; + mDependencies.push_back(element); } - STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported."); - DFTDependencyPointer element = std::make_shared>(mNextId++, nameDep, trigger, children[i], probability); - mElements[element->name()] = element; - mDependencies.push_back(element); + } else { + } return true; } @@ -213,6 +222,8 @@ namespace storm { bool pandDefaultInclusive; // If true, the standard gate adders make a pand inclusive, and exclusive otherwise. bool porDefaultInclusive; + + bool binaryDependencies; }; } diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h index 2c5b7d0cc..957048d68 100644 --- a/src/storm-dft/storage/dft/elements/DFTDependency.h +++ b/src/storm-dft/storage/dft/elements/DFTDependency.h @@ -12,35 +12,28 @@ namespace storm { using DFTBEPointer = std::shared_ptr>; protected: - std::string mNameTrigger; - std::string mNameDependent; ValueType mProbability; DFTGatePointer mTriggerEvent; DFTBEPointer mDependentEvent; public: - DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent, ValueType probability) : - DFTElement(id, name), mNameTrigger(trigger), mNameDependent(dependent), mProbability(probability) + DFTDependency(size_t id, std::string const& name, ValueType probability) : + DFTElement(id, name), mProbability(probability) { } virtual ~DFTDependency() {} - void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) { - STORM_LOG_ASSERT(triggerEvent->name() == mNameTrigger, "Name does not match."); - STORM_LOG_ASSERT(dependentEvent->name() == mNameDependent, "Name does not match."); + void setTriggerElement(DFTGatePointer const& triggerEvent) { mTriggerEvent = triggerEvent; - mDependentEvent = dependentEvent; - } - std::string nameTrigger() const { - return mNameTrigger; } - std::string nameDependent() const { - return mNameDependent; + void setDependentEvent(DFTBEPointer const& dependentEvent) { + mDependentEvent = dependentEvent; } + ValueType const& probability() const { return mProbability; }