Matthias Volk
6 years ago
28 changed files with 635 additions and 385 deletions
-
22src/storm-dft/builder/DFTBuilder.cpp
-
4src/storm-dft/builder/DFTBuilder.h
-
26src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
-
16src/storm-dft/generator/DftNextStateGenerator.cpp
-
8src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
-
25src/storm-dft/parser/DFTJsonParser.cpp
-
25src/storm-dft/storage/dft/DFT.cpp
-
21src/storm-dft/storage/dft/DFT.h
-
70src/storm-dft/storage/dft/DFTElementType.h
-
3src/storm-dft/storage/dft/DFTElements.h
-
83src/storm-dft/storage/dft/DFTIsomorphism.h
-
58src/storm-dft/storage/dft/DFTState.cpp
-
34src/storm-dft/storage/dft/DftJsonExporter.cpp
-
61src/storm-dft/storage/dft/elements/BEConst.h
-
103src/storm-dft/storage/dft/elements/BEExponential.h
-
6src/storm-dft/storage/dft/elements/DFTAnd.h
-
143src/storm-dft/storage/dft/elements/DFTBE.h
-
58src/storm-dft/storage/dft/elements/DFTConst.h
-
10src/storm-dft/storage/dft/elements/DFTDependency.h
-
112src/storm-dft/storage/dft/elements/DFTElement.h
-
4src/storm-dft/storage/dft/elements/DFTOr.h
-
5src/storm-dft/storage/dft/elements/DFTPand.h
-
5src/storm-dft/storage/dft/elements/DFTPor.h
-
30src/storm-dft/storage/dft/elements/DFTRestriction.h
-
1src/storm-dft/storage/dft/elements/DFTSpare.h
-
5src/storm-dft/storage/dft/elements/DFTVot.h
-
63src/storm-dft/transformations/DftToGspnTransformator.cpp
-
19src/storm-dft/transformations/DftToGspnTransformator.h
@ -0,0 +1,61 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include "DFTBE.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace storage { |
||||
|
|
||||
|
/*! |
||||
|
* BE which is either constant failed or constant failsafe. |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
class BEConst : public DFTBE<ValueType> { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Constructor. |
||||
|
* @param id Id. |
||||
|
* @param name Name. |
||||
|
* @param failed True iff the const BE is failed, otherwise it is failsafe. |
||||
|
*/ |
||||
|
BEConst(size_t id, std::string const& name, bool failed) : DFTBE<ValueType>(id, name), mFailed(failed) { |
||||
|
// Intentionally empty |
||||
|
} |
||||
|
|
||||
|
DFTElementType type() const override { |
||||
|
return DFTElementType::BE_CONST; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Return whether the BE has failed. |
||||
|
* @return True iff the BE is const failed. |
||||
|
*/ |
||||
|
bool failed() const { |
||||
|
return mFailed; |
||||
|
} |
||||
|
|
||||
|
bool canFail() const override { |
||||
|
return this->failed(); |
||||
|
} |
||||
|
|
||||
|
bool isTypeEqualTo(DFTElement <ValueType> const& other) const override { |
||||
|
if (!DFTElement<ValueType>::isTypeEqualTo(other)) { |
||||
|
return false; |
||||
|
} |
||||
|
auto& otherBE = static_cast<BEConst<ValueType> const&>(other); |
||||
|
return this->failed() == otherBE.failed(); |
||||
|
} |
||||
|
|
||||
|
std::string toString() const override { |
||||
|
std::stringstream stream; |
||||
|
stream << "{" << this->name() << "} BE(const " << (this->failed() ? "failed" : "failsafe") << ")"; |
||||
|
return stream.str(); |
||||
|
} |
||||
|
|
||||
|
private: |
||||
|
bool mFailed; |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,103 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include "DFTBE.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace storage { |
||||
|
|
||||
|
/*! |
||||
|
* BE with exponential failure rate. |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
class BEExponential : public DFTBE<ValueType> { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Constructor. |
||||
|
* @param id Id. |
||||
|
* @param name Name. |
||||
|
* @param failureRate Active failure rate. |
||||
|
* @param dormancyFactor Dormancy factor. |
||||
|
* @param transient True iff the BE experiences transient failures. |
||||
|
*/ |
||||
|
BEExponential(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) : |
||||
|
DFTBE<ValueType>(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate), mTransient(transient) { |
||||
|
STORM_LOG_ASSERT(!storm::utility::isZero<ValueType>(failureRate), "Exponential failure rate should not be zero."); |
||||
|
} |
||||
|
|
||||
|
DFTElementType type() const override { |
||||
|
return DFTElementType::BE_EXP; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Return failure rate in active state. |
||||
|
* @return Active failure rate. |
||||
|
*/ |
||||
|
ValueType const& activeFailureRate() const { |
||||
|
return mActiveFailureRate; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Return failure rate in passive state. |
||||
|
* @return Passive failure rate. |
||||
|
*/ |
||||
|
ValueType const& passiveFailureRate() const { |
||||
|
return mPassiveFailureRate; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Return dormancy factor given by passive_failure_rate/active_failure_rate. |
||||
|
* @return Dormancy factor. |
||||
|
*/ |
||||
|
ValueType dormancyFactor() const { |
||||
|
if (storm::utility::isZero<ValueType>(this->activeFailureRate())) { |
||||
|
// Return default value of 1 |
||||
|
return storm::utility::one<ValueType>(); |
||||
|
} else { |
||||
|
return this->passiveFailureRate() / this->activeFailureRate(); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Return whether the BE experiences transient failures. |
||||
|
* @return True iff BE is transient. |
||||
|
*/ |
||||
|
bool isTransient() const { |
||||
|
return mTransient; |
||||
|
} |
||||
|
|
||||
|
bool canFail() const override { |
||||
|
return !storm::utility::isZero(this->activeFailureRate()); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Return whether the BE is a cold BE, i.e., passive failure rate = 0. |
||||
|
* @return True iff BE is cold BE. |
||||
|
*/ |
||||
|
bool isColdBasicElement() const { |
||||
|
return storm::utility::isZero(this->passiveFailureRate()); |
||||
|
} |
||||
|
|
||||
|
bool isTypeEqualTo(DFTElement <ValueType> const& other) const override { |
||||
|
if (!DFTElement<ValueType>::isTypeEqualTo(other)) { |
||||
|
return false; |
||||
|
} |
||||
|
auto& otherBE = static_cast<BEExponential<ValueType> const&>(other); |
||||
|
return (this->activeFailureRate() == otherBE.activeFailureRate()) && (this->passiveFailureRate() == otherBE.passiveFailureRate()); |
||||
|
} |
||||
|
|
||||
|
std::string toString() const override { |
||||
|
std::stringstream stream; |
||||
|
stream << "{" << this->name() << "} BE exp(" << this->activeFailureRate() << ", " << this->passiveFailureRate() << ")"; |
||||
|
return stream.str(); |
||||
|
} |
||||
|
|
||||
|
private: |
||||
|
ValueType mActiveFailureRate; |
||||
|
ValueType mPassiveFailureRate; |
||||
|
bool mTransient; |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -1,131 +1,98 @@ |
|||||
#pragma once |
#pragma once |
||||
|
|
||||
|
#include "DFTElement.h" |
||||
|
|
||||
namespace storm { |
namespace storm { |
||||
namespace storage { |
namespace storage { |
||||
|
|
||||
|
/*! |
||||
|
* Abstract base class for basic elements (BEs) in DFTs. |
||||
|
*/ |
||||
template<typename ValueType> |
template<typename ValueType> |
||||
class DFTBE : public DFTElement<ValueType> { |
class DFTBE : public DFTElement<ValueType> { |
||||
|
|
||||
using DFTDependencyPointer = std::shared_ptr<DFTDependency<ValueType>>; |
|
||||
using DFTDependencyVector = std::vector<DFTDependencyPointer>; |
|
||||
|
|
||||
protected: |
|
||||
ValueType mActiveFailureRate; |
|
||||
ValueType mPassiveFailureRate; |
|
||||
DFTDependencyVector mIngoingDependencies; |
|
||||
bool mTransient; |
|
||||
|
|
||||
public: |
public: |
||||
DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) : |
|
||||
DFTElement<ValueType>(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate), mTransient(transient) |
|
||||
{} |
|
||||
|
|
||||
DFTElementType type() const override { |
|
||||
return DFTElementType::BE; |
|
||||
|
/*! |
||||
|
* Constructor. |
||||
|
* @param id Id. |
||||
|
* @param name Name. |
||||
|
*/ |
||||
|
DFTBE(size_t id, std::string const& name) : DFTElement<ValueType>(id, name) { |
||||
|
// Intentionally empty |
||||
} |
} |
||||
|
|
||||
virtual size_t nrChildren() const override { |
|
||||
|
size_t nrChildren() const override { |
||||
return 0; |
return 0; |
||||
} |
} |
||||
|
|
||||
ValueType const& activeFailureRate() const { |
|
||||
return mActiveFailureRate; |
|
||||
} |
|
||||
|
|
||||
ValueType const& passiveFailureRate() const { |
|
||||
return mPassiveFailureRate; |
|
||||
} |
|
||||
|
|
||||
ValueType dormancyFactor() const { |
|
||||
if (storm::utility::isZero<ValueType>(this->activeFailureRate())) { |
|
||||
// Return default value of 0 |
|
||||
return storm::utility::zero<ValueType>(); |
|
||||
} else { |
|
||||
return this->passiveFailureRate() / this->activeFailureRate(); |
|
||||
} |
|
||||
} |
|
||||
|
/*! |
||||
|
* Return whether the BE can fail. |
||||
|
* @return True iff BE is not failsafe. |
||||
|
*/ |
||||
|
virtual bool canFail() const = 0; |
||||
|
|
||||
bool isTransient() const { |
|
||||
return mTransient; |
|
||||
} |
|
||||
|
|
||||
bool canFail() const { |
|
||||
return !storm::utility::isZero(mActiveFailureRate); |
|
||||
} |
|
||||
|
|
||||
bool addIngoingDependency(DFTDependencyPointer const& e) { |
|
||||
// TODO write this assertion for n-ary dependencies, probably by addign a method to the dependencies to support this. |
|
||||
|
/*! |
||||
|
* Add dependency which can trigger this BE. |
||||
|
* @param dependency Ingoing dependency. |
||||
|
*/ |
||||
|
void addIngoingDependency(std::shared_ptr<DFTDependency<ValueType>> const& dependency) { |
||||
|
// TODO write this assertion for n-ary dependencies, probably by adding a method to the dependencies to support this. |
||||
//STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match."); |
//STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match."); |
||||
if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) { |
|
||||
return false; |
|
||||
} |
|
||||
else |
|
||||
{ |
|
||||
mIngoingDependencies.push_back(e); |
|
||||
return true; |
|
||||
} |
|
||||
|
STORM_LOG_ASSERT(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), dependency) == mIngoingDependencies.end(), |
||||
|
"Ingoing Dependency " << dependency << " already present."); |
||||
|
mIngoingDependencies.push_back(dependency); |
||||
} |
} |
||||
|
|
||||
|
|
||||
|
/*! |
||||
|
* Return whether the BE has ingoing dependencies. |
||||
|
* @return True iff BE can be triggered by dependencies. |
||||
|
*/ |
||||
bool hasIngoingDependencies() const { |
bool hasIngoingDependencies() const { |
||||
return !mIngoingDependencies.empty(); |
return !mIngoingDependencies.empty(); |
||||
} |
} |
||||
|
|
||||
size_t nrIngoingDependencies() const { |
|
||||
return mIngoingDependencies.size(); |
|
||||
} |
|
||||
|
|
||||
DFTDependencyVector const& ingoingDependencies() const { |
|
||||
|
|
||||
|
/*! |
||||
|
* Return ingoing dependencies. |
||||
|
* @return List of dependencies which can trigger this BE. |
||||
|
*/ |
||||
|
std::vector<std::shared_ptr<DFTDependency<ValueType>>> const& ingoingDependencies() const { |
||||
return mIngoingDependencies; |
return mIngoingDependencies; |
||||
} |
} |
||||
|
|
||||
std::string toString() const override { |
|
||||
std::stringstream stream; |
|
||||
stream << *this; |
|
||||
return stream.str(); |
|
||||
} |
|
||||
|
|
||||
|
|
||||
bool isBasicElement() const override { |
bool isBasicElement() const override { |
||||
return true; |
return true; |
||||
} |
} |
||||
|
|
||||
bool isColdBasicElement() const { |
|
||||
return storm::utility::isZero(mPassiveFailureRate); |
|
||||
} |
|
||||
|
|
||||
virtual void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { |
|
||||
if(elemsInSubtree.count(this->id())) { |
|
||||
|
|
||||
|
void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { |
||||
|
if (elemsInSubtree.count(this->id())) { |
||||
return; |
return; |
||||
} |
} |
||||
DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); |
DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); |
||||
if(elemsInSubtree.empty()) { |
|
||||
|
if (elemsInSubtree.empty()) { |
||||
// Parent in the subdft, ie it is *not* a subdft |
// Parent in the subdft, ie it is *not* a subdft |
||||
return; |
return; |
||||
} |
} |
||||
for(auto const& incDep : mIngoingDependencies) { |
|
||||
|
for (auto const& incDep : ingoingDependencies()) { |
||||
incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); |
incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); |
||||
if(elemsInSubtree.empty()) { |
|
||||
|
if (elemsInSubtree.empty()) { |
||||
// Parent in the subdft, ie it is *not* a subdft |
// Parent in the subdft, ie it is *not* a subdft |
||||
return; |
return; |
||||
} |
} |
||||
} |
} |
||||
} |
} |
||||
|
|
||||
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 { |
|
||||
if(DFTElement<ValueType>::checkDontCareAnymore(state, queues)) { |
|
||||
state.beNoLongerFailable(this->mId); |
|
||||
|
|
||||
|
bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues <ValueType>& queues) const override { |
||||
|
if (DFTElement<ValueType>::checkDontCareAnymore(state, queues)) { |
||||
|
state.beNoLongerFailable(this->id()); |
||||
return true; |
return true; |
||||
} |
} |
||||
return false; |
return false; |
||||
} |
} |
||||
|
|
||||
|
private: |
||||
|
std::vector<std::shared_ptr<DFTDependency<ValueType>>> mIngoingDependencies; |
||||
|
|
||||
}; |
}; |
||||
|
|
||||
template<typename ValueType> |
|
||||
inline std::ostream& operator<<(std::ostream& os, DFTBE<ValueType> const& be) { |
|
||||
return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")"; |
|
||||
} |
|
||||
} |
} |
||||
} |
} |
||||
@ -1,58 +0,0 @@ |
|||||
#pragma once |
|
||||
|
|
||||
|
|
||||
#include "DFTElement.h" |
|
||||
namespace storm { |
|
||||
namespace storage { |
|
||||
template<typename ValueType> |
|
||||
class DFTConst : public DFTElement<ValueType> { |
|
||||
|
|
||||
bool mFailed; |
|
||||
|
|
||||
public: |
|
||||
DFTConst(size_t id, std::string const& name, bool failed) : |
|
||||
DFTElement<ValueType>(id, name), mFailed(failed) |
|
||||
{} |
|
||||
|
|
||||
DFTElementType type() const override { |
|
||||
if(mFailed) { |
|
||||
return DFTElementType::CONSTF; |
|
||||
} else { |
|
||||
return DFTElementType::CONSTS; |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
|
|
||||
bool failed() const { |
|
||||
return mFailed; |
|
||||
} |
|
||||
|
|
||||
virtual bool isConstant() const override { |
|
||||
return true; |
|
||||
} |
|
||||
|
|
||||
virtual size_t nrChildren() const override { |
|
||||
return 0; |
|
||||
} |
|
||||
|
|
||||
std::string toString() const override { |
|
||||
std::stringstream stream; |
|
||||
stream << *this; |
|
||||
return stream.str(); |
|
||||
} |
|
||||
|
|
||||
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); |
|
||||
} |
|
||||
|
|
||||
}; |
|
||||
|
|
||||
template<typename ValueType> |
|
||||
inline std::ostream& operator<<(std::ostream& os, DFTConst<ValueType> const& be) { |
|
||||
return os << "{" << be.name() << "} BE(const " << (be.failed() ? "failed" : "failsafe") << ")"; |
|
||||
} |
|
||||
|
|
||||
} |
|
||||
} |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue