Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
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

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.