From 7111674ec81822b684b53513dfa20b50fb2d5356 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 8 Feb 2021 12:31:56 +0100 Subject: [PATCH] Support for simulation of PDEP --- src/storm-dft/simulator/DFTTraceSimulator.cpp | 43 +++++++++++++------ src/storm-dft/simulator/DFTTraceSimulator.h | 13 +++++- src/storm/utility/random.cpp | 7 +++ src/storm/utility/random.h | 8 ++++ .../storm-dft/simulator/DftSimulatorTest.cpp | 12 ++++++ 5 files changed, 70 insertions(+), 13 deletions(-) diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp index eae3a004c..4baba8e07 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.cpp +++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp @@ -26,7 +26,7 @@ namespace storm { } template - double DFTTraceSimulator::randomStep() { + std::tuple DFTTraceSimulator::randomNextFailure() { auto iterFailable = state->getFailableElements().begin(); // Check for absorbing state: @@ -34,7 +34,7 @@ namespace storm { // - no BE can fail if (!state->hasOperationalRelevantEvent() || iterFailable == state->getFailableElements().end()) { STORM_LOG_TRACE("No sucessor states available for " << state->getId()); - return -1; + return std::make_tuple(iterFailable, -1, true); } // Get all failable elements @@ -43,9 +43,16 @@ namespace storm { // We take the first dependeny to resolve the non-determinism STORM_LOG_WARN("Non-determinism present! We take the dependency with the lowest id"); } - STORM_LOG_TRACE("Let dependency " << *iterFailable.getFailBE(dft).second << " fail"); - bool res = step(iterFailable); - return res ? 0 : -1; + + auto dependency = iterFailable.getFailBE(dft).second; + if (!dependency->isFDEP()) { + // Flip a coin whether the PDEP is successful + storm::utility::BernoulliDistributionGenerator probGenerator(dependency->probability()); + bool successful = probGenerator.random(randomGenerator); + return std::make_tuple(iterFailable, 0, successful); + } + STORM_LOG_TRACE("Let dependency " << *dependency << " fail"); + return std::make_tuple(iterFailable, 0, true); } else { // Consider all "normal" BE failures // Initialize with first BE @@ -68,27 +75,39 @@ namespace storm { } } STORM_LOG_TRACE("Let BE " << *nextFail.getFailBE(dft).first << " fail after time " << smallestTimebound); - bool res = step(nextFail); - return res ? smallestTimebound : -1; + return std::make_tuple(nextFail, smallestTimebound, true); } } template<> - double DFTTraceSimulator::randomStep() { + std::tuple DFTTraceSimulator::randomNextFailure() { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs."); } + template + double DFTTraceSimulator::randomStep() { + auto retTuple = this->randomNextFailure(); + storm::dft::storage::FailableElements::const_iterator nextFailable = std::get<0>(retTuple); + double time = std::get<1>(retTuple); + bool successful = std::get<2>(retTuple); + //double time = pairNextFailure.second; + if (time < 0) { + return -1; + } else { + // Apply next failure + bool res = step(nextFailable, successful); + return res ? time : -1; + } + } template - bool DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement) { + bool DFTTraceSimulator::step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful) { if (nextFailElement == state->getFailableElements().end()) { return false; } auto nextBEPair = nextFailElement.getFailBE(dft); - auto newState = generator.createSuccessorState(state, nextBEPair.first, nextBEPair.second); - - // TODO handle PDEP + auto newState = generator.createSuccessorState(state, nextBEPair.first, nextBEPair.second, dependencySuccessful); if(newState->isInvalid() || newState->isTransient()) { STORM_LOG_TRACE("Step is invalid because new state " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored")); diff --git a/src/storm-dft/simulator/DFTTraceSimulator.h b/src/storm-dft/simulator/DFTTraceSimulator.h index 7f9203207..6ef4e1ea0 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.h +++ b/src/storm-dft/simulator/DFTTraceSimulator.h @@ -52,9 +52,20 @@ namespace storm { * Perform one simulation step by letting the next element fail. * * @param nextFailElement Iterator giving the next element which should fail. + * @param dependencySuccessful Whether the triggering dependency was successful. + * If the dependency is unsuccessful, no BE fails and only the depedendy is marked as failed. * @return True iff step could be performed successfully. */ - bool step(storm::dft::storage::FailableElements::const_iterator nextFailElement); + bool step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful = true); + + /*! + * Randomly pick an element which fails next (either a BE or a dependency which triggers a BE) and the time after which it fails. + * The time is 0 for a dependency and -1 if no failure can take place. + * In the latter case, the next failable element is not defined. + * + * @return Tuple of next failable element, time after which is fails and whether a possible failure through the dependency is successful. + */ + std::tuple randomNextFailure(); /*! * Perform a random step by using the random number generator. diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp index 8c576cf95..ddeb4038f 100644 --- a/src/storm/utility/random.cpp +++ b/src/storm/utility/random.cpp @@ -37,6 +37,13 @@ namespace storm { } + BernoulliDistributionGenerator::BernoulliDistributionGenerator(double prob) : distribution(prob) { + } + + bool BernoulliDistributionGenerator::random(boost::mt19937& engine) { + return distribution(engine); + } + ExponentialDistributionGenerator::ExponentialDistributionGenerator(double rate) : distribution(rate) { } diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h index 80a8d5e61..d99f81f53 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -42,6 +42,14 @@ namespace storm { }; + class BernoulliDistributionGenerator { + public: + BernoulliDistributionGenerator(double prob); + bool random(boost::mt19937& engine); + private: + boost::random::bernoulli_distribution<> distribution; + }; + class ExponentialDistributionGenerator { public: ExponentialDistributionGenerator(double rate); diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index 3bc92bb7f..bfb07e3fa 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -87,6 +87,18 @@ namespace { EXPECT_NEAR(result, 0.9985116987, 0.01); } + TEST(DftSimulatorTest, PdepUnreliability) { + double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft", 1, 10000); + EXPECT_NEAR(result, 0.2017690905, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft", 1, 10000); + EXPECT_NEAR(result, 0.2401091405, 0.01); + result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft", 1, 10000); + EXPECT_NEAR(result, 0.2259856274, 0.01); + // Examle pdep4 contains non-determinism which is not handled in simulation + //result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft", 1, 10000); + //EXPECT_NEAR(result, 0.008122157897, 0.01); + } + TEST(DftSimulatorTest, SpareUnreliability) { double result = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/spare.dft", 1, 10000); EXPECT_NEAR(result, 0.1118530638, 0.01);