FDeps are parsed and constructed but not used yet

Former-commit-id: fbd2a95f9c

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));

src/storage/dft/DFTBuilder.cpp

@@ -18,11 +18,30 @@ namespace storm {
             for(auto& elem : mChildNames) {
                 DFTGatePointer gate = std::static_pointer_cast<DFTGate<ValueType>>(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<DFTGate<ValueType>>(mElements[dependency->nameTrigger()]);
+                std::shared_ptr<DFTBE<ValueType>> dependentEvent = std::static_pointer_cast<DFTBE<ValueType>>(mElements[dependency->nameDependent()]);
+                dependency->initialize(triggerEvent, dependentEvent);
+            }
+
             // Sort elements topologically
             // compute rank
             for (auto& elem : mElements) {
@@ -40,7 +59,7 @@ namespace storm {
         template<typename ValueType>
         unsigned DFTBuilder<ValueType>::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<DFTGate<ValueType>>(elem);

src/storage/dft/DFTBuilder.h

@@ -19,12 +19,14 @@ namespace storm {
             using DFTElementVector = std::vector<DFTElementPointer>;
             using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
             using DFTGateVector = std::vector<DFTGatePointer>;
+            using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
 
         private:
             std::size_t mNextId = 0;
             std::string topLevelIdentifier;
             std::unordered_map<std::string, DFTElementPointer> mElements;
             std::unordered_map<DFTElementPointer, std::vector<std::string>> mChildNames;
+            std::vector<DFTDependencyPointer> mDependencies;
             
         public:
             DFTBuilder() {
@@ -51,6 +53,29 @@ namespace storm {
                 return addStandardGate(name, children, DFTElementTypes::SPARE);
             }
             
+            bool addFDepElement(std::string const& name, std::vector<std::string> 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<DFTDependency<ValueType>>(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<std::string> const& children) {
                 assert(children.size() > 0);
                 if(mElements.count(name) != 0) {

src/storage/dft/DFTElements.h

@@ -75,6 +75,10 @@ namespace storm {
                 return false;
             }
 
+            virtual bool isDependency() const {
+                return false;
+            }
+
             virtual void setId(size_t newId) {
                 mId = newId;
             }
@@ -357,6 +361,79 @@ namespace storm {
         };
 
 
+        template<typename ValueType>
+        class DFTDependency : public DFTElement<ValueType> {
+
+            using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
+            using DFTBEPointer = std::shared_ptr<DFTBE<ValueType>>;
+            using DFTBEVector = std::vector<DFTBEPointer>;
+
+        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<ValueType>(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<size_t> independentUnit() const override {
+                std::set<size_t> unit = {this->mId};
+                mDependentEvent->extendUnit(unit);
+                if(unit.count(mTriggerEvent->id()) != 0) {
+                    return {};
+                }
+                return std::vector<size_t>(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<typename ValueType>
         class DFTAnd : public DFTGate<ValueType> {