diff --git a/src/builder/ExplicitDFTModelBuilder.h b/src/builder/ExplicitDFTModelBuilder.h new file mode 100644 index 000000000..e8c169976 --- /dev/null +++ b/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 mStateIndices; + size_t newIndex = 0; + //std::stack> 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>, 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 parent : nextBE.first->parents()) { + if(newState.isOperational(parent->id())) { + queues.propagateFailure(parent); + } + } + + + + while(!queues.failurePropagationDone()) { + std::shared_ptr next = queues.nextFailurePropagation(); + next->checkFails(newState, queues); + } + + while(!queues.failsafePropagationDone()) { + std::shared_ptr next = queues.nextFailsafePropagation(); + next->checkFailsafe(newState, queues); + } + + while(!queues.dontCarePropagationDone()) { + std::shared_ptr 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 */ + diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp new file mode 100644 index 000000000..79e969260 --- /dev/null +++ b/src/parser/DFTGalileoParser.cpp @@ -0,0 +1,102 @@ +#include "DFTGalileoParser.h" + +#include +#include +#include +#include +#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 tokens; + boost::split(tokens, line, boost::is_any_of(" ")); + std::string name(stripQuotsFromName(tokens[0])); + + std::vector 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(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(tokens[1].substr(7)), boost::lexical_cast(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; + } + + + } +} \ No newline at end of file diff --git a/src/parser/DFTGalileoParser.h b/src/parser/DFTGalileoParser.h new file mode 100644 index 000000000..3dc6f11eb --- /dev/null +++ b/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 + + + +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 */ + diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 923916793..f74ac0312 100644 --- a/src/storage/BitVector.cpp +++ b/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(bucketCount, 0); } + } template @@ -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."); diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index ec4cce693..4759d358c 100644 --- a/src/storage/BitVector.h +++ b/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. * diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp new file mode 100644 index 000000000..e06661988 --- /dev/null +++ b/src/storage/dft/DFT.cpp @@ -0,0 +1,121 @@ +#include "DFT.h" + +namespace storm { + namespace storage { + + DFT::DFT(std::vector> const& elements, std::shared_ptr 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(elem)->children()) { + if(mActivationIndex.count(spareReprs->id()) == 0) { + mActivationIndex[spareReprs->id()] = stateIndex++; + } + std::set module = {spareReprs->id()}; + spareReprs->extendSpareModule(module); + std::vector 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(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 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(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::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::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; + + + } + } + } +} diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h new file mode 100644 index 000000000..1f8939fd7 --- /dev/null +++ b/src/storage/dft/DFT.h @@ -0,0 +1,184 @@ + +#ifndef DFT_H +#define DFT_H + + +#include "DFTElements.h" +#include "../BitVector.h" +#include +#include +#include +#include + +#include "../../utility/math.h" +#include + +namespace storm { + namespace storage { + + + struct DFTElementSort { + bool operator()(std::shared_ptr const& a, std::shared_ptr const& b) const { + if (a->rank() == 0 && b->rank() == 0) { + return a->isConstant(); + } else { + return a->rank() < b->rank(); + } + } + }; + + class DFT { + + + + private: + std::vector> mElements; + size_t mNrOfBEs; + size_t mNrOfSpares; + size_t mTopLevelIndex; + size_t mUsageInfoBits; + size_t mStateSize; + std::map mActivationIndex; + std::map> mSpareModules; + std::vector mTopModule; + std::vector mIdToFailureIndex; + std::map mUsageIndex; + + + public: + DFT(std::vector> const& elements, std::shared_ptr 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(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 getSpareIndices() const { + std::vector indices; + for(auto const& elem : mElements) { + if(elem->isSpareGate()) { + indices.push_back(elem->id()); + } + } + return indices; + } + + std::vector 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 nonColdBEs() const { + std::vector result; + for(std::shared_ptr elem : mElements) { + if(elem->isBasicElement() && !elem->isColdBasicElement()) { + result.push_back(elem->id()); + } + } + return result; + } + + std::shared_ptr const& getElement(size_t index) const { + assert(index < nrElements()); + return mElements[index]; + } + + std::shared_ptr> getBasicElement(size_t index) const { + assert(mElements[index]->isBasicElement()); + return std::static_pointer_cast>(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 */ + diff --git a/src/storage/dft/DFTBuilder.cpp b/src/storage/dft/DFTBuilder.cpp new file mode 100644 index 000000000..f6364a523 --- /dev/null +++ b/src/storage/dft/DFTBuilder.cpp @@ -0,0 +1,132 @@ + + +#include "DFTBuilder.h" + +#include "DFT.h" +#include +#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 gate = std::static_pointer_cast(elem.first); + gate->pushBackChild(mElements[child]); + mElements[child]->addParent(gate); + } + } + + // Sort elements topologically + + + + // compute rank + for (auto& elem : mElements) { + computeRank(elem.second); + } + + std::vector> elems = topoSort(); + size_t id = 0; + for(std::shared_ptr 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 const& elem) { + if(elem->rank() == -1) { + if(elem->nrChildren() == 0) { + elem->setRank(0); + return 0; + } + std::shared_ptr gate = std::static_pointer_cast(elem); + unsigned maxrnk = 0; + unsigned newrnk = 0; + + for(std::shared_ptr 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 const& children, DFTElementTypes tp) { + assert(children.size() > 0); + if(mElements.count(name) != 0) { + // Element with that name already exists. + return false; + } + std::shared_ptr element; + switch(tp) { + case DFTElementTypes::AND: + element = std::make_shared(mNextId++, name); + break; + case DFTElementTypes::OR: + element = std::make_shared(mNextId++, name); + break; + case DFTElementTypes::PAND: + element = std::make_shared(mNextId++, name); + break; + case DFTElementTypes::POR: + element = std::make_shared(mNextId++, name); + break; + case DFTElementTypes::SPARE: + element = std::make_shared(mNextId++, name); + break; + } + mElements[name] = element; + mChildNames[element] = children; + return true; + } + + + void DFTBuilder::topoVisit(std::shared_ptr const& n, std::map, topoSortColour>& visited, std::vector>& 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 const& c : std::static_pointer_cast(n)->children()) { + topoVisit(c, visited, L); + } + } + visited[n] = topoSortColour::BLACK; + L.push_back(n); + + } + } + + std::vector> DFTBuilder::topoSort() { + std::map, topoSortColour> visited; + for(auto const& e : mElements) { + visited.insert(std::make_pair(e.second, topoSortColour::WHITE)); + } + + std::vector> L; + for(auto const& e : visited) { + topoVisit(e.first, visited, L); + } + //std::reverse(L.begin(), L.end()); + return L; + } + + } +} + diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h new file mode 100644 index 000000000..e29a8aa02 --- /dev/null +++ b/src/storage/dft/DFTBuilder.h @@ -0,0 +1,116 @@ + +#ifndef DFTBUILDER_H +#define DFTBUILDER_H + +#include "DFTElements.h" +#include +#include +#include + +namespace storm { + namespace storage { + class DFT; + + class DFTBuilder { + + std::size_t mNextId = 0; + std::string topLevelIdentifier; + std::unordered_map> mElements; + std::unordered_map, std::vector> mChildNames; + + public: + DFTBuilder() { + + } + + bool addAndElement(std::string const& name, std::vector const& children) { + return addStandardGate(name, children, DFTElementTypes::AND); + } + + bool addOrElement(std::string const& name, std::vector const& children) { + return addStandardGate(name, children, DFTElementTypes::OR); + } + + bool addPandElement(std::string const& name, std::vector const& children) { + return addStandardGate(name, children, DFTElementTypes::PAND); + } + + bool addPorElement(std::string const& name, std::vector const& children) { + return addStandardGate(name, children, DFTElementTypes::POR); + } + + bool addSpareElement(std::string const& name, std::vector const& children) { + return addStandardGate(name, children, DFTElementTypes::SPARE); + } + + + + bool addVotElement(std::string const& name, unsigned threshold, std::vector 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 element = std::make_shared(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>(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 const& elem); + + bool addStandardGate(std::string const& name, std::vector const& children, DFTElementTypes tp); + + enum class topoSortColour {WHITE, BLACK, GREY}; + + void topoVisit(std::shared_ptr const& n, std::map, topoSortColour>& visited, std::vector>& L); + std::vector> topoSort(); + + + }; + } +} + + + +#endif /* DFTBUILDER_H */ + diff --git a/src/storage/dft/DFTElementState.h b/src/storage/dft/DFTElementState.h new file mode 100644 index 000000000..1926745bf --- /dev/null +++ b/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 */ + diff --git a/src/storage/dft/DFTElements.cpp b/src/storage/dft/DFTElements.cpp new file mode 100644 index 000000000..b96ceafb4 --- /dev/null +++ b/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 const& parent : mParents) { + if(state.isOperational(parent->id())) { + return false; + } + } + state.setDontCare(mId); + return true; + + } + return false; + } + + void DFTElement::extendSpareModule(std::set& 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::checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + if(DFTElement::checkDontCareAnymore(state, queues)) { + state.beNoLongerFailable(mId); + return true; + } + return false; + } + } +} diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h new file mode 100644 index 000000000..9d3338022 --- /dev/null +++ b/src/storage/dft/DFTElements.h @@ -0,0 +1,635 @@ +#ifndef DFTELEMENTS_H +#define DFTELEMENTS_H + +#include +#include +#include +#include +#include +#include +#include + +#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> 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 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> const& parents() const { + return mParents; + } + + virtual void extendSpareModule(std::set& 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> mChildren; + public: + DFTGate(size_t id, std::string const& name, std::vector> const& children) : + DFTElement(id, name), mChildren(children) + {} + + virtual ~DFTGate() {} + + void pushBackChild(std::shared_ptr elem) { + return mChildren.push_back(elem); + } + + size_t nrChildren() const { + return mChildren.size(); + } + + std::vector> 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& 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>::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 parent : mParents) { + if(state.isOperational(parent->id())) { + queues.propagateFailure(parent); + } + } + state.setFailed(mId); + } + + void failsafe(DFTState& state, DFTStateSpaceGenerationQueues& queues) const { + for(std::shared_ptr 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 + 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 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> 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> 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> 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> 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> 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> 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> 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 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 */ + diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp new file mode 100644 index 000000000..5536b05a6 --- /dev/null +++ b/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 alwaysActiveBEs = dft.nonColdBEs(); + mIsCurrentlyFailableBE.insert(mIsCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); + + } + + DFTElementState DFTState::getElementState(size_t id) const { + return static_cast(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(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>, bool> DFTState::letNextBEFail(size_t index) + { + assert(index < mIsCurrentlyFailableBE.size()); + //std::cout << "currently failable: "; + //printCurrentlyFailable(std::cout); + std::pair>,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 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 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; + } + } +} diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h new file mode 100644 index 000000000..719d49e37 --- /dev/null +++ b/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 + class DFTBE; + + + + class DFTState { + friend struct std::hash; + private: + storm::storage::BitVector mStatus; + std::vector mInactiveSpares; + std::vector mIsCurrentlyFailableBE; + std::vector 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 const& childIds); + + bool hasOutgoingEdges() const { + return !mIsCurrentlyFailableBE.empty(); + } + + size_t nrFailableBEs() const { + return mIsCurrentlyFailableBE.size(); + } + + std::pair>, 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 { + size_t operator()(storm::storage::DFTState const& s) const { + return hash()(s.mStatus); + } + }; +} + +#endif /* DFTSTATE_H */ + diff --git a/src/storage/dft/DFTStateSpaceGenerationQueues.h b/src/storage/dft/DFTStateSpaceGenerationQueues.h new file mode 100644 index 000000000..f748e8232 --- /dev/null +++ b/src/storage/dft/DFTStateSpaceGenerationQueues.h @@ -0,0 +1,78 @@ +#ifndef DFTSTATESPACEGENERATIONQUEUES_H +#define DFTSTATESPACEGENERATIONQUEUES_H + +#include +#include +#include +#include + +#include "OrderDFTElementsById.h" + +namespace storm { + namespace storage { + class DFTGate; + class DFTElement; + + + + class DFTStateSpaceGenerationQueues { + std::priority_queue, std::vector>, OrderElementsByRank> failurePropagation; + std::vector> failsafePropagation; + std::vector> dontcarePropagation; + std::vector> activatePropagation; + + public: + void propagateFailure(std::shared_ptr const& elem) { + failurePropagation.push(elem); + } + + bool failurePropagationDone() const { + return failurePropagation.empty(); + } + + std::shared_ptr nextFailurePropagation() { + std::shared_ptr next= failurePropagation.top(); + failurePropagation.pop(); + return next; + } + + bool failsafePropagationDone() const { + return failsafePropagation.empty(); + } + + void propagateFailsafe(std::shared_ptr const& gate) { + failsafePropagation.push_back(gate); + } + + std::shared_ptr nextFailsafePropagation() { + std::shared_ptr next = failsafePropagation.back(); + failsafePropagation.pop_back(); + return next; + } + + bool dontCarePropagationDone() const { + return dontcarePropagation.empty(); + } + + void propagateDontCare(std::shared_ptr const& elem) { + dontcarePropagation.push_back(elem); + } + + void propagateDontCare(std::vector> const& elems) { + dontcarePropagation.insert(dontcarePropagation.end(), elems.begin(), elems.end()); + } + + std::shared_ptr nextDontCarePropagation() { + std::shared_ptr next = dontcarePropagation.back(); + dontcarePropagation.pop_back(); + return next; + } + }; + } + +} + + + +#endif /* DFTSTATESPACEGENERATIONQUEUES_H */ + diff --git a/src/storage/dft/OrderDFTElementsById.cpp b/src/storage/dft/OrderDFTElementsById.cpp new file mode 100644 index 000000000..017969848 --- /dev/null +++ b/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 const& a , std::shared_ptr const& b) const { + return a->id() < b->id(); + } + bool OrderElementsById::operator ()(const std::shared_ptr& a, const std::shared_ptr& b) const { + return a->id() < b->id(); + } + + + bool OrderElementsByRank::operator ()(const std::shared_ptr& a, const std::shared_ptr& b) const { + return a->rank() < b->rank(); + } + } +} diff --git a/src/storage/dft/OrderDFTElementsById.h b/src/storage/dft/OrderDFTElementsById.h new file mode 100644 index 000000000..8dfc22da0 --- /dev/null +++ b/src/storage/dft/OrderDFTElementsById.h @@ -0,0 +1,24 @@ +#ifndef ORDERDFTELEMENTS_H +#define ORDERDFTELEMENTS_H + +#include + +namespace storm { + namespace storage { + class DFTGate; + class DFTElement; + + struct OrderElementsById { + bool operator()(std::shared_ptr const& a , std::shared_ptr const& b) const; + bool operator()(std::shared_ptr const& a, std::shared_ptr const& b) const; + }; + + struct OrderElementsByRank { + bool operator()(std::shared_ptr const& a, std::shared_ptr const& b) const; + }; + + } +} + +#endif /* ORDERDFTELEMENTSBYID_H */ + diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp new file mode 100644 index 000000000..39b614f8c --- /dev/null +++ b/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(); +} + diff --git a/src/utility/cli.h b/src/utility/cli.h index 40f50acfa..1a44610f4 100644 --- a/src/utility/cli.h +++ b/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(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(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); - logger.addAppender(fileLogAppender); - } /*! * Gives the current working directory diff --git a/src/utility/initialize.h b/src/utility/initialize.h new file mode 100644 index 000000000..a58e6d3c9 --- /dev/null +++ b/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(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(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); + logger.addAppender(fileLogAppender); + } + + } + } +} + +#endif /* INITIALIZE_H */ + diff --git a/src/utility/math.h b/src/utility/math.h index ba21bcfa1..b2c41adc2 100644 --- a/src/utility/math.h +++ b/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 + } } } }