Skip to content

Commit

Permalink
Revised DFT simulation (#582)
Browse files Browse the repository at this point in the history
  • Loading branch information
volkm authored Aug 12, 2024
2 parents 8289db9 + 42acfee commit ed78ed0
Show file tree
Hide file tree
Showing 7 changed files with 352 additions and 88 deletions.
137 changes: 75 additions & 62 deletions src/storm-dft/simulator/DFTTraceSimulator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ DFTTraceSimulator<ValueType>::DFTTraceSimulator(storm::dft::storage::DFT<ValueTy
storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo, boost::mt19937& randomGenerator)
: dft(dft), stateGenerationInfo(stateGenerationInfo), generator(dft, stateGenerationInfo), randomGenerator(randomGenerator) {
// Set initial state
state = generator.createInitialState();
resetToInitial();
}

template<typename ValueType>
Expand All @@ -18,14 +18,30 @@ void DFTTraceSimulator<ValueType>::setRandomNumberGenerator(boost::mt19937& rand

template<typename ValueType>
void DFTTraceSimulator<ValueType>::resetToInitial() {
state = generator.createInitialState();
resetToState(generator.createInitialState());
setTime(0);
}

template<typename ValueType>
void DFTTraceSimulator<ValueType>::resetToState(DFTStatePointer state) {
this->state = state;
}

template<typename ValueType>
void DFTTraceSimulator<ValueType>::setTime(double time) {
this->time = time;
}

template<typename ValueType>
typename DFTTraceSimulator<ValueType>::DFTStatePointer DFTTraceSimulator<ValueType>::getCurrentState() const {
return state;
}

template<typename ValueType>
double DFTTraceSimulator<ValueType>::getCurrentTime() const {
return time;
}

template<typename ValueType>
std::tuple<storm::dft::storage::FailableElements::const_iterator, double, bool> DFTTraceSimulator<ValueType>::randomNextFailure() {
auto iterFailable = state->getFailableElements().begin();
Expand Down Expand Up @@ -85,21 +101,29 @@ std::tuple<storm::dft::storage::FailableElements::const_iterator, double, bool>
}

template<typename ValueType>
std::pair<SimulationResult, double> DFTTraceSimulator<ValueType>::randomStep() {
auto [nextFailable, time, successful] = this->randomNextFailure();
if (time < 0) {
return std::make_pair(SimulationResult::UNSUCCESSFUL, -1);
} else {
// Apply next failure
return std::make_pair(step(nextFailable, successful), time);
SimulationStepResult DFTTraceSimulator<ValueType>::randomStep() {
// Randomly generate next failure
auto [nextFailable, addTime, successfulDependency] = this->randomNextFailure();
if (addTime < 0) {
// No next state can be reached, because no element can fail anymore.
STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because no element can fail anymore");
return SimulationStepResult::UNSUCCESSFUL;
}

// Apply next failure
auto stepResult = step(nextFailable, successfulDependency);
STORM_LOG_TRACE("Current state: " << dft.getStateString(state));

// Update time
this->time += addTime;
return stepResult;
}

template<typename ValueType>
SimulationResult DFTTraceSimulator<ValueType>::step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful) {
SimulationStepResult DFTTraceSimulator<ValueType>::step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful) {
if (nextFailElement == state->getFailableElements().end()) {
// No next failure possible
return SimulationResult::UNSUCCESSFUL;
return SimulationStepResult::UNSUCCESSFUL;
}

DFTStatePointer newState;
Expand All @@ -111,73 +135,62 @@ SimulationResult DFTTraceSimulator<ValueType>::step(storm::dft::storage::Failabl

if (newState->isInvalid() || newState->isTransient()) {
STORM_LOG_TRACE("Step is invalid because new state " << (newState->isInvalid() ? "is invalid." : "has transient fault."));
return SimulationResult::INVALID;
return SimulationStepResult::INVALID;
}

state = newState;
return SimulationResult::SUCCESSFUL;
return SimulationStepResult::SUCCESSFUL;
}

template<typename ValueType>
SimulationResult DFTTraceSimulator<ValueType>::simulateCompleteTrace(double timebound) {
SimulationTraceResult DFTTraceSimulator<ValueType>::simulateNextStep(double timebound) {
// Perform random step
SimulationStepResult stepResult = randomStep();

// Check current state
if (stepResult == SimulationStepResult::INVALID) {
// No next state can be reached, because the state is invalid.
STORM_LOG_TRACE("Invalid state " << dft.getStateString(state) << " was reached.");
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Handling of invalid states is not supported for simulation");
return SimulationTraceResult::INVALID;
} else if (stepResult == SimulationStepResult::UNSUCCESSFUL) {
STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because no further failures are possible.");
return SimulationTraceResult::UNSUCCESSFUL;
}
STORM_LOG_ASSERT(stepResult == SimulationStepResult::SUCCESSFUL, "Simulation step should be successful.");

if (getCurrentTime() > timebound) {
// Timebound was exceeded
return SimulationTraceResult::UNSUCCESSFUL;
} else if (state->hasFailed(dft.getTopLevelIndex())) {
// DFT is failed
STORM_LOG_TRACE("DFT has failed after " << getCurrentTime());
return SimulationTraceResult::SUCCESSFUL;
} else {
// No conclusive outcome was reached yet
return SimulationTraceResult::CONTINUE;
}
}

template<typename ValueType>
SimulationTraceResult DFTTraceSimulator<ValueType>::simulateCompleteTrace(double timebound) {
resetToInitial();

// Check whether DFT is initially already failed.
if (state->hasFailed(dft.getTopLevelIndex())) {
STORM_LOG_TRACE("DFT is initially failed");
return SimulationResult::SUCCESSFUL;
return SimulationTraceResult::SUCCESSFUL;
}

double time = 0;
while (time <= timebound) {
// Generate next failure
auto retTuple = randomNextFailure();
storm::dft::storage::FailableElements::const_iterator nextFailable = std::get<0>(retTuple);
double addTime = std::get<1>(retTuple);
bool successfulDependency = std::get<2>(retTuple);
if (addTime < 0) {
// No next state can be reached, because no element can fail anymore.
STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because no element can fail anymore");
return SimulationResult::UNSUCCESSFUL;
}

// TODO: exit if time would be up after this failure
// This is only correct if no invalid states are possible! (no restrictors and no transient failures)

// Apply next failure
auto stepResult = step(nextFailable, successfulDependency);
STORM_LOG_TRACE("Current state: " << dft.getStateString(state));

// Check whether state is invalid
if (stepResult != SimulationResult::SUCCESSFUL) {
STORM_LOG_ASSERT(stepResult == SimulationResult::INVALID, "Result of simulation step should be invalid.");
// No next state can be reached, because the state is invalid.
STORM_LOG_TRACE("No next state possible in state " << dft.getStateString(state) << " because simulation was invalid");
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Handling of invalid states is not supported for simulation");
return SimulationResult::INVALID;
}

// Check whether time is up
// Checking whether the time is up must be performed after checking if a state is invalid.
// Otherwise we would erroneously mark invalid traces as unsuccessful.
time += addTime;
if (time > timebound) {
STORM_LOG_TRACE("Time limit" << timebound << " exceeded: " << time);
return SimulationResult::UNSUCCESSFUL;
}

// Check whether DFT is failed
if (state->hasFailed(dft.getTopLevelIndex())) {
STORM_LOG_TRACE("DFT has failed after " << time);
return SimulationResult::SUCCESSFUL;
}
}
STORM_LOG_ASSERT(false, "Should not be reachable");
return SimulationResult::UNSUCCESSFUL;
SimulationTraceResult result = SimulationTraceResult::CONTINUE;
do {
result = simulateNextStep(timebound);
} while (result == SimulationTraceResult::CONTINUE);
return result;
}

template<>
SimulationResult DFTTraceSimulator<storm::RationalFunction>::simulateCompleteTrace(double timebound) {
SimulationTraceResult DFTTraceSimulator<storm::RationalFunction>::simulateCompleteTrace(double timebound) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Simulation not support for parametric DFTs.");
}

Expand Down
60 changes: 48 additions & 12 deletions src/storm-dft/simulator/DFTTraceSimulator.h
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,16 @@ namespace storm::dft {
namespace simulator {

/*!
* Simulation result.
* Result of a single simulation step.
*
*/
enum class SimulationResult { SUCCESSFUL, UNSUCCESSFUL, INVALID };
enum class SimulationStepResult { SUCCESSFUL, UNSUCCESSFUL, INVALID };

/*!
* Result of a simulation trace.
* CONTINUE is only used for partial traces to indicate that no conclusive outcome has been reached yet.
*/
enum class SimulationTraceResult { SUCCESSFUL, UNSUCCESSFUL, INVALID, CONTINUE };

/*!
* Simulator for DFTs.
Expand Down Expand Up @@ -45,26 +51,43 @@ class DFTTraceSimulator {
void setRandomNumberGenerator(boost::mt19937& randomNumberGenerator);

/*!
* Set the current state back to the intial state in order to start a new simulation.
* Set the current state back to the initial state in order to start a new simulation.
*/
void resetToInitial();

/*!
* Set the current state back to the given state.
*/
void resetToState(DFTStatePointer state);

/*!
* Set the elapsed time so far.
*/
void setTime(double time);

/*!
* Get the current DFT state.
*
* @return DFTStatePointer DFT state.
*/
DFTStatePointer getCurrentState() const;

/*!
* Get the total elapsed time so far.
*
* @return Elapsed time.
*/
double getCurrentTime() const;

/*!
* 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 Successful if step could be performed, unsuccesful if no element can fail or invalid if the next state is invalid (due to a restrictor).
* If the dependency is unsuccessful, no BE fails and only the dependency is marked as failed.
* @return Successful if step could be performed, unsuccessful if no element can fail or invalid if the next state is invalid (due to a restrictor).
*/
SimulationResult step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful = true);
SimulationStepResult 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.
Expand All @@ -78,9 +101,19 @@ class DFTTraceSimulator {
/*!
* Perform a random step by using the random number generator.
*
* @return Pair of the simulation result (successful, unsuccesful, invalid) and the time which progessed between the last step and this step.
* @return Result of the simulation step (successful, unsuccessful, invalid).
*/
std::pair<SimulationResult, double> randomStep();
SimulationStepResult randomStep();

/*!
* Simulate the (randomly chosen) next step and return the outcome of the current (partial) trace.
*
* @param timebound Time bound in which the system failure should occur.
* @return Result of (partial) trace is (1) SUCCESSFUL if the current state corresponds to a system failure and the current time does not exceed the
* timebound. (2) UNSUCCESSFUL, if the current time exceeds the timebound, (3) INVALID, if an invalid state (due to a restrictor) was reached, or (4)
* CONTINUE, if the simulation should continue.
*/
SimulationTraceResult simulateNextStep(double timebound);

/*!
* Perform a complete simulation of a failure trace by using the random number generator.
Expand All @@ -89,11 +122,11 @@ class DFTTraceSimulator {
* If an invalid state (due to a restrictor) was reached, the simulated trace is invalid.
*
* @param timebound Time bound in which the system failure should occur.
* @return Simulation result is (1) successful if a system failure occurred for the generated trace within the time bound,
* (2) unsuccesfull, if no system failure occurred within the time bound, or
* (3) invalid, if an invalid state (due to a restrictor) was reached during the trace generation.
* @return Result of simulation trace is (1) SUCCESSFUL if a system failure occurred for the generated trace within the time bound,
* (2) UNSUCCESSFUL, if no system failure occurred within the time bound, or
* (3) INVALID, if an invalid state (due to a restrictor) was reached during the trace generation.
*/
SimulationResult simulateCompleteTrace(double timebound);
SimulationTraceResult simulateCompleteTrace(double timebound);

protected:
// The DFT used for the generation of next states.
Expand All @@ -108,6 +141,9 @@ class DFTTraceSimulator {
// Current state
DFTStatePointer state;

// Currently elapsed time
double time;

// Random number generator
boost::mt19937& randomGenerator;
};
Expand Down
32 changes: 32 additions & 0 deletions src/storm-dft/simulator/ImportanceFunction.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
#include "ImportanceFunction.h"

namespace storm::dft {
namespace simulator {

template<typename ValueType>
ImportanceFunction<ValueType>::ImportanceFunction(storm::dft::storage::DFT<ValueType> const& dft) : dft(dft) {}

template<typename ValueType>
BECountImportanceFunction<ValueType>::BECountImportanceFunction(storm::dft::storage::DFT<ValueType> const& dft) : ImportanceFunction<ValueType>(dft) {}

template<typename ValueType>
double BECountImportanceFunction<ValueType>::getImportance(typename ImportanceFunction<ValueType>::DFTStatePointer state) const {
size_t count = 0;
for (auto be : this->dft.getBasicElements()) {
if (state->hasFailed(be->id())) {
++count;
}
}
return count;
}

template<typename ValueType>
std::pair<double, double> BECountImportanceFunction<ValueType>::getImportanceRange() const {
return std::make_pair(0, this->dft.nrBasicElements());
}

template class BECountImportanceFunction<double>;
template class BECountImportanceFunction<storm::RationalFunction>;

} // namespace simulator
} // namespace storm::dft
Loading

0 comments on commit ed78ed0

Please sign in to comment.