Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DFTTraceSimulator.cpp
Go to the documentation of this file.
1#include "DFTTraceSimulator.h"
2
3namespace storm::dft {
4namespace simulator {
5
6template<typename ValueType>
8 storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo, boost::mt19937& randomGenerator)
9 : dft(dft), stateGenerationInfo(stateGenerationInfo), generator(dft, stateGenerationInfo), randomGenerator(randomGenerator) {
10 // Set initial state
12}
13
14template<typename ValueType>
15void DFTTraceSimulator<ValueType>::setRandomNumberGenerator(boost::mt19937& randomNumberGenerator) {
16 this->randomGenerator = randomNumberGenerator;
17}
18
19template<typename ValueType>
21 resetToState(generator.createInitialState());
22 setTime(0);
23}
24
25template<typename ValueType>
26void DFTTraceSimulator<ValueType>::resetToState(DFTStatePointer state) {
27 this->state = state;
28}
29
30template<typename ValueType>
32 this->time = time;
33}
34
35template<typename ValueType>
36typename DFTTraceSimulator<ValueType>::DFTStatePointer DFTTraceSimulator<ValueType>::getCurrentState() const {
37 return state;
38}
39
40template<typename ValueType>
42 return time;
43}
44
45template<typename ValueType>
46std::tuple<storm::dft::storage::FailableElements::const_iterator, double, bool> DFTTraceSimulator<ValueType>::randomNextFailure() {
47 auto iterFailable = state->getFailableElements().begin();
48
49 // Check for absorbing state:
50 // - either no relevant event remains (i.e., all relevant events have failed already), or
51 // - no BE can fail
52 if (!state->hasOperationalRelevantEvent() || iterFailable == state->getFailableElements().end()) {
53 STORM_LOG_TRACE("No successor states available for " << state->getId());
54 return std::make_tuple(iterFailable, -1, true);
55 }
56
57 // Get all failable elements
58 if (iterFailable.isFailureDueToDependency()) {
59 if (iterFailable.isConflictingDependency()) {
60 // We take the first dependency to resolve the non-determinism
61 STORM_LOG_WARN("Non-determinism present! We take the dependency with the lowest id");
62 }
63
64 auto dependency = iterFailable.asDependency(dft);
65 bool successful = true;
66 if (!dependency->isFDEP()) {
67 // Flip a coin whether the PDEP is successful
68 storm::utility::BernoulliDistributionGenerator probGenerator(dependency->probability());
69 successful = probGenerator.random(randomGenerator);
70 }
71 STORM_LOG_TRACE("Let dependency " << *dependency << " " << (successful ? "successfully" : "unsuccessfully") << " fail");
72 return std::make_tuple(iterFailable, 0, successful);
73 } else {
74 // Consider all "normal" BE failures
75 // Initialize with first BE
77 double rate = state->getBERate(nextFail.asBE(dft)->id());
79 double smallestTimebound = rateGenerator.random(randomGenerator);
80 ++iterFailable;
81
82 // Consider all other BEs and find the one which fails first
83 for (; iterFailable != state->getFailableElements().end(); ++iterFailable) {
84 rate = state->getBERate(iterFailable.asBE(dft)->id());
86 double timebound = rateGenerator.random(randomGenerator);
87 if (timebound < smallestTimebound) {
88 // BE fails earlier -> use as nextFail
89 nextFail = iterFailable;
90 smallestTimebound = timebound;
91 }
92 }
93 STORM_LOG_TRACE("Let BE " << *nextFail.asBE(dft) << " fail after time " << smallestTimebound);
94 return std::make_tuple(nextFail, smallestTimebound, true);
95 }
96}
97
98template<>
99std::tuple<storm::dft::storage::FailableElements::const_iterator, double, bool> DFTTraceSimulator<storm::RationalFunction>::randomNextFailure() {
100 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs.");
101}
102
103template<typename ValueType>
105 // Randomly generate next failure
106 auto [nextFailable, addTime, successfulDependency] = this->randomNextFailure();
107 if (addTime < 0) {
108 // No next state can be reached, because no element can fail anymore.
109 STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because no element can fail anymore");
111 }
112
113 // Apply next failure
114 auto stepResult = step(nextFailable, successfulDependency);
115 STORM_LOG_TRACE("Current state: " << dft.getStateString(state));
116
117 // Update time
118 this->time += addTime;
119 return stepResult;
120}
121
122template<typename ValueType>
124 if (nextFailElement == state->getFailableElements().end()) {
125 // No next failure possible
127 }
128
129 DFTStatePointer newState;
130 if (nextFailElement.isFailureDueToDependency()) {
131 newState = generator.createSuccessorState(state, nextFailElement.asDependency(dft), dependencySuccessful);
132 } else {
133 newState = generator.createSuccessorState(state, nextFailElement.asBE(dft));
134 }
135
136 if (newState->isInvalid() || newState->isTransient()) {
137 STORM_LOG_TRACE("Step is invalid because new state " << (newState->isInvalid() ? "is invalid." : "has transient fault."));
139 }
140
141 state = newState;
143}
144
145template<typename ValueType>
147 // Perform random step
148 SimulationStepResult stepResult = randomStep();
149
150 // Check current state
151 if (stepResult == SimulationStepResult::INVALID) {
152 // No next state can be reached, because the state is invalid.
153 STORM_LOG_TRACE("Invalid state " << dft.getStateString(state) << " was reached.");
154 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Handling of invalid states is not supported for simulation");
156 } else if (stepResult == SimulationStepResult::UNSUCCESSFUL) {
157 STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because no further failures are possible.");
159 }
160 STORM_LOG_ASSERT(stepResult == SimulationStepResult::SUCCESSFUL, "Simulation step should be successful.");
161
162 if (getCurrentTime() > timebound) {
163 // Timebound was exceeded
165 } else if (state->hasFailed(dft.getTopLevelIndex())) {
166 // DFT is failed
167 STORM_LOG_TRACE("DFT has failed after " << getCurrentTime());
169 } else {
170 // No conclusive outcome was reached yet
172 }
173}
174
175template<typename ValueType>
177 resetToInitial();
178
179 // Check whether DFT is initially already failed.
180 if (state->hasFailed(dft.getTopLevelIndex())) {
181 STORM_LOG_TRACE("DFT is initially failed");
183 }
184
186 do {
187 result = simulateNextStep(timebound);
188 } while (result == SimulationTraceResult::CONTINUE);
189 return result;
190}
191
192template<>
194 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs.");
195}
196
197template class DFTTraceSimulator<double>;
199
200} // namespace simulator
201} // namespace storm::dft
SimulationStepResult step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful=true)
Perform one simulation step by letting the next element fail.
void resetToState(DFTStatePointer state)
Set the current state back to the given state.
std::tuple< storm::dft::storage::FailableElements::const_iterator, double, bool > randomNextFailure()
Randomly pick an element which fails next (either a BE or a dependency which triggers a BE) and the t...
SimulationTraceResult simulateNextStep(double timebound)
Simulate the (randomly chosen) next step and return the outcome of the current (partial) trace.
void setTime(double time)
Set the elapsed time so far.
double getCurrentTime() const
Get the total elapsed time so far.
SimulationStepResult randomStep()
Perform a random step by using the random number generator.
SimulationTraceResult simulateCompleteTrace(double timebound)
Perform a complete simulation of a failure trace by using the random number generator.
DFTTraceSimulator(storm::dft::storage::DFT< ValueType > const &dft, storm::dft::storage::DFTStateGenerationInfo const &stateGenerationInfo, boost::mt19937 &randomGenerator)
Constructor.
void resetToInitial()
Set the current state back to the initial state in order to start a new simulation.
void setRandomNumberGenerator(boost::mt19937 &randomNumberGenerator)
Set the random number generator.
DFTStatePointer getCurrentState() const
Get the current DFT state.
Represents a Dynamic Fault Tree.
Definition DFT.h:52
std::shared_ptr< storm::dft::storage::elements::DFTBE< ValueType > const > asBE(storm::dft::storage::DFT< ValueType > const &dft) const
Return the current iterator as a BE which fails next.
bool isFailureDueToDependency() const
Return whether the current failure is due to a dependency (or the BE itself).
std::shared_ptr< storm::dft::storage::elements::DFTDependency< ValueType > const > asDependency(storm::dft::storage::DFT< ValueType > const &dft) const
Return the current iterator as a dependency which triggers next.
bool random(boost::mt19937 &engine)
Definition random.cpp:39
double random(boost::mt19937 &engine)
Definition random.cpp:45
#define STORM_LOG_WARN(message)
Definition logging.h:30
#define STORM_LOG_TRACE(message)
Definition logging.h:17
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SimulationStepResult
Result of a single simulation step.
SimulationTraceResult
Result of a simulation trace.