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:
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. | |
| lts & | operator= (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< transition > | m_transitions |
| std::vector< state_label_fsm > | m_state_labels |
| std::vector< action_label_string > | m_action_labels |
| std::set< labels_size_type > | m_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.
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] filename Name 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] filename Name 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:
- lts/include/mcrl2/lts/lts_fsm.h
- lts/source/liblts_fsm.cpp
