diff --git a/src/storm-dft/storage/dft/elements/BEConst.cpp b/src/storm-dft/storage/dft/elements/BEConst.cpp new file mode 100644 index 000000000..cb2457a04 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BEConst.cpp @@ -0,0 +1,16 @@ +#include "BEConst.h" + +namespace storm { + namespace storage { + + template + ValueType BEConst::getUnreliability(ValueType time) const { + return failed() ? storm::utility::one() : storm::utility::zero(); + } + + // Explicitly instantiate the class. + template class BEConst; + template class BEConst; + + } // namespace storage +} // namespace storm diff --git a/src/storm-dft/storage/dft/elements/BEConst.h b/src/storm-dft/storage/dft/elements/BEConst.h index 050cdf51e..3f0cdd949 100644 --- a/src/storm-dft/storage/dft/elements/BEConst.h +++ b/src/storm-dft/storage/dft/elements/BEConst.h @@ -39,6 +39,8 @@ namespace storm { return this->failed(); } + ValueType getUnreliability(ValueType time) const override; + bool isTypeEqualTo(DFTElement const& other) const override { if (!DFTElement::isTypeEqualTo(other)) { return false; diff --git a/src/storm-dft/storage/dft/elements/BEExponential.cpp b/src/storm-dft/storage/dft/elements/BEExponential.cpp new file mode 100644 index 000000000..a93113e31 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BEExponential.cpp @@ -0,0 +1,24 @@ +#include "BEExponential.h" + +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace storage { + + template <> + double BEExponential::getUnreliability(double time) const { + // 1 - e^(-lambda * t) + return 1 - exp(-this->activeFailureRate() * time); + } + + template + ValueType BEExponential::getUnreliability(ValueType time) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing cumulative failure probability not supported for this data type."); + } + + // Explicitly instantiate the class. + template class BEExponential; + template class BEExponential; + + } +} diff --git a/src/storm-dft/storage/dft/elements/BEExponential.h b/src/storm-dft/storage/dft/elements/BEExponential.h index 71786fda8..e29d44642 100644 --- a/src/storm-dft/storage/dft/elements/BEExponential.h +++ b/src/storm-dft/storage/dft/elements/BEExponential.h @@ -50,14 +50,12 @@ namespace storm { * @return Dormancy factor. */ ValueType dormancyFactor() const { - if (storm::utility::isZero(this->activeFailureRate())) { - // Return default value of 1 - return storm::utility::one(); - } else { - return this->passiveFailureRate() / this->activeFailureRate(); - } + STORM_LOG_ASSERT(!storm::utility::isZero(this->activeFailureRate()), "Active failure rate of non-const BE should not be zero."); + return this->passiveFailureRate() / this->activeFailureRate(); } + ValueType getUnreliability(ValueType time) const override; + /*! * Return whether the BE experiences transient failures. * @return True iff BE is transient. diff --git a/src/storm-dft/storage/dft/elements/DFTBE.cpp b/src/storm-dft/storage/dft/elements/DFTBE.cpp new file mode 100644 index 000000000..369039547 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/DFTBE.cpp @@ -0,0 +1,33 @@ +#include "DFTBE.h" + +#include "storm-dft/storage/dft/elements/DFTGate.h" +#include "storm-dft/storage/dft/elements/DFTDependency.h" + +namespace storm { + namespace storage { + + template + void DFTBE::extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const { + if (elemsInSubtree.count(this->id())) { + return; + } + DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); + if (elemsInSubtree.empty()) { + // Parent in the subDFT, i.e., it is *not* a subDFT + return; + } + for (auto const& inDep : ingoingDependencies()) { + inDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); + if (elemsInSubtree.empty()) { + // Parent in the subDFT, i.e., it is *not* a subDFT + return; + } + } + } + + // Explicitly instantiate the class. + template class DFTBE; + template class DFTBE; + + } +} diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 899ece201..1dd2d91d0 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/src/storm-dft/storage/dft/elements/DFTBE.h @@ -36,6 +36,15 @@ namespace storm { 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. @@ -73,23 +82,7 @@ namespace storm { return true; } - void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { - if (elemsInSubtree.count(this->id())) { - return; - } - DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if (elemsInSubtree.empty()) { - // Parent in the subDFT, i.e., it is *not* a subDFT - return; - } - for (auto const& inDep : ingoingDependencies()) { - inDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if (elemsInSubtree.empty()) { - // Parent in the subDFT, i.e., it is *not* a subDFT - return; - } - } - } + void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override; bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { if (DFTElement::checkDontCareAnymore(state, queues)) { diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt index a0e96ee36..a2ef04a4b 100644 --- a/src/test/storm-dft/CMakeLists.txt +++ b/src/test/storm-dft/CMakeLists.txt @@ -9,7 +9,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) -foreach (testsuite api) +foreach (testsuite api storage) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-dft-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) diff --git a/src/test/storm-dft/storage/DftBETest.cpp b/src/test/storm-dft/storage/DftBETest.cpp new file mode 100644 index 000000000..38c2f2112 --- /dev/null +++ b/src/test/storm-dft/storage/DftBETest.cpp @@ -0,0 +1,29 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm-dft/storage/dft/DFTElements.h" + +namespace { + + TEST(DftBETest, FailureConstant) { + storm::storage::BEConst be(0, "Test", true); + EXPECT_TRUE(be.failed()); + EXPECT_TRUE(be.canFail()); + + EXPECT_EQ(1, be.getUnreliability(0)); + EXPECT_EQ(1, be.getUnreliability(10)); + } + + TEST(DftBETest, FailureExponential) { + storm::storage::BEExponential be(0, "Test", 3, 0.5); + + EXPECT_TRUE(be.canFail()); + EXPECT_EQ(1.5, be.passiveFailureRate()); + + EXPECT_EQ(0, be.getUnreliability(0)); + EXPECT_FLOAT_EQ(0.7768698399, be.getUnreliability(0.5)); + EXPECT_FLOAT_EQ(0.9502129316, be.getUnreliability(1)); + EXPECT_FLOAT_EQ(0.9975212478, be.getUnreliability(2)); + } + +}