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

Some more refactoring

main
Matthias Volk 7 years ago
parent
9d81730fe3
commit
8090448564
5 changed files with 192 additions and 136 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  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) {
if(state.isOperational(parent->id())) {
for (DFTGatePointer const& parent : mParents) {
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) {
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()); 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(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. // 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) {
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; 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;
} }
/**
* 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 { 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 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 false;
} }
} }
return true; 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 { 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;
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 { 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) {
if((*it)->id() == mId) {
for (; it != restr->children().cend(); ++it) {
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) {
if((*it)->id() == mId) {
for (; it != restr->children().cend(); ++it) {
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
Loading…
Cancel
Save