Storm
A Modern Probabilistic Model Checker
|
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::RationalFunctionVariable > | getParameters (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) |
|
strong |
Enumerator | |
---|---|
Passive | |
Unsuccessful | |
Successful | |
DontCare |
Definition at line 42 of file DFTElementState.h.
|
strong |
Enumerator | |
---|---|
Operational | |
Failed | |
Failsafe | |
DontCare |
Definition at line 8 of file DFTElementState.h.
std::set< storm::RationalFunctionVariable > storm::dft::storage::getParameters | ( | DFT< storm::RationalFunction > const & | dft | ) |
|
inline |
Definition at line 44 of file DFTElementState.h.
|
inline |
Definition at line 10 of file DFTElementState.h.
std::ostream & storm::dft::storage::operator<< | ( | std::ostream & | os, |
DftSymmetries const & | symmetries | ||
) |
Definition at line 148 of file DftSymmetries.cpp.
bool storm::dft::storage::operator== | ( | BEColourClass< ValueType > const & | lhs, |
BEColourClass< ValueType > const & | rhs | ||
) |
Definition at line 82 of file DFTIsomorphism.h.
|
inline |
Definition at line 60 of file DFTElementState.h.
|
inline |
Definition at line 26 of file DFTElementState.h.