mcrl2::lts::detail Namespace Reference

A base class for the lts_dot labelled transition system. More...

Namespaces
namespace	bisim_dnj
namespace	bisim_gjkw
namespace	bisimulation_gj

Classes
class	action_detector
class	action_index_pair
	A simple class storing the index of a label and an index. More...
class	bisim_partitioner
class	bisim_partitioner_dnj
	implements the main algorithm for the branching bisimulation quotient More...
class	bisim_partitioner_gj
	implements the main algorithm for the branching bisimulation quotient More...
class	bisim_partitioner_gjkw
	implements the main algorithm for the stutter equivalence quotient More...
class	bisim_partitioner_minimal_depth
class	branching_bisim_partitioner_minimal_depth
class	check_complexity
	class for time complexity checks More...
class	compare_transitions_lts
class	compare_transitions_slt
class	compare_transitions_target
class	compare_transitions_tl
class	compare_transitions_tls
class	compare_transitions_tsl
class	constln_ptr_less
	function object to compare two constln_t pointers based on their contents More...
class	convertor
class	convertor< lts_aut_base, lts_lts_base >
class	convertor< lts_fsm_base, lts_dot_base >
class	convertor< lts_fsm_base, lts_lts_base >
class	convertor< lts_lts_base, lts_dot_base >
class	convertor< lts_lts_base, lts_fsm_base >
class	counter_example_constructor
	A class that can be used to store counterexample trees and. More...
struct	cs_game_move
struct	cs_game_node
class	deadlock_detector
class	divergence_detector
class	dummy_counter_example_constructor
	A class that can be used to construct counter examples if no. More...
class	embedded_list
class	embedded_list_node
class	fixed_vector
struct	fsm_builder
class	fsm_parameter
class	fsm_transition
	Transitions in an FSM. More...
class	indexed_sorted_vector_for_tau_transitions
class	indexed_sorted_vector_for_transitions
class	lts_aut_base
class	lts_cache
class	lts_dot_base
class	lts_fsm_base
class	lts_lts_base
	a base class for lts_lts_t and probabilistic_lts_t. More...
class	my_pool
class	nondeterminism_detector
class	prob_bisim_partitioner_bem
class	prob_bisim_partitioner_grv
class	progress_monitor
class	ready_sim_partitioner
class	scc_partitioner
	This class contains an scc partitioner removing inert tau loops. More...
class	sim_partitioner
class	simple_fsm_parser
class	simple_list
	a simple implementation of lists More...
class	state_states_counter_example_index_triple
class	trace_constructor

Typedefs
typedef std::size_t	state_type
	type used to store state (numbers and) counts
typedef std::size_t	trans_type
	type used to store transition (numbers and) counts
typedef std::make_signed< trans_type >::type	signed_trans_type
	type used to store differences between transition counters
typedef std::size_t	label_type
	type used to store label numbers and counts
typedef std::set< state_type >	set_of_states
typedef std::multimap< detail::state_type, detail::set_of_states >	anti_chain_type
typedef std::set< label_type >	action_label_set
template<class El >
using	iterator_or_null_t = typename simple_list< El >::iterator_or_null
typedef std::set< bisim_gjkw::constln_t *, constln_ptr_less >	R_map_t

Enumerations
enum	t_reach { unknown , reached , explored }

Functions
std::string	split_string_until (std::string &s, const std::string &c1, const std::string &c2="")
lts_fsm_base::probabilistic_state	parse_distribution (const std::string &distribution)
template<class LTS_TYPE >
void	add_an_action_loop_to_each_state (LTS_TYPE &l, std::size_t action)
template<class LTS_TYPE >
void	bisimulation_reduce (LTS_TYPE &l, const bool branching=false, const bool preserve_divergences=false)
	Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
