storm::modelchecker::helper::internal Namespace Reference

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)

Enumeration Type Documentation

LraViTransitionsType

enum class storm::modelchecker::helper::internal::LraViTransitionsType

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.

Enumerator
DetTsNoIs
DetTsNondetIs	deterministic choice at timed states, no instant states (as in DTMCs and CTMCs)
DetTsDetIs	deterministic choice at timed states, nondeterministic choice at instant states (as in Markov Automata)
NondetTsNoIs	deterministic choice at timed states, deterministic choice at instant states (as in Markov Automata without any nondeterminisim) nondeterministic choice at timed states, no instant states (as in MDPs)

Definition at line 22 of file LraViHelper.h.

Function Documentation

componentElementChoicesContains() [1/2]

bool storm::modelchecker::helper::internal::componentElementChoicesContains ( storm::storage::MaximalEndComponent::map_type::value_type const &  element, uint64_t  choice  )

inline

Definition at line 43 of file ComponentUtility.h.

componentElementChoicesContains() [2/2]

bool storm::modelchecker::helper::internal::componentElementChoicesContains ( typename storm::storage::StronglyConnectedComponent::value_type const &  element, uint64_t  choice  )

inline

Definition at line 25 of file ComponentUtility.h.

getComponentElementChoiceCount() [1/2]

uint64_t storm::modelchecker::helper::internal::getComponentElementChoiceCount ( typename storm::storage::MaximalEndComponent::map_type::value_type const &  element )

inline

Definition at line 32 of file ComponentUtility.h.

getComponentElementChoiceCount() [2/2]

constexpr uint64_t storm::modelchecker::helper::internal::getComponentElementChoiceCount ( typename storm::storage::StronglyConnectedComponent::value_type const &  )

inlineconstexpr

Definition at line 16 of file ComponentUtility.h.

getComponentElementChoicesBegin() [1/2]

storm::storage::MaximalEndComponent::set_type::const_iterator storm::modelchecker::helper::internal::getComponentElementChoicesBegin ( typename storm::storage::MaximalEndComponent::map_type::value_type const &  element )

inline

Definition at line 35 of file ComponentUtility.h.

getComponentElementChoicesBegin() [2/2]

uint64_t const * storm::modelchecker::helper::internal::getComponentElementChoicesBegin ( typename storm::storage::StronglyConnectedComponent::value_type const &  element )

inline

Definition at line 19 of file ComponentUtility.h.

getComponentElementChoicesEnd() [1/2]

storm::storage::MaximalEndComponent::set_type::const_iterator storm::modelchecker::helper::internal::getComponentElementChoicesEnd ( typename storm::storage::MaximalEndComponent::map_type::value_type const &  element )

inline

Definition at line 39 of file ComponentUtility.h.

getComponentElementChoicesEnd() [2/2]

uint64_t const * storm::modelchecker::helper::internal::getComponentElementChoicesEnd ( typename storm::storage::StronglyConnectedComponent::value_type const &  element )

inline

Definition at line 22 of file ComponentUtility.h.

getComponentElementState() [1/2]

uint64_t storm::modelchecker::helper::internal::getComponentElementState ( typename storm::storage::MaximalEndComponent::map_type::value_type const &  element )

inline

Definition at line 29 of file ComponentUtility.h.

getComponentElementState() [2/2]

uint64_t storm::modelchecker::helper::internal::getComponentElementState ( typename storm::storage::StronglyConnectedComponent::value_type const &  element )

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.