Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::dft::storage Namespace Reference

Namespaces

namespace  elements
 

Classes

struct  BEColourClass
 
struct  BijectionCandidates
 
class  BucketPriorityQueue
 Priority queue based on buckets. More...
 
class  DFT
 Represents a Dynamic Fault Tree. More...
 
class  DFTColouring
 
struct  DFTElementSort
 
class  DftIndependentModule
 Represents an independent module/subtree. More...
 
class  DFTIsomorphismCheck
 Saves isomorphism between subtrees. More...
 
class  DftJsonExporter
 Exports a DFT into the JSON format. More...
 
struct  DFTLayoutInfo
 
class  DftModule
 Represents a module/subtree in a DFT. More...
 
class  DFTState
 
class  DFTStateGenerationInfo
 
class  DFTStateSpaceGenerationQueues
 
class  DftSymmetries
 
class  FailableElements
 Handling of currently failable elements (BEs) either due to their own failure or because of dependencies. More...
 
struct  GateGroupToHash
 
struct  OrderElementsById
 
struct  OrderElementsByRank
 
class  SylvanBddManager
 Simple Manager for Sylvan. More...
 

Enumerations

enum class  DFTElementState { Operational = 0 , Failed = 2 , Failsafe = 1 , DontCare = 3 }
 
enum class  DFTDependencyState { Passive = 0 , Unsuccessful = 1 , Successful = 2 , DontCare = 3 }
 

Functions

std::set< storm::RationalFunctionVariablegetParameters (DFT< storm::RationalFunction > const &dft)
 Get all rate/probability parameters occurring in the DFT.
 
std::ostream & operator<< (std::ostream &os, DFTElementState st)
 
char toChar (DFTElementState st)
 
std::ostream & operator<< (std::ostream &os, DFTDependencyState st)
 
char toChar (DFTDependencyState st)
 
template<typename ValueType >
bool operator== (BEColourClass< ValueType > const &lhs, BEColourClass< ValueType > const &rhs)
 
std::ostream & operator<< (std::ostream &os, DftSymmetries const &symmetries)
 

Enumeration Type Documentation

◆ DFTDependencyState

Enumerator
Passive 
Unsuccessful 
Successful 
DontCare 

Definition at line 42 of file DFTElementState.h.

◆ DFTElementState

Enumerator
Operational 
Failed 
Failsafe 
DontCare 

Definition at line 8 of file DFTElementState.h.

Function Documentation

◆ getParameters()

std::set< storm::RationalFunctionVariable > storm::dft::storage::getParameters ( DFT< storm::RationalFunction > const &  dft)

Get all rate/probability parameters occurring in the DFT.

Parameters
dftDFT.
Returns
Set of parameters.

Definition at line 825 of file DFT.cpp.

◆ operator<<() [1/3]

std::ostream & storm::dft::storage::operator<< ( std::ostream &  os,
DFTDependencyState  st 
)
inline

Definition at line 44 of file DFTElementState.h.

◆ operator<<() [2/3]

std::ostream & storm::dft::storage::operator<< ( std::ostream &  os,
DFTElementState  st 
)
inline

Definition at line 10 of file DFTElementState.h.

◆ operator<<() [3/3]

std::ostream & storm::dft::storage::operator<< ( std::ostream &  os,
DftSymmetries const &  symmetries 
)

Definition at line 148 of file DftSymmetries.cpp.

◆ operator==()

template<typename ValueType >
bool storm::dft::storage::operator== ( BEColourClass< ValueType > const &  lhs,
BEColourClass< ValueType > const &  rhs 
)

Definition at line 82 of file DFTIsomorphism.h.

◆ toChar() [1/2]

char storm::dft::storage::toChar ( DFTDependencyState  st)
inline

Definition at line 60 of file DFTElementState.h.

◆ toChar() [2/2]

char storm::dft::storage::toChar ( DFTElementState  st)
inline

Definition at line 26 of file DFTElementState.h.