template<class LTS_TYPE >
bool	destructive_bisimulation_compare (LTS_TYPE &l1, LTS_TYPE &l2, const bool branching=false, const bool preserve_divergences=false, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
	Checks whether the two initial states of two lts's are strong or branching bisimilar.
template<class LTS_TYPE >
bool	bisimulation_compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const bool branching=false, const bool preserve_divergences=false, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
	Checks whether the two initial states of two lts's are strong or branching bisimilar.
template<class LTS_TYPE >
void	bisimulation_reduce_dnj (LTS_TYPE &l, bool const branching=false, bool const preserve_divergence=false)
	Reduce transition system l with respect to strong or (divergence-preserving) branching bisimulation.
template<class LTS_TYPE >
bool	destructive_bisimulation_compare_dnj (LTS_TYPE &l1, LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false, bool const generate_counter_examples=false, const std::string &="", bool=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
template<class LTS_TYPE >
bool	bisimulation_compare_dnj (const LTS_TYPE &l1, const LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
template<class LTS_TYPE >
void	bisimulation_reduce_gj (LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false)
	nonmember functions serving as interface with the rest of mCRL2
template<class LTS_TYPE >
bool	destructive_bisimulation_compare_gj (LTS_TYPE &l1, LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false, const bool generate_counter_examples=false, const std::string &="", bool=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
template<class LTS_TYPE >
bool	bisimulation_compare_gj (const LTS_TYPE &l1, const LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
template<class LTS_TYPE >
void	bisimulation_reduce_gjkw (LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)
	Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
template<class LTS_TYPE >
bool	destructive_bisimulation_compare_gjkw (LTS_TYPE &l1, LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false, bool generate_counter_examples=false)
	Checks whether the two initial states of two LTSs are strong or branching bisimilar.
template<class LTS_TYPE >
bool	bisimulation_compare_gjkw (const LTS_TYPE &l1, const LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false)
	Checks whether the two initial states of two LTSs are strong or branching bisimilar.
template<class LTS_TYPE >
bool	destructive_bisimulation_compare_gjkw (LTS_TYPE &l1, LTS_TYPE &l2, bool branching, bool preserve_divergence, bool generate_counter_examples, const std::string &, bool)
template<class LTS_TYPE >
bool	destructive_bisimulation_compare_minimal_depth (LTS_TYPE &l1, LTS_TYPE &l2, const std::string &counter_example_file)
template<class LTS_TYPE >
bool	destructive_branching_bisimulation_compare_minimal_depth (LTS_TYPE &l1, LTS_TYPE &l2, const std::string &counter_example_file)
bool	operator== (const cs_game_node &n0, const cs_game_node &n1)
bool	operator!= (const cs_game_node &n0, const cs_game_node &n1)
bool	operator< (const cs_game_node &n0, const cs_game_node &n1)
std::string	to_string (const cs_game_node &n)
bool	equals (const cs_game_move &m0, const cs_game_move &m1, bool weak_transition=false)
bool	operator< (const cs_game_move &m0, const cs_game_move &m1)
template<class LTS_TYPE >
bool	coupled_simulation_compare (LTS_TYPE &l1, LTS_TYPE &l2)
template<class COUNTER_EXAMPLE_CONSTRUCTOR >
bool	antichain_insert (anti_chain_type &anti_chain, const state_states_counter_example_index_triple< COUNTER_EXAMPLE_CONSTRUCTOR > &impl_spec)
template<class LTS_TYPE >
set_of_states	collect_reachable_states_via_taus (const state_type s, const lts_cache< LTS_TYPE > &weak_property_cache, const bool weak_reduction)
template<class LTS_TYPE >
set_of_states	collect_reachable_states_via_an_action (const state_type s, const label_type e, const lts_cache< LTS_TYPE > &weak_property_cache, const bool weak_reduction, const LTS_TYPE &l)
template<class LTS_TYPE >
bool	refusals_contained_in (const state_type impl, const set_of_states &spec, const lts_cache< LTS_TYPE > &weak_property_cache, label_type &culprit, const LTS_TYPE &l, const bool provide_a_counter_example, const bool structured_output)
	This function checks that the refusals(impl) are contained in the refusals of spec, where the refusals of spec are defined by { r | exists s in spec. r in refusals(s) and stable(r) }.
template<class LTS_TYPE >
set_of_states	collect_reachable_states_via_taus (const set_of_states &s, const lts_cache< LTS_TYPE > &weak_property_cache, const bool weak_reduction)
template<class LTS_TYPE >
const set_of_states &	calculate_tau_reachable_states (const set_of_states &states, const lts_cache< LTS_TYPE > &weak_property_cache)
template<class LTS_TYPE >
void	merge (LTS_TYPE &l1, const LTS_TYPE &l2)
template<class LTS_TYPE >
void	probabilistic_bisimulation_reduce_bem (LTS_TYPE &l, utilities::execution_timer &timer)
	Reduce transition system l with respect to probabilistic bisimulation.
template<class LTS_TYPE >
bool	destructive_probabilistic_bisimulation_compare_bem (LTS_TYPE &l1, LTS_TYPE &l2, utilities::execution_timer &timer)
	Checks whether the two initial states of two plts's are probabilistic bisimilar.
template<class LTS_TYPE >
bool	probabilistic_bisimulation_compare_bem (const LTS_TYPE &l1, const LTS_TYPE &l2, utilities::execution_timer &timer)
	Checks whether the two initial states of two plts's are probabilistic bisimilar.
template<class LTS_TYPE >
void	probabilistic_bisimulation_reduce_grv (LTS_TYPE &l, utilities::execution_timer &timer)
	Reduce transition system l with respect to probabilistic bisimulation.
template<class LTS_TYPE >
bool	destructive_probabilistic_bisimulation_compare_grv (LTS_TYPE &l1, LTS_TYPE &l2, utilities::execution_timer &timer)
	Checks whether the two initial states of two plts's are probabilistic bisimilar.
template<class LTS_TYPE >
bool	probabilistic_bisimulation_compare_grv (const LTS_TYPE &l1, const LTS_TYPE &l2, utilities::execution_timer &timer)
	Checks whether the two initial states of two plts's are probabilistic bisimilar.
template<class LTS_TYPE >
void	plts_merge (LTS_TYPE &l1, const LTS_TYPE &l2)
template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
void	swap_to_non_probabilistic_lts (probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &l_probabilistic, lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > &l_plain)
template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >
void	translate_to_probabilistic_lts (const lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > &l_plain, probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &l_probabilistic)
template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE_CLASS >
std::map< std::size_t, std::set< typename lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS >::states_size_type > >	calculate_non_reflexive_transitive_tau_closure (lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l, const bool forward)
	This procedure calculates the transitive tau closure as a separate vector of transitions, for a given transition system. \parameter l A labelled transition system \parameter forward A boolean that indicates whether the resulting closure.
template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE_CLASS >
void	reflexive_transitive_tau_closure (lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l)
template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE_CLASS >
void	remove_redundant_transitions (lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l)
	Removes each transition s-a->s' if also transitions s-a->-tau->s' or s-tau->-a->s' are present. It uses the hidden_label_set to determine whether transitions are internal.
template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE_CLASS >
void	tau_star_reduce (lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &l)
template<class LTS_TYPE >
void	weak_bisimulation_reduce (LTS_TYPE &l, const bool preserve_divergences=false)
	Reduce LTS l with respect to (divergence-preserving) weak bisimulation.
template<class LTS_TYPE >
bool	destructive_weak_bisimulation_compare (LTS_TYPE &l1, LTS_TYPE &l2, const bool preserve_divergences=false)
	Checks whether the initial states of two LTSs are weakly bisimilar.
template<class LTS_TYPE >
bool	weak_bisimulation_compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const bool preserve_divergences=false)
	Checks whether the initial states of two LTSs are weakly bisimilar.
utilities::probabilistic_arbitrary_precision_fraction	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	lts_convert_probabilistic_state (const PROBABILISTIC_STATE1 &)
mcrl2::utilities::probabilistic_arbitrary_precision_fraction	translate_probability_data_prob (const data::data_expression &d)
action_label_lts	translate_label_aux (const action_label_string &l1, const data::data_specification &data, lps::multi_action_type_checker &typechecker)
void	lts_convert_base_class (const lts_lts_base &base_in, lts_lts_base &base_out)
void	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	lts_convert_translate_label (const action_label_lts &l_in, convertor< lts_lts_base, lts_lts_base > &)
void	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	lts_convert_base_class (const lts_lts_base &base_in, lts_fsm_base &base_out)
action_label_string	lts_convert_translate_label (const action_label_lts &l_in, convertor< lts_lts_base, lts_fsm_base > &)
void	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	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	lts_convert_base_class (const lts_lts_base &, lts_aut_base &)
void	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	lts_convert_translate_label (const action_label_lts &l_in, convertor< lts_lts_base, lts_aut_base > &)
void	lts_convert_translate_state (const state_label_lts &, state_label_empty &state_label_out, convertor< lts_lts_base, lts_aut_base > &)
void	lts_convert_base_class (const lts_lts_base &, lts_dot_base &)
void	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	lts_convert_translate_label (const action_label_lts &l_in, convertor< lts_lts_base, lts_dot_base > &)
void	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	lts_convert_base_class (const lts_fsm_base &, lts_lts_base &)
void	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	lts_convert_translate_label (const action_label_string &l1, convertor< lts_fsm_base, lts_lts_base > &c)
void	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	lts_convert_base_class (const lts_fsm_base &base_in, lts_fsm_base &base_out)
void	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	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	lts_convert_translate_label (const action_label_string &l_in, convertor< lts_fsm_base, lts_fsm_base > &)
void	lts_convert_base_class (const lts_fsm_base &, lts_aut_base &)
void	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	lts_convert_translate_state (const state_label_fsm &, state_label_empty &state_label_out, convertor< lts_fsm_base, lts_aut_base > &)
action_label_string	lts_convert_translate_label (const action_label_string &l_in, convertor< lts_fsm_base, lts_aut_base > &)
void	lts_convert_base_class (const lts_fsm_base &, lts_dot_base &)
void	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	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	lts_convert_translate_label (const action_label_string &l_in, convertor< lts_fsm_base, lts_dot_base > &)
void	lts_convert_base_class (const lts_aut_base &, lts_lts_base &)
void	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	lts_convert_translate_label (const action_label_string &l_in, convertor< lts_aut_base, lts_lts_base > &c)
void	lts_convert_translate_state (const state_label_empty &, state_label_lts &state_label_out, convertor< lts_aut_base, lts_lts_base > &)
void	lts_convert_base_class (const lts_aut_base &, lts_fsm_base &base_out)
void	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	lts_convert_translate_label (const action_label_string &l_in, convertor< lts_aut_base, lts_fsm_base > &)
void	lts_convert_translate_state (const state_label_empty &, state_label_fsm &state_label_out, convertor< lts_aut_base, lts_fsm_base > &)
void	lts_convert_base_class (const lts_aut_base &base_in, lts_aut_base &base_out)
void	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	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	lts_convert_translate_label (const action_label_string &l_in, convertor< lts_aut_base, lts_aut_base > &)
void	lts_convert_base_class (const lts_aut_base &, lts_dot_base &)
void	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	lts_convert_translate_state (const state_label_empty &, state_label_dot &state_label_out, convertor< lts_aut_base, lts_dot_base > &)
action_label_string	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	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	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	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	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	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	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	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	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	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	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	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	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)
void	add_options (utilities::interface_description &desc)
template<class LTS_TYPE >
void	load_lts (const utilities::command_line_parser &parser, const std::string &ltsfilename, LTS_TYPE &result)
template<class LTS_TYPE >
lps::stochastic_specification	extract_specification (const LTS_TYPE &l)
std::size_t	apply_hidden_labels (const std::size_t n, const std::set< std::size_t > &hidden_action_set)
template<class LTS_TYPE >
void	get_trans (const outgoing_transitions_per_state_t &begin, tree_set_store &tss, std::size_t d, std::vector< transition > &d_trans, LTS_TYPE &aut)
lts_type	guess_format (std::string const &s, const bool be_verbose=true)
	Determines the LTS format from a filename by its extension.
lts_type	parse_format (std::string const &s)
	Determines the LTS format from a format specification string.
std::string	string_for_type (const lts_type type)
	Gives a string representation of an LTS format.
std::string	extension_for_type (const lts_type type)
	Gives the filename extension associated with an LTS format.
std::string	mime_type_for_type (const lts_type type)
	Gives the MIME type associated with an LTS format.
const std::set< lts_type > &	supported_lts_formats ()
	Gives the set of all supported LTS formats.
std::string	supported_lts_formats_text (lts_type default_format=lts_none, const std::set< lts_type > &supported=supported_lts_formats())
	Gives a textual list describing supported LTS formats.
std::string	supported_lts_formats_text (const std::set< lts_type > &supported)
	Gives a textual list describing supported LTS formats.
std::string	lts_extensions_as_string (const std::string &sep=",", const std::set< lts_type > &supported=supported_lts_formats())
	Gives a list of extensions for supported LTS formats.
std::string	lts_extensions_as_string (const std::set< lts_type > &supported)
	Gives a list of extensions for supported LTS formats.
void	read_lps_context (const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels, data::variable_list &process_parameters)
void	read_data_context (const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels)
void	read_mcrl2_context (const std::string &data_file, data::data_specification &data, process::action_label_list &action_labels)
template<class LTS_TYPE_IN , class LTS_TYPE_OUT >
void	convert_to_lts_lts (LTS_TYPE_IN &src, LTS_TYPE_OUT &dest, const data_file_type_t extra_data_file_type, const std::string &extra_data_file_name)
template<class LABEL_TYPE >
LABEL_TYPE	make_divergence_label (const std::string &s)
template<>
mcrl2::lts::action_label_lts	make_divergence_label< mcrl2::lts::action_label_lts > (const std::string &s)
template<class LTS_TYPE >
std::size_t	mark_explicit_divergence_transitions (LTS_TYPE &l)
template<class LTS_TYPE >
void	unmark_explicit_divergence_transitions (LTS_TYPE &l, const std::size_t divergent_transition_label)
bool	save_trace (class trace &tr, const std::string &filename)
void	save_traces (class trace &tr, const std::string &filename1, class trace &tr2, const std::string &filename2)
static const std::set< lts_type > &	initialise_supported_lts_formats ()
template<typename T >
bool	lts_named_cmp (const std::string N[], T a, T b)
static const atermpp::aterm &	transition_mark ()
static const atermpp::aterm &	probabilistic_transition_mark ()
static const atermpp::aterm &	initial_state_mark ()
static const atermpp::aterm &	labelled_transition_system_mark ()
static void	set_initial_state (lts_lts_t &lts, const probabilistic_lts_lts_t::probabilistic_state_t &initial_state)
static void	set_initial_state (probabilistic_lts_lts_t &lts, const probabilistic_lts_lts_t::probabilistic_state_t &initial_state)
template<class LTS >
static void	read_lts (atermpp::aterm_istream &stream, LTS &lts)
template<class LTS_TRANSITION_SYSTEM >
static void	read_from_lts (LTS_TRANSITION_SYSTEM &lts, const std::string &filename)
void	write_initial_state (atermpp::aterm_ostream &stream, const probabilistic_lts_lts_t &lts)
void	write_initial_state (atermpp::aterm_ostream &stream, const lts_lts_t &lts)
template<class LTS >
static void	write_lts (atermpp::aterm_ostream &stream, const LTS &lts)
template<class LTS_TRANSITION_SYSTEM >
static void	write_to_lts (const LTS_TRANSITION_SYSTEM &lts, const std::string &filename)

Variables
const unsigned char	NODE_ATK = 0
const unsigned char	NODE_DEF = 1
const unsigned char	NODE_CPL = 2
static const std::string	type_strings [] = { "unknown", "lts", "aut", "fsm", "dot" }
static const std::string	extension_strings [] = { "", "lts", "aut", "fsm", "dot" }
static std::string	type_desc_strings []
static std::string	mime_type_strings []

Detailed Description

A base class for the lts_dot labelled transition system.

Typedef Documentation

action_label_set

typedef std::set< label_type > mcrl2::lts::detail::action_label_set

Definition at line 37 of file liblts_failures_refinement.h.

anti_chain_type

typedef std::multimap<detail::state_type,detail::set_of_states> mcrl2::lts::detail::anti_chain_type

Definition at line 36 of file liblts_failures_refinement.h.

iterator_or_null_t

template<class El >

using mcrl2::lts::detail::iterator_or_null_t = typedef typename simple_list<El>::iterator_or_null

Definition at line 612 of file simple_list.h.

label_type

typedef std::size_t mcrl2::lts::detail::label_type

type used to store label numbers and counts

It would be better to define it as LTS_TYPE::labels_size_type, but that would require most classes to become templates.

Definition at line 113 of file liblts_bisim_dnj.h.

R_map_t

typedef std::set<bisim_gjkw::constln_t*, constln_ptr_less> mcrl2::lts::detail::R_map_t

Definition at line 2984 of file liblts_bisim_gjkw.cpp.

set_of_states

typedef std::set<state_type> mcrl2::lts::detail::set_of_states

Definition at line 35 of file liblts_failures_refinement.h.

signed_trans_type

typedef std::make_signed<trans_type>::type mcrl2::lts::detail::signed_trans_type

type used to store differences between transition counters

Definition at line 114 of file check_complexity.h.

state_type

typedef std::size_t mcrl2::lts::detail::state_type

type used to store state (numbers and) counts

defined here because this is the most basic #include header that uses it.

It would be better to define it as LTS_TYPE::states_size_type but that would require most classes to become templates.

Definition at line 97 of file check_complexity.h.

trans_type

typedef std::size_t mcrl2::lts::detail::trans_type

type used to store transition (numbers and) counts

defined here because this is the most basic #include header that uses it.

It would be better to define it as LTS_TYPE::transitions_size_type but that would require most classes to become templates.

Definition at line 107 of file check_complexity.h.

Enumeration Type Documentation

t_reach

enum mcrl2::lts::detail::t_reach

Enumerator
unknown
reached
explored

Definition at line 26 of file liblts_tau_star_reduce.h.

Function Documentation

add_an_action_loop_to_each_state()

template<class LTS_TYPE >

void mcrl2::lts::detail::add_an_action_loop_to_each_state	(	LTS_TYPE &	l,
		std::size_t	action
	)

Definition at line 25 of file liblts_add_an_action_loop.h.

add_options()

void mcrl2::lts::detail::add_options ( utilities::interface_description &  desc )

inline

Definition at line 26 of file lts_load.h.

add_probabilities()

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  )

inline

Definition at line 906 of file lts_convert.h.

antichain_insert()

template<class COUNTER_EXAMPLE_CONSTRUCTOR >

bool mcrl2::lts::detail::antichain_insert ( anti_chain_type &  anti_chain, const state_states_counter_example_index_triple< COUNTER_EXAMPLE_CONSTRUCTOR > &  impl_spec  )

inline

Definition at line 504 of file liblts_failures_refinement.h.

apply_hidden_labels()

std::size_t mcrl2::lts::detail::apply_hidden_labels ( const std::size_t  n, const std::set< std::size_t > &  hidden_action_set  )

inline

Definition at line 25 of file transition.h.

bisimulation_compare()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisimulation_compare	(	const LTS_TYPE &	l1,
		const LTS_TYPE &	l2,
		const bool	branching = false,
		const bool	preserve_divergences = false,
		const bool	generate_counter_examples = false,
		const std::string &	counter_example_file = "",
		const bool	structured_output = false
	)

Checks whether the two initial states of two lts's are strong or branching bisimilar.

The current transitions system and the lts l2 are first duplicated and subsequently reduced modulo bisimulation. If memory space is a concern, one could consider to use destructive_bisimulation_compare. This routine uses the Groote-Vaandrager branching bisimulation routine. It runs in O(mn) and uses O(n) memory where n is the number of states and m is the number of transitions.

Parameters

	[in/out]	l1 A first transition system.
	[in/out]	l2 A second transistion system.
[in]	branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
[in]	preserve_divergences	If true and branching is true, preserve tau loops on states.
[in]	generate_counter_examples	Whether to generate a counter example
[in]	counter_example_file	The file to store the counter example in
[in]	structured_output

Return values

True	iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar

Definition at line 1214 of file liblts_bisim.h.

bisimulation_compare_gj()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisimulation_compare_gj ( const LTS_TYPE &  l1, const LTS_TYPE &  l2, const bool  branching = false, const bool  preserve_divergence = false  )

inline

Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.

The LTSs l1 and l2 are first duplicated and subsequently reduced modulo bisimulation. If memory is a concern, one could consider to use destructive_bisimulation_compare(). This routine uses the O(m log n) branching bisimulation algorithm developed in 2018 by David N. Jansen. It runs in O(m log n) time and uses O(m) memory, where n is the number of states and m is the number of transitions.

Parameters

l1	A first transition system.
l2	A second transistion system.
branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
preserve_divergence	If true and branching is true, preserve tau loops on states.

Return values

True	iff the initial states of the transition systems l1 and l2 are ((divergence-preserving) branching) bisimilar.

Definition at line 7136 of file liblts_bisim_gj.h.

bisimulation_reduce()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisimulation_reduce	(	LTS_TYPE &	l,
		const bool	branching = false,
		const bool	preserve_divergences = false
	)

Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.

Parameters

	[in/out]	l The transition system that is reduced.
[in]	branching	If true branching bisimulation is applied, otherwise strong bisimulation.
[in]	preserve_divergences	Indicates whether loops of internal actions on states must be preserved. If false these are removed. If true these are preserved.

Definition at line 1195 of file liblts_bisim.h.

bisimulation_reduce_gj()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisimulation_reduce_gj	(	LTS_TYPE &	l,
		const bool	branching = false,
		const bool	preserve_divergence = false
	)

nonmember functions serving as interface with the rest of mCRL2

These functions are copied, almost without changes, from liblts_bisim_gw.h, which was written by Anton Wijs.

Reduce transition system l with respect to strong or (divergence-preserving) branching bisimulation.

Parameters

[in,out]	l	The transition system that is reduced.
	branching	If true branching bisimulation is applied, otherwise strong bisimulation.
	preserve_divergence	Indicates whether loops of internal actions on states must be preserved. If false these are removed. If true these are preserved.

Definition at line 7043 of file liblts_bisim_gj.h.

calculate_non_reflexive_transitive_tau_closure()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE_CLASS >

std::map< std::size_t, std::set< typename lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS >::states_size_type > > mcrl2::lts::detail::calculate_non_reflexive_transitive_tau_closure	(	lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &	l,
		const bool	forward
	)

This procedure calculates the transitive tau closure as a separate vector of transitions, for a given transition system. \parameter l A labelled transition system \parameter forward A boolean that indicates whether the resulting closure.

Returns

A map from states to sets of states indicating for each state those

Definition at line 40 of file liblts_tau_star_reduce.h.

calculate_tau_reachable_states()

template<class LTS_TYPE >

const set_of_states & mcrl2::lts::detail::calculate_tau_reachable_states	(	const set_of_states &	states,
		const lts_cache< LTS_TYPE > &	weak_property_cache
	)

Definition at line 543 of file liblts_failures_refinement.h.

collect_reachable_states_via_an_action()

template<class LTS_TYPE >

set_of_states mcrl2::lts::detail::collect_reachable_states_via_an_action	(	const state_type	s,
		const label_type	e,
		const lts_cache< LTS_TYPE > &	weak_property_cache,
		const bool	weak_reduction,
		const LTS_TYPE &	l
	)

Definition at line 468 of file liblts_failures_refinement.h.

collect_reachable_states_via_taus() [1/2]

template<class LTS_TYPE >

set_of_states mcrl2::lts::detail::collect_reachable_states_via_taus	(	const set_of_states &	s,
		const lts_cache< LTS_TYPE > &	weak_property_cache,
		const bool	weak_reduction
	)

Definition at line 428 of file liblts_failures_refinement.h.

collect_reachable_states_via_taus() [2/2]

template<class LTS_TYPE >

set_of_states mcrl2::lts::detail::collect_reachable_states_via_taus	(	const state_type	s,
		const lts_cache< LTS_TYPE > &	weak_property_cache,
		const bool	weak_reduction
	)

Definition at line 458 of file liblts_failures_refinement.h.

convert_to_lts_lts()

template<class LTS_TYPE_IN , class LTS_TYPE_OUT >

void mcrl2::lts::detail::convert_to_lts_lts ( LTS_TYPE_IN &  src, LTS_TYPE_OUT &  dest, const data_file_type_t  extra_data_file_type, const std::string &  extra_data_file_name  )

inline

Definition at line 153 of file lts_io.h.

coupled_simulation_compare()

template<class LTS_TYPE >

bool mcrl2::lts::detail::coupled_simulation_compare	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2
	)

(q,p1)a

Definition at line 148 of file liblts_coupledsim.h.

destructive_bisimulation_compare()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_bisimulation_compare	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		const bool	branching = false,
		const bool	preserve_divergences = false,
		const bool	generate_counter_examples = false,
		const std::string &	counter_example_file = "",
		const bool	structured_output = false
	)

Checks whether the two initial states of two lts's are strong or branching bisimilar.

This lts and the lts l2 are not usable anymore after this call. The space consumption is O(n) and time is O(nm). It uses the branching bisimulation algorithm by Groote and Vaandrager from 1990.

Parameters

	[in/out]	l1 A first transition system.
	[in/out]	l2 A second transition system.
[in]	branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
[in]	preserve_divergences	If true and branching is true, preserve tau loops on states.
[in]	generate_counter_examples	Whether to generate a counter example
[in]	counter_example_file	The file to store the counter example in
[in]	structured_output

Return values

True	iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar

Definition at line 1242 of file liblts_bisim.h.

destructive_bisimulation_compare_gj()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_bisimulation_compare_gj	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		const bool	branching = false,
		const bool	preserve_divergence = false,
		const bool	generate_counter_examples = false,
		const std::string &	= "",
		bool	= false
	)

Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.

This routine uses the O(m log n) branching bisimulation algorithm developed in 2018 by David N. Jansen. It runs in O(m log n) time and uses O(m) memory, where n is the number of states and m is the number of transitions.

The LTSs l1 and l2 are not usable anymore after this call.

Parameters

[in,out]	l1	A first transition system.
[in,out]	l2	A second transistion system.
	branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
	preserve_divergence	If true and branching is true, preserve tau loops on states.
	generate_counter_examples	(non-functional, only in the interface for historical reasons)

Returns

True iff the initial states of the transition systems l1 and l2 are ((divergence-preserving) branching) bisimilar.

Definition at line 7090 of file liblts_bisim_gj.h.

destructive_bisimulation_compare_minimal_depth()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_bisimulation_compare_minimal_depth	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		const std::string &	counter_example_file
	)

Definition at line 631 of file liblts_bisim_minimal_depth.h.

destructive_branching_bisimulation_compare_minimal_depth()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_branching_bisimulation_compare_minimal_depth	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		const std::string &	counter_example_file
	)

Definition at line 613 of file liblts_branching_bisim_minimal_depth.h.

destructive_probabilistic_bisimulation_compare_bem()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_probabilistic_bisimulation_compare_bem	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		utilities::execution_timer &	timer
	)

Checks whether the two initial states of two plts's are probabilistic bisimilar.

This lts and the lts l2 are not usable anymore after this call.

Parameters

[in/out]	l1 A first probabilistic transition system.
[in/out]	l2 A second probabilistic transition system.

Return values

True	iff the initial states of the current transition system and l2 are probabilistic bisimilar

Definition at line 834 of file liblts_pbisim_bem.h.

destructive_probabilistic_bisimulation_compare_grv()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_probabilistic_bisimulation_compare_grv	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		utilities::execution_timer &	timer
	)

Checks whether the two initial states of two plts's are probabilistic bisimilar.

This lts and the lts l2 are not usable anymore after this call.

Parameters

[in/out]	l1 A first probabilistic transition system.
[in/out]	l2 A second probabilistic transition system.

Return values

True	iff the initial states of the current transition system and l2 are probabilistic bisimilar

Definition at line 1378 of file liblts_pbisim_grv.h.

destructive_weak_bisimulation_compare()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_weak_bisimulation_compare	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		const bool	preserve_divergences = false
	)

Checks whether the initial states of two LTSs are weakly bisimilar.

The LTSs l1 and l2 are not usable anymore after this call. The space consumption is O(n) and running time is dominated by the transitive closure (after branching bisimulation).

Parameters

[in/out]	l1 A first transition system.
[in/out]	l2 A second transistion system.
[preserve_divergences]	If true and branching is true, preserve tau loops on states.

Return values

True	iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar

Definition at line 75 of file liblts_weak_bisim.h.

equals()

bool mcrl2::lts::detail::equals ( const cs_game_move &  m0, const cs_game_move &  m1, bool  weak_transition = false  )

inline

Definition at line 131 of file liblts_coupledsim.h.

extension_for_type()

std::string mcrl2::lts::detail::extension_for_type

(

const lts_type

type

)

Gives the filename extension associated with an LTS format.

Parameters

[in]

type

The LTS format.

Returns

The filename extension of the LTS format specified by type.

Definition at line 118 of file liblts.cpp.

extract_specification()

template<class LTS_TYPE >

lps::stochastic_specification mcrl2::lts::detail::extract_specification

(

const LTS_TYPE &

l

)

Definition at line 87 of file lts_load.h.

get_trans()

template<class LTS_TYPE >

void mcrl2::lts::detail::get_trans	(	const outgoing_transitions_per_state_t &	begin,
		tree_set_store &	tss,
		std::size_t	d,
		std::vector< transition > &	d_trans,
		LTS_TYPE &	aut
	)

Definition at line 1036 of file lts_algorithm.h.

guess_format()

lts_type mcrl2::lts::detail::guess_format	(	std::string const &	s,
		const bool	be_verbose = true
	)

Determines the LTS format from a filename by its extension.

Parameters

[in]	s	The name of the file of which the format will be determined.
[in]	be_verbose	If true, messages about the detected file format are printed in verbose mode.

Returns

The LTS format based on the extension of s. If no supported format can be determined from the extension then lts_none is returned.

Definition at line 26 of file liblts.cpp.

initial_state_mark()

static const atermpp::aterm & mcrl2::lts::detail::initial_state_mark ( )

static

Definition at line 102 of file liblts_lts.cpp.

initialise_supported_lts_formats()

static const std::set< lts_type > & mcrl2::lts::detail::initialise_supported_lts_formats ( )

static

Definition at line 128 of file liblts.cpp.

labelled_transition_system_mark()

static const atermpp::aterm & mcrl2::lts::detail::labelled_transition_system_mark ( )

static

Definition at line 108 of file liblts_lts.cpp.

load_lts()

template<class LTS_TYPE >

void mcrl2::lts::detail::load_lts	(	const utilities::command_line_parser &	parser,
		const std::string &	ltsfilename,
		LTS_TYPE &	result
	)

Definition at line 44 of file lts_load.h.

lts_convert() [1/8]

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  )

inline

Definition at line 826 of file lts_convert.h.

lts_convert() [2/8]

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  )

inline

Definition at line 835 of file lts_convert.h.

lts_convert() [3/8]

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  )

inline

Definition at line 918 of file lts_convert.h.

lts_convert() [4/8]

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  )

inline

Definition at line 927 of file lts_convert.h.

lts_convert() [5/8]

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  )

inline

Definition at line 879 of file lts_convert.h.

lts_convert() [6/8]

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  )

inline

Definition at line 891 of file lts_convert.h.

lts_convert() [7/8]

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  )

inline

Definition at line 956 of file lts_convert.h.

lts_convert() [8/8]

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  )

inline

Definition at line 966 of file lts_convert.h.

lts_convert_aux()

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  )

inline

Definition at line 789 of file lts_convert.h.

lts_convert_base_class() [1/24]

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

inline

Definition at line 751 of file lts_convert.h.

lts_convert_base_class() [2/24]

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

inline

Definition at line 688 of file lts_convert.h.

lts_convert_base_class() [3/24]

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

inline

Definition at line 646 of file lts_convert.h.

lts_convert_base_class() [4/24]

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

inline

Definition at line 720 of file lts_convert.h.

lts_convert_base_class() [5/24]

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  )

inline

Definition at line 725 of file lts_convert.h.

lts_convert_base_class() [6/24]

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  )

inline

Definition at line 756 of file lts_convert.h.

lts_convert_base_class() [7/24]

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  )

inline

Definition at line 694 of file lts_convert.h.

lts_convert_base_class() [8/24]

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  )

inline

Definition at line 651 of file lts_convert.h.

lts_convert_base_class() [9/24]

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

inline

Definition at line 541 of file lts_convert.h.

lts_convert_base_class() [10/24]

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

inline

Definition at line 586 of file lts_convert.h.

lts_convert_base_class() [11/24]

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

inline

Definition at line 436 of file lts_convert.h.

lts_convert_base_class() [12/24]

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  )

inline

Definition at line 546 of file lts_convert.h.

lts_convert_base_class() [13/24]

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  )

inline

Definition at line 591 of file lts_convert.h.

lts_convert_base_class() [14/24]

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

inline

Definition at line 510 of file lts_convert.h.

lts_convert_base_class() [15/24]

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  )

inline

Definition at line 515 of file lts_convert.h.

lts_convert_base_class() [16/24]

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  )

inline

Definition at line 441 of file lts_convert.h.

lts_convert_base_class() [17/24]

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

inline

Definition at line 343 of file lts_convert.h.

lts_convert_base_class() [18/24]

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

inline

Definition at line 386 of file lts_convert.h.

lts_convert_base_class() [19/24]

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  )

inline

Definition at line 348 of file lts_convert.h.

lts_convert_base_class() [20/24]

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  )

inline

Definition at line 391 of file lts_convert.h.

lts_convert_base_class() [21/24]

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

inline

Definition at line 271 of file lts_convert.h.

lts_convert_base_class() [22/24]

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  )

inline

Definition at line 286 of file lts_convert.h.

lts_convert_base_class() [23/24]

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

inline

Definition at line 225 of file lts_convert.h.

lts_convert_base_class() [24/24]

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  )

inline

Definition at line 230 of file lts_convert.h.

lts_convert_probabilistic_state()

template<class PROBABILISTIC_STATE1 , class PROBABILISTIC_STATE2 >

PROBABILISTIC_STATE2 mcrl2::lts::detail::lts_convert_probabilistic_state ( const PROBABILISTIC_STATE1 &  )

inline

Definition at line 50 of file lts_convert.h.

lts_convert_translate_label() [1/12]

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

inline

Definition at line 362 of file lts_convert.h.

lts_convert_translate_label() [2/12]

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

inline

Definition at line 405 of file lts_convert.h.

lts_convert_translate_label() [3/12]

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

inline

Definition at line 281 of file lts_convert.h.

lts_convert_translate_label() [4/12]

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

inline

Definition at line 244 of file lts_convert.h.

lts_convert_translate_label() [5/12]

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

inline

Definition at line 460 of file lts_convert.h.

lts_convert_translate_label() [6/12]

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

inline

Definition at line 744 of file lts_convert.h.

lts_convert_translate_label() [7/12]

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

inline

Definition at line 775 of file lts_convert.h.

lts_convert_translate_label() [8/12]

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

inline

Definition at line 708 of file lts_convert.h.

lts_convert_translate_label() [9/12]

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

inline

Definition at line 670 of file lts_convert.h.

lts_convert_translate_label() [10/12]

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

inline

Definition at line 565 of file lts_convert.h.

lts_convert_translate_label() [11/12]

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

inline

Definition at line 624 of file lts_convert.h.

lts_convert_translate_label() [12/12]

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

inline

Definition at line 534 of file lts_convert.h.

lts_convert_translate_state() [1/12]

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 > &    )

inline

Definition at line 770 of file lts_convert.h.

lts_convert_translate_state() [2/12]

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 > &    )

inline

Definition at line 713 of file lts_convert.h.

lts_convert_translate_state() [3/12]

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 > &    )

inline

Definition at line 675 of file lts_convert.h.

lts_convert_translate_state() [4/12]

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 > &    )

inline

Definition at line 739 of file lts_convert.h.

lts_convert_translate_state() [5/12]

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 > &    )

inline

Definition at line 560 of file lts_convert.h.

lts_convert_translate_state() [6/12]

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  )

inline

Definition at line 605 of file lts_convert.h.

lts_convert_translate_state() [7/12]

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 > &    )

inline

Definition at line 529 of file lts_convert.h.

lts_convert_translate_state() [8/12]

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  )

inline

Definition at line 465 of file lts_convert.h.

lts_convert_translate_state() [9/12]

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 > &    )

inline

Definition at line 367 of file lts_convert.h.

lts_convert_translate_state() [10/12]

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  )

inline

Definition at line 410 of file lts_convert.h.

lts_convert_translate_state() [11/12]

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  )

inline

Definition at line 300 of file lts_convert.h.

lts_convert_translate_state() [12/12]

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 > &    )

inline

Definition at line 249 of file lts_convert.h.

lts_extensions_as_string() [1/2]

std::string mcrl2::lts::detail::lts_extensions_as_string

(

const std::set< lts_type > &

supported

)

Gives a list of extensions for supported LTS formats.

Parameters

[in]

supported

The formats that should be considered supported.

Returns

A string containing a list of extensions of the formats in supported, separated by ','. E.g. "*.aut,*.lts"

Definition at line 220 of file liblts.cpp.

lts_extensions_as_string() [2/2]

std::string mcrl2::lts::detail::lts_extensions_as_string	(	const std::string &	sep = ",",
		const std::set< lts_type > &	supported = supported_lts_formats()
	)

Gives a list of extensions for supported LTS formats.

Parameters

[in]	sep	The separator to use between each extension.
[in]	supported	The formats that should be considered supported.

Returns

A string containing a list of extensions of the formats in supported, separated by sep. E.g. "*.aut,*.lts"

Definition at line 190 of file liblts.cpp.

lts_named_cmp()

template<typename T >

bool mcrl2::lts::detail::lts_named_cmp	(	const std::string	N[],
		T	a,
		T	b
	)

Definition at line 148 of file liblts.cpp.

make_divergence_label()

template<class LABEL_TYPE >

LABEL_TYPE mcrl2::lts::detail::make_divergence_label

(

const std::string &

s

)

Definition at line 784 of file lts_utilities.h.

make_divergence_label< mcrl2::lts::action_label_lts >()

template<>

mcrl2::lts::action_label_lts mcrl2::lts::detail::make_divergence_label< mcrl2::lts::action_label_lts > ( const std::string &  s )

inline

Definition at line 790 of file lts_utilities.h.

mark_explicit_divergence_transitions()

template<class LTS_TYPE >

std::size_t mcrl2::lts::detail::mark_explicit_divergence_transitions

(

LTS_TYPE &

l

)

Definition at line 800 of file lts_utilities.h.

merge()

template<class LTS_TYPE >

void mcrl2::lts::detail::merge	(	LTS_TYPE &	l1,
		const LTS_TYPE &	l2
	)

Definition at line 43 of file liblts_merge.h.

mime_type_for_type()

std::string mcrl2::lts::detail::mime_type_for_type

(

const lts_type

type

)

Gives the MIME type associated with an LTS format.

Parameters

[in]

type

The LTS format.

Returns

The MIME type of the LTS format specified by type.

Definition at line 123 of file liblts.cpp.

operator!=()

bool mcrl2::lts::detail::operator!= ( const cs_game_node &  n0, const cs_game_node &  n1  )

inline

Definition at line 87 of file liblts_coupledsim.h.

operator<() [1/2]

bool mcrl2::lts::detail::operator< ( const cs_game_move &  m0, const cs_game_move &  m1  )

inline

Definition at line 140 of file liblts_coupledsim.h.

operator<() [2/2]

bool mcrl2::lts::detail::operator< ( const cs_game_node &  n0, const cs_game_node &  n1  )

inline

Definition at line 93 of file liblts_coupledsim.h.

operator==()

bool mcrl2::lts::detail::operator== ( const cs_game_node &  n0, const cs_game_node &  n1  )

inline

Definition at line 77 of file liblts_coupledsim.h.

parse_distribution()

lts_fsm_base::probabilistic_state mcrl2::lts::detail::parse_distribution ( const std::string &  distribution )

inline

Definition at line 45 of file fsm_builder.h.

parse_format()

lts_type mcrl2::lts::detail::parse_format

(

std::string const &

s

)

Determines the LTS format from a format specification string.

This can be any of the following strings:

• "aut" for the Aldébaran format;
• "fsm" for the FSM format;
• "dot" for the GraphViz format;

Parameters

[in]

s

The format specification string.

Returns

The LTS format based on the value of s. If no supported format can be determined then lts_none is returned.

Definition at line 92 of file liblts.cpp.

plts_merge()

template<class LTS_TYPE >

void mcrl2::lts::detail::plts_merge	(	LTS_TYPE &	l1,
		const LTS_TYPE &	l2
	)

Definition at line 43 of file liblts_plts_merge.h.

probabilistic_bisimulation_compare_bem()

template<class LTS_TYPE >

bool mcrl2::lts::detail::probabilistic_bisimulation_compare_bem	(	const LTS_TYPE &	l1,
		const LTS_TYPE &	l2,
		utilities::execution_timer &	timer
	)

Checks whether the two initial states of two plts's are probabilistic bisimilar.

The current transitions system and the lts l2 are first duplicated and subsequently reduced modulo bisimulation. If memory space is a concern, one could consider to use destructive_bisimulation_compare.

Parameters

[in/out]	l1 A first transition system.
[in/out]	l2 A second transistion system.

Return values

True	iff the initial states of the current transition system and l2 are probabilistic bisimilar

Definition at line 823 of file liblts_pbisim_bem.h.

probabilistic_bisimulation_compare_grv()

template<class LTS_TYPE >

bool mcrl2::lts::detail::probabilistic_bisimulation_compare_grv	(	const LTS_TYPE &	l1,
		const LTS_TYPE &	l2,
		utilities::execution_timer &	timer
	)

Checks whether the two initial states of two plts's are probabilistic bisimilar.

The current transitions system and the lts l2 are first duplicated and subsequently reduced modulo bisimulation. If memory space is a concern, one could consider to use destructive_bisimulation_compare.

Parameters

[in/out]	l1 A first transition system.
[in/out]	l2 A second transistion system.

Return values

True	iff the initial states of the current transition system and l2 are probabilistic bisimilar

Definition at line 1367 of file liblts_pbisim_grv.h.

probabilistic_bisimulation_reduce_bem()

template<class LTS_TYPE >

void mcrl2::lts::detail::probabilistic_bisimulation_reduce_bem	(	LTS_TYPE &	l,
		utilities::execution_timer &	timer
	)

Reduce transition system l with respect to probabilistic bisimulation.

Parameters

[in/out]	l The transition system that is reduced.
[in/out]	timer A timer that can be used to report benchmarking results.

Definition at line 807 of file liblts_pbisim_bem.h.

probabilistic_bisimulation_reduce_grv()

template<class LTS_TYPE >

void mcrl2::lts::detail::probabilistic_bisimulation_reduce_grv	(	LTS_TYPE &	l,
		utilities::execution_timer &	timer
	)

Reduce transition system l with respect to probabilistic bisimulation.

Parameters

[in/out]

l The transition system that is reduced.

Definition at line 1352 of file liblts_pbisim_grv.h.

probabilistic_transition_mark()

static const atermpp::aterm & mcrl2::lts::detail::probabilistic_transition_mark ( )

static

Definition at line 96 of file liblts_lts.cpp.

read_data_context()

void mcrl2::lts::detail::read_data_context ( const std::string &  data_file, data::data_specification &  data, process::action_label_list &  action_labels  )

inline

Definition at line 127 of file lts_io.h.

read_from_lts()

template<class LTS_TRANSITION_SYSTEM >

static void mcrl2::lts::detail::read_from_lts ( LTS_TRANSITION_SYSTEM &  lts, const std::string &  filename  )

static

Definition at line 299 of file liblts_lts.cpp.

read_lps_context()

void mcrl2::lts::detail::read_lps_context ( const std::string &  data_file, data::data_specification &  data, process::action_label_list &  action_labels, data::variable_list &  process_parameters  )

inline

Definition at line 115 of file lts_io.h.

read_lts()

template<class LTS >

static void mcrl2::lts::detail::read_lts ( atermpp::aterm_istream &  stream, LTS &  lts  )

static

Definition at line 132 of file liblts_lts.cpp.

read_mcrl2_context()

void mcrl2::lts::detail::read_mcrl2_context ( const std::string &  data_file, data::data_specification &  data, process::action_label_list &  action_labels  )

inline

Definition at line 141 of file lts_io.h.

reflexive_transitive_tau_closure()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE_CLASS >

void mcrl2::lts::detail::reflexive_transitive_tau_closure

(

lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &

l

)

Definition at line 91 of file liblts_tau_star_reduce.h.

refusals_contained_in()

template<class LTS_TYPE >

bool mcrl2::lts::detail::refusals_contained_in	(	const state_type	impl,
		const set_of_states &	spec,
		const lts_cache< LTS_TYPE > &	weak_property_cache,
		label_type &	culprit,
		const LTS_TYPE &	l,
		const bool	provide_a_counter_example,
		const bool	structured_output
	)

This function checks that the refusals(impl) are contained in the refusals of spec, where the refusals of spec are defined by { r | exists s in spec. r in refusals(s) and stable(r) }.

This is equivalent to saying that for all enabled actions of impl it must be contained in the enabled actions of every stable state in spec. If enable(t') is not included in enable(s'), their is a problematic action a. This action is returned as "culprit". It can be used to construct an extended counterexample.

Definition at line 607 of file liblts_failures_refinement.h.

remove_probabilities()

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
	)

Definition at line 849 of file lts_convert.h.

remove_redundant_transitions()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE_CLASS >

void mcrl2::lts::detail::remove_redundant_transitions

(

lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &

l

)

Removes each transition s-a->s' if also transitions s-a->-tau->s' or s-tau->-a->s' are present. It uses the hidden_label_set to determine whether transitions are internal.

Definition at line 139 of file liblts_tau_star_reduce.h.

save_trace()

bool mcrl2::lts::detail::save_trace ( class trace &  tr, const std::string &  filename  )

inline

Definition at line 43 of file state_space_generator.h.

save_traces()

void mcrl2::lts::detail::save_traces ( class trace &  tr, const std::string &  filename1, class trace &  tr2, const std::string &  filename2  )

inline

Definition at line 62 of file state_space_generator.h.

set_initial_state() [1/2]

static void mcrl2::lts::detail::set_initial_state ( lts_lts_t &  lts, const probabilistic_lts_lts_t::probabilistic_state_t &  initial_state  )

static

Definition at line 116 of file liblts_lts.cpp.

set_initial_state() [2/2]

static void mcrl2::lts::detail::set_initial_state ( probabilistic_lts_lts_t &  lts, const probabilistic_lts_lts_t::probabilistic_state_t &  initial_state  )

static

Definition at line 126 of file liblts_lts.cpp.

split_string_until()

std::string mcrl2::lts::detail::split_string_until ( std::string &  s, const std::string &  c1, const std::string &  c2 = ""  )

inline

Definition at line 22 of file fsm_builder.h.

string_for_type()

std::string mcrl2::lts::detail::string_for_type

(

const lts_type

type

)

Gives a string representation of an LTS format.

This is the "inverse" of parse_format.

Parameters

[in]

type

The LTS format.

Returns

The name of the LTS format specified by type.

Definition at line 113 of file liblts.cpp.

supported_lts_formats()

const std::set< lts_type > & mcrl2::lts::detail::supported_lts_formats

(

)

Gives the set of all supported LTS formats.

Returns

The set of all supported LTS formats.

Definition at line 140 of file liblts.cpp.

supported_lts_formats_text() [1/2]

std::string mcrl2::lts::detail::supported_lts_formats_text

(

const std::set< lts_type > &

supported

)

Gives a textual list describing supported LTS formats.

Parameters

[in]

supported

The formats that should be considered supported.

Returns

A string containing lines of the form " 'name' for the ... format". Every line except the last is terminated with '\n'.

Definition at line 185 of file liblts.cpp.

supported_lts_formats_text() [2/2]

std::string mcrl2::lts::detail::supported_lts_formats_text	(	lts_type	default_format = lts_none,
		const std::set< lts_type > &	supported = supported_lts_formats()
	)

Gives a textual list describing supported LTS formats.

Parameters

[in]	default_format	The format that should be marked as default (or lts_none for no default).
[in]	supported	The formats that should be considered supported.

Returns

A string containing lines of the form " 'name' for the ... format". Every line except the last is terminated with '\n'.

Definition at line 153 of file liblts.cpp.

swap_to_non_probabilistic_lts()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

void mcrl2::lts::detail::swap_to_non_probabilistic_lts	(	probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &	l_probabilistic,
		lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > &	l_plain
	)

Definition at line 28 of file liblts_swap_to_from_probabilistic_lts.h.

tau_star_reduce()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class LTS_BASE_CLASS >

void mcrl2::lts::detail::tau_star_reduce

(

lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE_CLASS > &

l

)

Definition at line 245 of file liblts_tau_star_reduce.h.

to_string()

std::string mcrl2::lts::detail::to_string ( const cs_game_node &  n )

inline

Definition at line 103 of file liblts_coupledsim.h.

transition_mark()

static const atermpp::aterm & mcrl2::lts::detail::transition_mark ( )

static

Definition at line 90 of file liblts_lts.cpp.

translate_label_aux()

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  )

inline

Definition at line 198 of file lts_convert.h.

translate_probability_data_prob()

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

inline

Definition at line 92 of file lts_convert.h.

translate_probability_data_to_arbitrary_size_probability()

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

inline

Translate a fraction given as a data_expression to a representation with an arbitrary size fraction.

Definition at line 37 of file lts_convert.h.

translate_probability_labels()

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  )

inline

Definition at line 942 of file lts_convert.h.

translate_to_probabilistic_lts()

template<class STATE_LABEL_T , class ACTION_LABEL_T , class PROBABILISTIC_STATE_T , class LTS_BASE >

void mcrl2::lts::detail::translate_to_probabilistic_lts	(	const lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > &	l_plain,
		probabilistic_lts< STATE_LABEL_T, ACTION_LABEL_T, PROBABILISTIC_STATE_T, LTS_BASE > &	l_probabilistic
	)

Definition at line 63 of file liblts_swap_to_from_probabilistic_lts.h.

unmark_explicit_divergence_transitions()

template<class LTS_TYPE >

void mcrl2::lts::detail::unmark_explicit_divergence_transitions	(	LTS_TYPE &	l,
		const std::size_t	divergent_transition_label
	)

Definition at line 818 of file lts_utilities.h.

weak_bisimulation_compare()

template<class LTS_TYPE >

bool mcrl2::lts::detail::weak_bisimulation_compare	(	const LTS_TYPE &	l1,
		const LTS_TYPE &	l2,
		const bool	preserve_divergences = false
	)

Checks whether the initial states of two LTSs are weakly bisimilar.

The LTSs l1 and l2 are first duplicated and subsequently reduced modulo bisimulation. If memory space is a concern, one could consider to use destructive_weak_bisimulation_compare. The running time of this routine is dominated by the transitive closure (after branching bisimulation). It uses O(m+n) memory in addition to the copies of l1 and l2, where n is the number of states and m is the number of transitions.

Parameters

[in/out]	l1 A first transition system.
[in/out]	l2 A second transistion system.
[preserve_divergences]	If true and branching is true, preserve tau loops on states.

Return values

True	iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar

Definition at line 99 of file liblts_weak_bisim.h.

weak_bisimulation_reduce()

template<class LTS_TYPE >

void mcrl2::lts::detail::weak_bisimulation_reduce	(	LTS_TYPE &	l,
		const bool	preserve_divergences = false
	)

Reduce LTS l with respect to (divergence-preserving) weak bisimulation.

Parameters

	[in/out]	l The transition system that is reduced.
[in]	preserve_divergences	Indicates whether loops of internal actions on states must be preserved. If false these are removed. If true these are preserved.

Definition at line 36 of file liblts_weak_bisim.h.

write_initial_state() [1/2]

void mcrl2::lts::detail::write_initial_state	(	atermpp::aterm_ostream &	stream,
		const lts_lts_t &	lts
	)

Definition at line 347 of file liblts_lts.cpp.

write_initial_state() [2/2]

void mcrl2::lts::detail::write_initial_state	(	atermpp::aterm_ostream &	stream,
		const probabilistic_lts_lts_t &	lts
	)

Definition at line 341 of file liblts_lts.cpp.

write_lts()

template<class LTS >

static void mcrl2::lts::detail::write_lts ( atermpp::aterm_ostream &  stream, const LTS &  lts  )

static

Definition at line 354 of file liblts_lts.cpp.

write_to_lts()

template<class LTS_TRANSITION_SYSTEM >

static void mcrl2::lts::detail::write_to_lts ( const LTS_TRANSITION_SYSTEM &  lts, const std::string &  filename  )

static

Definition at line 394 of file liblts_lts.cpp.

Variable Documentation

extension_strings

const std::string mcrl2::lts::detail::extension_strings[] = { "", "lts", "aut", "fsm", "dot" }

static

Definition at line 73 of file liblts.cpp.

mime_type_strings

std::string mcrl2::lts::detail::mime_type_strings[]

static

Initial value:

= { "",
    "application/lts",
    "text/aut",
    "text/fsm",
    "text/dot"
                                         }

Definition at line 85 of file liblts.cpp.

NODE_ATK

const unsigned char mcrl2::lts::detail::NODE_ATK = 0

Definition at line 45 of file liblts_coupledsim.h.

NODE_CPL

const unsigned char mcrl2::lts::detail::NODE_CPL = 2

Definition at line 47 of file liblts_coupledsim.h.

NODE_DEF

const unsigned char mcrl2::lts::detail::NODE_DEF = 1

Definition at line 46 of file liblts_coupledsim.h.

type_desc_strings

std::string mcrl2::lts::detail::type_desc_strings[]

static

Initial value:

= {
    "unknown LTS format",
    "mCRL2 LTS format",
    "Aldebaran format (CADP)",
    "Finite State Machine format",
    "GraphViz format (no longer supported as input format)",
    "SVC format"
                                         }

Definition at line 75 of file liblts.cpp.

type_strings

const std::string mcrl2::lts::detail::type_strings[] = { "unknown", "lts", "aut", "fsm", "dot" }

static

Definition at line 71 of file liblts.cpp.