mcrl2::lts::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::lts_aut_t:

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::lts< state_label_empty, action_label_string, detail::lts_aut_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_empty > &	state_labels ()
	Provides the state labels of an LTS.
const std::vector< state_label_empty > &	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_transitions (const std::size_t n)
	Sets the number of transitions of this LTS and tries to shrink the datastructure.
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_empty &label=state_label_empty())
	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_empty &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_empty	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	add_state_number_as_state_information ()
	Label each state with its state number.
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_aut_base
lts_type	type ()
	Provides the type of this lts, in casu lts_aut.
void	swap (lts_aut_base &)
	Standard swap function.
bool	operator== (const lts_aut_base &) const
	Standard equality function.

Additional Inherited Members
Public Types inherited from mcrl2::lts::lts< state_label_empty, action_label_string, detail::lts_aut_base >
typedef state_label_empty	state_label_t
	The type of state labels.
typedef action_label_string	action_label_t
	The type of action labels.
typedef detail::lts_aut_base	base_t
	The type of the used lts base.
typedef std::vector< state_label_empty >::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.
Static Public Attributes inherited from mcrl2::lts::lts< state_label_empty, action_label_string, detail::lts_aut_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_empty, action_label_string, detail::lts_aut_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_empty, action_label_string, detail::lts_aut_base >
states_size_type	m_nstates
states_size_type	m_init_state
std::vector< transition >	m_transitions
std::vector< state_label_empty >	m_state_labels
std::vector< action_label_string >	m_action_labels
std::set< labels_size_type >	m_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 69 of file lts_aut.h.

Member Function Documentation

load() [1/2]

void mcrl2::lts::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]

filename

Name of the file from which this lts is read.

Definition at line 599 of file liblts_aut.cpp.

load() [2/2]

void mcrl2::lts::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]

is

The input stream.

Definition at line 619 of file liblts_aut.cpp.

save()

void mcrl2::lts::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]

filename

Name of the file to which this lts is written.

Definition at line 624 of file liblts_aut.cpp.

---

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

• lts/include/mcrl2/lts/lts_aut.h
• lts/source/liblts_aut.cpp