Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DftTransformer.h
Go to the documentation of this file.
1#pragma once
2
3#include "storm-dft/storage/DFT.h"
4
5namespace storm::dft {
6namespace transformations {
7
11template<typename ValueType>
12class DftTransformer {
13 public:
19 static bool hasUniqueFailedBE(storm::dft::storage::DFT<ValueType> const &dft);
20
29 static std::shared_ptr<storm::dft::storage::DFT<ValueType>> transformUniqueFailedBE(storm::dft::storage::DFT<ValueType> const &dft);
30
36 static bool hasNonBinaryDependency(storm::dft::storage::DFT<ValueType> const &dft);
37
44 static std::shared_ptr<storm::dft::storage::DFT<ValueType>> transformBinaryDependencies(storm::dft::storage::DFT<ValueType> const &dft);
45
51 static bool hasOnlyExponentialDistributions(storm::dft::storage::DFT<ValueType> const &dft);
52
61 static std::shared_ptr<storm::dft::storage::DFT<ValueType>> transformExponentialDistributions(storm::dft::storage::DFT<ValueType> const &dft);
62};
63
64} // namespace transformations
65} // namespace storm::dft
storm::dft::storage::DFT
Represents a Dynamic Fault Tree.
Definition DFT.h:52
storm::dft::transformations::DftTransformer
Transformer for operations on DFT.
Definition DftTransformer.h:12
storm::dft::transformations::DftTransformer::hasUniqueFailedBE
static bool hasUniqueFailedBE(storm::dft::storage::DFT< ValueType > const &dft)
Check whether at most one constant failed BE is present in the DFT.
Definition DftTransformer.cpp:12
storm::dft::transformations::DftTransformer::transformUniqueFailedBE
static std::shared_ptr< storm::dft::storage::DFT< ValueType > > transformUniqueFailedBE(storm::dft::storage::DFT< ValueType > const &dft)
Introduce unique BE which is always failed (instead of multiple ones).
Definition DftTransformer.cpp:40
storm::dft::transformations::DftTransformer::hasNonBinaryDependency
static bool hasNonBinaryDependency(storm::dft::storage::DFT< ValueType > const &dft)
Check whether the DFT has dependencies with multiple dependent events.
Definition DftTransformer.cpp:95
storm::dft::transformations::DftTransformer::transformBinaryDependencies
static std::shared_ptr< storm::dft::storage::DFT< ValueType > > transformBinaryDependencies(storm::dft::storage::DFT< ValueType > const &dft)
Introduce binary dependencies (with only one dependent event) instead of dependencies with multiple d...
Definition DftTransformer.cpp:108
storm::dft::transformations::DftTransformer::hasOnlyExponentialDistributions
static bool hasOnlyExponentialDistributions(storm::dft::storage::DFT< ValueType > const &dft)
Check whether the DFT contains only BEs with exponential distributions (or constant failed/failsafe B...
Definition DftTransformer.cpp:162
storm::dft::transformations::DftTransformer::transformExponentialDistributions
static std::shared_ptr< storm::dft::storage::DFT< ValueType > > transformExponentialDistributions(storm::dft::storage::DFT< ValueType > const &dft)
Replace certain BE distributions by DFT constructs using only exponential distributions to make them ...
Definition DftTransformer.cpp:176