This file contains lts_convert routines that translate different lts formats into each other. More...

Classes
class	mcrl2::lts::detail::convertor< BASE_LTS_IN, BASE_LTS_OUT >

class	mcrl2::lts::detail::convertor< lts_lts_base, lts_fsm_base >

class	mcrl2::lts::detail::convertor< lts_lts_base, lts_dot_base >

class	mcrl2::lts::detail::convertor< lts_fsm_base, lts_lts_base >

class	mcrl2::lts::detail::convertor< lts_fsm_base, lts_dot_base >

class	mcrl2::lts::detail::convertor< lts_aut_base, lts_lts_base >

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.

namespace	mcrl2::lts
	The main LTS namespace.

namespace	mcrl2::lts::detail
	A base class for the lts_dot labelled transition system.

Functions
utilities::probabilistic_arbitrary_precision_fraction	mcrl2::lts::detail::translate_probability_data_to_arbitrary_size_probability (const data::data_expression &d)
	Translate a fraction given as a data_expression to a representation with an arbitrary size fraction.

template<class PROBABILISTIC_STATE1 , class PROBABILISTIC_STATE2 >
PROBABILISTIC_STATE2	mcrl2::lts::detail::lts_convert_probabilistic_state (const PROBABILISTIC_STATE1 &)

mcrl2::utilities::probabilistic_arbitrary_precision_fraction	mcrl2::lts::detail::translate_probability_data_prob (const data::data_expression &d)

action_label_lts	mcrl2::lts::detail::translate_label_aux (const action_label_string &l1, const data::data_specification &data, lps::multi_action_type_checker &typechecker)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_lts_base &base_in, lts_lts_base &base_out)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_lts_base &base_in, lts_lts_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

action_label_lts	mcrl2::lts::detail::lts_convert_translate_label (const action_label_lts &l_in, convertor< lts_lts_base, lts_lts_base > &)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_lts &state_label_in, state_label_lts &state_label_out, convertor< lts_lts_base, lts_lts_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_lts_base &base_in, lts_fsm_base &base_out)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_lts &l_in, convertor< lts_lts_base, lts_fsm_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_lts_base &base_in, lts_fsm_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_lts &state_label_in, state_label_fsm &state_label_out, convertor< lts_lts_base, lts_fsm_base > &c)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_lts_base &, lts_aut_base &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_lts_base &base_in, lts_aut_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_lts &l_in, convertor< lts_lts_base, lts_aut_base > &)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_lts &, state_label_empty &state_label_out, convertor< lts_lts_base, lts_aut_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_lts_base &, lts_dot_base &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_lts_base &base_in, lts_dot_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_lts &l_in, convertor< lts_lts_base, lts_dot_base > &)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_lts &state_label_in, state_label_dot &state_label_out, convertor< lts_lts_base, lts_dot_base > &c)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_fsm_base &, lts_lts_base &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_fsm_base &base_in, lts_lts_base &base_out, const data::data_specification &data, const process::action_label_list &action_labels, const data::variable_list &process_parameters, const bool extra_data_is_defined=true)

action_label_lts	mcrl2::lts::detail::lts_convert_translate_label (const action_label_string &l1, convertor< lts_fsm_base, lts_lts_base > &c)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_fsm &state_label_in, state_label_lts &state_label_out, convertor< lts_fsm_base, lts_lts_base > &c)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_fsm_base &base_in, lts_fsm_base &base_out)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_fsm_base &base_in, lts_fsm_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_fsm &state_label_in, state_label_fsm &state_label_out, convertor< lts_fsm_base, lts_fsm_base > &)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_string &l_in, convertor< lts_fsm_base, lts_fsm_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_fsm_base &, lts_aut_base &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_fsm_base &base_in, lts_aut_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_fsm &, state_label_empty &state_label_out, convertor< lts_fsm_base, lts_aut_base > &)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_string &l_in, convertor< lts_fsm_base, lts_aut_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_fsm_base &, lts_dot_base &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_fsm_base &base_in, lts_dot_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_fsm &state_label_in, state_label_dot &state_label_out, convertor< lts_fsm_base, lts_dot_base > &c)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_string &l_in, convertor< lts_fsm_base, lts_dot_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_aut_base &, lts_lts_base &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_aut_base &base_in, lts_lts_base &base_out, const data::data_specification &data, const process::action_label_list &action_labels, const data::variable_list &process_parameters, const bool extra_data_is_defined=true)

