Small changes

Former-commit-id: aa36b0ae30

src/storage/dft/DFT.cpp

@@ -79,10 +79,6 @@ namespace storm {
 
         template<typename ValueType>
         DFTStateGenerationInfo DFT<ValueType>::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const {
-            // Use symmetry
-            // Collect all elements in the first subtree
-            // TODO make recursive to use for nested subtrees
-
             DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount);
             
             // Generate Pre and Post info for restrictions
@@ -93,18 +89,16 @@ namespace storm {
                 }
             }
 
-
-            // 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);
                 stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
             } else {
+                // Generate information according to symmetries
                 for (size_t symmetryIndex : symmetries.sortedSymmetries) {
                     assert(!visited[symmetryIndex]);
                     auto const& symmetryGroup = symmetries.groups.at(symmetryIndex);
@@ -430,7 +424,7 @@ namespace storm {
                 stream << "[" << elem->id() << "]";
                 stream << elem->toString();
                 if (elem->isDependency()) {
-                    stream << "\t** " << storm::storage::toChar(state->getDependencyState(elem->id()));
+                    stream << "\t** " << storm::storage::toChar(state->getDependencyState(elem->id())) << "[dep]";
                 } else {
                     stream << "\t** " << storm::storage::toChar(state->getElementState(elem->id()));
                     if(elem->isSpareGate()) {
@@ -446,9 +440,8 @@ namespace storm {
             return stream.str();
         }
         
-        // TODO rewrite to only use bitvector and id
         template<typename ValueType>
-        std::string DFT<ValueType>::getStateString(DFTStatePointer const& state) const{
+        std::string DFT<ValueType>::getStateString(DFTStatePointer const& state) const {
             std::stringstream stream;
             stream << "(" << state->getId() << ") ";
             for (auto const& elem : mElements) {
@@ -469,6 +462,37 @@ namespace storm {
             return stream.str();
         }        
 
+        template<typename ValueType>
+        std::string DFT<ValueType>::getStateString(storm::storage::BitVector const& status, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) const {
+            std::stringstream stream;
+            stream << "(" << id << ") ";
+            for (auto const& elem : mElements) {
+                size_t elemIndex = stateGenerationInfo.getStateIndex(elem->id());
+                int elementState = DFTState<ValueType>::getElementStateInt(status, elemIndex);
+                if (elem->isDependency()) {
+                    stream << storm::storage::toChar(static_cast<DFTDependencyState>(elementState)) << "[dep]";
+                } else {
+                    stream << storm::storage::toChar(static_cast<DFTElementState>(elementState));
+                    if(elem->isSpareGate()) {
+                        stream << "[";
+                        size_t nrUsedChild = status.getAsInt(stateGenerationInfo.getSpareUsageIndex(elem->id()), stateGenerationInfo.usageInfoBits());
+                        size_t useId;
+                        if (nrUsedChild == getMaxSpareChildCount()) {
+                            useId = elem->id();
+                        } else {
+                            useId = getChild(elem->id(), nrUsedChild);
+                        }
+                        bool isActive = status[stateGenerationInfo.getSpareActivationIndex(useId)];
+                        if(useId == elem->id() || isActive) {
+                            stream << "actively ";
+                        }
+                        stream << "using " << useId << "]";
+                    }
+                }
+            }
+            return stream.str();
+        }
+        
         template<typename ValueType>
         size_t DFT<ValueType>::getChild(size_t spareId, size_t nrUsedChild) const {
             assert(mElements[spareId]->isSpareGate());

src/storage/dft/DFT.h

@@ -130,8 +130,11 @@ namespace storm {
             std::vector<size_t> nonColdBEs() const {
                 std::vector<size_t> result;
                 for(DFTElementPointer elem : mElements) {
-                    if(elem->isBasicElement() && std::static_pointer_cast<DFTBE<ValueType>>(elem)->canFail() && !elem->isColdBasicElement()) {
-                        result.push_back(elem->id());
+                    if(elem->isBasicElement()) {
+                        std::shared_ptr<DFTBE<ValueType>> be = std::static_pointer_cast<DFTBE<ValueType>>(elem);
+                        if (be->canFail() && !be->isColdBasicElement()) {
+                            result.push_back(be->id());
+                        }
                     }
                 }
                 return result;
@@ -246,6 +249,8 @@ namespace storm {
 
             std::string getStateString(DFTStatePointer const& state) const;
 
+            std::string getStateString(storm::storage::BitVector const& status, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) const;
+
             std::vector<size_t> getIndependentSubDftRoots(size_t index) const;
 
             DFTColouring<ValueType> colourDFT() const;

src/storage/dft/DFTState.cpp

@@ -68,6 +68,11 @@ namespace storm {
             return mStatus.getAsInt(mStateGenerationInfo.getStateIndex(id), 2);
         }
         
+        template<typename ValueType>
+        int DFTState<ValueType>::getElementStateInt(storm::storage::BitVector const& state, size_t indexId) {
+            return state.getAsInt(indexId, 2);
+        }
+
         template<typename ValueType>
         size_t DFTState<ValueType>::getId() const {
             return mId;
@@ -246,8 +251,11 @@ namespace storm {
                 activate(representativeId);
             }
             for(size_t elem : mDft.module(representativeId)) {
-                if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem) && mDft.getBasicElement(elem)->canFail()) {
+                if(mDft.isBasicElement(elem) && isOperational(elem)) {
+                    std::shared_ptr<const DFTBE<ValueType>> be = mDft.getBasicElement(elem);
+                    if (be->isColdBasicElement() && be->canFail()) {
                         mIsCurrentlyFailableBE.push_back(elem);
+                    }
                 } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {
                     propagateActivation(uses(elem));
                 }

src/storage/dft/DFTState.h

@@ -47,6 +47,8 @@ namespace storm {
 
             int getElementStateInt(size_t id) const;
 
+            static int getElementStateInt(storm::storage::BitVector const& state, size_t indexId);
+            
             size_t getId() const;
 
             void setId(size_t id);

src/storage/dft/elements/DFTBE.h

@@ -67,11 +67,11 @@ namespace storm {
                 return stream.str();
             }
             
-            bool isBasicElement() const override{
+            bool isBasicElement() const override {
                 return true;
             }
             
-            bool isColdBasicElement() const override{
+            bool isColdBasicElement() const {
                 return storm::utility::isZero(mPassiveFailureRate);
             }
             

src/storage/dft/elements/DFTElement.h

@@ -93,10 +93,6 @@ namespace storm {
                 return false;
             }
             
-            virtual bool isColdBasicElement() const {
-                return false;
-            }
-
             /**
              * Returns true if the element is a spare gate
              */