Ignore relevant events for Don't care propagation

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -58,11 +58,17 @@ namespace storm {
                 dft(dft),
                 stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
                 relevantEvents(relevantEvents),
-                generator(dft, *stateGenerationInfo, relevantEvents, mergeFailedStates),
+                generator(dft, *stateGenerationInfo, mergeFailedStates),
                 matrixBuilder(!generator.isDeterministicModel()),
                 stateStorage(dft.stateBitVectorSize()),
                 explorationQueue(1, 0, 0.9, false)
         {
+            // Set relevant events
+            this->dft.setRelevantEvents(this->relevantEvents);
+            // Mark top level element as relevant
+            this->dft.getElement(this->dft.getTopLevelIndex())->setRelevance(true);
+
+
             // Compute independent subtrees
             if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
                 // We only support this for approximation with top level element OR

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -8,17 +8,17 @@
 
 namespace storm {
     namespace generator {
-        
+
         template<typename ValueType, typename StateType>
-        DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::set<size_t> const& relevantEvents, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), relevantEvents(relevantEvents), mergeFailedStates(mergeFailedStates) {
+        DftNextStateGenerator<ValueType, StateType>::DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool mergeFailedStates) : mDft(dft), mStateGenerationInfo(stateGenerationInfo), state(nullptr), mergeFailedStates(mergeFailedStates) {
             deterministicModel = !mDft.canHaveNondeterminism();
         }
-        
+
         template<typename ValueType, typename StateType>
         bool DftNextStateGenerator<ValueType, StateType>::isDeterministicModel() const {
             return deterministicModel;
         }
-        
+
         template<typename ValueType, typename StateType>
         std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
             DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
@@ -42,7 +42,7 @@ namespace storm {
             // Store a pointer to the state itself, because we need to be able to access it when expanding it.
             this->state = state;
         }
-        
+
         template<typename ValueType, typename StateType>
         StateBehavior<ValueType, StateType> DftNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
             STORM_LOG_DEBUG("Explore state: " << mDft.getStateString(state));
@@ -146,8 +146,8 @@ namespace storm {
                     }
 
                     // Propagate dont cares
-                    // TODO: do not set DC for relevant events
-                    while (relevantEvents.empty() && !queues.dontCarePropagationDone()) {
+                    // Relevance is considered for each element independently
+                    while (!queues.dontCarePropagationDone()) {
                         DFTElementPointer next = queues.nextDontCarePropagation();
                         next->checkDontCareAnymore(*newState, queues);
                     }

src/storm-dft/generator/DftNextStateGenerator.h

@@ -24,7 +24,7 @@ namespace storm {
         public:
             typedef std::function<StateType (DFTStatePointer const&)> StateToIdCallback;
             
-            DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::set<size_t> const& relevantEvents, bool mergeFailedStates);
+            DftNextStateGenerator(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTStateGenerationInfo const& stateGenerationInfo, bool mergeFailedStates);
                         
             bool isDeterministicModel() const;
             std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback);
@@ -55,9 +55,6 @@ namespace storm {
             // Current state
             DFTStatePointer state;
 
-            // List with ids of relevant events which should be observed.
-            std::set<size_t> const& relevantEvents;
-
             // Flag indication if all failed states should be merged into one.
             bool mergeFailedStates = true;
 

src/storm-dft/storage/dft/DFT.cpp

@@ -863,6 +863,17 @@ namespace storm {
             return (*iter)->id();
         }
 
+        template<typename ValueType>
+        void DFT<ValueType>::setRelevantEvents(std::set<size_t> const& relevantEvents) const {
+            for (auto const& elem : mElements) {
+                if (relevantEvents.find(elem->id()) != relevantEvents.end()) {
+                    elem->setRelevance(true);
+                } else {
+                    elem->setRelevance(false);
+                }
+            }
+        }
+
         template<typename ValueType>
         void DFT<ValueType>::writeStatsToStream(std::ostream& stream) const {
             // Count individual types of elements

src/storm-dft/storage/dft/DFT.h

@@ -318,6 +318,12 @@ namespace storm {
              */
             size_t getIndex(std::string const& name) const;
 
+            /*!
+             * Set the relevance flag for all elements according to the given relevant events.
+             * @param relevantEvents All elements which should be to relevant. All elements not occuring are set to irrelevant.
+             */
+            void setRelevantEvents(std::set<size_t> const& relevantEvents) const;
+
         private:
             std::tuple<std::vector<size_t>, std::vector<size_t>, std::vector<size_t>> getSortedParentAndDependencyIds(size_t index) const;
             

src/storm-dft/storage/dft/elements/DFTElement.cpp

@@ -9,6 +9,11 @@ namespace storm {
 
         template<typename ValueType>
         bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
+            if (this->isRelevant()) {
+                // Relevant events are ignored for Don't Care propagation
+                return false;
+            }
+
             if (state.dontCare(mId)) {
                 return false;
             }

src/storm-dft/storage/dft/elements/DFTElement.h

@@ -51,7 +51,7 @@ namespace storm {
              * @param id Id.
              * @param name Name.
              */
-            DFTElement(size_t id, std::string const& name) : mId(id), mName(name) {
+            DFTElement(size_t id, std::string const& name) : mId(id), mName(name), mRank(-1), mRelevant(false) {
                 // Intentionally left empty.
             }
 
@@ -117,6 +117,23 @@ namespace storm {
                 this->mRank = rank;
             }
 
+            /*!
+             * Get whether the element is relevant.
+             * Relevant elements are for example not set to Don't Care and their status is stored as a label in the generated Markov Chain.
+             * @return True iff the element is relevant.
+             */
+            virtual bool isRelevant() const {
+                return mRelevant;
+            }
+
+            /*!
+             * Set the relevancy of the element.
+             * @param relevant If true, the element is relevant.
+             */
+            virtual void setRelevance(bool relevant) const {
+                this->mRelevant = relevant;
+            }
+
             /*!
              * Checks whether the element is a basic element.
              * @return True iff element is a BE.
@@ -416,10 +433,11 @@ namespace storm {
         protected:
             std::size_t mId;
             std::string mName;
-            std::size_t mRank = -1;
+            std::size_t mRank;
             DFTGateVector mParents;
             DFTDependencyVector mOutgoingDependencies;
             DFTRestrictionVector mRestrictions;
+            mutable bool mRelevant; // Must be mutable to allow changes later on. TODO: avoid mutable
         };