Some refactoring

Former-commit-id: c5954a71a2

src/builder/ExplicitDFTModelBuilder.cpp

@@ -0,0 +1,72 @@
+#include "src/builder/ExplicitDFTModelBuilder.h"
+
+namespace storm {
+    namespace builder {
+
+        void ExplicitDFTModelBuilder::exploreStateSuccessors(storm::storage::DFTState const &state) {
+            size_t smallest = 0;
+
+            while(smallest < state.nrFailableBEs()) {
+                //std::cout << "exploring from: " << mDft.getStateString(state) << std::endl;
+
+                storm::storage::DFTState newState(state);
+                std::pair<std::shared_ptr<storm::storage::DFTBE<double>>, bool> nextBE = newState.letNextBEFail(smallest++);
+                if(nextBE.first == nullptr) {
+                    //std::cout << "break" << std::endl;
+                    break;
+
+                }
+                //std::cout << "with the failure of: " << nextBE.first->name() << " [" << nextBE.first->id() << "]" << std::endl;
+
+                storm::storage::DFTStateSpaceGenerationQueues queues;
+
+                for(std::shared_ptr<storm::storage::DFTGate> parent : nextBE.first->parents()) {
+                    if(newState.isOperational(parent->id())) {
+                        queues.propagateFailure(parent);
+                    }
+                }
+
+                while(!queues.failurePropagationDone()) {
+                    std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailurePropagation();
+                    next->checkFails(newState, queues);
+                }
+
+                while(!queues.failsafePropagationDone()) {
+                    std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailsafePropagation();
+                    next->checkFailsafe(newState, queues);
+                }
+
+                while(!queues.dontCarePropagationDone()) {
+                    std::shared_ptr<storm::storage::DFTElement> next = queues.nextDontCarePropagation();
+                    next->checkDontCareAnymore(newState, queues);
+                }
+
+                auto it = mStates.find(newState);
+                if (it == mStates.end()) {
+                    // New state
+                    newState.setId(newIndex++);
+                    mStates.insert(newState);
+                    //std::cout << "New state " << mDft.getStateString(newState) << std::endl;
+
+                    // Recursive call
+                    if(!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) {
+                        exploreStateSuccessors(newState);
+                    } else {
+                        if (mDft.hasFailed(newState)) {
+                            //std::cout << "Failed " << mDft.getStateString(newState) << std::endl;
+                        } else {
+                            assert(mDft.isFailsafe(newState));
+                            //std::cout << "Failsafe" << mDft.getStateString(newState) << std::endl;
+                        }
+                    }
+                } else {
+                    // State already exists
+                    //std::cout << "State " << mDft.getStateString(*it) << " already exists" << std::endl;
+                }
+            }
+        }
+
+    } // namespace builder
+} // namespace storm
+
+

src/builder/ExplicitDFTModelBuilder.h

@@ -3,91 +3,34 @@
 
 #include "../storage/dft/DFT.h"
 
+#include <unordered_set>
+
 namespace storm {
     namespace builder {
         class ExplicitDFTModelBuilder {
-            storm::storage::DFT const& mDft;
-            std::unordered_map<storm::storage::DFTState, size_t> mStateIndices;
+            storm::storage::DFT const &mDft;
+            std::unordered_set<storm::storage::DFTState> mStates;
             size_t newIndex = 0;
             //std::stack<std::shared_ptr<storm::storage::DFTState>> mStack;
-            
-        public:
-            ExplicitDFTModelBuilder(storm::storage::DFT const& dft) : mDft(dft)
-            {
-                
-            }
-            
-            
-            void exploreStateSuccessors(storm::storage::DFTState const& state) {
-                size_t smallest = 0; 
-                
-                while(smallest < state.nrFailableBEs()) {
-                    //std::cout << "exploring from :" << std::endl;
-                    //mDft.printElementsWithState(state);
-                    //std::cout << "***************" << std::endl;
-                    storm::storage::DFTState newState(state);
-                    std::pair<std::shared_ptr<storm::storage::DFTBE<double>>, bool> nextBE = newState.letNextBEFail(smallest++);
-                    if(nextBE.first == nullptr) {
-                        //std::cout << "break" << std::endl;
-                        break;
-                        
-                    }
-                    //std::cout << "with the failure of: " << nextBE.first->name() << std::endl;
-                        
-                    storm::storage::DFTStateSpaceGenerationQueues queues;
-                    for(std::shared_ptr<storm::storage::DFTGate> parent : nextBE.first->parents()) {
-                       if(newState.isOperational(parent->id())) {
-                            queues.propagateFailure(parent);
-                        }
-                    }
-
-
 
-                    while(!queues.failurePropagationDone()) {
-                        std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailurePropagation();
-                        next->checkFails(newState, queues);
-                    }
-                    
-                    while(!queues.failsafePropagationDone()) {
-                        std::shared_ptr<storm::storage::DFTGate> next = queues.nextFailsafePropagation();
-                        next->checkFailsafe(newState, queues);
-                    }
-                    
-                    while(!queues.dontCarePropagationDone()) {
-                        std::shared_ptr<storm::storage::DFTElement> next = queues.nextDontCarePropagation();
-                        next->checkDontCareAnymore(newState, queues);
-                    }
-                    
-                    
-                    
-                    if(!mDft.hasFailed(newState) && !mDft.isFailsafe(newState)) {
-                        auto it = mStateIndices.find(newState);
-                        if(it == mStateIndices.end()) {
-                            exploreStateSuccessors(newState);
-                            mStateIndices.insert(std::make_pair(newState, newIndex++));
-                            if(newIndex % 16384 == 0) std::cout << newIndex << std::endl;
-                        } 
-                        
-                    }
-                    else {
-                        //std::cout << "done." << std::endl;
-                    }
+        public:
+            ExplicitDFTModelBuilder(storm::storage::DFT const &dft) : mDft(dft) {
 
-                    
-                
-                }
             }
-            
-            void buildCtmc() {
-                storm::storage::DFTState state(mDft);
+
+            void buildCTMC() {
+                // Construct starting start
+                storm::storage::DFTState state(mDft, newIndex++);
+                mStates.insert(state);
+                // Begin model generation
                 exploreStateSuccessors(state);
-                std::cout << mStateIndices.size() << std::endl;
+                std::cout << "Generated " << mStates.size() << " states" << std::endl;
             }
-            
+
+        private:
+            void exploreStateSuccessors(storm::storage::DFTState const &state);
         };
     }
 }
 
-
-#endif	/* EXPLICITDFTMODELBUILDER_H */
-
+#endif	/* EXPLICITDFTMODELBUILDER_H */

src/storage/dft/DFT.cpp

@@ -114,9 +114,22 @@ namespace storm {
                     os << " using " << state.uses(elem->id());
                 } 
                 std::cout << std::endl;
+            }
+        }
 
-
+        std::string DFT::getStateString(DFTState const& state) const{
+            std::stringstream stream;
+            stream << "(" << state.getId() << ") ";
+            for (auto const& elem : mElements) {
+                stream << state.getElementStateInt(elem->id());
+                /*if(elem->isSpareGate()) {
+                    if(state.isActiveSpare(elem->id())) {
+                        os << " actively";
+                    }
+                    os << " using " << state.uses(elem->id());
+                }*/
             }
+            return stream.str();
         }
     }
 }

src/storage/dft/DFT.h

