mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > Class Template Reference

A class that contains a labelled transition system. More...

#include <probabilistic_lts.h>

Inheritance diagram for mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >:
mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >

Public Types

typedef lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > super
 
typedef PROBABILISTIC_STATE_T probabilistic_state_t
 The type of probabilistic labels.
 
typedef super::state_label_t state_label_t
 
typedef super::action_label_t action_label_t
 
typedef super::base_t base_t
 
typedef super::states_size_type states_size_type
 
typedef super::labels_size_type labels_size_type
 
typedef super::transitions_size_type transitions_size_type
 
- Public Types inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
typedef STATE_LABEL_T state_label_t
 The type of state labels.
 
typedef ACTION_LABEL_T action_label_t
 The type of action labels.
 
typedef LTS_BASE base_t
 The type of the used lts base.
 
typedef std::vector< STATE_LABEL_T >::size_type states_size_type
 The sort that contains the indices of states.
 
typedef std::vector< ACTION_LABEL_T >::size_type labels_size_type
 The sort that represents the indices of labels.
 
typedef std::vector< transition >::size_type transitions_size_type
 The sort that contains indices of transitions.
 

Public Member Functions

 probabilistic_lts ()
 Creates an empty LTS.
 
 probabilistic_lts (const probabilistic_lts &other)=default
 Standard copy constructor.
 
 probabilistic_lts (probabilistic_lts &&other)=default
 Standard move constructor.
 
probabilistic_ltsoperator= (const probabilistic_lts &other)=default
 Standard assignment operator.
 
probabilistic_ltsoperator= (probabilistic_lts &&other)=default
 Standard assignment move operator.
 
bool operator== (const probabilistic_lts &other) const
 Standard equality operator.
 
void swap (probabilistic_lts &other)
 Swap this lts with the supplied supplied LTS.
 
const PROBABILISTIC_STATE_T & initial_probabilistic_state () const
 Gets the initial state number of this LTS.
 
void set_initial_probabilistic_state (const PROBABILISTIC_STATE_T &state)
 Sets the probabilistic initial state number of this LTS.
 
labels_size_type num_probabilistic_states () const
 Gets the number of probabilistic states of this LTS.
 
states_size_type add_probabilistic_state (const PROBABILISTIC_STATE_T &s)
 Adds a probabilistic state to this LTS.
 
states_size_type add_and_reset_probabilistic_state (PROBABILISTIC_STATE_T &s)
 Adds a probabilistic state to this LTS and resets the state to empty.
 
void set_probabilistic_state (const states_size_type index, const PROBABILISTIC_STATE_T &s)
 Sets the probabilistic label corresponding to some index.
 
const PROBABILISTIC_STATE_T & probabilistic_state (const states_size_type index) const
 Gets the probabilistic label of an index.
 
void clear_probabilistic_states ()
 Clear the probabilistic states in this probabilistic transitions system.
 
void clear ()
 Clear the transitions system.
 
- Public Member Functions inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
 lts ()
 Creates an empty LTS.
 
 lts (const lts &l)
 Creates a copy of the supplied LTS.
 
ltsoperator= (const lts &l)
 Standard assignment operator.
 
bool operator== (const lts &other) const
 Standard equality operator.
 
void swap (lts &l)
 Swap this lts with the supplied supplied LTS.
 
states_size_type num_states () const
 Gets the number of states of this LTS.
 
std::vector< STATE_LABEL_T > & state_labels ()
 Provides the state labels of an LTS.
 
const std::vector< STATE_LABEL_T > & state_labels () const
 Provides the state labels of an LTS.
 
states_size_type num_state_labels () const
 Gets the number of state labels of this LTS.
 
void set_num_states (const states_size_type n, const bool has_state_labels=true)
 Sets the number of states of this LTS.
 
transitions_size_type num_transitions () const
 Gets the number of transitions of this LTS.
 
void set_num_action_labels (const labels_size_type n)
 Sets the number of action labels of this LTS.
 
labels_size_type num_action_labels () const
 Gets the number of action labels of this LTS.
 
states_size_type initial_state () const
 Gets the initial state number of this LTS.
 
void set_initial_state (const states_size_type state)
 Sets the initial state number of this LTS.
 
states_size_type add_state (const STATE_LABEL_T &label=STATE_LABEL_T())
 Adds a state to this LTS.
 
labels_size_type add_action (const ACTION_LABEL_T &label)
 Adds an action with a label to this LTS.
 
const labels_size_type tau_label_index () const
 Provide the index of the label that represents tau.
 
void set_state_label (const states_size_type state, const STATE_LABEL_T &label)
 Sets the label of a state.
 
const std::vector< ACTION_LABEL_T > & action_labels () const
 The action labels in this lts.
 
void set_action_label (const labels_size_type action, const ACTION_LABEL_T &label)
 Sets the label of an action.
 
