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

#include <lts_fsm.h>

Inheritance diagram for mcrl2::lts::probabilistic_lts_fsm_t:

Public Types
typedef probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state_t, detail::lts_fsm_base >	super

Public Types inherited from mcrl2::lts::probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >, detail::lts_fsm_base >
typedef lts< state_label_fsm, action_label_string, detail::lts_fsm_base >	super

typedef probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >	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.

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::probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >, detail::lts_fsm_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, mcrl2::utilities::probabilistic_arbitrary_precision_fraction > &	initial_probabilistic_state () const
	Gets the initial state number of this LTS.

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

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

const probabilistic_state< std::size_t, mcrl2::utilities::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.

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
Static Public Attributes inherited from mcrl2::lts::probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >, detail::lts_fsm_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_fsm, action_label_string, probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >, detail::lts_fsm_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_fsm, action_label_string, probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >, detail::lts_fsm_base >
std::vector< probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction > >	m_probabilistic_states

probabilistic_state< std::size_t, mcrl2::utilities::probabilistic_arbitrary_precision_fraction >	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

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 271 of file lts_fsm.h.

Member Typedef Documentation

◆ super

typedef probabilistic_lts< state_label_fsm, action_label_string, probabilistic_state_t, detail::lts_fsm_base > mcrl2::lts::probabilistic_lts_fsm_t::super

Definition at line 279 of file lts_fsm.h.

Member Function Documentation

◆ load()

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

◆ save()

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

Public Types