This class contains probabilistic labelled transition systems in .lts format. More...

#include <lts_lts.h>

Inheritance diagram for mcrl2::lts::probabilistic_lts_lts_t:

Public Member Functions
	probabilistic_lts_lts_t ()
	Creates an object containing no information.

void	load (const std::string &filename)
	Load the labelled transition system from file.

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_lts, action_label_lts, probabilistic_state< std::size_t, lps::probabilistic_data_expression >, detail::lts_lts_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_lts &	operator= (const probabilistic_lts &other)=default
	Standard assignment operator.

probabilistic_lts &	operator= (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< std::size_t, lps::probabilistic_data_expression > &	initial_probabilistic_state () const
	Gets the initial state number of this LTS.

void	set_initial_probabilistic_state (const probabilistic_state< std::size_t, lps::probabilistic_data_expression > &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< std::size_t, lps::probabilistic_data_expression > &s)
	Adds a probabilistic state to this LTS.

states_size_type	add_and_reset_probabilistic_state (probabilistic_state< std::size_t, lps::probabilistic_data_expression > &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< std::size_t, lps::probabilistic_data_expression > &s)
	Sets the probabilistic label corresponding to some index.

const probabilistic_state< std::size_t, lps::probabilistic_data_expression > &	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.

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_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_lts, action_label_lts, probabilistic_state< std::size_t, lps::probabilistic_data_expression >, detail::lts_lts_base >
typedef lts< state_label_lts, action_label_lts, detail::lts_lts_base >	super

typedef probabilistic_state< std::size_t, lps::probabilistic_data_expression >	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.

Static Public Attributes inherited from mcrl2::lts::probabilistic_lts< state_label_lts, action_label_lts, probabilistic_state< std::size_t, lps::probabilistic_data_expression >, detail::lts_lts_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_lts, action_label_lts, probabilistic_state< std::size_t, lps::probabilistic_data_expression >, detail::lts_lts_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_lts, action_label_lts, probabilistic_state< std::size_t, lps::probabilistic_data_expression >, detail::lts_lts_base >
std::vector< probabilistic_state< std::size_t, lps::probabilistic_data_expression > >	m_probabilistic_states

probabilistic_state< std::size_t, lps::probabilistic_data_expression >	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< transition >	m_transitions

std::vector< STATE_LABEL_T >	m_state_labels

std::vector< ACTION_LABEL_T >	m_action_labels

std::set< labels_size_type >	m_hidden_label_set

Detailed Description

This class contains probabilistic labelled transition systems in .lts format.

In this .lts format, an action label is a multi action, and a state label is an expression of the form STATE(t1,...,tn) where ti are data expressions.

Definition at line 401 of file lts_lts.h.

Constructor & Destructor Documentation

◆ probabilistic_lts_lts_t()

mcrl2::lts::probabilistic_lts_lts_t::probabilistic_lts_lts_t ( )

inline

Creates an object containing no information.

Definition at line 409 of file lts_lts.h.

Member Function Documentation

◆ load()

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

Load the labelled transition system from file.

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

Parameters

[in] filename Name of the file to which this lts is written.

Definition at line 514 of file liblts_lts.cpp.

◆ save()

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

Save the labelled transition system to file.

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

Parameters

[in] filename Name of the file from which this lts is read.

Definition at line 502 of file liblts_lts.cpp.

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

lts/include/mcrl2/lts/lts_lts.h
lts/source/liblts_lts.cpp