Fixed problems with pdeps

Former-commit-id: c46c88b177

benchmark_dft.py

@@ -31,8 +31,9 @@ benchmarks = [
     ("or", False, [1, 1]),
     ("pand", False, ["inf", 0.666667]),
     ("pand_param", True, ["-1", "(x)/(y+x)"]),
-    ("pdep", False, [0, 1]), #Compute
+    ("pdep", False, [2.66667, 1]),
     ("pdep2", False, [0, 1]), #Compute
+    ("pdep3", False, [2.79167, 1]),
     ("spare", False, [3.53846, 1]),
     ("spare2", False, [1.86957, 1]),
     ("spare3", False, [1.27273, 1]),

examples/dft/pdep3.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C" "F";
+"F" pdep=0.3 "B" "C";
+"B" lambda=0.4 dorm=0;
+"C" lambda=0.8 dorm=0;

src/builder/ExplicitDFTModelBuilder.cpp

@@ -77,17 +77,20 @@ namespace storm {
             // TODO Matthias: avoid transforming back and forth
             storm::storage::SparseMatrix<ValueType> rateMatrix(modelComponents.transitionMatrix);
             for (uint_fast64_t row = 0; row < rateMatrix.getRowCount(); ++row) {
+                assert(row < modelComponents.markovianStates.size());
                 if (modelComponents.markovianStates.get(row)) {
                     for (auto& entry : rateMatrix.getRow(row)) {
                         entry.setValue(entry.getValue() * modelComponents.exitRates[row]);
                     }
                 }
             }
+            
             if (deterministic) {
                 model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling));
             } else {
                 model = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(rateMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.markovianStates), std::move(modelComponents.exitRates));
             }
+            
             model->printModelInformationToStream(std::cout);
             return model;
         }
@@ -143,9 +146,6 @@ namespace storm {
                     assert(nextBEPair.second == hasDependencies);
                     STORM_LOG_TRACE("with the failure of: " << nextBE->name() << " [" << nextBE->id() << "]");
 
-                    // Update failable dependencies
-                    newState->updateFailableDependencies(nextBE->id());
-
                     // Propagate failures
                     storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
 
@@ -169,6 +169,9 @@ namespace storm {
                         DFTElementPointer next = queues.nextDontCarePropagation();
                         next->checkDontCareAnymore(*newState, queues);
                     }
+                    
+                    // Update failable dependencies
+                    newState->updateFailableDependencies(nextBE->id());
 
                     if (mStates.contains(newState->status())) {
                         // State already exists
@@ -180,7 +183,7 @@ namespace storm {
                         mStates.findOrAdd(newState->status(), newState);
                         STORM_LOG_TRACE("New state " << mDft.getStateString(newState));
 
-                        // Add state to search
+                        // Add state to search queue
                         stateQueue.push(newState);
                     }
 
@@ -188,8 +191,37 @@ namespace storm {
                     if (hasDependencies) {
                         // Failure is due to dependency -> add non-deterministic choice
                         std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1));
-                        transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), dependency->probability());
+                        transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, newState->getId(), dependency->probability());
                         STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with probability " << dependency->probability());
