Dependencies working

Former-commit-id: e262bfc5aa

src/builder/ExplicitDFTModelBuilder.cpp

@@ -40,7 +40,7 @@ namespace storm {
             STORM_LOG_DEBUG("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
             STORM_LOG_DEBUG("Exit rates: " << modelComponents.exitRates);
             STORM_LOG_DEBUG("Markovian states: " << modelComponents.markovianStates);
-            assert(modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount());
+            assert(!deterministic || modelComponents.transitionMatrix.getRowCount() == modelComponents.transitionMatrix.getColumnCount());
 
             // Build state labeling
             modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size());
@@ -100,24 +100,26 @@ namespace storm {
             // TODO Matthias: set Markovian states directly as bitvector?
             std::map<size_t, ValueType> outgoingTransitions;
             size_t rowOffset = 0; // Captures number of non-deterministic choices
-            ValueType exitRate;
             bool deterministic = true;
-            //TODO Matthias: Handle dependencies!
 
             while (!stateQueue.empty()) {
                 // Initialization
                 outgoingTransitions.clear();
-                exitRate = storm::utility::zero<ValueType>();
+                ValueType exitRate = storm::utility::zero<ValueType>();
 
                 // Consider next state
                 DFTStatePointer state = stateQueue.front();
                 stateQueue.pop();
 
+                bool hasDependencies = state->nrFailableDependencies() > 0;
+                deterministic &= !hasDependencies;
+                size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
                 size_t smallest = 0;
 
+                transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
+
                 // Add self loop for target states
                 if (mDft.hasFailed(state) || mDft.isFailsafe(state)) {
-                    transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
                     transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, state->getId(), storm::utility::one<ValueType>());
                     STORM_LOG_TRACE("Added self loop for " << state->getId());
                     exitRates.push_back(storm::utility::one<ValueType>());
@@ -130,18 +132,21 @@ namespace storm {
                 }
 
                 // Let BE fail
-                while (smallest < state->nrFailableBEs()) {
+                while (smallest < failableCount) {
                     STORM_LOG_TRACE("exploring from: " << mDft.getStateString(state));
 
                     // Construct new state as copy from original one
                     DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
                     std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType>>, bool> nextBEPair = newState->letNextBEFail(smallest++);
                     std::shared_ptr<storm::storage::DFTBE<ValueType>> nextBE = nextBEPair.first;
-                    if (nextBE == nullptr) {
-                        break;
-                    }
+                    assert(nextBE);
+                    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;
 
                     for (DFTGatePointer parent : nextBE->parents()) {
@@ -179,6 +184,11 @@ namespace storm {
                         stateQueue.push(newState);
                     }
 
+                    // Set transitions
+                    if (hasDependencies) {
+                        // Failure is due to dependency -> add non-deterministic choice
+                        transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), storm::utility::one<ValueType>());
+                    } else {
                         // Set failure rate according to usage
                         bool isUsed = true;
                         if (mDft.hasRepresentant(nextBE->id())) {
@@ -200,21 +210,27 @@ namespace storm {
                             STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate);
                         }
                         exitRate += rate;
+                    }
 
                 } // end while failing BE
 
-                // Add all transitions
-                transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
+                if (hasDependencies) {
+                    rowOffset--; // One increment to many
+                } else {
+                    // Add all probability transitions
                     for (auto it = outgoingTransitions.begin(); it != outgoingTransitions.end(); ++it)
                     {
                         ValueType probability = it->second / exitRate; // Transform rate to probability
                         transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability);
                     }
+
+                    markovianStates.push_back(state->getId());
+                }
                 exitRates.push_back(exitRate);
                 assert(exitRates.size()-1 == state->getId());
-                markovianStates.push_back(state->getId());
 
             } // end while queue
+            assert(!deterministic || rowOffset == 0);
             return deterministic;
         }
 

src/storage/dft/DFT.cpp

@@ -39,6 +39,8 @@ namespace storm {
                     mUsageIndex.insert(std::make_pair(elem->id(), stateIndex));
                     stateIndex += mUsageInfoBits;
 
+                } else if (elem->isDependency()) {
+                    mDependencies.push_back(elem->id());
                 }
             }
 

src/storage/dft/DFT.h

@@ -51,6 +51,7 @@ namespace storm {
             size_t mStateSize;
             std::map<size_t, size_t> mActivationIndex;
             std::map<size_t, std::vector<size_t>> mSpareModules;
+            std::vector<size_t> mDependencies;
             std::vector<size_t> mTopModule;
             std::vector<size_t> mIdToFailureIndex;
             std::map<size_t, size_t> mUsageIndex;
@@ -120,6 +121,10 @@ namespace storm {
                 }
             }
             
+            std::vector<size_t> const& getDependencies() const {
+                return mDependencies;
+            }
+
             void propagateActivation(DFTState<ValueType>& state, size_t representativeId) const {
                 state.activate(representativeId);
                 for(size_t id : module(representativeId)) {

src/storage/dft/DFTState.cpp

@@ -78,18 +78,42 @@ namespace storm {
             }
         }
 
+        template<typename ValueType>
+        bool DFTState<ValueType>::updateFailableDependencies(size_t id) {
+            assert(hasFailed(id));
+            for (size_t i = 0; i < mDft.getDependencies().size(); ++i) {
+                std::shared_ptr<DFTDependency<ValueType>> dependency = std::static_pointer_cast<DFTDependency<ValueType>>(mDft.getElement(mDft.getDependencies()[i]));
+                if (dependency->triggerEvent()->id() == id) {
+                    if (!hasFailed(dependency->dependentEvent()->id())) {
+                        mFailableDependencies.push_back(dependency->id());
+                        STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
+                    }
+                }
+            }
+            return nrFailableDependencies() > 0;
+        }
+
         template<typename ValueType>
         std::pair<std::shared_ptr<DFTBE<ValueType>>, bool> DFTState<ValueType>::letNextBEFail(size_t index)
         {
-            assert(index < mIsCurrentlyFailableBE.size());
             STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
-            // TODO set when implementing functional dependencies
-            bool dueToFdep = false;
-            std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), dueToFdep);
+            if (nrFailableDependencies() > 0) {
+                // Consider failure due to dependency
+                assert(index < nrFailableDependencies());
+                std::shared_ptr<DFTDependency<ValueType>> dependency = std::static_pointer_cast<DFTDependency<ValueType>>(mDft.getElement(mFailableDependencies[index]));
+                std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
+                mFailableDependencies.erase(mFailableDependencies.begin() + index);
+                setFailed(res.first->id());
+                return res;
+            } else {
+                // Consider "normal" failure
+                assert(index < nrFailableBEs());
+                std::pair<std::shared_ptr<DFTBE<ValueType>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
                 mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
                 setFailed(res.first->id());
                 return res;
             }
+        }
 
         template<typename ValueType>
         void DFTState<ValueType>::activate(size_t repr) {

src/storage/dft/DFTState.h

@@ -25,6 +25,7 @@ namespace storm {
             size_t mId;
             std::vector<size_t> mInactiveSpares;
             std::vector<size_t> mIsCurrentlyFailableBE;
+            std::vector<size_t> mFailableDependencies;
             std::vector<size_t> mUsedRepresentants;
             bool mValid = true;
             const DFT<ValueType>& mDft;
@@ -110,6 +111,17 @@ namespace storm {
                 return mIsCurrentlyFailableBE.size();
             }
 
+            size_t nrFailableDependencies() const {
+                return mFailableDependencies.size();
+            }
+
+            /**
+             * Sets all failable BEs due to dependencies from newly failed element
+             * @param id Id of the newly failed element
+             * @return true if failable dependent events exist
+             */
+            bool updateFailableDependencies(size_t id);
+
             /**
              * Sets the next BE as failed
              * @param smallestIndex Index in currentlyFailableBE of BE to fail
@@ -119,6 +131,19 @@ namespace storm {
             
             std::string getCurrentlyFailableString() const {
                 std::stringstream stream;
+                if (nrFailableDependencies() > 0) {
+                    auto it = mFailableDependencies.begin();
+                    stream << "{Dependencies: ";
+                    if (it != mFailableDependencies.end()) {
+                        stream << *it;
+                    }
+                    ++it;
+                    while(it != mFailableDependencies.end()) {
+                        stream << ", " << *it;
+                        ++it;
+                    }
+                    stream << "} ";
+                } else {
                     auto it = mIsCurrentlyFailableBE.begin();
                     stream << "{";
                     if(it != mIsCurrentlyFailableBE.end()) {
@@ -130,6 +155,7 @@ namespace storm {
                         ++it;
                     }
                     stream << "}";
+                }
                 return stream.str();
             }