From 9c226f8336d94f5c1a3b409e914d5d5e5b0f1871 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 11 Apr 2019 11:02:45 +0200 Subject: [PATCH] Added support for MUTEX (but without DC support) --- src/storm-dft/builder/DFTBuilder.cpp | 5 +- src/storm-dft/parser/DFTGalileoParser.cpp | 2 + src/storm-dft/parser/DFTJsonParser.cpp | 2 + src/storm-dft/storage/dft/DFTElements.h | 3 +- src/storm-dft/storage/dft/DftJsonExporter.cpp | 5 +- src/storm-dft/storage/dft/elements/DFTMutex.h | 61 +++++++++++++++++++ .../storage/dft/elements/DFTRestriction.h | 56 +---------------- src/storm-dft/storage/dft/elements/DFTSeq.h | 59 ++++++++++++++++++ 8 files changed, 134 insertions(+), 59 deletions(-) create mode 100644 src/storm-dft/storage/dft/elements/DFTMutex.h create mode 100644 src/storm-dft/storage/dft/elements/DFTSeq.h diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index 3c856407b..fce5d7962 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -137,7 +137,7 @@ namespace storm { template bool DFTBuilder::addRestriction(std::string const& name, std::vector const& children, storm::storage::DFTElementType tp) { if (children.size() <= 1) { - STORM_LOG_ERROR("Sequence enforcers require at least two children"); + STORM_LOG_ERROR("Restrictions require at least two children"); } if (nameInUse(name)) { STORM_LOG_ERROR("Element with name '" << name << "' already exists."); @@ -149,8 +149,7 @@ namespace storm { restr = std::make_shared>(mNextId++, name); break; case storm::storage::DFTElementType::MUTEX: - // TODO notice that mutex state generation support is lacking anyway, as DONT CARE propagation would be broken for this. - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); + restr = std::make_shared>(mNextId++, name); break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index bf1dced78..8d44637f9 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -137,6 +137,8 @@ namespace storm { success = builder.addSpareElement(name, childNames); } else if (type == "seq") { success = builder.addSequenceEnforcer(name, childNames); + } else if (type == "mutex") { + success = builder.addMutex(name, childNames); } else if (type == "fdep") { STORM_LOG_THROW(childNames.size() >= 2, storm::exceptions::WrongFormatException, "FDEP gate needs at least two children in line " << lineNo << "."); success = builder.addDepElement(name, childNames, storm::utility::one()); diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 7975a0d5b..96eeeb762 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -88,6 +88,8 @@ namespace storm { success = builder.addSpareElement(name, childNames); } else if (type == "seq") { success = builder.addSequenceEnforcer(name, childNames); + } else if (type == "mutex") { + success = builder.addMutex(name, childNames); } else if (type == "fdep") { success = builder.addDepElement(name, childNames, storm::utility::one()); } else if (type == "pdep") { diff --git a/src/storm-dft/storage/dft/DFTElements.h b/src/storm-dft/storage/dft/DFTElements.h index 3173446fb..36d671703 100644 --- a/src/storm-dft/storage/dft/DFTElements.h +++ b/src/storm-dft/storage/dft/DFTElements.h @@ -4,9 +4,10 @@ #include "storm-dft/storage/dft/elements/BEConst.h" #include "storm-dft/storage/dft/elements/DFTAnd.h" #include "storm-dft/storage/dft/elements/DFTDependency.h" +#include "storm-dft/storage/dft/elements/DFTMutex.h" #include "storm-dft/storage/dft/elements/DFTOr.h" #include "storm-dft/storage/dft/elements/DFTPand.h" #include "storm-dft/storage/dft/elements/DFTPor.h" -#include "storm-dft/storage/dft/elements/DFTRestriction.h" +#include "storm-dft/storage/dft/elements/DFTSeq.h" #include "storm-dft/storage/dft/elements/DFTSpare.h" #include "storm-dft/storage/dft/elements/DFTVot.h" diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 2eb811095..9ff66615e 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -61,10 +61,11 @@ namespace storm { nodeData["voting"] = std::static_pointer_cast const>(element)->threshold(); } } else if (element->isRestriction()) { + // TODO use same method for gates and restrictions // Set children for restriction - auto seq = std::static_pointer_cast const>(element); + auto restriction = std::static_pointer_cast const>(element); std::vector children; - for (DFTElementPointer const& child : seq->children()) { + for (DFTElementPointer const& child : restriction->children()) { children.push_back(std::to_string(child->id())); } nodeData["children"] = children; diff --git a/src/storm-dft/storage/dft/elements/DFTMutex.h b/src/storm-dft/storage/dft/elements/DFTMutex.h new file mode 100644 index 000000000..cbc18a69b --- /dev/null +++ b/src/storm-dft/storage/dft/elements/DFTMutex.h @@ -0,0 +1,61 @@ +#pragma once + +#include "DFTRestriction.h" + +namespace storm { + namespace storage { + + /*! + * Mutex restriction (MUTEX). + * Only one of the children can fail. + * A child which has failed prevents the failure of all other children. + */ + template + class DFTMutex : public DFTRestriction { + + public: + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param children Children. + */ + DFTMutex(size_t id, std::string const& name, std::vector>> const& children = {}) : DFTRestriction(id, name, children) { + // Intentionally left empty. + } + + DFTElementType type() const override { + return DFTElementType::MUTEX; + } + + bool isSeqEnforcer() const override { + return true; + } + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished."); + bool childFailed = false; + for (auto const& child : this->children()) { + if (state.hasFailed(child->id())) { + if (childFailed) { + // Two children have failed + this->fail(state, queues); + return; + } else { + childFailed = true; + } + } + } + } + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + } + + bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + // Actually, it doesnt matter what we return here.. + return false; + } + }; + + } +} diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h index b83ba44f7..92c9a69ec 100644 --- a/src/storm-dft/storage/dft/elements/DFTRestriction.h +++ b/src/storm-dft/storage/dft/elements/DFTRestriction.h @@ -61,70 +61,20 @@ namespace storm { // Do nothing } - bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { + bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { return false; } protected: - void fail(DFTState & state, DFTStateSpaceGenerationQueues & queues) const override { + void fail(DFTState & state, DFTStateSpaceGenerationQueues& queues) const override { state.markAsInvalid(); } - void failsafe(DFTState & state, DFTStateSpaceGenerationQueues & queues) const override { + void failsafe(DFTState & state, DFTStateSpaceGenerationQueues& queues) const override { // Do nothing } }; - - /*! - * Sequence enforcer (SEQ). - * All children can only fail in order from first to last child. - * A child which has not failed yet prevents the failure of all children to the right of it. - */ - template - class DFTSeq : public DFTRestriction { - - public: - /*! - * Constructor. - * @param id Id. - * @param name Name. - * @param children Children. - */ - DFTSeq(size_t id, std::string const& name, std::vector>> const&children = {}) : DFTRestriction(id, name, children) { - // Intentionally left empty. - } - - DFTElementType type() const override { - return DFTElementType::SEQ; - } - - bool isSeqEnforcer() const override { - return true; - } - - void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { - STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished."); - bool childOperationalBefore = false; - for (auto const& child : this->children()) { - if (!state.hasFailed(child->id())) { - childOperationalBefore = true; - } else if (childOperationalBefore && state.hasFailed(child->id())) { - this->fail(state, queues); - return; - } - } - } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { - } - - bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { - // Actually, it doesnt matter what we return here.. - return false; - } - }; - } } diff --git a/src/storm-dft/storage/dft/elements/DFTSeq.h b/src/storm-dft/storage/dft/elements/DFTSeq.h new file mode 100644 index 000000000..8cef64e21 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/DFTSeq.h @@ -0,0 +1,59 @@ +#pragma once + +#include "DFTRestriction.h" + +namespace storm { + namespace storage { + + /*! + * Sequence enforcer (SEQ). + * All children can only fail in order from first to last child. + * A child which has not failed yet prevents the failure of all children to the right of it. + */ + template + class DFTSeq : public DFTRestriction { + + public: + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param children Children. + */ + DFTSeq(size_t id, std::string const& name, std::vector>> const& children = {}) : DFTRestriction(id, name, children) { + // Intentionally left empty. + } + + DFTElementType type() const override { + return DFTElementType::SEQ; + } + + bool isSeqEnforcer() const override { + return true; + } + + void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + STORM_LOG_ASSERT(queues.failurePropagationDone(), "Failure propagation not finished."); + bool childOperationalBefore = false; + for (auto const& child : this->children()) { + if (!state.hasFailed(child->id())) { + childOperationalBefore = true; + } else if (childOperationalBefore && state.hasFailed(child->id())) { + // Child has failed before left sibling. + this->fail(state, queues); + return; + } + } + } + + void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + } + + bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { + // Actually, it doesnt matter what we return here.. + return false; + } + }; + + } +}