First version of the monolithic state space generation

Former-commit-id: fab8f6e356

src/builder/ExplicitDFTModelBuilder.h

@@ -0,0 +1,93 @@
+#ifndef EXPLICITDFTMODELBUILDER_H
+#define	EXPLICITDFTMODELBUILDER_H
+
+#include "../storage/dft/DFT.h"
+
+namespace storm {
+    namespace builder {
+        class ExplicitDFTModelBuilder {
+            storm::storage::DFT const& mDft;
+            std::unordered_map<storm::storage::DFTState, size_t> mStateIndices;
+            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;
+                    }
+
+                    
+                
+                }
+            }
+            
+            void buildCtmc() {
+                storm::storage::DFTState state(mDft);
+                exploreStateSuccessors(state);
+                std::cout << mStateIndices.size() << std::endl;
+            }
+            
+        };
+    }
+}
+
+
+#endif	/* EXPLICITDFTMODELBUILDER_H */
+

src/parser/DFTGalileoParser.cpp

@@ -0,0 +1,102 @@
+#include "DFTGalileoParser.h"
+
+#include <iostream>
+#include <fstream>
+#include <boost/algorithm/string.hpp>
+#include <boost/lexical_cast.hpp>
+#include "../exceptions/FileIoException.h"
+#include "../exceptions/NotSupportedException.h"
+#include "src/utility/macros.h"
+
+namespace storm {
+    namespace parser {
+        storm::storage::DFT DFTGalileoParser::parseDFT(const std::string& filename) {
+            if(readFile(filename)) {
+                return mBuilder.build();
+            } else {
+                throw storm::exceptions::FileIoException();
+            }
+        }
+        
+        std::string stripQuotsFromName(std::string const& name) {
+            size_t firstQuots = name.find("\"");
+            size_t secondQuots = name.find("\"", firstQuots+1);
+            
+            if(firstQuots == std::string::npos) {
+                return name;
+            } else {
+                return name.substr(firstQuots+1,secondQuots-1);
+            }
+        }
+        
+        bool DFTGalileoParser::readFile(const std::string& filename) {
+            // constants
+            std::string topleveltoken = "toplevel";
+            
+            
+            std::string toplevelId;
+           
+            
+            std::ifstream file;
+            file.exceptions ( std::ifstream::failbit );
+            try {
+                file.open(filename);
+            }
+            catch (std::ifstream::failure e) {
+                std::cerr << "Exception during file opening on " << filename << "." << std::endl;
+                return false;
+            }
+            file.exceptions( 0 );
+
+
+            std::string line;
+            while(std::getline(file, line))
+            {
+                std::cout << line << std::endl;
+                size_t commentstarts = line.find("//");
+                line = line.substr(0, commentstarts);
+                size_t firstsemicolon = line.find(";");
+                line = line.substr(0, firstsemicolon);
+
+                // Top level indicator.
+                if(boost::starts_with(line, topleveltoken)) {
+                    toplevelId = stripQuotsFromName(line.substr(topleveltoken.size()+1));
+                }
+                else
+                {
+                    std::vector<std::string> tokens;
+                    boost::split(tokens, line, boost::is_any_of(" "));
+                    std::string name(stripQuotsFromName(tokens[0]));
+
+                    std::vector<std::string> childNames;
+                    for(unsigned i = 2; i < tokens.size(); ++i) {
+                        childNames.push_back(stripQuotsFromName(tokens[i]));
+                    }
+                    if(tokens[1] == "and") {
+                        mBuilder.addAndElement(name, childNames);
+                    } else if(tokens[1] == "or") {
+                        mBuilder.addOrElement(name, childNames);
+                    } else if(boost::starts_with(tokens[1], "vot")) {
+                        mBuilder.addVotElement(name, boost::lexical_cast<unsigned>(tokens[1].substr(3)), childNames);
+                    } else if(tokens[1] == "pand") {
+                        mBuilder.addPandElement(name, childNames);
+                    } else if(tokens[1] == "wsp" || tokens[1] == "csp") {
+                        mBuilder.addSpareElement(name, childNames);
+                    } else if(boost::starts_with(tokens[1], "lambda=")) {
+                        mBuilder.addBasicElement(name, boost::lexical_cast<double>(tokens[1].substr(7)), boost::lexical_cast<double>(tokens[2].substr(5)));
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " + tokens[1] + "  not recognized.");
+                    }
+                }
+
+            }
+            if(!mBuilder.setTopLevel(toplevelId)) {
+                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown.");
+            }
+            file.close();
+            return true;                        
+        }
+        
+        
+    }
+}

src/parser/DFTGalileoParser.h

@@ -0,0 +1,29 @@
+#ifndef DFTGALILEOPARSER_H
+#define	DFTGALILEOPARSER_H
+
+#include "../storage/dft/DFT.h"
+#include "../storage/dft/DFTBuilder.h"
+
+#include <map>
+
+
+
+namespace storm {
+    namespace parser {
+        class DFTGalileoParser {
+            storm::storage::DFTBuilder mBuilder;
+        public:
+            storm::storage::DFT parseDFT(std::string const& filename);
+            
+        private:
+            bool readFile(std::string const& filename);
+            
+    
+    };
+}
+}
+
+
+
+#endif	/* DFTGALILEOPARSER_H */
+

src/storage/BitVector.cpp

@@ -9,6 +9,7 @@
 #include "src/utility/OsDetection.h"
 #include "src/utility/Hash.h"
 #include "src/utility/macros.h"
+#include "resources/3rdparty/glpk-4.53/src/zlib/zconf.h"
 
 namespace storm {
     namespace storage {
@@ -71,6 +72,7 @@ namespace storm {
             } else {
                 bucketVector = std::vector<uint64_t>(bucketCount, 0);
             }
+            
         }
         
         template<typename InputIterator>
@@ -440,6 +442,29 @@ namespace storm {
             }
         }
         
