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

The class lts_fsm_t contains labelled transition systems in .fsm format. More...

#include <lts_fsm.h>

Inheritance diagram for mcrl2::lts::lts_fsm_t:
mcrl2::lts::lts< state_label_fsm, action_label_string, detail::lts_fsm_base > mcrl2::lts::detail::lts_fsm_base

Public Types

typedef lts< state_label_fsm, action_label_string, detail::lts_fsm_basesuper
 
- Public Types inherited from mcrl2::lts::lts< state_label_fsm, action_label_string, detail::lts_fsm_base >
typedef state_label_fsm state_label_t
 The type of state labels.
 
typedef action_label_string action_label_t
 The type of action labels.
 
typedef detail::lts_fsm_base base_t
 The type of the used lts base.
 
typedef std::vector< state_label_fsm >::size_type states_size_type
 The sort that contains the indices of states.
 
typedef std::vector< action_label_string >::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 Types inherited from mcrl2::lts::detail::lts_fsm_base
typedef mcrl2::lts::probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fractionprobabilistic_state
 
typedef mcrl2::lps::state_probability_pair< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fractionstate_probability_pair
 

Public Member Functions

void load (const std::string &filename)
 Save the labelled transition system to file.
 
void save (const std::string &filename) const
 Save the labelled transition system to file.
 
- Public Member Functions inherited from mcrl2::lts::lts< state_label_fsm, action_label_string, detail::lts_fsm_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_fsm > & state_labels ()
 Provides the state labels of an LTS.
 
const std::vector< state_label_fsm > & 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_fsm &label=state_label_fsm())
 Adds a state to this LTS.
 
labels_size_type add_action (const action_label_string &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_fsm &label)
 Sets the label of a state.
 
const std::vector< action_label_string > & action_labels () const
 The action labels in this lts.
 
void set_action_label (const labels_size_type action, const action_label_string &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_fsm 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_string 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::detail::lts_fsm_base
bool operator== (const lts_fsm_base &other) const
 
lts_type type () const
 The lts_type of this labelled transition system. In this case lts_fsm.
 
void swap (lts_fsm_base &other)
 Standard swap function.
 
void clear ()
 Clear the transitions system.
 
const std::vector< std::string > & state_element_values (std::size_t idx) const
 Provides the vector of strings that correspond to the values of the number at position idx in a vector.
 
std::string state_label_to_string (const state_label_fsm &l) const
 Pretty print a state value of this FSM.
 
std::size_t add_state_element_value (std::size_t idx, const std::string &s)
 Adds a string to the state element values for the idx-th position in a state vector. Returns the number given to this string.
 
std::string state_element_value (std::size_t parameter_index, std::size_t element_index) const
 Returns the element_index'th element for the parameter with index parameter_index.
 
std::vector< std::pair< std::string, std::string > > process_parameters () const
 Return the parameters of the state vectors stored in this LTS.
 
std::pair< std::string, std::string > process_parameter (std::size_t i) const
 Returns the i-th parameter of the state vectors stored in this LTS.
 
void clear_process_parameters ()
 Clear the state parameters for this LTS.
 
void add_process_parameter (const std::string &name, const std::string &sort)
 Set the state parameters for this LTS.
 

Additional Inherited Members

- Static Public Attributes inherited from mcrl2::lts::lts< state_label_fsm, action_label_string, detail::lts_fsm_base >
static constexpr bool is_probabilistic_lts
 An indicator that this is not a probabilistic lts.
 
- Protected Member Functions inherited from mcrl2::lts::lts< state_label_fsm, action_label_string, detail::lts_fsm_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_string &a, const labels_size_type i, std::map< labels_size_type, labels_size_type > &action_rename_map)
 
- Protected Attributes inherited from mcrl2::lts::lts< state_label_fsm, action_label_string, detail::lts_fsm_base >
states_size_type m_nstates
 
states_size_type m_init_state
 
std::vector< transitionm_transitions
 
std::vector< state_label_fsmm_state_labels
 
std::vector< action_label_stringm_action_labels
 
std::set< labels_size_typem_hidden_label_set
 
- Protected Attributes inherited from mcrl2::lts::detail::lts_fsm_base
std::vector< std::vector< std::string > > m_state_element_values
 state_element_values contain the values that can occur at the i-th position of a state label
 
std::vector< std::pair< std::string, std::string > > m_parameters
 m_parameters contain the parameters corresponding to the consecutive elements of a state vector. A parameter consists of two strings: a variable name and a string indicating its sort.
 

Detailed Description

The class lts_fsm_t contains labelled transition systems in .fsm format.

The .fsm format consists of an labelled transition system where the action labels are strings, and the state labels are vectors of integers. The integers at position i corresponds to a string, which are maintained in a separate vector for memory efficiency.

Definition at line 247 of file lts_fsm.h.

Member Typedef Documentation

◆ super

Member Function Documentation

◆ load()

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

Save the labelled transition system to file.

If the filename is empty, the result is read from stdout.

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

Definition at line 197 of file liblts_fsm.cpp.

◆ save()

void mcrl2::lts::lts_fsm_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 208 of file liblts_fsm.cpp.


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