+
+                        if (!storm::utility::isOne(dependency->probability())) {
+                            // Add transition to state where dependency was unsuccessful
+                            DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
+                            unsuccessfulState->letDependencyBeUnsuccessful(smallest-1);
+                            
+                            if (mStates.contains(unsuccessfulState->status())) {
+                                // Unsuccessful state already exists
+                                unsuccessfulState = mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState);
+                                STORM_LOG_TRACE("State " << mDft.getStateString(unsuccessfulState) << " already exists");
+                            } else {
+                                // New unsuccessful state
+                                unsuccessfulState->setId(newIndex++);
+                                mStates.findOrAdd(unsuccessfulState->status(), unsuccessfulState);
+                                STORM_LOG_TRACE("New state " << mDft.getStateString(unsuccessfulState));
+                                
+                                // Add unsuccessful state to search queue
+                                stateQueue.push(unsuccessfulState);
+                            }
+
+                            ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability();
+                            transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, unsuccessfulState->getId(), remainingProbability);
+                            STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << unsuccessfulState->getId() << " with probability " << remainingProbability);
+                        } else {
+                            // Self-loop with probability one cannot be eliminated later one.
+                            assert(state->getId() != newState->getId());
+                        }
+                        ++rowOffset;
+
                     } else {
                         // Set failure rate according to usage
                         bool isUsed = true;

src/storage/dft/DFT.cpp

@@ -118,13 +118,17 @@ namespace storm {
             for (auto const& elem : mElements) {
                 stream << "[" << elem->id() << "]";
                 stream << elem->toString();
-                stream << "\t** " << state->getElementState(elem->id());
-                if(elem->isSpareGate()) {
-                    if(state->isActiveSpare(elem->id())) {
-                        stream << " actively";
+                if (elem->isDependency()) {
+                    stream << "\t** " << storm::storage::toChar(state->getDependencyState(elem->id()));
+                } else {
+                    stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id()));
+                    if(elem->isSpareGate()) {
+                        if(state->isActiveSpare(elem->id())) {
+                            stream << " actively";
+                        }
+                        stream << " using " << state->uses(elem->id());
                     }
-                    stream << " using " << state->uses(elem->id());
-                } 
+                }
                 stream << std::endl;
             }
             return stream.str();
@@ -135,13 +139,17 @@ namespace storm {
             std::stringstream stream;
             stream << "(" << state->getId() << ") ";
             for (auto const& elem : mElements) {
-                stream << state->getElementStateInt(elem->id());
-                if(elem->isSpareGate()) {
-                    stream << "[";
-                    if(state->isActiveSpare(elem->id())) {
-                        stream << "actively ";
+                if (elem->isDependency()) {
+                    stream << storm::storage::toChar(state->getDependencyState(elem->id())) << "[dep]";
+                } else {
+                    stream << storm::storage::toChar(state->getElementState(elem->id()));
+                    if(elem->isSpareGate()) {
+                        stream << "[";
+                        if(state->isActiveSpare(elem->id())) {
+                            stream << "actively ";
+                        }
+                        stream << "using " << state->uses(elem->id()) << "]";
                     }
-                    stream << "using " << state->uses(elem->id()) << "]";
                 }
             }
             return stream.str();

src/storage/dft/DFTBuilder.cpp

@@ -40,6 +40,7 @@ namespace storm {
                 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);
+                triggerEvent->addDependency(dependency);
             }
 
             // Sort elements topologically

src/storage/dft/DFTElementState.h

@@ -2,9 +2,11 @@
 #ifndef DFTELEMENTSTATE_H
 #define	DFTELEMENTSTATE_H
 
+#include <cassert>
+
 namespace storm {
     namespace storage {
-        enum class DFTElementState  {Operational = 0, Failed = 2, Failsafe = 1, DontCare = 3};
+        enum class DFTElementState {Operational = 0, Failed = 2, Failsafe = 1, DontCare = 3};
         
         inline std::ostream& operator<<(std::ostream& os, DFTElementState st) {
             switch(st) {
@@ -17,7 +19,53 @@ namespace storm {
                 case DFTElementState::DontCare:
                     return os << "Don't Care";
             }
+            assert(false);
+        }
+        
+        inline char toChar(DFTElementState st) {
+            switch(st) {
+                case DFTElementState::Operational:
+                    return 'O';
+                case DFTElementState::Failed:
+                    return 'F';
+                case DFTElementState::Failsafe:
+                    return 'S';
+                case DFTElementState::DontCare:
+                    return '-';
+            }
+            assert(false);
+        }
+        
+        enum class DFTDependencyState {Passive = 0, Unsuccessful = 1, Successful = 2, DontCare = 3};
+        
+        inline std::ostream& operator<<(std::ostream& os, DFTDependencyState st) {
+            switch(st) {
+                case DFTDependencyState::Passive:
+                    return os << "Passive";
+                case DFTDependencyState::Successful:
+                    return os << "Successful";
+                case DFTDependencyState::Unsuccessful:
+                    return os << "Unsuccessful";
+                case DFTDependencyState::DontCare:
+                    return os << "Don't Care";
+            }
+            assert(false);
         }
+        
+        inline char toChar(DFTDependencyState st) {
+            switch(st) {
+                case DFTDependencyState::Passive:
+                    return 'P';
+                case DFTDependencyState::Successful:
+                    return 'S';
+                case DFTDependencyState::Unsuccessful:
+                    return 'U';
+                case DFTDependencyState::DontCare:
+                    return '-';
+            }
+            assert(false);
+        }
+
     }
 }
 

src/storage/dft/DFTElements.cpp

@@ -7,7 +7,7 @@ namespace storm {
 
         template<typename ValueType>
         bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
-            if(!state.dontCare(mId))
+            if(!state.dontCare(mId) && !hasDependencies())
             {
                 for(DFTGatePointer const& parent : mParents) {
                     if(state.isOperational(parent->id())) {

src/storage/dft/DFTElements.h

@@ -23,12 +23,17 @@ namespace storm {
 
         template<typename ValueType>
         class DFTGate;
+        
+        template<typename ValueType>
+        class DFTDependency;
 
         template<typename ValueType>
         class DFTElement {
 
             using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
             using DFTGateVector = std::vector<DFTGatePointer>;
+            using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>;
+            using DFTDependencyVector = std::vector<DFTDependencyPointer>;
 
 
         protected:
@@ -36,6 +41,7 @@ namespace storm {
             std::string mName;
             size_t mRank = -1;
             DFTGateVector mParents;
+            DFTDependencyVector dependencies;
 
         public:
             DFTElement(size_t id, std::string const& name) :
@@ -132,6 +138,29 @@ namespace storm {
                 }
                 return res;
             }
+            
+            bool addDependency(DFTDependencyPointer const& e) {
+                if(std::find(dependencies.begin(), dependencies.end(), e) != dependencies.end()) {
+                    return false;
+                }
+                else
+                {
+                    dependencies.push_back(e);
+                    return true;
+                }
+            }
+            
+            bool hasDependencies() const {
+                return !dependencies.empty();
+            }
+            
+            size_t nrDependencies() const {
+                return dependencies.size();
+            }
+            
+            DFTDependencyVector const& getDependencies() const {
+                return dependencies;
+            }
 
             virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
             
@@ -433,8 +462,7 @@ namespace storm {
 
             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;

src/storage/dft/DFTState.cpp

@@ -19,6 +19,11 @@ namespace storm {
         DFTElementState DFTState<ValueType>::getElementState(size_t id) const {
             return static_cast<DFTElementState>(getElementStateInt(id));
         }
+        
+        template<typename ValueType>
+        DFTDependencyState DFTState<ValueType>::getDependencyState(size_t id) const {
+            return static_cast<DFTDependencyState>(getElementStateInt(id));
+        }
 
         template<typename ValueType>
         int DFTState<ValueType>::getElementStateInt(size_t id) const {
@@ -54,6 +59,20 @@ namespace storm {
         bool DFTState<ValueType>::dontCare(size_t id) const {
             return getElementState(id) == DFTElementState::DontCare;
         }
+        
+        template<typename ValueType>
+        bool DFTState<ValueType>::dependencyTriggered(size_t id) const {
+            return getElementStateInt(id) > 0;
+        }
+        
+        template<typename ValueType>
+        bool DFTState<ValueType>::dependencySuccessful(size_t id) const {
+            return mStatus[mDft.failureIndex(id)];
+        }
+        template<typename ValueType>
+        bool DFTState<ValueType>::dependencyUnsuccessful(size_t id) const {
+            return mStatus[mDft.failureIndex(id)+1];
+        }
 
         template<typename ValueType>
         void DFTState<ValueType>::setFailed(size_t id) {
@@ -69,6 +88,16 @@ namespace storm {
         void DFTState<ValueType>::setDontCare(size_t id) {
             mStatus.setFromInt(mDft.failureIndex(id), 2, static_cast<uint_fast64_t>(DFTElementState::DontCare) );
         }
+        
+        template<typename ValueType>
+        void DFTState<ValueType>::setDependencySuccessful(size_t id) {
+            mStatus.set(mDft.failureIndex(id));
+        }
+
+        template<typename ValueType>
+        void DFTState<ValueType>::setDependencyUnsuccessful(size_t id) {
+            mStatus.set(mDft.failureIndex(id)+1);
+        }
 
         template<typename ValueType>
         void DFTState<ValueType>::beNoLongerFailable(size_t id) {
@@ -84,7 +113,8 @@ namespace storm {
             for (size_t i = 0; i < mDft.getDependencies().size(); ++i) {
                 std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mDft.getDependencies()[i]);
                 if (dependency->triggerEvent()->id() == id) {
-                    if (!hasFailed(dependency->dependentEvent()->id())) {
+                    if (getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
+                        assert(!isFailsafe(dependency->dependentEvent()->id()));
                         mFailableDependencies.push_back(dependency->id());
                         STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
                     }
@@ -99,10 +129,12 @@ namespace storm {
             STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
             if (nrFailableDependencies() > 0) {
                 // Consider failure due to dependency
+                assert(index < nrFailableDependencies());
                 std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(getDependencyId(index));
                 std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
                 mFailableDependencies.erase(mFailableDependencies.begin() + index);
                 setFailed(res.first->id());
+                setDependencySuccessful(dependency->id());
                 return res;
             } else {
                 // Consider "normal" failure
@@ -113,6 +145,14 @@ namespace storm {
                 return res;
             }
         }
+ 
+        template<typename ValueType>
+        void DFTState<ValueType>::letDependencyBeUnsuccessful(size_t index) {
+            assert(nrFailableDependencies() > 0 && index < nrFailableDependencies());
+            std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(getDependencyId(index));
+            mFailableDependencies.erase(mFailableDependencies.begin() + index);
+            setDependencyUnsuccessful(dependency->id());
+        }
 
         template<typename ValueType>
         void DFTState<ValueType>::activate(size_t repr) {

src/storage/dft/DFTState.h

@@ -22,6 +22,7 @@ namespace storm {
         class DFTState {
             friend struct std::hash<DFTState>;
         private:
+            // Status is bitvector where each element has two bits with the meaning according to DFTElementState
             storm::storage::BitVector mStatus;
             size_t mId;
             std::vector<size_t> mInactiveSpares;
@@ -35,6 +36,8 @@ namespace storm {
             DFTState(DFT<ValueType> const& dft, size_t id);
             
             DFTElementState getElementState(size_t id) const;
+            
+            DFTDependencyState getDependencyState(size_t id) const;
 
             int getElementStateInt(size_t id) const;
 
@@ -50,12 +53,22 @@ namespace storm {
             
             bool dontCare(size_t id) const;
             
+            bool dependencyTriggered(size_t id) const;
+
+            bool dependencySuccessful(size_t id) const;
+
+            bool dependencyUnsuccessful(size_t id) const;
+
             void setFailed(size_t id);
             
             void setFailsafe(size_t id);
             
             void setDontCare(size_t id);
             
+            void setDependencySuccessful(size_t id);
+
+            void setDependencyUnsuccessful(size_t id);
+
             void beNoLongerFailable(size_t id);
             
             void activate(size_t repr);
@@ -135,10 +148,16 @@ namespace storm {
 
             /**
              * Sets the next BE as failed
-             * @param smallestIndex Index in currentlyFailableBE of BE to fail
+             * @param index Index in currentlyFailableBE of BE to fail
              * @return Pair of BE which fails and flag indicating if the failure was due to functional dependencies
              */
-            std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> letNextBEFail(size_t smallestIndex = 0);
+            std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> letNextBEFail(size_t index = 0);
+            
+            /**
+             * Sets the dependency as unsuccesful meaning no BE will fail.
+             * @param index Index of dependency to fail.
+             */
+            void letDependencyBeUnsuccessful(size_t index = 0);
             
             std::string getCurrentlyFailableString() const {
                 std::stringstream stream;