sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Some more refactoring

main
Matthias Volk 6 years ago
parent
694c87c2b1
commit
26366e43cf
5 changed files with 192 additions and 136 deletions
Unified View
  1. 24
      src/storm-dft/storage/dft/elements/DFTDependency.h
  2. 48
      src/storm-dft/storage/dft/elements/DFTElement.cpp
  3. 249
      src/storm-dft/storage/dft/elements/DFTElement.h
  4. 5
      src/storm-dft/storage/dft/elements/DFTGate.h
  5. 2
      src/storm-dft/storage/dft/elements/DFTRestriction.h

24
src/storm-dft/storage/dft/elements/DFTDependency.h
View File

@ -55,6 +55,18 @@ namespace storm {
return mProbability; 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. * Get trigger event, i.e., the first child.
* @return Trigger event. * @return Trigger event.
@ -106,18 +118,6 @@ namespace storm {
return 1; 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 { bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
if (!DFTElement<ValueType>::isTypeEqualTo(other)) { if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
return false; return false;

48
src/storm-dft/storage/dft/elements/DFTElement.cpp
View File

@ -6,13 +6,13 @@
namespace storm { namespace storm {
namespace storage { namespace storage {
template<typename ValueType> template<typename ValueType>
bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const { bool DFTElement<ValueType>::checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
if (state.dontCare(mId)) { if (state.dontCare(mId)) {
return false; return false;
} }
// Check that no outgoing dependencies can be triggered anymore // Check that no outgoing dependencies can be triggered anymore
// Notice that n-ary dependencies are supported via rewriting them during build-time // Notice that n-ary dependencies are supported via rewriting them during build-time
for (DFTDependencyPointer dependency : mOutgoingDependencies) { for (DFTDependencyPointer dependency : mOutgoingDependencies) {
@ -21,23 +21,23 @@ namespace storm {
return false; return false;
} }
} }
bool hasParentSpare = false; bool hasParentSpare = false;
// Check that no parent can fail anymore // Check that no parent can fail anymore
for(DFTGatePointer const& parent : mParents) { for (DFTGatePointer const& parent : mParents) {
if(state.isOperational(parent->id())) { if (state.isOperational(parent->id())) {
return false; return false;
} }
if (parent->isSpareGate()) { if (parent->isSpareGate()) {
hasParentSpare = true; hasParentSpare = true;
} }
} }
if (!mRestrictions.empty() && state.hasOperationalPostSeqElements(mId)) {
if(!mRestrictions.empty() && state.hasOperationalPostSeqElements(mId)) {
return false; return false;
} }
state.setDontCare(mId); state.setDontCare(mId);
if (hasParentSpare) { if (hasParentSpare) {
// Activate child for consistency in failed spares // Activate child for consistency in failed spares
@ -48,8 +48,8 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void DFTElement<ValueType>::extendSpareModule(std::set<size_t>& elementsInModule) const { void DFTElement<ValueType>::extendSpareModule(std::set<size_t>& elementsInModule) const {
for(auto const& parent : mParents) { for (auto const& parent : mParents) {
if(elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) { if (elementsInModule.count(parent->id()) == 0 && !parent->isSpareGate()) {
elementsInModule.insert(parent->id()); elementsInModule.insert(parent->id());
parent->extendSpareModule(elementsInModule); parent->extendSpareModule(elementsInModule);
} }
@ -78,48 +78,42 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void DFTElement<ValueType>::extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const { 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 (elemsInSubtree.count(this->id()) > 0) return;
if(std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) { if (std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), mId) != parentsOfSubRoot.end()) {
// This is a parent of the suspected root, thus it is not a subdft. // This is a parent of the suspected root, thus it is not a subdft.
elemsInSubtree.clear(); elemsInSubtree.clear();
return; return;
} }
elemsInSubtree.insert(mId); elemsInSubtree.insert(mId);
for(auto const& parent : mParents) { for (auto const& parent : mParents) {
if(blockParents && std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), parent->id()) != parentsOfSubRoot.end()) { if (blockParents && std::find(parentsOfSubRoot.begin(), parentsOfSubRoot.end(), parent->id()) != parentsOfSubRoot.end()) {
continue; continue;
} }
parent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); parent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
if(elemsInSubtree.empty()) { if (elemsInSubtree.empty()) {
return; return;
} }
} }
for(auto const& dep : mOutgoingDependencies) { for (auto const& dep : mOutgoingDependencies) {
dep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); dep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
if(elemsInSubtree.empty()) { if (elemsInSubtree.empty()) {
return; return;
} }
} }
for (auto const& restr : mRestrictions) {
for(auto const& restr : mRestrictions) {
restr->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); restr->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
if(elemsInSubtree.empty()) { if (elemsInSubtree.empty()) {
return; return;
} }
} }
} }
// Explicitly instantiate the class. // Explicitly instantiate the class.
template class DFTElement<double>; template class DFTElement<double>;
#ifdef STORM_HAVE_CARL
template class DFTElement<RationalFunction>; template class DFTElement<RationalFunction>;
#endif
} }
} }

249
src/storm-dft/storage/dft/elements/DFTElement.h
View File

@ -1,4 +1,4 @@
#pragma once #pragma once
#include <string> #include <string>
#include <cstdlib> #include <cstdlib>
@ -16,23 +16,25 @@
#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h"
namespace storm { namespace storm {
namespace storage { namespace storage {
using std::size_t; using std::size_t;
// Forward declarations // Forward declarations
template<typename ValueType> template<typename ValueType>
class DFTGate; class DFTGate;
template<typename ValueType> template<typename ValueType>
class DFTDependency; class DFTDependency;
template<typename ValueType> template<typename ValueType>
class DFTRestriction; class DFTRestriction;
/*!
* Abstract base class for DFT elements.
* It is the most general class.
*/
template<typename ValueType> template<typename ValueType>
class DFTElement { class DFTElement {
@ -43,16 +45,6 @@ namespace storm {
using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>; using DFTRestrictionPointer = std::shared_ptr<DFTRestriction<ValueType>>;
using DFTRestrictionVector = std::vector<DFTRestrictionPointer>; 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: public:
/*! /*!
* Constructor. * Constructor.
@ -60,12 +52,14 @@ namespace storm {
* @param name Name. * @param name Name.
*/ */
DFTElement(size_t id, std::string const& name) : mId(id), mName(name) { DFTElement(size_t id, std::string const& name) : mId(id), mName(name) {
// Intentionally left empty.
} }
/*! /*!
* Destructor. * Destructor.
*/ */
virtual ~DFTElement() { virtual ~DFTElement() {
// Intentionally left empty.
} }
/*! /*!
@ -99,6 +93,10 @@ namespace storm {
*/ */
virtual DFTElementType type() const = 0; virtual DFTElementType type() const = 0;
/*!
* Get type as string.
* @return String with type information.
*/
virtual std::string typestring() const { virtual std::string typestring() const {
return storm::storage::toString(this->type()); return storm::storage::toString(this->type());
} }
@ -119,10 +117,6 @@ namespace storm {
this->mRank = rank; this->mRank = rank;
} }
virtual bool isConstant() const {
return false;
}
/*! /*!
* Checks whether the element is a basic element. * Checks whether the element is a basic element.
* @return True iff element is a BE. * @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. * @return True iff element is a gate.
*/ */
virtual bool isGate() const { virtual bool isGate() const {
return false; return false;
} }
/*!
/** * Check whether the element is a SPARE gate.
* Returns true if the element is a spare gate * @return True iff element is a SPARE gate.
*/ */
virtual bool isSpareGate() const { virtual bool isSpareGate() const {
return false; return false;
} }
/*!
* Check whether the element is a dependency.
* @return True iff element is a dependency.
*/
virtual bool isDependency() const { virtual bool isDependency() const {
return false; return false;
} }
/*!
* Check whether the element is a restriction.
* @return True iff element is a restriction.
*/
virtual bool isRestriction() const { virtual bool isRestriction() const {
return false; 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 the number of parents.
return false; * @return Number of parents.
} */
else size_t nrParents() const {
{ return mParents.size();
mParents.push_back(e); }
return true; /*!
} * 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()) { * Add parent.
return false; * @param parent Parent.
} else { */
mRestrictions.push_back(e); void addParent(DFTGatePointer const& parent) {
return true; 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) { * Check whether the element has only static gates as parents.
if(!isStaticGateType(parent->type())) { * @return True iff all parents are static gates.
*/
bool hasOnlyStaticParents() const {
for (auto const& parent : this->parents()) {
if (!isStaticGateType(parent->type())) {
return false; return false;
} }
} }
return true; return true;
} }
/*!
bool hasParents() const { * Return whether the element has restrictions.
return !mParents.empty(); * @return True iff at least one restriction exists.
} */
size_t nrParents() const {
return mParents.size();
}
DFTGateVector const& parents() const {
return mParents;
}
bool hasRestrictions() const { bool hasRestrictions() const {
return !mRestrictions.empty(); return !mRestrictions.empty();
} }
/*!
* Return the number of restrictions.
* @return Number of restrictions.
*/
size_t nrRestrictions() const { size_t nrRestrictions() const {
return mRestrictions.size(); return mRestrictions.size();
} }
/*!
* Get restrictions.
* @return Restrictions.
*/
DFTRestrictionVector const& restrictions() const { DFTRestrictionVector const& restrictions() const {
return mRestrictions; return mRestrictions;
} }
std::vector<size_t> parentIds() const { /*!
std::vector<size_t> res; * Add restriction.
for(auto parent : parents()) { * @param restrictions Restriction.
res.push_back(parent->id()); */
} void addRestriction(DFTRestrictionPointer const& restriction) {
return res; if (std::find(this->restrictions().begin(), this->restrictions().end(), restriction) == this->restrictions().end()) {
} // Restriction does not exist yet
mRestrictions.push_back(restriction);
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;
} }
} }
/*!
* Return whether the element has outgoing dependencies.
* @return True iff at least one restriction exists.
*/
bool hasOutgoingDependencies() const { bool hasOutgoingDependencies() const {
return !mOutgoingDependencies.empty(); return !mOutgoingDependencies.empty();
} }
/*!
* Return the number of outgoing dependencies.
* @return Number of outgoing dependencies.
*/
size_t nrOutgoingDependencies() const { size_t nrOutgoingDependencies() const {
return mOutgoingDependencies.size(); 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 * Obtains ids of elements which are the direct successor in the list of children of a restriction
* @return A vector of ids * @return A vector of ids
@ -244,24 +295,24 @@ namespace storm {
std::vector<size_t> seqRestrictionPosts() const { std::vector<size_t> seqRestrictionPosts() const {
std::vector<size_t> res; std::vector<size_t> res;
for (auto const& restr : mRestrictions) { for (auto const& restr : mRestrictions) {
if(!restr->isSeqEnforcer()) { if (!restr->isSeqEnforcer()) {
continue; continue;
} }
auto it = restr->children().cbegin(); auto it = restr->children().cbegin();
for(; it != restr->children().cend(); ++it) { for (; it != restr->children().cend(); ++it) {
if((*it)->id() == mId) { if ((*it)->id() == mId) {
break; break;
} }
} }
STORM_LOG_ASSERT(it != restr->children().cend(), "Child not found."); STORM_LOG_ASSERT(it != restr->children().cend(), "Child not found.");
++it; ++it;
if(it != restr->children().cend()) { if (it != restr->children().cend()) {
res.push_back((*it)->id()); res.push_back((*it)->id());
} }
} }
return res; return res;
} }
/** /**
* Obtains ids of elements which are the direct predecessor in the list of children of a restriction * Obtains ids of elements which are the direct predecessor in the list of children of a restriction
* @return A vector of ids * @return A vector of ids
@ -269,31 +320,27 @@ namespace storm {
std::vector<size_t> seqRestrictionPres() const { std::vector<size_t> seqRestrictionPres() const {
std::vector<size_t> res; std::vector<size_t> res;
for (auto const& restr : mRestrictions) { for (auto const& restr : mRestrictions) {
if(!restr->isSeqEnforcer()) { if (!restr->isSeqEnforcer()) {
continue; continue;
} }
auto it = restr->children().cbegin(); auto it = restr->children().cbegin();
for(; it != restr->children().cend(); ++it) { for (; it != restr->children().cend(); ++it) {
if((*it)->id() == mId) { if ((*it)->id() == mId) {
break; break;
} }
} }
STORM_LOG_ASSERT(it != restr->children().cend(), "Child not found."); STORM_LOG_ASSERT(it != restr->children().cend(), "Child not found.");
if(it != restr->children().cbegin()) { if (it != restr->children().cbegin()) {
--it; --it;
res.push_back((*it)->id()); res.push_back((*it)->id());
} }
} }
return res; return res;
} }
DFTDependencyVector const& outgoingDependencies() const {
return mOutgoingDependencies;
}
virtual void extendSpareModule(std::set<size_t>& elementsInModule) const; 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. * Get number of children.
* @return Nr 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. * 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; virtual std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves = false) const;
/** /**
* Helper to the independent subtree computation * Helper to the independent subtree computation
* @see independentSubDft * @see independentSubDft
*/ */
virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const; 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 { virtual bool isTypeEqualTo(DFTElement<ValueType> const& other) const {
return type() == other.type(); return type() == other.type();
} }
@ -338,8 +391,12 @@ namespace storm {
protected: 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) { inline std::ostream& operator<<(std::ostream& os, DFTElement<ValueType> const& element) {
return os << element.toString(); return os << element.toString();
} }
template<typename ValueType> template<typename ValueType>
bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) { bool equalType(DFTElement<ValueType> const& e1, DFTElement<ValueType> const& e2) {
return e1.isTypeEqualTo(e2); return e1.isTypeEqualTo(e2);

5
src/storm-dft/storage/dft/elements/DFTGate.h
View File

@ -90,6 +90,11 @@ namespace storm {
this->childrenDontCare(state, queues); 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 { void childrenDontCare(DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const {
queues.propagateDontCare(this->children()); queues.propagateDontCare(this->children());
} }

2
src/storm-dft/storage/dft/elements/DFTRestriction.h
View File

@ -72,7 +72,7 @@ namespace storm {
} }
void failsafe(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override { void failsafe(DFTState <ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override {
// Do nothing
} }
}; };

Write Preview
|||||||
100:0
Loading…
Cancel
Save