From 8755e75a60f12bc9e9cf91fd9ccbfe2367bc623c Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 19 Feb 2016 18:13:05 +0100 Subject: [PATCH] towards a new element (and actually added a folder) Former-commit-id: 0bca77dfa7b9800ef60225ca2fcc3e01d5e1e157 --- src/CMakeLists.txt | 2 + src/storage/dft/DFTElementType.h | 7 ++- src/storage/dft/DFTElements.h | 54 ----------------------- src/storage/dft/elements/DFTRestriction.h | 13 ++++++ 4 files changed, 18 insertions(+), 58 deletions(-) create mode 100644 src/storage/dft/elements/DFTRestriction.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3aa121a0a..60fbadab9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -38,6 +38,7 @@ file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SO file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp) file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) file(GLOB STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/*.cpp) +file(GLOB STORM_STORAGE_DFT_ELEMENTS_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/elements/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/elements/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) @@ -94,6 +95,7 @@ source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES}) source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES}) source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES}) source_group(storage\\dft FILES ${STORM_STORAGE_DFT_FILES}) +source_group(storage\\dft\\elements FILES ${STORM_STORAGE_DFT_ELEMENTS_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) # Add custom additional include or link directories diff --git a/src/storage/dft/DFTElementType.h b/src/storage/dft/DFTElementType.h index a32745cdf..d4bf3bfc2 100644 --- a/src/storage/dft/DFTElementType.h +++ b/src/storage/dft/DFTElementType.h @@ -4,20 +4,20 @@ namespace storm { namespace storage { - enum class DFTElementType : int {AND = 0, COUNTING = 1, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQAND = 11}; + enum class DFTElementType : int {AND = 0, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQ = 11, MUTEX=12}; inline bool isGateType(DFTElementType const& tp) { switch(tp) { case DFTElementType::AND: - case DFTElementType::COUNTING: case DFTElementType::OR: case DFTElementType::VOT: case DFTElementType::PAND: case DFTElementType::SPARE: case DFTElementType::POR: - case DFTElementType::SEQAND: return true; + case DFTElementType::SEQ: + case DFTElementType::MUTEX: case DFTElementType::BE: case DFTElementType::CONSTF: case DFTElementType::CONSTS: @@ -40,7 +40,6 @@ namespace storm { case DFTElementType::POR: case DFTElementType::SPARE: case DFTElementType::PAND: - case DFTElementType::SEQAND: return false; default: assert(false); diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 11fc31948..c51e180c7 100644 --- a/src/storage/dft/DFTElements.h +++ b/src/storage/dft/DFTElements.h @@ -726,60 +726,6 @@ namespace storm { - template - 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(this->mId)) { - bool childOperationalBefore = false; - for(auto const& child : this->mChildren) - { - if(!state.hasFailed(child->id())) { - childOperationalBefore = true; - } - else { - if(childOperationalBefore) { - state.markAsInvalid(); - return; - } - } - } - if(!childOperationalBefore) { - fail(state, queues); - } - - } - } - - void checkFailsafe(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const{ - assert(hasFailsafeChild(state)); - if(state.isOperational(this->mId)) { - failsafe(state, queues); - //return true; - } - //return false; - } - - virtual DFTElementType type() const override { - return DFTElementType::SEQAND; - } - - std::string typestring() const override { - return "SEQAND"; - } - }; - - template - inline std::ostream& operator<<(std::ostream& os, DFTSeqAnd const& gate) { - return os << gate.toString(); - } - - template class DFTPand : public DFTGate { diff --git a/src/storage/dft/elements/DFTRestriction.h b/src/storage/dft/elements/DFTRestriction.h new file mode 100644 index 000000000..8bd586deb --- /dev/null +++ b/src/storage/dft/elements/DFTRestriction.h @@ -0,0 +1,13 @@ +#pragma once + +#include "../DFTElements.h" + +namespace storm { + namespace storage { + template + class DFTRestriction : public DFTElement { + + }; + + } +} \ No newline at end of file