From 26366e43cf40895f4078d0af19c1d768480e4d4f Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 5 Apr 2019 16:13:24 +0200
Subject: [PATCH] Some more refactoring
---
.../storage/dft/elements/DFTDependency.h | 24 +-
.../storage/dft/elements/DFTElement.cpp | 48 ++--
.../storage/dft/elements/DFTElement.h | 249 +++++++++++-------
src/storm-dft/storage/dft/elements/DFTGate.h | 5 +
.../storage/dft/elements/DFTRestriction.h | 2 +-
5 files changed, 192 insertions(+), 136 deletions(-)
diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h
index c055c119f..a7cca4f36 100644
--- a/src/storm-dft/storage/dft/elements/DFTDependency.h
+++ b/src/storm-dft/storage/dft/elements/DFTDependency.h
@@ -55,6 +55,18 @@ namespace storm {
return mProbability;
}
+ bool isDependency() const override {
+ return true;
+ }
+
+ /*!
+ * Check whether the dependency is an FDEP, i.e., p=1.
+ * @return True iff p=1.
+ */
+ bool isFDEP() const {
+ return storm::utility::isOne(this->probability());
+ }
+
/*!
* Get trigger event, i.e., the first child.
* @return Trigger event.
@@ -106,18 +118,6 @@ namespace storm {
return 1;
}
- bool isDependency() const override {
- return true;
- }
-
- /*!
- * Check whether the dependency is an FDEP, i.e., p=1.
- * @return True iff p=1.
- */
- bool isFDEP() const {
- return storm::utility::isOne(this->probability());
- }
-
bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
return false;
diff --git a/src/storm-dft/storage/dft/elements/DFTElement.cpp b/src/storm-dft/storage/dft/elements/DFTElement.cpp
index 287af8e98..5f04b9d65 100644
--- a/src/storm-dft/storage/dft/elements/DFTElement.cpp
+++ b/src/storm-dft/storage/dft/elements/DFTElement.cpp
@@ -6,13 +6,13 @@
namespace storm {
namespace storage {
-
+
template<typename ValueType>
bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if (state.dontCare(mId)) {
return false;
}
-
+
// Check that no outgoing dependencies can be triggered anymore
// Notice that n-ary dependencies are supported via rewriting them during build-time
for (DFTDependencyPointer dependency : mOutgoingDependencies) {
@@ -21,23 +21,23 @@ namespace storm {
return false;
}
}
-
+
bool hasParentSpare = false;
// Check that no parent can fail anymore
- for(DFTGatePointer const& parent : mParents) {
- if(state.isOperational(parent->id())) {
+ for (DFTGatePointer const& parent : mParents) {
+ if (state.isOperational(parent->id())) {
return false;
}
if (parent->isSpareGate()) {
hasParentSpare = true;
}
}
-
- if(!mRestrictions.empty() && state.hasOperationalPostSeqElements(mId)) {
+
+ if (!mRestrictions.empty() && state.hasOperationalPostSeqElements(mId)) {
return false;
}
-
+
state.setDontCare(mId);
if (hasParentSpare) {
// Activate child for consistency in failed spares
@@ -48,8 +48,8 @@ namespace storm {
template<typename ValueType>
void DFTElement<ValueType>::extendSpareModule(std::set<size_t>& elementsInModule) const {
- for(auto const& parent : mParents) {
- if(elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) {
+ for (auto const& parent : mParents) {
+ if (elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) {
elementsInModule.insert(parent->id());
parent->extendSpareModule(elementsInModule);
}
@@ -78,48 +78,42 @@ namespace storm {
template<typename ValueType>
void DFTElement<ValueType>::extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const {
- if(elemsInSubtree.count(this->id()) > 0) return;
- if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) {
+ if (elemsInSubtree.count(this->id()) > 0) return;
+ if (std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) {
// This is a parent of the suspected root, thus it is not a subdft.
elemsInSubtree.clear();
return;
}
elemsInSubtree.insert(mId);
- for(auto const& parent : mParents) {
- if(blockParents && std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), parent->id()) != parentsOfSubRoot.end()) {
+ for (auto const& parent : mParents) {
+ if (blockParents && std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), parent->id()) != parentsOfSubRoot.end()) {
continue;
}
parent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
- if(elemsInSubtree.empty()) {
+ if (elemsInSubtree.empty()) {
return;
}
}
- for(auto const& dep : mOutgoingDependencies) {
+ for (auto const& dep : mOutgoingDependencies) {
dep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
- if(elemsInSubtree.empty()) {
+ if (elemsInSubtree.empty()) {
return;
}
}
-
- for(auto const& restr : mRestrictions) {
+
+ for (auto const& restr : mRestrictions) {
restr->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
- if(elemsInSubtree.empty()) {
+ if (elemsInSubtree.empty()) {
return;
}
}
-
+
}
-
-
// Explicitly instantiate the class.
template class DFTElement<double>;
-
-#ifdef STORM_HAVE_CARL
template class DFTElement<RationalFunction>;
-#endif
-
}
}
diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h
index 5690f5f0c..b287ae863 100644
--- a/src/storm-dft/storage/dft/elements/DFTElement.h
+++ b/src/storm-dft/storage/dft/elements/DFTElement.h
@@ -1,4 +1,4 @@
-#pragma once
+#pragma once
#include <string>
#include <cstdlib>
@@ -16,23 +16,25 @@
#include "storm/adapters/RationalFunctionAdapter.h"
-
-
namespace storm {
namespace storage {
-
+
using std::size_t;
// Forward declarations
template<typename ValueType>
class DFTGate;
-
+
template<typename ValueType>
class DFTDependency;
+
template<typename ValueType>
class DFTRestriction;
-
+ /*!
+ * Abstract base class for DFT elements.
+ * It is the most general class.
+ */
template<typename ValueType>
class DFTElement {
@@ -43,16 +45,6 @@ namespace storm {
using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
using DFTRestrictionVector = std::vector<DFTRestrictionPointer>;
-
- protected:
- std::size_t mId;
- std::string mName;
- std::size_t mRank = -1;
- DFTGateVector mParents;
- DFTDependencyVector mOutgoingDependencies;
- DFTRestrictionVector mRestrictions;
-
-
public:
/*!
* Constructor.
@@ -60,12 +52,14 @@ namespace storm {
* @param name Name.
*/
DFTElement(size_t id, std::string const& name) : mId(id), mName(name) {
+ // Intentionally left empty.
}
/*!
* Destructor.
*/
virtual ~DFTElement() {
+ // Intentionally left empty.
}
/*!
@@ -99,6 +93,10 @@ namespace storm {
*/
virtual DFTElementType type() const = 0;
+ /*!
+ * Get type as string.
+ * @return String with type information.
+ */
virtual std::string typestring() const {
return storm::storage::toString(this->type());
}
@@ -119,10 +117,6 @@ namespace storm {
this->mRank = rank;
}
- virtual bool isConstant() const {
- return false;
- }
-
/*!
* Checks whether the element is a basic element.
* @return True iff element is a BE.
@@ -132,111 +126,168 @@ namespace storm {
}
/*!
- * Check wether the element is a gate.
+ * Check whether the element is a gate.
* @return True iff element is a gate.
*/
virtual bool isGate() const {
return false;
}
-
- /**
- * Returns true if the element is a spare gate
+
+ /*!
+ * Check whether the element is a SPARE gate.
+ * @return True iff element is a SPARE gate.
*/
virtual bool isSpareGate() const {
return false;
}
+ /*!
+ * Check whether the element is a dependency.
+ * @return True iff element is a dependency.
+ */
virtual bool isDependency() const {
return false;
}
-
+
+ /*!
+ * Check whether the element is a restriction.
+ * @return True iff element is a restriction.
+ */
virtual bool isRestriction() const {
return false;
}
+ /*!
+ * Return whether the element has parents.
+ * @return True iff at least one parent exists.
+ */
+ bool hasParents() const {
+ return !mParents.empty();
+ }
- bool addParent(DFTGatePointer const& e) {
- if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) {
- return false;
- }
- else
- {
- mParents.push_back(e);
- return true;
- }
+ /*!
+ * Return the number of parents.
+ * @return Number of parents.
+ */
+ size_t nrParents() const {
+ return mParents.size();
+ }
+
+ /*!
+ * Get parents.
+ * @return Parents.
+ */
+ DFTGateVector const& parents() const {
+ return mParents;
}
- bool addRestriction(DFTRestrictionPointer const& e) {
- if (std::find(mRestrictions.begin(), mRestrictions.end(), e) != mRestrictions.end()) {
- return false;
- } else {
- mRestrictions.push_back(e);
- return true;
+ /*!
+ * Add parent.
+ * @param parent Parent.
+ */
+ void addParent(DFTGatePointer const& parent) {
+ if (std::find(this->parents().begin(), this->parents().end(), parent) == this->parents().end()) {
+ // Parent does not exist yet
+ mParents.push_back(parent);
+ };
+ }
+
+ /*!
+ * Return Ids of parents.
+ * @return Parent ids.
+ */
+ std::vector<size_t> parentIds() const {
+ std::vector<size_t> ids;
+ for (auto parent : this->parents()) {
+ ids.push_back(parent->id());
}
+ return ids;
}
- bool hasOnlyStaticParents() const {
- for(auto const& parent : mParents) {
- if(!isStaticGateType(parent->type())) {
+ /*!
+ * Check whether the element has only static gates as parents.
+ * @return True iff all parents are static gates.
+ */
+ bool hasOnlyStaticParents() const {
+ for (auto const& parent : this->parents()) {
+ if (!isStaticGateType(parent->type())) {
return false;
}
}
return true;
}
-
- bool hasParents() const {
- return !mParents.empty();
- }
-
- size_t nrParents() const {
- return mParents.size();
- }
-
- DFTGateVector const& parents() const {
- return mParents;
- }
-
+ /*!
+ * Return whether the element has restrictions.
+ * @return True iff at least one restriction exists.
+ */
bool hasRestrictions() const {
return !mRestrictions.empty();
}
-
+
+ /*!
+ * Return the number of restrictions.
+ * @return Number of restrictions.
+ */
size_t nrRestrictions() const {
return mRestrictions.size();
}
-
+
+ /*!
+ * Get restrictions.
+ * @return Restrictions.
+ */
DFTRestrictionVector const& restrictions() const {
return mRestrictions;
}
- std::vector<size_t> parentIds() const {
- std::vector<size_t> res;
- for(auto parent : parents()) {
- res.push_back(parent->id());
- }
- return res;
- }
-
- bool addOutgoingDependency(DFTDependencyPointer const& e) {
- STORM_LOG_ASSERT(e->triggerEvent()->id() == this->id(), "Ids do not match.");
- if(std::find(mOutgoingDependencies.begin(), mOutgoingDependencies.end(), e) != mOutgoingDependencies.end()) {
- return false;
- }
- else
- {
- mOutgoingDependencies.push_back(e);
- return true;
+ /*!
+ * Add restriction.
+ * @param restrictions Restriction.
+ */
+ void addRestriction(DFTRestrictionPointer const& restriction) {
+ if (std::find(this->restrictions().begin(), this->restrictions().end(), restriction) == this->restrictions().end()) {
+ // Restriction does not exist yet
+ mRestrictions.push_back(restriction);
}
}
-
+
+ /*!
+ * Return whether the element has outgoing dependencies.
+ * @return True iff at least one restriction exists.
+ */
bool hasOutgoingDependencies() const {
return !mOutgoingDependencies.empty();
}
-
+
+ /*!
+ * Return the number of outgoing dependencies.
+ * @return Number of outgoing dependencies.
+ */
size_t nrOutgoingDependencies() const {
return mOutgoingDependencies.size();
}
-
+
+ /*!
+ * Get outgoing dependencies.
+ * @return Outgoing dependencies.
+ */
+ DFTDependencyVector const& outgoingDependencies() const {
+ return mOutgoingDependencies;
+ }
+
+ /*!
+ * Add outgoing dependency.
+ * @param outgoingDependency Outgoing dependency.
+ */
+ void addOutgoingDependency(DFTDependencyPointer const& outgoingDependency) {
+ STORM_LOG_ASSERT(outgoingDependency->triggerEvent()->id() == this->id(), "Ids do not match.");
+ if (std::find(this->outgoingDependencies().begin(), this->outgoingDependencies().end(), outgoingDependency) == this->outgoingDependencies().end()) {
+ // Outgoing dependency does not exist yet
+ mOutgoingDependencies.push_back(outgoingDependency);
+ };
+ }
+
/**
* Obtains ids of elements which are the direct successor in the list of children of a restriction
* @return A vector of ids
@@ -244,24 +295,24 @@ namespace storm {
std::vector<size_t> seqRestrictionPosts() const {
std::vector<size_t> res;
for (auto const& restr : mRestrictions) {
- if(!restr->isSeqEnforcer()) {
+ if (!restr->isSeqEnforcer()) {
continue;
}
auto it = restr->children().cbegin();
- for(; it != restr->children().cend(); ++it) {
- if((*it)->id() == mId) {
+ for (; it != restr->children().cend(); ++it) {
+ if ((*it)->id() == mId) {
break;
}
}
STORM_LOG_ASSERT(it != restr->children().cend(), "Child not found.");
++it;
- if(it != restr->children().cend()) {
+ if (it != restr->children().cend()) {
res.push_back((*it)->id());
}
}
return res;
}
-
+
/**
* Obtains ids of elements which are the direct predecessor in the list of children of a restriction
* @return A vector of ids
@@ -269,31 +320,27 @@ namespace storm {
std::vector<size_t> seqRestrictionPres() const {
std::vector<size_t> res;
for (auto const& restr : mRestrictions) {
- if(!restr->isSeqEnforcer()) {
+ if (!restr->isSeqEnforcer()) {
continue;
}
auto it = restr->children().cbegin();
- for(; it != restr->children().cend(); ++it) {
- if((*it)->id() == mId) {
+ for (; it != restr->children().cend(); ++it) {
+ if ((*it)->id() == mId) {
break;
}
}
STORM_LOG_ASSERT(it != restr->children().cend(), "Child not found.");
- if(it != restr->children().cbegin()) {
+ if (it != restr->children().cbegin()) {
--it;
res.push_back((*it)->id());
}
}
return res;
}
-
- DFTDependencyVector const& outgoingDependencies() const {
- return mOutgoingDependencies;
- }
-
+
virtual void extendSpareModule(std::set<size_t>& elementsInModule) const;
- // virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;
+ // virtual void extendImmediateFailureCausePathEvents(std::set<size_t>& ) const;
/*!
* Get number of children.
* @return Nr of children.
@@ -320,12 +367,18 @@ namespace storm {
* such that there exists a path from x to a child of this does not go through this.
*/
virtual std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves = false) const;
+
/**
* Helper to the independent subtree computation
* @see independentSubDft
*/
virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const;
+ /*!
+ * Check whether two elements have the same type.
+ * @param other Other element.
+ * @return True iff this and other have the same type.
+ */
virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
return type() == other.type();
}
@@ -338,8 +391,12 @@ namespace storm {
protected:
- // virtual bool checkIsomorphicSubDftHelper(DFTElement const& otherElem, std::vector<std::pair<DFTElement const&, DFTElement const&>>& mapping, std::vector<DFTElement const&> const& order ) const = 0;
-
+ std::size_t mId;
+ std::string mName;
+ std::size_t mRank = -1;
+ DFTGateVector mParents;
+ DFTDependencyVector mOutgoingDependencies;
+ DFTRestrictionVector mRestrictions;
};
@@ -347,7 +404,7 @@ namespace storm {
inline std::ostream& operator<<(std::ostream& os, DFTElement<ValueType> const& element) {
return os << element.toString();
}
-
+
template<typename ValueType>
bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) {
return e1.isTypeEqualTo(e2);
diff --git a/src/storm-dft/storage/dft/elements/DFTGate.h b/src/storm-dft/storage/dft/elements/DFTGate.h
index 9f95ed751..e997c1a4a 100644
--- a/src/storm-dft/storage/dft/elements/DFTGate.h
+++ b/src/storm-dft/storage/dft/elements/DFTGate.h
@@ -90,6 +90,11 @@ namespace storm {
this->childrenDontCare(state, queues);
}
+ /*!
+ * Propagate Don't Care to children.
+ * @param state Current DFT state.
+ * @param queues Propagation queues.
+ */
void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
queues.propagateDontCare(this->children());
}
diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h
index 9b93ae63a..b83ba44f7 100644
--- a/src/storm-dft/storage/dft/elements/DFTRestriction.h
+++ b/src/storm-dft/storage/dft/elements/DFTRestriction.h
@@ -72,7 +72,7 @@ namespace storm {
}
void failsafe(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
-
+ // Do nothing
}
};