const std::set< labels_size_type > & hidden_label_set () const
 Returns the hidden label set that tells for each label what its corresponding hidden label is.
 
std::set< labels_size_type > & hidden_label_set ()
 Returns the hidden label set that tells for each label what its corresponding hidden label is.
 
void set_hidden_label_set (const std::set< labels_size_type > &m)
 Sets the hidden label map that tells for each label what its corresponding hidden label is.
 
labels_size_type apply_hidden_label_map (const labels_size_type action) const
 If the action label is registered hidden, it returns tau, otherwise the original label.
 
STATE_LABEL_T state_label (const states_size_type state) const
 Gets the label of a state.
 
bool is_probabilistic (const states_size_type state) const
 Gets the label of a state.
 
ACTION_LABEL_T action_label (const labels_size_type action) const
 Gets the label of an action.
 
void clear_transitions (const std::size_t n=0)
 Clear the transitions of an lts.
 
void clear_actions ()
 Clear the action labels of an lts.
 
void clear_state_labels ()
 Clear the labels of an lts.
 
void clear ()
 Clear the transitions system.
 
const std::vector< transition > & get_transitions () const
 Gets a const reference to the vector of transitions of the current lts.
 
std::vector< transition > & get_transitions ()
 Gets a reference to the vector of transitions of the current lts.
 
void add_transition (const transition &t)
 Add a transition to the lts.
 
bool is_tau (labels_size_type action) const
 Checks whether an action is a tau action.
 
void record_hidden_actions (const std::vector< std::string > &tau_actions)
 Records all actions with a string that occurs in tau_actions internally.
 
void apply_hidden_actions (const std::vector< std::string > &tau_actions)
 Rename actions in the lts by hiding the actions in the vector tau_actions.
 
bool has_state_info () const
 Checks whether this LTS has state values associated with its states.
 
bool has_action_info () const
 Checks whether this LTS has labels associated with its actions, which are numbers.
 

Static Public Attributes

static constexpr bool is_probabilistic_lts =true
 An indicator that this is a probabilistic lts.
 
- Static Public Attributes inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
static constexpr bool is_probabilistic_lts
 An indicator that this is not a probabilistic lts.
 

Protected Member Functions

states_size_type initial_state () const
 
void set_initial_state (const states_size_type s)
 
- Protected Member Functions inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
void rename_labels (const std::map< labels_size_type, labels_size_type > &action_rename_map)
 
void store_action_label_to_be_renamed (const ACTION_LABEL_T &a, const labels_size_type i, std::map< labels_size_type, labels_size_type > &action_rename_map)
 

Protected Attributes

std::vector< PROBABILISTIC_STATE_T > m_probabilistic_states
 
PROBABILISTIC_STATE_T m_init_probabilistic_state
 
- Protected Attributes inherited from mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE >
states_size_type m_nstates
 
states_size_type m_init_state
 
std::vector< transitionm_transitions
 
std::vector< STATE_LABEL_T > m_state_labels
 
std::vector< ACTION_LABEL_T > m_action_labels
 
std::set< labels_size_typem_hidden_label_set
 

Detailed Description

template<class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE>
class mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >

A class that contains a labelled transition system.

The state labels and action labels can be any type. Essentially, a labelled transition system consists of a vector of transitions. Each transition is a triple of three numbers <from, label, to>. For these numbers, there can be associated state labels (for 'from' and 'to'), and action labels (for 'label'). But it is also possible, that no state or action labels are provided. For all action labels it is maintained whether this action label is an internal 'tau' action. This can be indicated for each action label separately. Finally, the number of states is recalled as a separate variable.

Definition at line 46 of file probabilistic_lts.h.

Member Typedef Documentation

◆ action_label_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
typedef super::action_label_t mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::action_label_t

Definition at line 57 of file probabilistic_lts.h.

◆ base_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
typedef super::base_t mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::base_t

Definition at line 58 of file probabilistic_lts.h.

◆ labels_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
typedef super::labels_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::labels_size_type

Definition at line 60 of file probabilistic_lts.h.

◆ probabilistic_state_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
typedef PROBABILISTIC_STATE_T mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_state_t

The type of probabilistic labels.

Definition at line 54 of file probabilistic_lts.h.

◆ state_label_t

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
typedef super::state_label_t mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::state_label_t

Definition at line 56 of file probabilistic_lts.h.

◆ states_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
typedef super::states_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::states_size_type

Definition at line 59 of file probabilistic_lts.h.

◆ super

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
typedef lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE> mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::super

Definition at line 50 of file probabilistic_lts.h.

◆ transitions_size_type

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
typedef super::transitions_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::transitions_size_type

Definition at line 61 of file probabilistic_lts.h.

Constructor & Destructor Documentation

◆ probabilistic_lts() [1/3]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_lts ( )
inline

Creates an empty LTS.

