diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index bb79be089..04b822914 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -26,7 +26,7 @@ namespace storm { std::unordered_map identifierMapping; public: - DFTGalileoParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { + DFTGalileoParser(bool defaultInclusive = true) : builder(defaultInclusive), manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { } storm::storage::DFT parseDFT(std::string const& filename); @@ -38,6 +38,8 @@ namespace storm { std::string parseNodeIdentifier(std::string const& name); ValueType parseRationalExpression(std::string const& expr); + + bool defaultInclusive; }; } } diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 612008226..10c84f5f6 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -144,10 +144,10 @@ namespace storm { element = std::make_shared>(mNextId++, name); break; case DFTElementType::PAND: - element = std::make_shared>(mNextId++, name); + element = std::make_shared>(mNextId++, name, pandDefaultInclusive); break; case DFTElementType::POR: - element = std::make_shared>(mNextId++, name); + element = std::make_shared>(mNextId++, name, porDefaultInclusive); break; case DFTElementType::SPARE: element = std::make_shared>(mNextId++, name); diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index f9a11d52b..55c1cb588 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -35,7 +35,7 @@ namespace storm { std::vector mRestrictions; public: - DFTBuilder() { + DFTBuilder(bool defaultInclusive = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive) { } @@ -51,6 +51,13 @@ namespace storm { return addStandardGate(name, children, DFTElementType::PAND); } + bool addPandElement(std::string const& name, std::vector const& children, bool inclusive) { + bool tmpDefault = pandDefaultInclusive; + bool result = addStandardGate(name, children, DFTElementType::PAND); + pandDefaultInclusive = tmpDefault; + return result; + } + bool addPorElement(std::string const& name, std::vector const& children) { return addStandardGate(name, children, DFTElementType::POR); } @@ -187,6 +194,11 @@ namespace storm { DFTElementVector topoSort(); + // If true, the standard gate adders make a pand inclusive, and exclusive otherwise. + bool pandDefaultInclusive; + // If true, the standard gate adders make a pand inclusive, and exclusive otherwise. + bool porDefaultInclusive; + }; } } diff --git a/src/storm-dft/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h index bb18efe72..d89e357b1 100644 --- a/src/storm-dft/storage/dft/elements/DFTPand.h +++ b/src/storm-dft/storage/dft/elements/DFTPand.h @@ -7,11 +7,13 @@ namespace storm { class DFTPand : public DFTGate { public: - DFTPand(size_t id, std::string const& name, std::vector>> const& children = {}) : - DFTGate(id, name, children) + DFTPand(size_t id, std::string const& name, bool inclusive, std::vector>> const& children = {}) : + DFTGate(id, name, children), + inclusive(inclusive) {} void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + assert(inclusive); if(state.isOperational(this->mId)) { bool childOperationalBefore = false; for(auto const& child : this->mChildren) @@ -31,6 +33,7 @@ namespace storm { } void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + bool(inclusive); STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child."); if(state.isOperational(this->mId)) { this->failsafe(state, queues); @@ -42,9 +45,15 @@ namespace storm { return DFTElementType::PAND; } + bool isInclusive() const { + return inclusive; + } + std::string typestring() const override { - return "PAND"; + return "PAND" + inclusive ? "" : "-ex"; } + protected: + bool inclusive; }; template diff --git a/src/storm-dft/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h index 6e2fe731c..3adaf16fc 100644 --- a/src/storm-dft/storage/dft/elements/DFTPor.h +++ b/src/storm-dft/storage/dft/elements/DFTPor.h @@ -6,12 +6,14 @@ namespace storm { template class DFTPor : public DFTGate { public: - DFTPor(size_t id, std::string const& name, std::vector>> const& children = {}) : - DFTGate(id, name, children) + DFTPor(size_t id, std::string const& name, bool inclusive, std::vector>> const& children = {}) : + DFTGate(id, name, children), + inclusive(inclusive) {} void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - if(state.isOperational(this->mId)) { + assert(inclusive); + if(state.isOperational(this->mId)) { if (state.hasFailed(this->mChildren.front()->id())) { // First child has failed before others this->fail(state, queues); @@ -28,6 +30,7 @@ namespace storm { } void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + assert(inclusive); if (state.isFailsafe(this->mChildren.front()->id())) { this->failsafe(state, queues); this->childrenDontCare(state, queues); @@ -39,8 +42,14 @@ namespace storm { } std::string typestring() const override { - return "POR"; + return "POR" + inclusive ? "" : "-ex"; } + + bool isInclusive() { + return inclusive; + } + protected: + bool inclusive; }; template