@@ -151,7 +151,9 @@ namespace storm {
             
             void printSpareModules(std::ostream& os = std::cout) const;
             
-            void printElementsWithState(DFTState const& state, std::ostream& os = std::cout) const; 
+            void printElementsWithState(DFTState const& state, std::ostream& os = std::cout) const;
+
+            std::string getStateString(DFTState const& state) const;
             
         private:
             bool elementIndicesCorrect() const {

src/storage/dft/DFTState.cpp

@@ -5,7 +5,7 @@
 namespace storm {
     namespace storage {
         
-        DFTState::DFTState(DFT const& dft) : mStatus(dft.stateSize()), mDft(dft)  {
+        DFTState::DFTState(DFT const& dft, size_t id) : mStatus(dft.stateSize()), mDft(dft), mId(id)  {
             mInactiveSpares = dft.getSpareIndices();
             dft.initializeUses(*this);
             dft.initializeActivation(*this);
@@ -15,7 +15,19 @@ namespace storm {
         }
         
         DFTElementState DFTState::getElementState(size_t id) const {
-            return static_cast<DFTElementState>(mStatus.getAsInt(mDft.failureIndex(id), 2));
+            return static_cast<DFTElementState>(getElementStateInt(id));
+        }
+
+        int DFTState::getElementStateInt(size_t id) const {
+            return mStatus.getAsInt(mDft.failureIndex(id), 2);
+        }
+
+        size_t DFTState::getId() const {
+            return mId;
+        }
+
+        void DFTState::setId(size_t id) {
+            mId = id;
         }
 
         bool DFTState::isOperational(size_t id) const {
@@ -58,7 +70,7 @@ namespace storm {
         {
             assert(index < mIsCurrentlyFailableBE.size());
             //std::cout << "currently failable: ";
-            //printCurrentlyFailable(std::cout);
+            //printCurrentlyFailable();
             std::pair<std::shared_ptr<DFTBE<double>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
             mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
             setFailed(res.first->id());
@@ -98,8 +110,6 @@ namespace storm {
             
         }
         
-        
-        
         void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) {
             mStatus.setFromInt(usageIndex, mDft.usageInfoBits(), child);
             mUsedRepresentants.push_back(child);
@@ -121,5 +131,6 @@ namespace storm {
             }
             return false;
         }
+
     }
 }

src/storage/dft/DFTState.h

@@ -4,6 +4,7 @@
 #include "../BitVector.h"
 #include "DFTElementState.h"
 
+#include <iostream>
 
 namespace storm {
     namespace storage {
@@ -18,6 +19,7 @@ namespace storm {
             friend struct std::hash<DFTState>;
         private:
             storm::storage::BitVector mStatus;
+            size_t mId;
             std::vector<size_t> mInactiveSpares;
             std::vector<size_t> mIsCurrentlyFailableBE;
             std::vector<size_t> mUsedRepresentants;
@@ -25,9 +27,15 @@ namespace storm {
             const DFT& mDft;
             
         public:
-            DFTState(DFT const& dft);
+            DFTState(DFT const& dft, size_t id);
             
             DFTElementState getElementState(size_t id) const;
+
+            int getElementStateInt(size_t id) const;
+
+            size_t getId() const;
+
+            void setId(size_t id);
             
             bool isOperational(size_t id) const;
             
@@ -103,7 +111,7 @@ namespace storm {
             
             std::pair<std::shared_ptr<DFTBE<double>>, bool> letNextBEFail(size_t smallestIndex = 0);
             
-            void printCurrentlyFailable(std::ostream& os) {
+            void printCurrentlyFailable(std::ostream& os = std::cout) {
                 auto it = mIsCurrentlyFailableBE.begin();
                 os << "{";
                 if(it != mIsCurrentlyFailableBE.end()) {
@@ -116,7 +124,7 @@ namespace storm {
                 }
                 os << "}" << std::endl;
             }
-            
+
             friend bool operator==(DFTState const& a, DFTState const& b) {
                 return a.mStatus == b.mStatus;
             }

src/storm-dyftee.cpp

@@ -22,7 +22,7 @@ int main(int argc, char** argv) {
 
     std::cout << "Building CTMC..." << std::endl;
     storm::builder::ExplicitDFTModelBuilder builder(dft);
-    builder.buildCtmc();
+    builder.buildCTMC();
     std::cout << "Built CTMC" << std::endl;
 
     //std::cout << "Model checking..." << std::endl;