diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 163bc1488..d623821e6 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/src/parser/DFTGalileoParser.cpp @@ -107,7 +107,7 @@ namespace storm { } else if (tokens[1] == "wsp" || tokens[1] == "csp") { success = builder.addSpareElement(name, childNames); } else if (boost::starts_with(tokens[1], "fdep")) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Functional dependencies currently not supported"); + success = builder.addFDepElement(name, childNames); } else if (boost::starts_with(tokens[1], "lambda=")) { ValueType failureRate = parseRationalExpression(tokens[1].substr(7)); ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5)); diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp index d49bfd067..4ee258dd1 100644 --- a/src/storage/dft/DFTBuilder.cpp +++ b/src/storage/dft/DFTBuilder.cpp @@ -18,11 +18,30 @@ namespace storm { for(auto& elem : mChildNames) { DFTGatePointer gate = std::static_pointer_cast>(elem.first); for(auto const& child : elem.second) { - gate->pushBackChild(mElements[child]); - mElements[child]->addParent(gate); + auto itFind = mElements.find(child); + if (itFind != mElements.end()) { + // Child found + DFTElementPointer childElement = itFind->second; + assert(!childElement->isDependency()); + gate->pushBackChild(childElement); + childElement->addParent(gate); + } else { + // Child not found -> find first dependent event to assure that child is dependency + auto itFind = mElements.find(child + "_1"); + assert(itFind != mElements.end()); + assert(itFind->second->isDependency()); + STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name()); + } } } + // Initialize dependencies + for (auto& dependency : mDependencies) { + DFTGatePointer triggerEvent = std::static_pointer_cast>(mElements[dependency->nameTrigger()]); + std::shared_ptr> dependentEvent = std::static_pointer_cast>(mElements[dependency->nameDependent()]); + dependency->initialize(triggerEvent, dependentEvent); + } + // Sort elements topologically // compute rank for (auto& elem : mElements) { @@ -40,7 +59,7 @@ namespace storm { template unsigned DFTBuilder::computeRank(DFTElementPointer const& elem) { if(elem->rank() == -1) { - if(elem->nrChildren() == 0) { + if(elem->nrChildren() == 0 || elem->isDependency()) { elem->setRank(0); } else { DFTGatePointer gate = std::static_pointer_cast>(elem); diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 12d5e88c3..9dfb80ac2 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/src/storage/dft/DFTBuilder.h @@ -19,12 +19,14 @@ namespace storm { using DFTElementVector = std::vector; using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; + using DFTDependencyPointer = std::shared_ptr>; private: std::size_t mNextId = 0; std::string topLevelIdentifier; std::unordered_map mElements; std::unordered_map> mChildNames; + std::vector mDependencies; public: DFTBuilder() { @@ -51,6 +53,29 @@ namespace storm { return addStandardGate(name, children, DFTElementTypes::SPARE); } + bool addFDepElement(std::string const& name, std::vector const& children) { + assert(children.size() > 1); + if(mElements.count(name) != 0) { + // Element with that name already exists. + return false; + } + std::string trigger = children[0]; + for (size_t i = 1; i < children.size(); ++i) { + // TODO Matthias: better code + std::stringstream stream; + stream << name << "_" << i; + std::string s = stream.str(); + if(mElements.count(s) != 0) { + // Element with that name already exists. + return false; + } + DFTDependencyPointer element = std::make_shared>(mNextId++, s, trigger, children[i]); + mElements[element->name()] = element; + mDependencies.push_back(element); + } + return true; + } + bool addVotElement(std::string const& name, unsigned threshold, std::vector const& children) { assert(children.size() > 0); if(mElements.count(name) != 0) { diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 7f92ebb19..d8f9e19b1 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -74,7 +74,11 @@ namespace storm { virtual bool isSpareGate() const { return false; } - + + virtual bool isDependency() const { + return false; + } + virtual void setId(size_t newId) { mId = newId; } @@ -357,6 +361,79 @@ namespace storm { }; + template + class DFTDependency : public DFTElement { + + using DFTGatePointer = std::shared_ptr>; + using DFTBEPointer = std::shared_ptr>; + using DFTBEVector = std::vector; + + protected: + std::string mNameTrigger; + std::string mNameDependent; + DFTGatePointer mTriggerEvent; + DFTBEPointer mDependentEvent; + + public: + DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent) : + DFTElement(id, name), mNameTrigger(trigger), mNameDependent(dependent) + { + } + + virtual ~DFTDependency() {} + + void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) { + assert(triggerEvent->name() == mNameTrigger); + assert(dependentEvent->name() == mNameDependent); + mTriggerEvent = triggerEvent; + mDependentEvent = dependentEvent; + } + + std::string nameTrigger() { + return mNameTrigger; + } + + std::string nameDependent() { + return mNameDependent; + } + + DFTGatePointer const& triggerEvent() const { + assert(mTriggerEvent); + return mTriggerEvent; + } + + DFTBEPointer const& dependentEvent() const { + assert(mDependentEvent); + return mDependentEvent; + } + + virtual size_t nrChildren() const override { + return 1; + } + + virtual bool isDependency() const override { + return true; + } + + virtual std::vector independentUnit() const override { + std::set unit = {this->mId}; + mDependentEvent->extendUnit(unit); + if(unit.count(mTriggerEvent->id()) != 0) { + return {}; + } + return std::vector(unit.begin(), unit.end()); + } + + virtual std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} FDEP(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")"; + return stream.str(); + } + + protected: + + }; + template class DFTAnd : public DFTGate {