DFTTraceSimulator.h

Go to the documentation of this file.

#pragma once
 
#include "storm-dft/generator/DftNextStateGenerator.h"
#include "storm-dft/storage/DFT.h"
#include "storm-dft/storage/DFTState.h"
#include "storm-dft/storage/FailableElements.h"
 
#include "storm/utility/random.h"
 
namespace storm::dft {
namespace simulator {
 
enum class SimulationStepResult { SUCCESSFUL, UNSUCCESSFUL, INVALID };
 
enum class SimulationTraceResult { SUCCESSFUL, UNSUCCESSFUL, INVALID, CONTINUE };
 
template<typename ValueType>
class DFTTraceSimulator {
    using DFTStatePointer = std::shared_ptr<storm::dft::storage::DFTState<ValueType>>;
 
   public:
    DFTTraceSimulator(storm::dft::storage::DFT<ValueType> const& dft, storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo,
                      boost::mt19937& randomGenerator);
 
    void setRandomNumberGenerator(boost::mt19937& randomNumberGenerator);
 
    void resetToInitial();
 
    void resetToState(DFTStatePointer state);
 
    void setTime(double time);
 
    DFTStatePointer getCurrentState() const;
 
    double getCurrentTime() const;
 
    SimulationStepResult step(storm::dft::storage::FailableElements::const_iterator nextFailElement, bool dependencySuccessful = true);
 
    std::tuple<storm::dft::storage::FailableElements::const_iterator, double, bool> randomNextFailure();
 
    SimulationStepResult randomStep();
 
    SimulationTraceResult simulateNextStep(double timebound);
 
    SimulationTraceResult simulateCompleteTrace(double timebound);
 
   protected:
    // The DFT used for the generation of next states.
    storm::dft::storage::DFT<ValueType> const& dft;
 
    // General information for the state generation.
    storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo;
 
    // Generator for creating next state in DFT
    storm::dft::generator::DftNextStateGenerator<ValueType> generator;
 
    // Current state
    DFTStatePointer state;
 
    // Currently elapsed time
    double time;
 
    // Random number generator
    boost::mt19937& randomGenerator;
};
 
}  // namespace simulator
}  // namespace storm::dft