From 8d0046a9a7a2c2477e9bb0426df801b9f2794e1e Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 18 Feb 2016 15:44:31 +0100
Subject: [PATCH 1/4] Dftelements: equalType Former-commit-id:
77b9b382462ed78812fe866db851db130a3be68e
---
src/storage/dft/DFTElements.h | 42 ++++++++++++++++++++++++++++++-----
1 file changed, 37 insertions(+), 5 deletions(-)
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index e49b91901..b7fca51c0 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -122,7 +122,7 @@ namespace storm {
bool hasParents() const {
return !mParents.empty();
}
-
+
size_t nrParents() const {
return mParents.size();
}
@@ -194,7 +194,9 @@ namespace storm {
*/
virtual void extendSubDft(std::set<size_t> elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot) const;
-
+ virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
+ return type() == other.type();
+ }
protected:
@@ -368,7 +370,7 @@ namespace storm {
}
return false;
}
-
+
};
@@ -413,6 +415,13 @@ namespace storm {
bool isColdBasicElement() const override{
return storm::utility::isZero(mPassiveFailureRate);
}
+
+ bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+ DFTBE<ValueType> const& otherBE = static_cast<DFTBE<ValueType> const&>(other);
+ return (mActiveFailureRate == otherBE.mActiveFailureRate) && (mPassiveFailureRate == otherBE.mPassiveFailureRate);
+ }
+
virtual bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override;
};
@@ -454,6 +463,12 @@ namespace storm {
return 0;
}
+ bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+ DFTConst<ValueType> const& otherCNST = static_cast<DFTConst<ValueType> const&>(other);
+ return (mFailed == otherCNST.mFailed);
+ }
+
};
@@ -518,6 +533,13 @@ namespace storm {
virtual bool isDependency() const override {
return true;
}
+
+ virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+ DFTDependency<ValueType> const& otherDEP= static_cast<DFTDependency<ValueType> const&>(other);
+ return (mProbability == otherDEP.mProbability);
+ }
+
virtual std::vector<size_t> independentUnit() const override {
std::set<size_t> unit = {this->mId};
@@ -819,7 +841,12 @@ namespace storm {
std::string typestring() const override{
return "VOT (" + std::to_string(mThreshold) + ")";
}
-
+
+ virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
+ if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
+ DFTVot<ValueType> const& otherVOT = static_cast<DFTVot<ValueType> const&>(other);
+ return (mThreshold == otherVOT.mThreshold);
+ }
};
template<typename ValueType>
@@ -887,7 +914,12 @@ namespace storm {
}
}
};
-
+
+ template<typename ValueType>
+ bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) {
+ return e1.isTypeEqualTo(e2);
+ }
+
}
}
From cd3af54bb5192288b66fd7f40b8b1f8fadc0be20 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 18 Feb 2016 15:44:54 +0100
Subject: [PATCH 2/4] Dftelementstype: is static gate Former-commit-id:
a7b82e8ea97b61e48b27b88d1d58bea2d19d9416
---
src/storage/dft/DFTElementType.h | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
diff --git a/src/storage/dft/DFTElementType.h b/src/storage/dft/DFTElementType.h
index 98d58df5c..a0d801816 100644
--- a/src/storage/dft/DFTElementType.h
+++ b/src/storage/dft/DFTElementType.h
@@ -6,6 +6,24 @@ namespace storm {
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};
+ inline bool isStaticGateType(DFTElementType const& tp) {
+ if(!isGateType(tp)) return false;
+ switch(tp) {
+ case DFTElementType::AND:
+ case DFTElementType::OR:
+ case DFTElementType::VOT:
+ return true;
+ case DFTElementType::POR:
+ case DFTElementType::SPARE:
+ case DFTElementType::PAND:
+ case DFTElementType::SEQAND:
+ return false;
+ default:
+ assert(false);
+ }
+ }
+
+
inline bool isGateType(DFTElementType const& tp) {
switch(tp) {
case DFTElementType::AND:
From c0dfaef066c965b51bc4907c08f70f85f853b0de Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 18 Feb 2016 15:45:18 +0100
Subject: [PATCH 3/4] DFTElement: hasOnlyStaticParents Former-commit-id:
449222f331d3f59e65d6291dd109e4258d8f319e
---
src/storage/dft/DFTElements.h | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index b7fca51c0..747dfb611 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -119,6 +119,16 @@ namespace storm {
}
}
+ bool hasOnlyStaticParents() const {
+ for(auto const& parent : parents) {
+ if(!isStaticGateType(parents->type()) {
+ return false;
+ }
+ }
+ return true;
+ }
+
+
bool hasParents() const {
return !mParents.empty();
}
From d00b32b5480ac055fee52e5e8f36fa1e30a38215 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 18 Feb 2016 16:04:32 +0100
Subject: [PATCH 4/4] fix of static parents and fixed warning in element types
Former-commit-id: 816efd9c557cf59e78bd19c4a23d80c428adbfc4
---
src/storage/dft/DFTElementType.h | 36 ++++++++++++++++++--------------
src/storage/dft/DFTElements.h | 4 ++--
2 files changed, 22 insertions(+), 18 deletions(-)
diff --git a/src/storage/dft/DFTElementType.h b/src/storage/dft/DFTElementType.h
index a0d801816..a32745cdf 100644
--- a/src/storage/dft/DFTElementType.h
+++ b/src/storage/dft/DFTElementType.h
@@ -6,45 +6,49 @@ namespace storm {
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};
- inline bool isStaticGateType(DFTElementType const& tp) {
- if(!isGateType(tp)) return false;
+
+ inline bool isGateType(DFTElementType const& tp) {
switch(tp) {
case DFTElementType::AND:
+ case DFTElementType::COUNTING:
case DFTElementType::OR:
case DFTElementType::VOT:
- return true;
- case DFTElementType::POR:
- case DFTElementType::SPARE:
case DFTElementType::PAND:
+ case DFTElementType::SPARE:
+ case DFTElementType::POR:
case DFTElementType::SEQAND:
+ return true;
+ case DFTElementType::BE:
+ case DFTElementType::CONSTF:
+ case DFTElementType::CONSTS:
+ case DFTElementType::PDEP:
return false;
default:
assert(false);
+ return false;
}
}
+
-
- inline bool isGateType(DFTElementType const& tp) {
+ inline bool isStaticGateType(DFTElementType const& tp) {
+ if(!isGateType(tp)) return false;
switch(tp) {
case DFTElementType::AND:
- case DFTElementType::COUNTING:
case DFTElementType::OR:
case DFTElementType::VOT:
- case DFTElementType::PAND:
- case DFTElementType::SPARE:
+ return true;
case DFTElementType::POR:
+ case DFTElementType::SPARE:
+ case DFTElementType::PAND:
case DFTElementType::SEQAND:
- return true;
- case DFTElementType::BE:
- case DFTElementType::CONSTF:
- case DFTElementType::CONSTS:
- case DFTElementType::PDEP:
return false;
default:
assert(false);
+ return false;
}
}
-
+
+
}
}
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index 747dfb611..6ab165a04 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -120,8 +120,8 @@ namespace storm {
}
bool hasOnlyStaticParents() const {
- for(auto const& parent : parents) {
- if(!isStaticGateType(parents->type()) {
+ for(auto const& parent : mParents) {
+ if(!isStaticGateType(parent->type())) {
return false;
}
}