Definition at line 88 of file probabilistic_lts.h.

◆ probabilistic_lts() [2/3]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_lts ( const probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &  other)
default

Standard copy constructor.

Parameters
[in]otherThe LTS to copy.

◆ probabilistic_lts() [3/3]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_lts ( probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &&  other)
default

Standard move constructor.

Parameters
[in]otherThe LTS to copy.

Member Function Documentation

◆ add_and_reset_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
states_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::add_and_reset_probabilistic_state ( PROBABILISTIC_STATE_T &  s)
inline

Adds a probabilistic state to this LTS and resets the state to empty.

This is more efficient than using add_probabilistic state, as this variant does not copy the probabilistic state. It is not checked whether this probabilistic state already exists.

Parameters
[in]sThe probabilistic state.
Returns
The index of the added probabilistic state.

Definition at line 167 of file probabilistic_lts.h.

◆ add_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
states_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::add_probabilistic_state ( const PROBABILISTIC_STATE_T &  s)
inline

Adds a probabilistic state to this LTS.

It is not checked whether this probabilistic state already exists.

Parameters
[in]sThe probabilistic state.
Returns
The index of the added probabilistic.

Definition at line 155 of file probabilistic_lts.h.

◆ clear()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::clear ( )
inline

Clear the transitions system.

The state values, action values and transitions are reset. The number of states, actions and transitions are set to 0.

Definition at line 203 of file probabilistic_lts.h.

◆ clear_probabilistic_states()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::clear_probabilistic_states ( )
inline

Clear the probabilistic states in this probabilistic transitions system.

Definition at line 195 of file probabilistic_lts.h.

◆ initial_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
const PROBABILISTIC_STATE_T & mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::initial_probabilistic_state ( ) const
inline

Gets the initial state number of this LTS.

Returns
The number of the initial state of this LTS.

Definition at line 127 of file probabilistic_lts.h.

◆ initial_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
states_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::initial_state ( ) const
inlineprotected

Definition at line 73 of file probabilistic_lts.h.

◆ num_probabilistic_states()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
labels_size_type mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::num_probabilistic_states ( ) const
inline

Gets the number of probabilistic states of this LTS.

Returns
The number of action labels of this LTS.

Definition at line 146 of file probabilistic_lts.h.

◆ operator=() [1/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
probabilistic_lts & mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::operator= ( const probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &  other)
default

Standard assignment operator.

Parameters
[in]otherThe LTS to assign.

◆ operator=() [2/2]

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
probabilistic_lts & mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::operator= ( probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &&  other)
default

Standard assignment move operator.

Parameters
[in]otherThe LTS to assign.

◆ operator==()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
bool mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::operator== ( const probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &  other) const
inline

Standard equality operator.

Parameters
[in]otherThe LTS to compare this probabilistic lts with.

Definition at line 109 of file probabilistic_lts.h.

◆ probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
const PROBABILISTIC_STATE_T & mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::probabilistic_state ( const states_size_type  index) const
inline

Gets the probabilistic label of an index.

Parameters
[in]indexThe index of an action.
Returns
The probabilistic state belonging to the index.

Definition at line 187 of file probabilistic_lts.h.

◆ set_initial_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::set_initial_probabilistic_state ( const PROBABILISTIC_STATE_T &  state)
inline

Sets the probabilistic initial state number of this LTS.

Parameters
[in]stateThe number of the state that will become the initial state.

Definition at line 135 of file probabilistic_lts.h.

◆ set_initial_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::set_initial_state ( const states_size_type  s)
inlineprotected

Definition at line 79 of file probabilistic_lts.h.

◆ set_probabilistic_state()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::set_probabilistic_state ( const states_size_type  index,
const PROBABILISTIC_STATE_T &  s 
)
inline

Sets the probabilistic label corresponding to some index.

Parameters
[in]indexThe index of the state.
[in]sThe new probabilistic state belonging to this index.

Definition at line 178 of file probabilistic_lts.h.

◆ swap()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
void mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::swap ( probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &  other)
inline

Swap this lts with the supplied supplied LTS.

Parameters
[in]lThe LTS to swap.

Definition at line 118 of file probabilistic_lts.h.

Member Data Documentation

◆ is_probabilistic_lts

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
constexpr bool mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::is_probabilistic_lts =true
staticconstexpr

An indicator that this is a probabilistic lts.

Definition at line 65 of file probabilistic_lts.h.

◆ m_init_probabilistic_state

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
PROBABILISTIC_STATE_T mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::m_init_probabilistic_state
protected

Definition at line 70 of file probabilistic_lts.h.

◆ m_probabilistic_states

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
std::vector<PROBABILISTIC_STATE_T> mcrl2::lts::probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE >::m_probabilistic_states
protected

Definition at line 69 of file probabilistic_lts.h.


The documentation for this class was generated from the following file: