mCRL2
Loading...
Searching...
No Matches
lts_convert.h File Reference

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

Go to the source code of this file.

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

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::lts::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.