Merge branch 'monolithic-dft' of https://sselab.de/lab9/private/git/storm into monolithic-dft

Former-commit-id: eeded60a67

examples/dft/pdep_symmetry.dft

@@ -0,0 +1,11 @@
+toplevel "A";
+"A" and "B" "B'";
+"B" and "C" "D" "PDEP";
+"B'" and "C'" "D'" "PDEP'";
+"PDEP" pdep=0.6 "B" "C";
+"PDEP'" pdep=0.6 "B'" "C'";
+"C" lambda=0.5 dorm=0;
+"D" lambda=0.5 dorm=0;
+"C'" lambda=0.5 dorm=0;
+"D'" lambda=0.5 dorm=0;
+

examples/dft/spare_symmetry.dft

@@ -0,0 +1,9 @@
+toplevel "A";
+"A" and "B" "C";
+"B" wsp "I" "J";
+"C" wsp "K" "L";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"K" lambda=0.5 dorm=0.3;
+"L" lambda=0.5 dorm=0.3;
+

src/storage/dft/DFT.cpp

@@ -11,7 +11,7 @@ namespace storm {
     namespace storage {
 
         template<typename ValueType>
-        DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()) {
+        DFT<ValueType>::DFT(DFTElementVector const& elements, DFTElementPointer const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) {
             assert(elementIndicesCorrect());
             size_t nrRepresentatives = 0;
             
@@ -25,6 +25,7 @@ namespace storm {
                 else if (elem->isSpareGate()) {
                     ++mNrOfSpares;
                     bool firstChild = true;
+                    mMaxSpareChildCount = std::max(mMaxSpareChildCount, std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children().size());
                     for(auto const& spareReprs : std::static_pointer_cast<DFTSpare<ValueType>>(elem)->children()) {
                         std::set<size_t> module = {spareReprs->id()};
                         spareReprs->extendSpareModule(module);
@@ -63,7 +64,9 @@ namespace storm {
             }
             mTopModule = std::vector<size_t>(topModuleSet.begin(), topModuleSet.end());
             
-            size_t usageInfoBits = mElements.size() > 1 ? storm::utility::math::uint64_log2(mElements.size()-1) + 1 : 1;
+            //Reserve space for failed spares
+            ++mMaxSpareChildCount;
+            size_t usageInfoBits = storm::utility::math::uint64_log2(mMaxSpareChildCount) + 1;
             mStateVectorSize = nrElements() * 2 + mNrOfSpares * usageInfoBits + nrRepresentatives;
         }
 
@@ -73,7 +76,7 @@ namespace storm {
             // Collect all elements in the first subtree
             // TODO make recursive to use for nested subtrees
 
-            DFTStateGenerationInfo generationInfo(nrElements());
+            DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount);
 
             // Perform DFS and insert all elements of subtree sequentially
             size_t stateIndex = 0;
@@ -296,7 +299,25 @@ namespace storm {
             }
             return stream.str();
         }
-
+        
+        template<typename ValueType>
+        size_t DFT<ValueType>::getChild(size_t spareId, size_t nrUsedChild) const {
+            assert(mElements[spareId]->isSpareGate());
+            return getGate(spareId)->children()[nrUsedChild]->id();
+        }
+        
+        template<typename ValueType>
+        size_t DFT<ValueType>::getNrChild(size_t spareId, size_t childId) const {
+            assert(mElements[spareId]->isSpareGate());
+            DFTElementVector children = getGate(spareId)->children();
+            for (size_t nrChild = 0; nrChild < children.size(); ++nrChild) {
+                if (children[nrChild]->id() == childId) {
+                    return nrChild;
+                }
+            }
+            assert(false);
+        }
+        
         template <typename ValueType>
         std::vector<size_t> DFT<ValueType>::getIndependentSubDftRoots(size_t index) const {
             auto elem = getElement(index);

src/storage/dft/DFT.h

@@ -45,7 +45,8 @@ namespace storm {
             
         public:
             
-            DFTStateGenerationInfo(size_t nrElements) : mUsageInfoBits(nrElements > 1 ? storm::utility::math::uint64_log2(nrElements-1) + 1 : 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));
             }
 
             size_t usageInfoBits() const {
@@ -80,8 +81,8 @@ namespace storm {
                 return mSpareActivationIndex.at(id);
             }
             
-            size_t addSymmetry(size_t lenght, std::vector<size_t>& startingIndices) {
-                mSymmetries.push_back(std::make_pair(lenght, startingIndices));
+            void addSymmetry(size_t length, std::vector<size_t>& startingIndices) {
+                mSymmetries.push_back(std::make_pair(length, startingIndices));
             }
             
             size_t getSymmetrySize() const {
@@ -144,6 +145,7 @@ namespace storm {
             size_t mNrOfSpares;
             size_t mTopLevelIndex;
             size_t mStateVectorSize;
+            size_t mMaxSpareChildCount;
             std::map<size_t, std::vector<size_t>> mSpareModules;
             std::vector<size_t> mDependencies;
             std::vector<size_t> mTopModule;
@@ -175,6 +177,10 @@ namespace storm {
                 return mTopLevelIndex;
             }
             
+            size_t getMaxSpareChildCount() const {
+                return mMaxSpareChildCount;
+            }
+            
             std::vector<size_t> getSpareIndices() const {
                 std::vector<size_t> indices;
                 for(auto const& elem : mElements) {
@@ -288,6 +294,10 @@ namespace storm {
                 return storm::storage::DFTState<ValueType>::isFailsafe(state, stateGenerationInfo.getStateIndex(mTopLevelIndex));
             }
             
+            size_t getChild(size_t spareId, size_t nrUsedChild) const;
+            
+            size_t getNrChild(size_t spareId, size_t childId) const;
+            
             std::string getElementsString() const;
 
             std::string getInfoString() const;

src/storage/dft/DFTElements.h

@@ -412,12 +412,12 @@ namespace storm {
             }
 
             /**
-             * Finish failed/failsafe spare gate by activating the children and setting the useIndex to the spare id.
+             * Finish failed/failsafe spare gate by activating the children and setting the useIndex to the maximum value.
              * This prevents multiple fail states with different usages or activations.
              * @param state The current state.
              */
             void finalizeSpare(DFTState<ValueType>& state) const {
-                state.setUses(this->mId, this->mId);
+                state.finalizeUses(this->mId);
                 for (auto child : this->children()) {
                     if (!state.isActive(child->id())) {
                         state.activate(child->id());

src/storage/dft/DFTState.cpp

@@ -201,7 +201,12 @@ namespace storm {
 
         template<typename ValueType>
         uint_fast64_t DFTState<ValueType>::uses(size_t id) const {
-            return extractUses(mStateGenerationInfo.getSpareUsageIndex(id));
+            size_t nrUsedChild = extractUses(mStateGenerationInfo.getSpareUsageIndex(id));
+            if (nrUsedChild == mDft.getMaxSpareChildCount()) {
+                return id;
+            } else {
+                return mDft.getChild(id, nrUsedChild);
+            }
         }
 
         template<typename ValueType>
@@ -217,9 +222,15 @@ namespace storm {
 
         template<typename ValueType>
         void DFTState<ValueType>::setUses(size_t spareId, size_t child) {
-            mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), child);
+            mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getNrChild(spareId, child));
             mUsedRepresentants.push_back(child);
         }
+        
+        template<typename ValueType>
+        void DFTState<ValueType>::finalizeUses(size_t spareId) {
+            assert(hasFailed(spareId));
+            mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getMaxSpareChildCount());
+        }
 
         template<typename ValueType>
         bool DFTState<ValueType>::claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children) {

src/storage/dft/DFTState.h

@@ -93,9 +93,10 @@ namespace storm {
             }
            
             /**
-             * This method gets the usage information for a spare
+             * This method returns the id of the used child for a spare. If no element is used, it returns the given id.
              * @param id Id of the spare
-             * @return The child that currently is used.
+             * @return The id of the currently used child or if non is used (because of spare failure) the id of
+             * the spare.
              */
             uint_fast64_t uses(size_t id) const;
             
@@ -120,6 +121,12 @@ namespace storm {
              */
             void setUses(size_t spareId, size_t child);
             
+            /**
+             * Sets the use for the spare to a default value to gain consistent states after failures.
+             * @param spareId Id of the spare
+             */
+            void finalizeUses(size_t spareId);
+            
             bool claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children);
             
             bool hasOutgoingEdges() const {

src/storage/dft/elements/DFTRestriction.h

@@ -183,7 +183,7 @@ namespace storm {
 
             }
             
-            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) {
+            bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 
             }
 

src/storm-dyftee.cpp

@@ -32,7 +32,6 @@ void analyzeDFT(std::string filename, std::string property, bool symred = false)
     std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
     storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
     if(symred) {
-        std::cout << dft.getElementsString() << std::endl;
         auto colouring = dft.colourDFT();
         symmetries = dft.findSymmetries(colouring);
         std::cout << "Symmetries: " << symmetries << std::endl;