Storm
A Modern Probabilistic Model Checker
|
Classes | |
class | LraViHelper |
Helper class that performs iterations of the value iteration method. More... | |
class | SparseLTLSchedulerHelper |
Helper class for scheduler construction in LTL model checking. More... | |
Enumerations | |
enum class | LraViTransitionsType { DetTsNoIs , DetTsNondetIs , DetTsDetIs , NondetTsNoIs } |
Specifies differnt kinds of transition types with which this helper can be used Ts means timed states (cf. More... | |
Functions | |
uint64_t | getComponentElementState (typename storm::storage::StronglyConnectedComponent::value_type const &element) |
Auxiliary functions that deal with the different kinds of components (MECs on potentially nondeterministic models and BSCCs on deterministic models) | |
constexpr uint64_t | getComponentElementChoiceCount (typename storm::storage::StronglyConnectedComponent::value_type const &) |
uint64_t const * | getComponentElementChoicesBegin (typename storm::storage::StronglyConnectedComponent::value_type const &element) |
uint64_t const * | getComponentElementChoicesEnd (typename storm::storage::StronglyConnectedComponent::value_type const &element) |
bool | componentElementChoicesContains (typename storm::storage::StronglyConnectedComponent::value_type const &element, uint64_t choice) |
uint64_t | getComponentElementState (typename storm::storage::MaximalEndComponent::map_type::value_type const &element) |
uint64_t | getComponentElementChoiceCount (typename storm::storage::MaximalEndComponent::map_type::value_type const &element) |
storm::storage::MaximalEndComponent::set_type::const_iterator | getComponentElementChoicesBegin (typename storm::storage::MaximalEndComponent::map_type::value_type const &element) |
storm::storage::MaximalEndComponent::set_type::const_iterator | getComponentElementChoicesEnd (typename storm::storage::MaximalEndComponent::map_type::value_type const &element) |
bool | componentElementChoicesContains (storm::storage::MaximalEndComponent::map_type::value_type const &element, uint64_t choice) |
|
strong |
Specifies differnt kinds of transition types with which this helper can be used Ts means timed states (cf.
Markovian states in a Markov Automaton) and Is means instant states (cf. probabilistic states in a Markov automaton). The way to think about this is that time can only pass in a timed state, whereas transitions emerging from an instant state fire immediately In an MDP, all states are seen as timed. In this enum, we also specify whether there can be a nondeterministic choice at the corresponding states or not.
Definition at line 22 of file LraViHelper.h.
|
inline |
Definition at line 43 of file ComponentUtility.h.
|
inline |
Definition at line 25 of file ComponentUtility.h.
|
inline |
Definition at line 32 of file ComponentUtility.h.
|
inlineconstexpr |
Definition at line 16 of file ComponentUtility.h.
|
inline |
Definition at line 35 of file ComponentUtility.h.
|
inline |
Definition at line 19 of file ComponentUtility.h.
|
inline |
Definition at line 39 of file ComponentUtility.h.
|
inline |
Definition at line 22 of file ComponentUtility.h.
|
inline |
Definition at line 29 of file ComponentUtility.h.
|
inline |
Auxiliary functions that deal with the different kinds of components (MECs on potentially nondeterministic models and BSCCs on deterministic models)
Definition at line 13 of file ComponentUtility.h.