action_label_lts	mcrl2::lts::detail::lts_convert_translate_label (const action_label_string &l_in, convertor< lts_aut_base, lts_lts_base > &c)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_empty &, state_label_lts &state_label_out, convertor< lts_aut_base, lts_lts_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_aut_base &, lts_fsm_base &base_out)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_aut_base &base_in, lts_fsm_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_string &l_in, convertor< lts_aut_base, lts_fsm_base > &)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_empty &, state_label_fsm &state_label_out, convertor< lts_aut_base, lts_fsm_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_aut_base &base_in, lts_aut_base &base_out)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_aut_base &base_in, lts_aut_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_empty &state_label_in, state_label_empty &state_label_out, convertor< lts_aut_base, lts_aut_base > &)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_string &l_in, convertor< lts_aut_base, lts_aut_base > &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_aut_base &, lts_dot_base &)

void	mcrl2::lts::detail::lts_convert_base_class (const lts_aut_base &base_in, lts_dot_base &base_out, const data::data_specification &, const process::action_label_list &, const data::variable_list &, const bool extra_data_is_defined=true)

void	mcrl2::lts::detail::lts_convert_translate_state (const state_label_empty &, state_label_dot &state_label_out, convertor< lts_aut_base, lts_dot_base > &)

action_label_string	mcrl2::lts::detail::lts_convert_translate_label (const action_label_string &l_in, convertor< lts_aut_base, lts_dot_base > &)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert_aux (const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert (const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert (const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out, const data::data_specification &ds, const process::action_label_list &all, const data::variable_list &vl, const bool extra_data_is_defined=true)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class PROBABILISTIC_STATE1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class LTS_BASE2 >
void	mcrl2::lts::detail::remove_probabilities (const probabilistic_lts< STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class LTS_BASE1 , class PROBABILISTIC_STATE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert (const probabilistic_lts< STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class PROBABILISTIC_STATE1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert (const probabilistic_lts< STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out, const data::data_specification &data, const process::action_label_list &action_label_list, const data::variable_list &process_parameters, const bool extra_data_is_defined=true)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class PROBABILISTIC_STATE2 , class LTS_BASE2 >
void	mcrl2::lts::detail::add_probabilities (const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, probabilistic_lts< STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2 > &lts_out)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class PROBABILISTIC_STATE2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert (const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, probabilistic_lts< STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2 > &lts_out)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class PROBABILISTIC_STATE2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert (const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, probabilistic_lts< STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2 > &lts_out, const data::data_specification &data, const process::action_label_list &action_label_list, const data::variable_list &process_parameters, const bool extra_data_is_defined=true)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class PROBABILISTIC_STATE1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class PROBABILISTIC_STATE2 , class LTS_BASE2 >
void	mcrl2::lts::detail::translate_probability_labels (const probabilistic_lts< STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1 > &lts_in, probabilistic_lts< STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2 > &lts_out)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class PROBABILISTIC_STATE1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class PROBABILISTIC_STATE2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert (const probabilistic_lts< STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1 > &lts_in, probabilistic_lts< STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2 > &lts_out)

template<class STATE_LABEL1 , class ACTION_LABEL1 , class PROBABILISTIC_STATE1 , class LTS_BASE1 , class STATE_LABEL2 , class ACTION_LABEL2 , class PROBABILISTIC_STATE2 , class LTS_BASE2 >
void	mcrl2::lts::detail::lts_convert (const probabilistic_lts< STATE_LABEL1, ACTION_LABEL1, PROBABILISTIC_STATE1, LTS_BASE1 > &lts_in, probabilistic_lts< STATE_LABEL2, ACTION_LABEL2, PROBABILISTIC_STATE2, LTS_BASE2 > &lts_out, const data::data_specification &data, const process::action_label_list &action_label_list, const data::variable_list &process_parameters, const bool extra_data_is_defined=true)

Detailed Description

This file contains lts_convert routines that translate different lts formats into each other.

For each pair of lts formats there is a translation of one format into the other, if such a translation is possible.

Author: Jan Friso Groote, Muck van Weerdenburg

Definition in file lts_convert.h.

Classes

Namespaces

Functions

Detailed Description