mCRL2
Loading...
Searching...
No Matches
mcrl2::lts::probabilistic_lts_aut_t Class Reference

A simple labelled transition format with only strings as action labels. More...

#include <lts_aut.h>

Inheritance diagram for mcrl2::lts::probabilistic_lts_aut_t:
mcrl2::lts::probabilistic_lts< state_label_empty, action_label_string, mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction >, detail::lts_aut_base > mcrl2::lts::lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > mcrl2::lts::lts_default_base

Public Member Functions

void load (const std::string &filename)
 Load the labelled transition system from a file.
 
void load (std::istream &is)
 Load the labelled transition system from an input stream.
 
void save (const std::string &filename) const
 Save the labelled transition system to file.
 
- Public Member Functions inherited from mcrl2::lts::probabilistic_lts< state_label_empty, action_label_string, mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction >, detail::lts_aut_base >
 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 mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > & initial_probabilistic_state () const
 Gets the initial state number of this LTS.
 
void set_initial_probabilistic_state (const mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > &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 mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > &s)
 Adds a probabilistic state to this LTS.
 
states_size_type add_and_reset_probabilistic_state (mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > &s)
 Adds a probabilistic state to this LTS and resets the state to empty.
 
void set_probabilistic_state (const states_size_type index, const mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > &s)
 Sets the probabilistic label corresponding to some index.
 
const mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > & 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.
 
- Public Member Functions inherited from mcrl2::lts::lts_default_base
lts_type type ()
 Provides the type of this lts, in casu lts_none.

 
void swap (lts_default_base &)
 Standard swap function.
 
bool operator== (const lts_default_base &) const
 Standard equality function.
 

Additional Inherited Members

- Public Types inherited from mcrl2::lts::probabilistic_lts< state_label_empty, action_label_string, mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction >, detail::lts_aut_base >
typedef lts< state_label_empty, action_label_string, detail::lts_aut_basesuper
 
typedef mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fractionprobabilistic_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.
 
- Static Public Attributes inherited from mcrl2::lts::probabilistic_lts< state_label_empty, action_label_string, mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction >, detail::lts_aut_base >
static constexpr bool is_probabilistic_lts
 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 =false
 An indicator that this is not a probabilistic lts.
 
- Protected Member Functions inherited from mcrl2::lts::probabilistic_lts< state_label_empty, action_label_string, mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction >, detail::lts_aut_base >
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 inherited from mcrl2::lts::probabilistic_lts< state_label_empty, action_label_string, mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction >, detail::lts_aut_base >
std::vector< mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fraction > > m_probabilistic_states
 
mcrl2::lts::probabilistic_state< std::size_t, mcrl2::lts::probabilistic_arbitrary_precision_fractionm_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

A simple labelled transition format with only strings as action labels.

This lts format corresponds to the Ceasar/Aldebaran labelled transition system format. There are no state labels, only transition labels which are plain strings.

Definition at line 98 of file lts_aut.h.

Member Function Documentation

◆ load() [1/2]

void mcrl2::lts::probabilistic_lts_aut_t::load ( const std::string &  filename)

Load the labelled transition system from a file.

If the filename is empty, the result is read from stdin. The input file must be in .aut format.

Parameters
[in]filenameName of the file from which this lts is read.

Definition at line 547 of file liblts_aut.cpp.

◆ load() [2/2]

void mcrl2::lts::probabilistic_lts_aut_t::load ( std::istream &  is)

Load the labelled transition system from an input stream.

The input stream must be in .aut format.

Parameters
[in]isThe input stream.

Definition at line 567 of file liblts_aut.cpp.

◆ save()

void mcrl2::lts::probabilistic_lts_aut_t::save ( const std::string &  filename) const

Save the labelled transition system to file.

If the filename is empty, the result is written to stdout.

Parameters
[in]filenameName of the file to which this lts is written.

Definition at line 572 of file liblts_aut.cpp.


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