+        uint_fast64_t BitVector::getTwoBitsAligned(uint_fast64_t bitIndex) const {
+            // Check whether it is aligned.
+            assert(bitIndex % 64 != 63);
+            uint64_t bucket = bitIndex >> 6;
+            uint64_t bitIndexInBucket = bitIndex & mod64mask;
+            
+            uint64_t mask;
+            if (bitIndexInBucket == 0) {
+                mask = -1ull;
+            } else {
+                mask = (1ull << (64 - bitIndexInBucket)) - 1ull;
+            }
+            
+            if (bitIndexInBucket  < 62) { // bitIndexInBucket + 2 < 64
+                // If the value stops before the end of the bucket, we need to erase some lower bits.
+                mask &= ~((1ull << (62 - (bitIndexInBucket))) - 1ull);
+                return (bucketVector[bucket] & mask) >> (62 - bitIndexInBucket);
+            } else {
+                // In this case, it suffices to take the current mask.
+                return bucketVector[bucket] & mask;
+            }
+        }
+        
         void BitVector::setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value) {
             STORM_LOG_ASSERT((value >> numberOfBits) == 0, "Integer value too large to fit in the given number of bits.");
             

src/storage/BitVector.h

@@ -358,6 +358,13 @@ namespace storm {
              */
             uint_fast64_t getAsInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const;
             
+            /*!
+             * 
+             * @param bitIndex The index of the first of the two bits to get
+             * @return A value between 0 and 3, encoded as a byte.
+             */
+            uint_fast64_t getTwoBitsAligned(uint_fast64_t bitIndex) const;
+            
             /*!
              * Sets the selected number of lowermost bits of the provided value at the given bit index.
              *

src/storage/dft/DFT.cpp

@@ -0,0 +1,121 @@
+#include "DFT.h"
+
+namespace storm {
+    namespace storage {
+        
+        DFT::DFT(std::vector<std::shared_ptr<DFTElement>> const& elements, std::shared_ptr<DFTElement> const& tle) : mElements(elements), mNrOfBEs(0), mNrOfSpares(0)
+        {
+            assert(elementIndicesCorrect());
+
+            size_t stateIndex = 0;
+            mUsageInfoBits = storm::utility::math::uint64_log2(mElements.size()-1)+1;
+
+            for(auto& elem : mElements) {
+                mIdToFailureIndex.push_back(stateIndex);
+                stateIndex += 2;
+                if(elem->isBasicElement()) {
+                    ++mNrOfBEs;
+                }
+                else if(elem->isSpareGate()) {
+                    ++mNrOfSpares;
+                    for(auto const& spareReprs : std::static_pointer_cast<DFTSpare>(elem)->children()) {
+                        if(mActivationIndex.count(spareReprs->id()) == 0) {
+                            mActivationIndex[spareReprs->id()] =  stateIndex++;
+                        }
+                        std::set<size_t> module = {spareReprs->id()};
+                        spareReprs->extendSpareModule(module);
+                        std::vector<size_t> sparesAndBes;
+                        for(auto const& modelem : module) {
+                            if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) {
+                                sparesAndBes.push_back(modelem);
+                            }
+                        }
+                        mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes));
+
+                    }
+                    std::static_pointer_cast<DFTSpare>(elem)->setUseIndex(stateIndex);
+                    mUsageIndex.insert(std::make_pair(elem->id(), stateIndex));
+                    stateIndex += mUsageInfoBits;
+
+
+                }
+            }
+
+            // For the top module, we assume, contrary to [Jun15], that we have all spare gates and basic elements which are not in another module.
+            std::set<size_t> topModuleSet;
+            // Initialize with all ids.
+            for(auto const& elem : mElements) {
+                if (elem->isBasicElement() || elem->isSpareGate()) {
+                    topModuleSet.insert(elem->id());
+                }
+            }
+
+            for(auto const& module : mSpareModules) {
+                for(auto const& index : module.second) {
+                    topModuleSet.erase(index);
+                }
+            }
+            mTopModule = std::vector<size_t>(topModuleSet.begin(), topModuleSet.end());
+
+            mStateSize = stateIndex;
+            mTopLevelIndex = tle->id();
+
+        }
+        
+        void DFT::printElements(std::ostream& os) const {
+            for (auto const& elem : mElements) {
+                elem->print(os);
+                os << std::endl;
+            }
+        }
+
+        void DFT::printInfo(std::ostream& os) const {
+            os << "Top level index: " << mTopLevelIndex << std::endl << "Nr BEs" << mNrOfBEs << std::endl;
+        }
+
+        void DFT::printSpareModules(std::ostream& os) const {
+            std::cout << "[" << mElements[mTopLevelIndex] << "] {";
+            std::vector<size_t>::const_iterator it = mTopModule.begin();
+            assert(it != mTopModule.end());
+            os << mElements[(*it)]->name();
+            ++it;
+            while(it != mTopModule.end()) {
+                os <<  ", " << mElements[(*it)]->name();
+                ++it;
+            }
+            os << "}" << std::endl;
+
+            for(auto const& spareModule : mSpareModules) {
+                std::cout << "[" << mElements[spareModule.first]->name() << "] = {";
+                os.flush();
+                std::vector<size_t>::const_iterator it = spareModule.second.begin();
+                assert(it != spareModule.second.end());
+                os << mElements[(*it)]->name();
+                ++it;
+                while(it != spareModule.second.end()) {
+                    os <<  ", " << mElements[(*it)]->name();
+                    os.flush();
+                    ++it;
+                }
+                os << "}" << std::endl;
+            }
+        }
+
+        void DFT::printElementsWithState(DFTState const& state, std::ostream& os) const{
+            for (auto const& elem : mElements) {
+                os << "[" << elem->id() << "]";
+                elem->print(os);
+                os << "\t** " << state.getElementState(elem->id());
+                if(elem->isSpareGate()) {
+                    if(state.isActiveSpare(elem->id())) {
+                        os << " actively";
+                    }
+                    os << " using " << state.uses(elem->id());
+                } 
+                std::cout << std::endl;
+
+
+            }
+        }
+    }
+}

src/storage/dft/DFT.h

@@ -0,0 +1,184 @@
+
+#ifndef DFT_H
+#define	DFT_H
+
+
+#include "DFTElements.h"
+#include "../BitVector.h"
+#include <memory>
+#include <unordered_map>
+#include <list>
+#include <map>
+
+#include "../../utility/math.h"
+#include <boost/iterator/counting_iterator.hpp>
+
+namespace storm {
+    namespace storage {
+
+                
+        struct DFTElementSort {
+            bool operator()(std::shared_ptr<DFTElement> const& a, std::shared_ptr<DFTElement> const& b)  const {
+                if (a->rank() == 0 && b->rank() == 0) {
+                    return a->isConstant();
+                } else {
+                    return a->rank() < b->rank();
+                }
+            }
+        };
+        
+        class DFT {
+
+            
+
+        private:
+            std::vector<std::shared_ptr<DFTElement>> mElements;
+            size_t mNrOfBEs;
+            size_t mNrOfSpares;
+            size_t mTopLevelIndex;
+            size_t mUsageInfoBits;
+            size_t mStateSize;
+            std::map<size_t, size_t> mActivationIndex;
+            std::map<size_t, std::vector<size_t>> mSpareModules;
+            std::vector<size_t> mTopModule;
+            std::vector<size_t> mIdToFailureIndex;
+            std::map<size_t, size_t> mUsageIndex;
+            
+            
+        public:
+            DFT(std::vector<std::shared_ptr<DFTElement>> const& elements, std::shared_ptr<DFTElement> const& tle);
+            
+            
+            size_t stateSize() const {
+                return mStateSize;
+            }
+            
+            size_t nrElements() const {
+                return mElements.size();
+            }
+            
+            size_t nrBasicElements() const {
+                return mNrOfBEs;
+            }
+            
+            size_t usageInfoBits() const {
+                return mUsageInfoBits;
+            }
+            
+            size_t usageIndex(size_t id) const {
+                assert(mUsageIndex.find(id) != mUsageIndex.end());
+                return mUsageIndex.find(id)->second;
+            }
+            
+            size_t failureIndex(size_t id) const {
+                return mIdToFailureIndex[id];
+            }
+            
+            void initializeUses(DFTState& state) const {
+                for(auto const& elem : mElements) {
+                    if(elem->isSpareGate()) {
+                        std::static_pointer_cast<DFTSpare>(elem)->initializeUses(state);
+                    }
+                }
+            }
+            
+            void initializeActivation(DFTState& state) const {
+                state.activate(mTopLevelIndex);
+                for(auto const& elem : mTopModule) {
+                    if(mElements[elem]->isSpareGate()) {
+                        propagateActivation(state, state.uses(elem));
+                    }
+                }
+            }
+            
+            std::vector<size_t> getSpareIndices() const {
+                std::vector<size_t> indices;
+                for(auto const& elem : mElements) {
+                    if(elem->isSpareGate()) {
+                        indices.push_back(elem->id());
+                    }
+                }
+                return indices;
+            }
+            
+            std::vector<size_t> const& module(size_t representativeId) const {
+                if(representativeId == mTopLevelIndex) {
+                    return mTopModule;
+                } else {
+                    assert(mSpareModules.count(representativeId)>0);
+                    return mSpareModules.find(representativeId)->second;
+                }
+            }
+            
+            
+            void propagateActivation(DFTState& state, size_t representativeId) const {
+                state.activate(representativeId);
+                for(size_t id : module(representativeId)) {
+                    if(mElements[id]->isSpareGate()) {
+                        propagateActivation(state, state.uses(id));
+                    }
+                }
+            }
+            
+            std::vector<size_t> nonColdBEs() const {
+                std::vector<size_t> result;
+                for(std::shared_ptr<DFTElement> elem : mElements) {
+                    if(elem->isBasicElement() && !elem->isColdBasicElement()) {
+                        result.push_back(elem->id());
+                    }
+                }
+                return result;
+            }
+            
+            std::shared_ptr<DFTElement> const& getElement(size_t index) const {
+                assert(index < nrElements());
+                return mElements[index];
+            }
+            
+            std::shared_ptr<DFTBE<double>> getBasicElement(size_t index) const {
+                assert(mElements[index]->isBasicElement());
+                return std::static_pointer_cast<DFTBE<double>>(mElements[index]);
+            }
+            
+            bool hasFailed(DFTState const& state) const {
+                return state.hasFailed(mTopLevelIndex);
+            }
+            
+            bool isFailsafe(DFTState const& state) const {
+                return state.isFailsafe(mTopLevelIndex);
+            }
+                    
+            
+            void printElements(std::ostream& os = std::cout) const;
+            
+            void printInfo(std::ostream& os = std::cout) const;
+            
+            void printSpareModules(std::ostream& os = std::cout) const;
+            
+            void printElementsWithState(DFTState const& state, std::ostream& os = std::cout) const; 
+            
+        private:
+            bool elementIndicesCorrect() const {
+                for(size_t i = 0; i < mElements.size(); ++i) {
+                    if(mElements[i]->id() != i) return false;
+                }
+                return true;
+            }
+
+
+
+
+        };
+        
+        
+        
+       
+
+        
+        
+        
+       
+    }
+}
+#endif	/* DFT_H */
+

src/storage/dft/DFTBuilder.cpp

@@ -0,0 +1,132 @@
+
+
+#include "DFTBuilder.h"
+
+#include "DFT.h"
+#include <algorithm>
+#include "OrderDFTElementsById.h"
+#include "../../exceptions/WrongFormatException.h"
+
+
+namespace storm {
+    namespace storage {
+        
+         
+        DFT DFTBuilder::build() {
+            for(auto& elem : mChildNames) {
+                for(auto const& child : elem.second) {
+                    std::shared_ptr<DFTGate> gate = std::static_pointer_cast<DFTGate>(elem.first);
+                    gate->pushBackChild(mElements[child]);
+                    mElements[child]->addParent(gate);
+                }
+            }
+
+            // Sort elements topologically
+
+
+
+            // compute rank
+            for (auto& elem : mElements) {
+                computeRank(elem.second);
+            }
+
+            std::vector<std::shared_ptr<DFTElement>> elems = topoSort();
+            size_t id = 0;
+            for(std::shared_ptr<DFTElement> e : elems) {
+                e->setId(id++);
+            }
+            for(auto& e : elems) {
+                std::cout << "[" << e->id() << "] ";
+                e->print();
+                std::cout << std::endl;
+            }
+            return DFT(elems, mElements[topLevelIdentifier]);
+
+        }
+        
+        unsigned DFTBuilder::computeRank(std::shared_ptr<DFTElement> const& elem) {
+            if(elem->rank() == -1) {
+                if(elem->nrChildren() == 0) {
+                    elem->setRank(0);
+                    return 0;
+                }
+                std::shared_ptr<DFTGate> gate = std::static_pointer_cast<DFTGate>(elem);
+                unsigned maxrnk = 0;
+                unsigned newrnk = 0;
+
+                for(std::shared_ptr<DFTElement> const& child : gate->children()) {
+                    newrnk = computeRank(child);
+                    if(newrnk > maxrnk) {
+                        maxrnk = newrnk;
+                    }
+                }
+                elem->setRank(maxrnk+1);
+                return maxrnk + 1;
+            } else {
+                return elem->rank();
+            }
+        }
+        
+        bool DFTBuilder::addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementTypes tp) {
+            assert(children.size() > 0);
+            if(mElements.count(name) != 0) {
+                // Element with that name already exists.
+                return false;
+            }
+            std::shared_ptr<DFTElement> element;
+            switch(tp) {
+                case DFTElementTypes::AND:
+                    element = std::make_shared<DFTAnd>(mNextId++, name);
+                    break;
+                case DFTElementTypes::OR:
+                    element = std::make_shared<DFTOr>(mNextId++, name);
+                    break;
+                case DFTElementTypes::PAND:
+                    element = std::make_shared<DFTPand>(mNextId++, name);
+                    break;
+                case DFTElementTypes::POR:
+                    element = std::make_shared<DFTPor>(mNextId++, name);
+                    break;
+                case DFTElementTypes::SPARE:
+                   element = std::make_shared<DFTSpare>(mNextId++, name);
+                   break;
+            }
+            mElements[name] = element;
+            mChildNames[element] = children;
+            return true;
+        }
+        
+        
+        void DFTBuilder::topoVisit(std::shared_ptr<DFTElement> const& n, std::map<std::shared_ptr<DFTElement>, topoSortColour>& visited, std::vector<std::shared_ptr<DFTElement>>& L) {
+            if(visited[n] == topoSortColour::GREY) {
+                throw storm::exceptions::WrongFormatException("DFT is cyclic");
+            } else if(visited[n] == topoSortColour::WHITE) {
+                if(n->isGate()) {
+                    visited[n] = topoSortColour::GREY;
+                    for(std::shared_ptr<DFTElement> const& c : std::static_pointer_cast<DFTGate>(n)->children()) {
+                        topoVisit(c, visited, L);
+                    }
+                }
+                visited[n] = topoSortColour::BLACK;
+                L.push_back(n);
+               
+            }
+        }
+
+        std::vector<std::shared_ptr<DFTElement>> DFTBuilder::topoSort() {
+            std::map<std::shared_ptr<DFTElement>, topoSortColour> visited;
+            for(auto const& e : mElements) {
+                visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); 
+            }
+
+            std::vector<std::shared_ptr<DFTElement>> L;
+            for(auto const& e : visited) {
+                topoVisit(e.first, visited, L);
+            }
+            //std::reverse(L.begin(), L.end()); 
+            return L;
+       }
+
+    }
+}
+            

src/storage/dft/DFTBuilder.h

@@ -0,0 +1,116 @@
+
+#ifndef DFTBUILDER_H
+#define	DFTBUILDER_H
+
+#include "DFTElements.h"
+#include <iostream>
+#include <unordered_map>
+#include <map>
+
+namespace storm {
+    namespace storage {
+        class DFT;
+        
+        class DFTBuilder {
+            
+            std::size_t mNextId = 0;
+            std::string topLevelIdentifier;
+            std::unordered_map<std::string, std::shared_ptr<DFTElement>> mElements;
+            std::unordered_map<std::shared_ptr<DFTElement>, std::vector<std::string>> mChildNames;
+            
+        public:
+            DFTBuilder() {
+                
+            }
+            
+            bool addAndElement(std::string const& name, std::vector<std::string> const& children) {
+                return addStandardGate(name, children, DFTElementTypes::AND);
+            }
+            
+            bool addOrElement(std::string const& name, std::vector<std::string> const& children) {
+                return addStandardGate(name, children, DFTElementTypes::OR);
+            }
+            
+            bool addPandElement(std::string const& name, std::vector<std::string> const& children) {
+                return addStandardGate(name, children, DFTElementTypes::PAND);
+            }
+            
+            bool addPorElement(std::string const& name, std::vector<std::string> const& children) {
+                return addStandardGate(name, children, DFTElementTypes::POR);
+            }
+            
+            bool addSpareElement(std::string const& name, std::vector<std::string> const& children) {
+                return addStandardGate(name, children, DFTElementTypes::SPARE);
+            }
+            
+            
+            
+            bool addVotElement(std::string const& name, unsigned threshold, std::vector<std::string> const& children) {
+                assert(children.size() > 0);
+                if(mElements.count(name) != 0) {
+                    std::cerr << "Element with name: " << name << " already exists." << std::endl;
+                    return false;
+                }
+                // It is an and-gate
+                if(children.size() == threshold) {
+                    return addAndElement(name, children);
+                }
+                // It is an or-gate
+                if(threshold == 1) {
+                    return addOrElement(name, children);
+                }
+                
+                if(threshold > children.size()) {
+                    std::cerr << "Voting gates with threshold higher than the number of children is not supported." << std::endl;
+                    return false;
+                }
+                std::shared_ptr<DFTElement> element = std::make_shared<DFTVot>(mNextId++, name, threshold);
+                
+                mElements[name] = element;
+                mChildNames[element] = children;
+                return true;
+            }
+            
+            bool addBasicElement(std::string const& name, double failureRate, double dormancyFactor) {
+                if(failureRate <= 0.0) {
+                    std::cerr << "Failure rate must be positive." << std::endl;
+                    return false;
+                }
+                
+                if(dormancyFactor < 0.0 || dormancyFactor > 1.0) {
+                    std::cerr << "Dormancy factor must be between 0 and 1." << std::endl;
+                    return false;
+                }
+                
+                mElements[name] = std::make_shared<DFTBE<double>>(mNextId++, name, failureRate, dormancyFactor);
+                return true;
+            }
+            
+            bool setTopLevel(std::string const& tle) {
+                topLevelIdentifier = tle;
+                return mElements.count(tle) > 0;
+            }
+            
+            DFT build();
+
+         
+        private:
+            
+            unsigned computeRank(std::shared_ptr<DFTElement> const& elem);
+            
+            bool addStandardGate(std::string const& name, std::vector<std::string> const& children, DFTElementTypes tp);
+            
+            enum class topoSortColour {WHITE, BLACK, GREY}; 
+            
+            void topoVisit(std::shared_ptr<DFTElement> const& n, std::map<std::shared_ptr<DFTElement>, topoSortColour>& visited, std::vector<std::shared_ptr<DFTElement>>& L);
+            std::vector<std::shared_ptr<DFTElement>> topoSort();
+
+            
+        };
+    }
+}
+
+
+
+#endif	/* DFTBUILDER_H */
+

src/storage/dft/DFTElementState.h

@@ -0,0 +1,26 @@
+
+#ifndef DFTELEMENTSTATE_H
+#define	DFTELEMENTSTATE_H
+
+namespace storm {
+    namespace storage {
+        enum class DFTElementState  {Operational = 0, Failed = 2, Failsafe = 1, DontCare = 3};
+        
+        inline std::ostream& operator<<(std::ostream& os, DFTElementState st) {
+            switch(st) {
+                case DFTElementState::Operational:
+                    return os << "Operational";
+                case DFTElementState::Failed:
+                    return os << "Failed";
+                case DFTElementState::Failsafe:
+                    return os << "Failsafe";
+                case DFTElementState::DontCare:
+                    return os << "Don't Care";
+            }
+        }
+    }
+}
+
+
+#endif	/* DFTELEMENTSTATE_H */
+

src/storage/dft/DFTElements.cpp

@@ -0,0 +1,38 @@
+#include "DFTElements.h"
+
+namespace storm {
+    namespace storage {
+        bool DFTElement::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+            if(!state.dontCare(mId))
+            {
+                for(std::shared_ptr<DFTGate> const& parent : mParents) {
+                    if(state.isOperational(parent->id())) {
+                        return false;
+                    }
+                }
+                state.setDontCare(mId);
+                return true;
+
+            }
+            return false;
+        }
+        
+        void DFTElement::extendSpareModule(std::set<size_t>& elementsInModule) const {
+            for(auto const& parent : mParents) {
+                if(elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) {
+                    elementsInModule.insert(parent->id());
+                    parent->extendSpareModule(elementsInModule);
+                }
+            }
+        }
+        
+        template<>
+        bool DFTBE<double>::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+            if(DFTElement::checkDontCareAnymore(state, queues)) {
+                state.beNoLongerFailable(mId);
+                return true;
+            }
+            return false;
+        }
+    }
+}

src/storage/dft/DFTElements.h

@@ -0,0 +1,635 @@
+#ifndef DFTELEMENTS_H
+#define	DFTELEMENTS_H
+
+#include <set>
+#include <vector>
+#include <memory>
+#include <string>
+#include <cassert>
+#include <cstdlib>
+#include <iostream>
+
+#include "DFTState.h"
+#include "DFTStateSpaceGenerationQueues.h"
+
+using std::size_t;
+
+namespace storm {
+    namespace storage {
+        class DFTGate;
+        
+        class DFTElement {
+        protected:
+            size_t mId;
+            std::string mName;
+            size_t mRank = -1;
+            std::vector<std::shared_ptr<DFTGate>> mParents;
+            
+
+            
+
+        public:
+            DFTElement(size_t id, std::string const& name) : mId(id), mName(name)
+            {}
+            virtual ~DFTElement() {}
+
+            
+            virtual size_t id() const {
+                return mId;
+            }
+            
+            virtual void setRank(size_t rank) {
+                mRank = rank;
+            }
+            
+            virtual size_t rank() const {
+                return mRank;
+            }
+            
+            virtual bool isConstant() const {
+                return false;
+            }
+            
+            virtual bool isGate() const {
+                return false;
+            }
+            
+            virtual bool isBasicElement() const {
+                return false;
+            }
+            
+            virtual bool isColdBasicElement() const {
+                return false;
+            }
+            
+            virtual bool isSpareGate() const {
+                return false;
+            }
+            
+            virtual void setId(size_t newId) {
+                mId = newId;
+            }
+            
+            virtual std::string const& name() const {
+                return mName;
+            }
+            
+            bool addParent(std::shared_ptr<DFTGate> const& e) {
+                if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) {
+                    return false;
+                }
+                else 
+                {
+                    mParents.push_back(e);
+                    return true;
+                }
+            }
+
+            bool hasParents() const {
+                return !mParents.empty();
+            }
+            
+            std::vector<std::shared_ptr<DFTGate>> const& parents() const {
+                return mParents;
+            }
+            
+            virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
+            
+            virtual size_t nrChildren() const = 0;
+            virtual void print(std::ostream& = std::cout) const = 0;
+            
+            virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
+        };
+
+
+        enum class DFTElementTypes {AND, COUNTING, OR, VOT, BE, CONSTF, CONSTS, PAND, SPARE, POR, FDEP, SEQAND};
+
+        inline bool isGateType(DFTElementTypes const& tp) {
+            switch(tp) {
+                case DFTElementTypes::AND:
+                case DFTElementTypes::COUNTING:
+                case DFTElementTypes::OR:
+                case DFTElementTypes::VOT:
+                case DFTElementTypes::PAND:
+                case DFTElementTypes::SPARE:
+                case DFTElementTypes::POR:
+                case DFTElementTypes::SEQAND:
+                    return true;
+                case DFTElementTypes::BE:
+                case DFTElementTypes::CONSTF:
+                case DFTElementTypes::CONSTS:
+                case DFTElementTypes::FDEP:
+                    return false;
+                default:
+                    assert(false);
+            }
+        }
+        
+        class DFTGate : public DFTElement {
+        protected:
+            std::vector<std::shared_ptr<DFTElement>> mChildren;
+        public:
+            DFTGate(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children) :
+            DFTElement(id, name), mChildren(children)
+            {}
+            
+            virtual ~DFTGate() {}
+            
+            void pushBackChild(std::shared_ptr<DFTElement> elem) {
+                return mChildren.push_back(elem);
+            }
+
+            size_t nrChildren() const {
+                return mChildren.size();
+            }
+            
+            std::vector<std::shared_ptr<DFTElement>> const& children() const {
+                return mChildren;
+            }
+            
+            virtual bool isGate() const {
+                return true;
+            }
+            
+            
+            virtual std::string typestring() const = 0;
+            virtual void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0;
+            virtual void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const = 0;
+            
+            virtual void extendSpareModule(std::set<size_t>& elementsInSpareModule) const override {
+                DFTElement::extendSpareModule(elementsInSpareModule);
+                for(auto const& child : mChildren) {
+                    if(elementsInSpareModule.count(child->id()) == 0) {
+                        elementsInSpareModule.insert(child->id());
+                        child->extendSpareModule(elementsInSpareModule);
+                    }
+                }
+            }
+            
+            virtual void print(std::ostream& os = std::cout) const {
+                os << "{" << name() << "} " << typestring() << "( ";
+                std::vector<std::shared_ptr<DFTElement>>::const_iterator it = mChildren.begin();
+                os << (*it)->name();
+                ++it;
+                while(it != mChildren.end()) {
+                    os <<  ", " << (*it)->name();
+                    ++it;
+                }
+                os << ")";
+            }    
+            
+            virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                if(DFTElement::checkDontCareAnymore(state, queues)) {
+                    childrenDontCare(state, queues);
+                    return true;
+                }
+                return false;
+            }
+        protected:
+            void fail(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                for(std::shared_ptr<DFTGate> parent : mParents) {
+                    if(state.isOperational(parent->id())) {
+                        queues.propagateFailure(parent);
+                    }
+                }
+                state.setFailed(mId);        
+            }
+            
+            void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                for(std::shared_ptr<DFTGate> parent : mParents) {
+                    if(state.isOperational(parent->id())) {
+                        queues.propagateFailsafe(parent);
+                    }
+                }
+                state.setFailsafe(mId);
+            }
+            
+            void childrenDontCare(DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                queues.propagateDontCare(mChildren);
+            }
+            
+            bool hasFailsafeChild(DFTState& state) const {
+                for(auto const& child : mChildren) {
+                    if(state.isFailsafe(child->id()))
+                    {
+                        return true;
+                    }
+                }
+                return false;
+            }
+            
+            
+            bool hasFailedChild(DFTState& state) const {
+                for(auto const& child : mChildren) {
+                    if(state.hasFailed(child->id())) {
+                        return true;
+                    }
+                }
+                return false;
+            }
+
+        };
+        
+       
+
+        template<typename FailureRateType>
+        class DFTBE : public DFTElement {
+
+            
+            FailureRateType mActiveFailureRate;
+            FailureRateType mPassiveFailureRate;
+        public:
+            DFTBE(size_t id, std::string const& name, FailureRateType failureRate, FailureRateType dormancyFactor) :
+            DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate)
+            {
+                
+            }
+                        
+            virtual size_t nrChildren() const {
+                return 0;
+            }
+            
+            FailureRateType const& activeFailureRate() const {
+                return mActiveFailureRate;
+            }
+            
+            FailureRateType const& passiveFailureRate() const {
+                return mPassiveFailureRate;
+            }
+        
+            void print(std::ostream& os = std::cout) const {
+                os << *this;
+            }
+            
+            bool isBasicElement() const {
+                return true;
+            }
+            
+            bool isColdBasicElement() const {
+                return mPassiveFailureRate == 0;
+            }
+            
+
+            virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const;
+        };
+        
+        inline std::ostream& operator<<(std::ostream& os, DFTBE<double> const& be) {
+            return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")";
+        }
+
+        
+        
+
+        class DFTConst : public DFTElement {
+            bool mFailed;
+        public:
+            DFTConst(size_t id, std::string const& name, bool failed) : DFTElement(id, name), mFailed(failed) 
+            {
+                
+            }
+            
+            bool failed() const {
+                return mFailed;
+            }
+            
+            virtual bool isConstant() const {
+                return true;
+            }
+            
+            virtual size_t nrChildren() const {
+                return 0;
+            }
+            
+        };
+
+        class DFTAnd : public DFTGate {
+            
+        public:
+            DFTAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
+            DFTGate(id, name, children) 
+            {}
+            
+            void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                
+                if(state.isOperational(mId)) {
+                    for(auto const& child : mChildren)
+                    {
+                        if(!state.hasFailed(child->id())) {
+                            return;// false;
+                        }
+                    }
+                    fail(state, queues);
+                    //return true;
+                } 
+                //return false;
+            }
+            
+            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
+                assert(hasFailsafeChild(state));
+                if(state.isOperational(mId)) {
+                    failsafe(state, queues);
+                    childrenDontCare(state, queues);
+                    //return true;
+                }
+                //return false;
+            }
+            
+            std::string typestring() const {
+                return "AND";
+            }
+        };
+        
+        inline std::ostream& operator<<(std::ostream& os, DFTAnd const& gate) {
+            gate.print(os);
+            return os;
+        }
+       
+        
+
+        class DFTOr : public DFTGate {
+        public:
+            DFTOr(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
+            DFTGate(id, name, children) 
+            {}
+            
+             void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                 assert(hasFailedChild(state));
+                if(state.isOperational(mId)) {
+                    fail(state, queues);
+                    //return true;
+                } 
+                // return false;
+            }
+             
+            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
+                 for(auto const& child : mChildren) {
+                     if(!state.isFailsafe(child->id())) {
+                         return;// false;
+                     }
+                 }
+                 failsafe(state, queues);
+                 //return true;
+            }
+            
+            std::string typestring() const {
+                return "OR";
+            }
+        private:
+            //static const std::string typestring = "or";
+        };
+        
+         inline std::ostream& operator<<(std::ostream& os, DFTOr const& gate) {
+            gate.print(os);
+            return os;
+        }
+
+        class DFTSeqAnd : public DFTGate {
+        public:
+            DFTSeqAnd(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
+            DFTGate(id, name, children) 
+            {}
+            
+            void checkFails(storm::storage::DFTState& state,  DFTStateSpaceGenerationQueues& queues) const {
+                
+                if(!state.hasFailed(mId)) {
+                    bool childOperationalBefore = false;
+                    for(auto const& child : mChildren)
+                    {
+                        if(!state.hasFailed(child->id())) {
+                            childOperationalBefore = true;
+                        }
+                        else {
+                            if(childOperationalBefore) {
+                                state.markAsInvalid();
+                                return; //false;
+                            }
+                        }
+                    }
+                    if(!childOperationalBefore) {
+                       fail(state, queues);
+                       //return true;
+                    }
+                  
+                } 
+                //return false;
+            }
+            
+            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
+                assert(hasFailsafeChild(state));
+                if(state.isOperational(mId)) {
+                    failsafe(state, queues);
+                    //return true;
+                }
+                //return false;
+            }
+            
+            std::string  typestring() const {
+                return "SEQAND";
+            }
+        private:
+            //static const std::string typestring = "seqand"; 
+        };
+        
+         inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) {
+            gate.print(os);
+            return os;
+        }
+        
+        class DFTPand : public DFTGate {
+        public:
+            DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
+            DFTGate(id, name, children) 
+            {}
+            
+            void checkFails(storm::storage::DFTState& state,  DFTStateSpaceGenerationQueues& queues) const {
+                if(state.isOperational(mId)) {
+                    bool childOperationalBefore = false;
+                    for(auto const& child : mChildren)
+                    {
+                        if(!state.hasFailed(child->id())) {
+                            childOperationalBefore = true;
+                        } else if(childOperationalBefore && state.hasFailed(child->id())){
+                            failsafe(state, queues);
+                            childrenDontCare(state, queues);
+                            return; //false;
+                        }
+                    }
+                    if(!childOperationalBefore) {
+                        fail(state, queues);
+                        //return true;
+                    }
+                }
+                // return false;
+            }
+             
+            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
+                assert(hasFailsafeChild(state));
+                if(state.isOperational(mId)) {
+                    failsafe(state, queues);
+                    childrenDontCare(state, queues);
+                    //return true;
+                }
+                //return false;
+            } 
+            
+            std::string typestring() const {
+                return "PAND";
+            }
+        };
+        
+         inline std::ostream& operator<<(std::ostream& os, DFTPand const& gate) {
+            gate.print(os);
+            return os;
+        }
+        
+        class DFTPor : public DFTGate {
+        public:
+            DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
+            DFTGate(id, name, children) 
+            {}
+            
+            void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                 assert(false);
+            }
+             
+            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
+                assert(false);
+            }
+            
+            std::string  typestring() const {
+                return "POR";
+            }
+        };
+        
+         inline std::ostream& operator<<(std::ostream& os, DFTPor const& gate) {
+            gate.print(os);
+            return os;
+        }
+
+        class DFTVot : public DFTGate {
+        private:
+            unsigned mThreshold;
+        public:
+            DFTVot(size_t id, std::string const& name, unsigned threshold, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
+            DFTGate(id, name, children), mThreshold(threshold)
+            {}
+            
+            void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                
+                if(state.isOperational(mId)) {
+                    unsigned nrFailedChildren = 0;
+                    for(auto const& child : mChildren)
+                    {
+                        if(state.hasFailed(child->id())) {
+                            ++nrFailedChildren;
+                            if(nrFailedChildren >= mThreshold) 
+                            {
+                                fail(state, queues);
+                                return;// true;
+                            }
+                        }
+                    }
+                  
+                } 
+                //    return false;
+               
+            }
+            
+            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{
+                assert(hasFailsafeChild(state));
+                if(state.isOperational(mId)) {
+                    unsigned nrFailsafeChildren = 0;
+                    for(auto const& child : mChildren)
+                    {
+                        if(state.isFailsafe(child->id())) {
+                            ++nrFailsafeChildren;
+                            if(nrFailsafeChildren > nrChildren() - mThreshold) 
+                            {
+                                failsafe(state, queues);
+                                childrenDontCare(state, queues);
+                                return;// true;
+                            }
+                        }
+                    }
+                }
+                //return false;
+            }
+            
+            std::string typestring() const {
+                return "VOT (" + std::to_string(mThreshold) + ")";
+            }
+
+        };
+
+        inline std::ostream& operator<<(std::ostream& os, DFTVot const& gate) {
+            gate.print(os);
+            return os;
+        }        
+        
+        class DFTSpare : public DFTGate {
+            size_t mUseIndex;
+            size_t mActiveIndex;
+            
+        public:
+            DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement>> const& children = {}) :
+            DFTGate(id, name, children)
+            {
+                
+            }
+            
+            
+            std::string typestring() const {
+                return "SPARE";
+            }
+            
+            bool isSpareGate() const {
+                return true;
+            }
+            
+            void setUseIndex(size_t useIndex) {
+                mUseIndex = useIndex; 
+            }
+            
+            void setActiveIndex(size_t activeIndex) {
+                mActiveIndex = activeIndex;
+            }
+            
+            void initializeUses(storm::storage::DFTState& state) {
+                assert(mChildren.size() > 0);
+                state.setUsesAtPosition(mUseIndex, mChildren[0]->id());
+            }
+            
+            void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                if(state.isOperational(mId)) {
+                    size_t uses = state.extractUses(mUseIndex);
+                    if(!state.isOperational(uses)) {
+                        // TODO compute children ids before.
+                        std::vector<size_t> childrenIds;
+                        for(auto const& child : mChildren) {
+                            childrenIds.push_back(child->id());
+                        }
+                        
+                        bool claimingSuccessful = state.claimNew(mId, mUseIndex, uses, childrenIds);
+                        if(!claimingSuccessful) {
+                            fail(state, queues);
+                        }
+                    }                  
+                } 
+            }
+            
+            void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const {
+                if(state.isOperational(mId)) {
+                    if(state.isFailsafe(state.extractUses((mUseIndex)))) {
+                        failsafe(state, queues);
+                        childrenDontCare(state, queues);
+                    }
+                }
+            }
+        };
+    }
+}
+
+
+
+#endif	/* DFTELEMENTS_H */
+

src/storage/dft/DFTState.cpp

@@ -0,0 +1,125 @@
+#include "DFTState.h"
+#include "DFTElements.h"
+#include "DFT.h"
+
+namespace storm {
+    namespace storage {
+        
+        DFTState::DFTState(DFT const& dft) : mStatus(dft.stateSize()), mDft(dft)  {
+            mInactiveSpares = dft.getSpareIndices();
+            dft.initializeUses(*this);
+            dft.initializeActivation(*this);
+            std::vector<size_t> alwaysActiveBEs = dft.nonColdBEs();
+            mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end());
+            
+        }
+        
+        DFTElementState DFTState::getElementState(size_t id) const {
+            return static_cast<DFTElementState>(mStatus.getAsInt(mDft.failureIndex(id), 2));
+        }
+
+        bool DFTState::isOperational(size_t id) const {
+            return getElementState(id) == DFTElementState::Operational;
+        }
+
+        bool DFTState::hasFailed(size_t id) const {
+            return mStatus[mDft.failureIndex(id)];
+        }
+
+        bool DFTState::isFailsafe(size_t id) const {
+            return mStatus[mDft.failureIndex(id)+1];
+        }
+
+        bool DFTState::dontCare(size_t id) const {
+            return getElementState(id) == DFTElementState::DontCare;
+        }
+
+        void DFTState::setFailed(size_t id) {
+            mStatus.set(mDft.failureIndex(id));
+        }
+
+        void DFTState::setFailsafe(size_t id) {
+            mStatus.set(mDft.failureIndex(id)+1);
+        }
+
+        void DFTState::setDontCare(size_t id) {
+            mStatus.setFromInt(mDft.failureIndex(id), 2, static_cast<uint_fast64_t>(DFTElementState::DontCare) );
+        }
+        
+        void DFTState::beNoLongerFailable(size_t id) {
+            auto it = std::find(mIsCurrentlyFailableBE.begin(), mIsCurrentlyFailableBE.end(), id);
+            if(it != mIsCurrentlyFailableBE.end()) {
+                mIsCurrentlyFailableBE.erase(it);
+            }
+        }
+
+        
+        std::pair<std::shared_ptr<DFTBE<double>>, bool> DFTState::letNextBEFail(size_t index) 
+        {
+            assert(index < mIsCurrentlyFailableBE.size());
+            //std::cout << "currently failable: ";
+            //printCurrentlyFailable(std::cout);
+            std::pair<std::shared_ptr<DFTBE<double>>,bool> res(mDft.getBasicElement(mIsCurrentlyFailableBE[index]), false);
+            mIsCurrentlyFailableBE.erase(mIsCurrentlyFailableBE.begin() + index);
+            setFailed(res.first->id());
+            return res;
+        }
+        
+        void DFTState::activate(size_t repr) {
+            std::vector<size_t>  const& module = mDft.module(repr);
+            for(size_t elem : module) {
+                if(mDft.getElement(elem)->isColdBasicElement() && isOperational(elem)) {
+                    mIsCurrentlyFailableBE.push_back(elem);
+                }
+                else if(mDft.getElement(elem)->isSpareGate()) {
+                    assert(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem) != mInactiveSpares.end());
+                    mInactiveSpares.erase(std::find(mInactiveSpares.begin(), mInactiveSpares.end(), elem));
+                }
+            }
+        }
+        
+        
+        bool DFTState::isActiveSpare(size_t id) const {
+            assert(mDft.getElement(id)->isSpareGate());
+            return (std::find(mInactiveSpares.begin(), mInactiveSpares.end(), id) == mInactiveSpares.end());
+        }
+        
+        uint_fast64_t DFTState::uses(size_t id) const {
+            return extractUses(mDft.usageIndex(id));
+        }
+        
+        uint_fast64_t DFTState::extractUses(size_t from) const {
+            assert(mDft.usageInfoBits() < 64);
+            return mStatus.getAsInt(from, mDft.usageInfoBits());
+        }
+        
+        bool DFTState::isUsed(size_t child) {
+            return (std::find(mUsedRepresentants.begin(), mUsedRepresentants.end(), child) != mUsedRepresentants.end());
+            
+        }
+        
+        
+        
+        void DFTState::setUsesAtPosition(size_t usageIndex, size_t child) {
+            mStatus.setFromInt(usageIndex, mDft.usageInfoBits(), child);
+            mUsedRepresentants.push_back(child);
+        }
+        
+        bool DFTState::claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector<size_t> const& childIds) {
+            auto it = find(childIds.begin(), childIds.end(), currentlyUses);
+            assert(it != childIds.end());
+            ++it;
+            while(it != childIds.end()) {
+                if(!hasFailed(*it) && !isUsed(*it)) {
+                    setUsesAtPosition(usageIndex, *it);
+                    if(isActiveSpare(spareId)) {
+                        mDft.propagateActivation(*this,*it);
+                    }
+                    return true;
+                }
+                ++it;
+            }
+            return false;
+        }
+    }
+}

src/storage/dft/DFTState.h

@@ -0,0 +1,138 @@
+#ifndef DFTSTATE_H
+#define	DFTSTATE_H
+
+#include "../BitVector.h"
+#include "DFTElementState.h"
+
+
+namespace storm {
+    namespace storage {
+       
+        class DFT; 
+        template<typename T>
+        class DFTBE;
+        
+        
+        
+        class DFTState {
+            friend struct std::hash<DFTState>;
+        private:
+            storm::storage::BitVector mStatus;
+            std::vector<size_t> mInactiveSpares;
+            std::vector<size_t> mIsCurrentlyFailableBE;
+            std::vector<size_t> mUsedRepresentants;
+            bool mValid = true;
+            const DFT& mDft;
+            
+        public:
+            DFTState(DFT const& dft);
+            
+            DFTElementState getElementState(size_t id) const;
+            
+            bool isOperational(size_t id) const;
+            
+            bool hasFailed(size_t id) const;
+            
+            bool isFailsafe(size_t id) const ;
+            
+            bool dontCare(size_t id) const;
+            
+            void setFailed(size_t id);
+            
+            void setFailsafe(size_t id);
+            
+            void setDontCare(size_t id);
+            
+            void beNoLongerFailable(size_t id);
+            
+            void activate(size_t repr);
+            
+            bool isActiveSpare(size_t id) const;
+            
+            void markAsInvalid() {
+                mValid = false;
+            }
+           
+            bool isInvalid() {
+                return !mValid;
+            }
+            
+            storm::storage::BitVector const& status() const {
+                return mStatus;
+            }
+           
+            /**
+             * This method gets the usage information for a spare
+             * @param id Id of the spare
+             * @return The child that currently is used.
+             */
+            uint_fast64_t uses(size_t id) const;
+            
+            /**
+             * This method is commonly used to get the usage information for spares. 
+             * @param from Starting index where the usage info is.
+             * @return The child that currently is used.
+             */
+            uint_fast64_t extractUses(size_t from) const;
+            
+            /**
+             * Checks whether an element is currently used.
+             * @param child The id of the child for which we want to know whether it is currently used.
+             * @return true iff it is currently used by any of the spares.
+             */
+            bool isUsed(size_t child);
+            
+            /**
+             * Sets to to the usageIndex which child is now used.
+             * @param usageIndex 
+             * @param child
+             */
+            void setUsesAtPosition(size_t usageIndex, size_t child);
+            
+            
+            
+            bool claimNew(size_t spareId, size_t usageIndex, size_t currentlyUses, std::vector<size_t> const& childIds);
+            
+            bool hasOutgoingEdges() const {
+                return !mIsCurrentlyFailableBE.empty();
+            }
+            
+            size_t nrFailableBEs() const {
+                return mIsCurrentlyFailableBE.size();
+            }
+            
+            std::pair<std::shared_ptr<DFTBE<double>>, bool> letNextBEFail(size_t smallestIndex = 0);
+            
+            void printCurrentlyFailable(std::ostream& os) {
+                auto it = mIsCurrentlyFailableBE.begin();
+                os << "{";
+                if(it != mIsCurrentlyFailableBE.end()) {
+                    os << *it;
+                }
+                ++it;
+                while(it != mIsCurrentlyFailableBE.end()) {
+                    os << ", " << *it;
+                    ++it;
+                }
+                os << "}" << std::endl;
+            }
+            
+            friend bool operator==(DFTState const& a, DFTState const& b) {
+                return a.mStatus == b.mStatus;
+            }
+        };
+
+    }
+}
+
+namespace std {
+    template<>
+    struct hash<storm::storage::DFTState> {
+        size_t operator()(storm::storage::DFTState const& s) const {
+            return hash<storm::storage::BitVector>()(s.mStatus);
+        }
+    };
+}
+
+#endif	/* DFTSTATE_H */
+

src/storage/dft/DFTStateSpaceGenerationQueues.h

@@ -0,0 +1,78 @@
+#ifndef DFTSTATESPACEGENERATIONQUEUES_H
+#define	DFTSTATESPACEGENERATIONQUEUES_H
+
+#include <list>
+#include <queue>
+#include <vector>
+#include <deque>
+
+#include "OrderDFTElementsById.h"
+
+namespace storm {
+    namespace storage {
+        class DFTGate;
+        class DFTElement;
+        
+    
+        
+        class DFTStateSpaceGenerationQueues {
+            std::priority_queue<std::shared_ptr<DFTGate>, std::vector<std::shared_ptr<DFTGate>>, OrderElementsByRank> failurePropagation;
+            std::vector<std::shared_ptr<DFTGate>> failsafePropagation;
+            std::vector<std::shared_ptr<DFTElement>> dontcarePropagation;
+            std::vector<std::shared_ptr<DFTElement>> activatePropagation;
+
+        public:
+            void propagateFailure(std::shared_ptr<DFTGate> const& elem) {
+                failurePropagation.push(elem);
+            }
+
+            bool failurePropagationDone() const {
+                return failurePropagation.empty();
+            }
+
+            std::shared_ptr<DFTGate> nextFailurePropagation() {
+                std::shared_ptr<DFTGate> next= failurePropagation.top();
+                failurePropagation.pop();
+                return next;
+            }
+            
+            bool failsafePropagationDone() const {
+                return failsafePropagation.empty();
+            }
+            
+            void propagateFailsafe(std::shared_ptr<DFTGate> const& gate) {
+                failsafePropagation.push_back(gate);
+            }
+            
+            std::shared_ptr<DFTGate> nextFailsafePropagation() {
+                std::shared_ptr<DFTGate> next = failsafePropagation.back();
+                failsafePropagation.pop_back();
+                return next;
+            }
+            
+            bool dontCarePropagationDone() const {
+                return dontcarePropagation.empty();
+            }
+            
+            void propagateDontCare(std::shared_ptr<DFTElement> const& elem) {
+                dontcarePropagation.push_back(elem);
+            }
+            
+            void propagateDontCare(std::vector<std::shared_ptr<DFTElement>> const& elems) {
+                dontcarePropagation.insert(dontcarePropagation.end(), elems.begin(), elems.end());
+            }
+            
+            std::shared_ptr<DFTElement> nextDontCarePropagation() {
+                std::shared_ptr<DFTElement> next = dontcarePropagation.back();
+                dontcarePropagation.pop_back();
+                return next;
+            }
+        };
+    }
+    
+}
+
+
+
+#endif	/* DFTSTATESPACEGENERATIONQUEUES_H */
+

src/storage/dft/OrderDFTElementsById.cpp

@@ -0,0 +1,18 @@
+#include "OrderDFTElementsById.h"
+#include "DFTElements.h"
+
+namespace storm {
+    namespace storage {
+        bool OrderElementsById::operator()(std::shared_ptr<DFTGate> const& a , std::shared_ptr<DFTGate> const& b) const {
+            return a->id() < b->id();
+        }
+        bool OrderElementsById::operator ()(const std::shared_ptr<DFTElement>& a, const std::shared_ptr<DFTElement>& b) const {
+            return a->id() < b->id();
+        }
+        
+        
+        bool OrderElementsByRank::operator ()(const std::shared_ptr<DFTGate>& a, const std::shared_ptr<DFTGate>& b) const {
+            return a->rank() < b->rank();
+        }
+    }
+}

src/storage/dft/OrderDFTElementsById.h

@@ -0,0 +1,24 @@
+#ifndef ORDERDFTELEMENTS_H
+#define	ORDERDFTELEMENTS_H
+
+#include <memory>
+
+namespace storm {
+    namespace storage {
+        class DFTGate;
+        class DFTElement;
+        
+        struct OrderElementsById {
+            bool operator()(std::shared_ptr<DFTGate> const& a , std::shared_ptr<DFTGate> const& b) const;
+            bool operator()(std::shared_ptr<DFTElement> const& a, std::shared_ptr<DFTElement> const& b) const;
+        };
+        
+        struct OrderElementsByRank {
+            bool operator()(std::shared_ptr<DFTGate> const& a, std::shared_ptr<DFTGate> const& b) const;
+        };
+
+    }
+}
+
+#endif	/* ORDERDFTELEMENTSBYID_H */
+

src/storm-dyftee.cpp

@@ -0,0 +1,22 @@
+#include "parser/DFTGalileoParser.h"
+#include "utility/initialize.h"
+#include "builder/ExplicitDFTModelBuilder.h"
+
+
+/*
+ * Entry point for the DyFTeE backend.
+ */
+int main(int argc, char** argv) {
+    if(argc != 2) {
+        std::cout <<  "Storm-DyFTeE should be called with a filename as argument." << std::endl;
+    }
+    storm::utility::initialize::setUp();
+    
+    storm::parser::DFTGalileoParser parser;
+    storm::storage::DFT dft = parser.parseDFT(argv[1]);
+    dft.printElements();
+    dft.printSpareModules();
+    storm::builder::ExplicitDFTModelBuilder builder(dft);
+    builder.buildCtmc();
+}
+

src/utility/cli.h

@@ -35,17 +35,7 @@
 #include "lib/smtrat.h"
 #endif
 
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-#include "log4cplus/consoleappender.h"
-#include "log4cplus/fileappender.h"
-log4cplus::Logger logger;
-log4cplus::Logger printer;
 
-// Headers that provide auxiliary functionality.
-#include "src/utility/storm-version.h"
-#include "src/utility/OsDetection.h"
-#include "src/settings/SettingsManager.h"
 
 // Headers related to parsing.
 #include "src/parser/AutoParser.h"
@@ -93,44 +83,6 @@ namespace storm {
     namespace utility {
         namespace cli {
             
-            /*!
-             * Initializes the logging framework and sets up logging to console.
-             */
-            void initializeLogger() {
-                logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main"));
-                log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender());
-                consoleLogAppender->setName("mainConsoleAppender");
-                consoleLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n")));
-                logger.addAppender(consoleLogAppender);
-                auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL;
-                logger.setLogLevel(loglevel);
-                consoleLogAppender->setThreshold(loglevel);
-            }
-            
-            /*!
-             * Performs some necessary initializations.
-             */
-            void setUp() {
-                initializeLogger();
-                std::cout.precision(10);
-            }
-            
-            /*!
-             * Performs some necessary clean-up.
-             */
-            void cleanUp() {
-                // Intentionally left empty.
-            }
-            
-            /*!
-             * Sets up the logging to file.
-             */
-            void initializeFileLogging() {
-                log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(storm::settings::debugSettings().getLogfilename()));
-                fileLogAppender->setName("mainFileAppender");
-                fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n")));
-                logger.addAppender(fileLogAppender);
-            }
             
             /*!
              * Gives the current working directory

src/utility/initialize.h

@@ -0,0 +1,68 @@
+
+
+#ifndef INITIALIZE_H
+#define	INITIALIZE_H
+
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+#include "log4cplus/consoleappender.h"
+#include "log4cplus/fileappender.h"
+log4cplus::Logger logger;
+log4cplus::Logger printer;
+
+
+// Headers that provide auxiliary functionality.
+#include "src/utility/storm-version.h"
+#include "src/utility/OsDetection.h"
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+    namespace utility {
+        namespace initialize {
+            
+            /*!
+             * Initializes the logging framework and sets up logging to console.
+             */
+            void initializeLogger() {
+                logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main"));
+                log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender());
+                consoleLogAppender->setName("mainConsoleAppender");
+                consoleLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n")));
+                logger.addAppender(consoleLogAppender);
+                auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL;
+                logger.setLogLevel(loglevel);
+                consoleLogAppender->setThreshold(loglevel);
+            }
+            
+            /*!
+             * Performs some necessary initializations.
+             */
+            void setUp() {
+                initializeLogger();
+                std::cout.precision(10);
+            }
+            
+            /*!
+             * Performs some necessary clean-up.
+             */
+            void cleanUp() {
+                // Intentionally left empty.
+            }
+            
+            /*!
+             * Sets up the logging to file.
+             */
+            void initializeFileLogging() {
+                log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(storm::settings::debugSettings().getLogfilename()));
+                fileLogAppender->setName("mainFileAppender");
+                fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n")));
+                logger.addAppender(fileLogAppender);
+            }
+            
+        }
+    }
+}
+
+#endif	/* INITIALIZE_H */
+

src/utility/math.h

@@ -17,6 +17,14 @@ namespace storm {
                 return std::log(number) / std::log(2);
 #		endif
             }
+            
+            inline uint64_t uint64_log2(uint64_t n)
+            {
+                assert(n != 0);
+                #define S(k) if (n >= (UINT64_C(1) << k)) { i += k; n >>= k; }
+                uint64_t i = 0; S(32); S(16); S(8); S(4); S(2); S(1); return i;
+                #undef S
+            }
         }
     }
 }