towards state space construction for SEQs

Former-commit-id: 890ce8bd85

src/storage/dft/DFT.h

@@ -10,6 +10,7 @@
 #include <boost/iterator/counting_iterator.hpp>
 
 #include "DFTElements.h"
+#include "elements/DFTRestriction.h"
 #include "../BitVector.h"
 #include "SymmetricUnits.h"
 #include "../../utility/math.h"

src/storage/dft/DFTElements.cpp

@@ -52,7 +52,7 @@ namespace storm {
 
         template<typename ValueType>
         std::vector<size_t> DFTElement<ValueType>::independentSubDft() const {
-            std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl;
+            //std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl;
             std::vector<size_t> res;
             res.push_back(this->id());
             return res;

src/storage/dft/DFTElements.h

@@ -159,6 +159,18 @@ namespace storm {
             DFTGateVector const& parents() const {
                 return mParents;
             }
+            
+            bool hasRestrictions() const {
+                return !mRestrictions.empty();
+            }
+            
+            size_t nrRestrictions() const {
+                return mRestrictions.size();
+            }
+            
+            DFTRestrictionVector const& restrictions() const {
+                return mRestrictions;
+            }
 
             std::vector<size_t> parentIds() const {
                 std::vector<size_t> res;
@@ -371,7 +383,11 @@ namespace storm {
                         queues.propagateFailure(parent);
                     }
                 }
+                for(std::shared_ptr<DFTRestriction<ValueType>> restr : this->mRestrictions) {
+                    queues.checkRestrictionLater(restr);
+                }
                 state.setFailed(this->mId);
+                // TODO can this be moved towards DFTSpare?
                 if (this->isSpareGate()) {
                     this->finalizeSpare(state);
                 }

src/storage/dft/DFTStateSpaceGenerationQueues.h

@@ -15,6 +15,8 @@ namespace storm {
         class DFTGate;
         template<typename ValueType>
         class DFTElement;
+        template<typename ValueType>
+        class DFTRestriction;
 
 
         template<typename ValueType>
@@ -24,11 +26,14 @@ namespace storm {
             using DFTElementVector = std::vector<DFTElementPointer>;
             using DFTGatePointer = std::shared_ptr<DFTGate<ValueType>>;
             using DFTGateVector = std::vector<DFTGatePointer>;
+            using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
+            using DFTRestrictionVector = std::vector<DFTRestrictionPointer>;
 
             std::priority_queue<DFTGatePointer, DFTGateVector, OrderElementsByRank<ValueType>> failurePropagation;
             DFTGateVector failsafePropagation;
             DFTElementVector dontcarePropagation;
             DFTElementVector activatePropagation;
+            DFTRestrictionVector restrictionChecks;
 
         public:
             void propagateFailure(DFTGatePointer const& elem) {
@@ -45,6 +50,21 @@ namespace storm {
                 return next;
             }
             
+            bool restrictionChecksDone() const {
+                return restrictionChecks.empty();
+            }
+            
+            DFTRestrictionPointer nextRestrictionCheck() {
+                assert(!restrictionChecksDone());
+                DFTRestrictionPointer next = restrictionChecks.back();
+                restrictionChecks.pop_back();
+                return next;
+            }
+            
+            void checkRestrictionLater(DFTRestrictionPointer const& restr) {
+                restrictionChecks.push_back(restr);
+            }
+            
             bool failsafePropagationDone() const {
                 return failsafePropagation.empty();
             }

src/storage/dft/elements/DFTRestriction.h

@@ -127,7 +127,7 @@ namespace storm {
         protected:
 
             void fail(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
-                //state.restrictionViolated(this->mId);
+                state.markAsInvalid();
             }
 
             void failsafe(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
@@ -187,7 +187,7 @@ namespace storm {
             }
 
             void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
-                assert(this->hasFailsafeChild(state));
+                
 
             }