diff --git a/src/storm-dft/storage/dft/DFTElementType.h b/src/storm-dft/storage/dft/DFTElementType.h index 3496f3c8d..fe0031c79 100644 --- a/src/storm-dft/storage/dft/DFTElementType.h +++ b/src/storm-dft/storage/dft/DFTElementType.h @@ -24,7 +24,8 @@ namespace storm { */ enum class BEType { CONSTANT, - EXPONENTIAL + EXPONENTIAL, + SAMPLES }; diff --git a/src/storm-dft/storage/dft/DFTElements.h b/src/storm-dft/storage/dft/DFTElements.h index 36d671703..ab605e3e5 100644 --- a/src/storm-dft/storage/dft/DFTElements.h +++ b/src/storm-dft/storage/dft/DFTElements.h @@ -1,13 +1,18 @@ #pragma once -#include "storm-dft/storage/dft/elements/BEExponential.h" +// BE types #include "storm-dft/storage/dft/elements/BEConst.h" +#include "storm-dft/storage/dft/elements/BEExponential.h" +#include "storm-dft/storage/dft/elements/BESamples.h" + +// Gates #include "storm-dft/storage/dft/elements/DFTAnd.h" -#include "storm-dft/storage/dft/elements/DFTDependency.h" -#include "storm-dft/storage/dft/elements/DFTMutex.h" #include "storm-dft/storage/dft/elements/DFTOr.h" +#include "storm-dft/storage/dft/elements/DFTVot.h" #include "storm-dft/storage/dft/elements/DFTPand.h" #include "storm-dft/storage/dft/elements/DFTPor.h" -#include "storm-dft/storage/dft/elements/DFTSeq.h" #include "storm-dft/storage/dft/elements/DFTSpare.h" -#include "storm-dft/storage/dft/elements/DFTVot.h" + +#include "storm-dft/storage/dft/elements/DFTDependency.h" +#include "storm-dft/storage/dft/elements/DFTSeq.h" +#include "storm-dft/storage/dft/elements/DFTMutex.h" diff --git a/src/storm-dft/storage/dft/elements/BESamples.cpp b/src/storm-dft/storage/dft/elements/BESamples.cpp new file mode 100644 index 000000000..3fb6ec462 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BESamples.cpp @@ -0,0 +1,20 @@ +#include "BESamples.h" + +#include "storm/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace storage { + + template <typename ValueType> + ValueType BESamples<ValueType>::getUnreliability(ValueType time) const { + auto iter = mActiveSamples.find(time); + STORM_LOG_THROW(iter!= mActiveSamples.end(), storm::exceptions::InvalidArgumentException, "No sample for time point " << time << " given."); + return iter->second; + } + + // Explicitly instantiate the class. + template class BESamples<double>; + template class BESamples<RationalFunction>; + + } +} diff --git a/src/storm-dft/storage/dft/elements/BESamples.h b/src/storm-dft/storage/dft/elements/BESamples.h new file mode 100644 index 000000000..79bc0b2c7 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BESamples.h @@ -0,0 +1,74 @@ +#pragma once + +#include "DFTBE.h" + +#include <map> + +namespace storm { + namespace storage { + + /*! + * BE where the failure distribution is defined by samples. + * A sample defines the unreliability at a time point (i.e. the cumulative distribution function F(x)). + */ + template<typename ValueType> + class BESamples : public DFTBE<ValueType> { + + public: + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param activeSamples Samples defining unreliability in active state for certain time points. + */ + BESamples(size_t id, std::string const& name, std::map<ValueType, ValueType> activeSamples) : + DFTBE<ValueType>(id, name), mActiveSamples(activeSamples) { + STORM_LOG_ASSERT(activeSamples.size() > 0, "At least one sample should be given."); + STORM_LOG_ASSERT(this->canFail(), "At least one sample should have a non-zero probability."); + } + + BEType beType() const override { + return BEType::SAMPLES; + } + + /*! + * Return samples defining unreliability in active state. + * @return Samples for active state. + */ + std::map<ValueType, ValueType> const& activeSamples() const { + return mActiveSamples; + } + + ValueType getUnreliability(ValueType time) const override; + + bool canFail() const override { + // At least one sample is not zero + for (auto const& sample : mActiveSamples) { + if (!storm::utility::isZero(sample.second)) { + return true; + } + } + return true; + } + + bool isTypeEqualTo(DFTElement<ValueType> const& other) const override { + if (!DFTBE<ValueType>::isTypeEqualTo(other)) { + return false; + } + + auto& otherBE = static_cast<BESamples<ValueType> const&>(other); + return mActiveSamples.size() == otherBE.activeSamples().size() && std::equal(mActiveSamples.begin(), mActiveSamples.end(), otherBE.activeSamples().begin()); + } + + std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} BE samples(" << this->activeSamples().size() << " samples)"; + return stream.str(); + } + + private: + std::map<ValueType, ValueType> mActiveSamples; + }; + + } +} diff --git a/src/test/storm-dft/storage/DftBETest.cpp b/src/test/storm-dft/storage/DftBETest.cpp index 38c2f2112..c73af3d9e 100644 --- a/src/test/storm-dft/storage/DftBETest.cpp +++ b/src/test/storm-dft/storage/DftBETest.cpp @@ -26,4 +26,27 @@ namespace { EXPECT_FLOAT_EQ(0.9975212478, be.getUnreliability(2)); } + TEST(DftBETest, FailureSamples) { + // Weibull distribution with shape 5 and scale 1 + std::map<double, double> samples = { + {0.0, 0.0}, + {0.25, 0.0009760858180243304}, + {0.5, 0.03076676552365587}, + {0.75, 0.21124907114638225}, + {1.0, 0.6321205588285577}, + {1.25, 0.9527242505937095}, + {1.5, 0.9994964109502631}, + {1.75, 0.999999925546118}, + {2.0, 0.9999999999999873} + }; + storm::storage::BESamples<double> be(0, "Weibull", samples); + + EXPECT_TRUE(be.canFail()); + + EXPECT_EQ(0, be.getUnreliability(0)); + for (double i = 0; i <= 2.0; i += 0.25) { + EXPECT_FLOAT_EQ(1-exp(-pow(i, 5)), be.getUnreliability(i)); + } + } + }