You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
109 lines
3.9 KiB
109 lines
3.9 KiB
#pragma once
|
|
|
|
#include "DFTElement.h"
|
|
|
|
namespace storm {
|
|
namespace storage {
|
|
|
|
/*!
|
|
* Abstract base class for basic events (BEs) in DFTs.
|
|
* BEs are atomic and not further subdivided.
|
|
*/
|
|
template<typename ValueType>
|
|
class DFTBE : public DFTElement<ValueType> {
|
|
|
|
public:
|
|
/*!
|
|
* Constructor.
|
|
* @param id Id.
|
|
* @param name Name.
|
|
*/
|
|
DFTBE(size_t id, std::string const& name) : DFTElement<ValueType>(id, name) {
|
|
// Intentionally empty
|
|
}
|
|
|
|
DFTElementType type() const override {
|
|
return DFTElementType::BE;
|
|
}
|
|
|
|
/*!
|
|
* Get type of BE (constant, exponential, etc.).
|
|
* @return BE type.
|
|
*/
|
|
virtual BEType beType() const = 0;
|
|
|
|
size_t nrChildren() const override {
|
|
return 0;
|
|
}
|
|
|
|
/*!
|
|
* Return the unreliability of the BE up to the given time point.
|
|
* Computes the cumulative distribution function F(x) for time x.
|
|
* Note that the computation assumes the BE is always active.
|
|
*
|
|
* @return Cumulative failure probability.
|
|
*/
|
|
virtual ValueType getUnreliability(ValueType time) const = 0;
|
|
|
|
/*!
|
|
* Return whether the BE can fail.
|
|
* @return True iff BE is not failsafe.
|
|
*/
|
|
virtual bool canFail() const = 0;
|
|
|
|
/*!
|
|
* Add dependency which can trigger this BE.
|
|
* @param dependency Ingoing dependency.
|
|
*/
|
|
void addIngoingDependency(std::shared_ptr<DFTDependency<ValueType>> const& dependency) {
|
|
STORM_LOG_ASSERT(dependency->containsDependentEvent(this->id()), "Dependency " << *dependency << " has no dependent BE " << *this << ".");
|
|
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 {
|
|
return !mIngoingDependencies.empty();
|
|
}
|
|
|
|
/*!
|
|
* Return ingoing dependencies.
|
|
* @return List of dependencies which can trigger this BE.
|
|
*/
|
|
std::vector<std::shared_ptr<DFTDependency<ValueType>>> const& ingoingDependencies() const {
|
|
return mIngoingDependencies;
|
|
}
|
|
|
|
bool isBasicElement() const override {
|
|
return true;
|
|
}
|
|
|
|
void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override;
|
|
|
|
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 false;
|
|
}
|
|
|
|
bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
|
|
if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
|
|
return false;
|
|
}
|
|
auto& otherBE = static_cast<DFTBE<ValueType> const&>(other);
|
|
return this->beType() == otherBE.beType();
|
|
}
|
|
|
|
private:
|
|
std::vector<std::shared_ptr<DFTDependency<ValueType>>> mIngoingDependencies;
|
|
|
|
};
|
|
|
|
}
|
|
}
|