post and pre SEQ elements for state space generation

Former-commit-id: 03e4408189

src/storage/dft/DFT.cpp

@@ -77,12 +77,22 @@ namespace storm {
             // TODO make recursive to use for nested subtrees
 
             DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount);
+            
+            // Generate Pre and Post info for restrictions
+            for(auto const& elem : mElements) {
+                if(!elem->isDependency() && !elem->isRestriction()) {
+                    generationInfo.setRestrictionPreElements(elem->id(), elem->seqRestrictionPres());
+                    generationInfo.setRestrictionPostElements(elem->id(), elem->seqRestrictionPosts());
+                }
+            }
+            
 
             // Perform DFS and insert all elements of subtree sequentially
             size_t stateIndex = 0;
             std::queue<size_t> visitQueue;
             storm::storage::BitVector visited(nrElements(), false);
 
+            // TODO make subfunction for this?
             if (symmetries.groups.empty()) {
                 // Perform DFS for whole tree
                 visitQueue.push(mTopLevelIndex);

src/storage/dft/DFTStateGenerationInfo.h

@@ -8,12 +8,16 @@ namespace storm {
             std::map<size_t, size_t> mSpareUsageIndex; // id spare -> index first bit in state
             std::map<size_t, size_t> mSpareActivationIndex; // id spare representative -> index in state
             std::vector<size_t> mIdToStateIndex; // id -> index first bit in state
-            std::map<size_t, size_t> mRestrictedItems;
+            std::map<size_t, std::vector<size_t>> mSeqRestrictionPreElements; // id -> list of restriction pre elements;
+            std::map<size_t, std::vector<size_t>> mSeqRestrictionPostElements; // id -> list of restriction post elements;
             std::vector<std::pair<size_t, std::vector<size_t>>> mSymmetries; // pair (lenght of symmetry group, vector indicating the starting points of the symmetry groups)
 
         public:
 
-            DFTStateGenerationInfo(size_t nrElements, size_t maxSpareChildCount) : mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), mIdToStateIndex(nrElements) {
+            DFTStateGenerationInfo(size_t nrElements, size_t maxSpareChildCount) :
+                mUsageInfoBits(storm::utility::math::uint64_log2(maxSpareChildCount) + 1), 
+                mIdToStateIndex(nrElements)
+            {
                 assert(maxSpareChildCount < pow(2, mUsageInfoBits));
             }
 
@@ -26,6 +30,14 @@ namespace storm {
                 mIdToStateIndex[id] = index;
             }
 
+            void setRestrictionPreElements(size_t id, std::vector<size_t> const& elems) {
+                mSeqRestrictionPreElements[id] = elems;
+            }
+            
+            void setRestrictionPostElements(size_t id, std::vector<size_t> const& elems) {
+                mSeqRestrictionPostElements[id] = elems;
+            }
+            
             void addSpareActivationIndex(size_t id, size_t index) {
                 mSpareActivationIndex[id] = index;
             }

src/storage/dft/elements/DFTElement.h

@@ -205,39 +205,55 @@ namespace storm {
                 return mOutgoingDependencies.size();
             }
             
-            /*std::set<DFTElement<ValueType>> restrictedItems() const {
-                std::set<DFTElement<ValueType>> result;
-                for(auto const& restr : mRestrictions) {
-                    bool foundThis = false;
-                    for(auto const& child : restr->children()) {
-                        if(!foundThis) {
-                            if(child->id() == mId) {
-                                foundThis = true;
-                            }
-                        } else if(result.count(child) == 0) {
-                            result.insert(child);
+            /**
+             * Obtains ids of elements which are the direct successor in the list of children of a restriction
+             * @return A vector of ids
+             */
+            std::vector<size_t> seqRestrictionPosts() const {
+                std::vector<size_t> res;
+                for (auto const& restr : mRestrictions) {
+                    if(!restr->isSeqEnforcer()) {
+                        continue;
+                    }
+                    auto it = restr->children().cbegin();
+                    for(; it != restr->children().cend(); ++it) {
+                        if((*it)->id() == mId) {
+                            break;
                         }
                     }
+                    assert(it != restr->children().cend());
+                    ++it;
+                    if(it != restr->children().cend()) {
+                        res.push_back((*it)->id());
+                    }
                 }
+                return res;
             }
             
-            std::set<DFTElement<ValueType>> restrictedItemsTC() const {
-                std::set<DFTElement<ValueType>> result;
-                for(auto const& restr : mRestrictions) {
-                    bool foundThis = false;
-                    for(auto const& child : restr->children()) {
-                        if(!foundThis) {
-                            if(child->id() == mId) {
-                                foundThis = true;
-                            }
-                        } else if(result.count(child) == 0) {
-                            result.insert(child);
-                            std::set<DFTElement<ValueType>> tmpRes = child->restrictedItemsTC();
-                            result.insert(tmpRes.begin(), tmpRes.end());
+            /**
+             * Obtains ids of elements which are the direct predecessor in the list of children of a restriction
+             * @return A vector of ids
+             */
+            std::vector<size_t> seqRestrictionPres() const {
+                std::vector<size_t> res;
+                for (auto const& restr : mRestrictions) {
+                    if(!restr->isSeqEnforcer()) {
+                        continue;
+                    }
+                    auto it = restr->children().cbegin();
+                    for(++it; it != restr->children().cend(); ++it) {
+                        if((*it)->id() == mId) {
+                            break;
                         }
                     }
+                    assert(it != restr->children().cend());
+                    if(it != restr->children().cbegin()) {
+                        --it;
+                        res.push_back((*it)->id());
+                    }
                 }
-            }*/
+                return res;
+            }
             
             DFTDependencyVector const& outgoingDependencies() const {
                 return mOutgoingDependencies;

src/storage/dft/elements/DFTRestriction.h

@@ -32,6 +32,10 @@ namespace storm {
             virtual bool isRestriction() const override {
                 return true;
             }
+            
+            virtual bool isSeqEnforcer() const {
+                return false;
+            }
 
 
             virtual std::string typestring() const = 0;
@@ -162,6 +166,12 @@ namespace storm {
                     DFTRestriction<ValueType>(id, name, children)
             {}
 
+            virtual bool isSeqEnforcer() const override {
+                return true;
+            }
+
+
+            
             void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 assert(queues.failurePropagationDone());
                 bool childOperationalBefore = false;