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
namespace	bisimulation_gj_lazy_BLC

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_gj_lazy_BLC
	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
using	state_type = std::size_t
	type used to store state (numbers and) counts
using	trans_type = std::size_t
	type used to store transition (numbers and) counts
using	signed_trans_type = std::make_signed_t< trans_type >
	type used to store differences between transition counters
using	R_map_t = std::set< bisim_gjkw::constln_t *, constln_ptr_less >
using	label_type = std::size_t
	type used to store label numbers and counts
using	set_of_states = boost::container::flat_set< state_type >
using	action_label_set = boost::container::flat_set< label_type >
using	anti_chain_type = std::multimap< detail::state_type, detail::set_of_states >
template<class El >
using	iterator_or_null_t = typename simple_list< El >::iterator_or_null

Enumerations
enum	t_reach { unknown , reached , explored }

Functions
lts_type	guess_format (std::string const &s, 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 (lts_type type)
	Gives a string representation of an LTS format.
std::string	extension_for_type (lts_type type)
	Gives the filename extension associated with an LTS format.
std::string	mime_type_for_type (lts_type type)
	Gives the MIME type associated with an LTS format.
static const std::set< lts_type > &	initialise_supported_lts_formats ()
const std::set< lts_type > &	supported_lts_formats ()
	Gives the set of all supported LTS formats.
template<std::size_t Size, typename T >
bool	lts_named_cmp (const std::array< std::string, Size > &N, T a, T b)
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.
template<class LTS_TYPE >
void	get_trans (const outgoing_transitions_per_state_t &begin, tree_set_store &tss, std::ptrdiff_t d, std::vector< transition > &d_trans, LTS_TYPE &aut)
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 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 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)
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)
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)
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, bool branching=false, 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, bool branching=false, bool preserve_divergences=false, bool generate_counter_examples=false, const std::string &counter_example_file="", 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, bool branching=false, bool preserve_divergences=false, bool generate_counter_examples=false, const std::string &counter_example_file="", 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_gj_lazy_BLC (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_lazy_BLC (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_lazy_BLC (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 >
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)
bool	antichain_include (anti_chain_type &anti_chain, const detail::state_type &impl, const detail::set_of_states &spec)
bool	antichain_insert (anti_chain_type &anti_chain, const detail::state_type &impl, const detail::set_of_states &spec)
template<class LTS_TYPE >
set_of_states	collect_reachable_states_via_taus (state_type s, const lts_cache< LTS_TYPE > &weak_property_cache, bool weak_reduction)
template<class LTS_TYPE >
set_of_states	collect_reachable_states_via_an_action (state_type s, label_type e, const lts_cache< LTS_TYPE > &weak_property_cache, 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)
bool	antichain_include_inverse (anti_chain_type &anti_chain, const detail::state_type &impl, const detail::set_of_states &spec)
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<typename LTS >
bool	destructive_impossible_futures (LTS &l1, LTS &l2, const lps::exploration_strategy strategy, std::string counter_example_file, bool generate_counter_example, bool structured_output)
	Checks impossible futures refinement for the given LTSs.
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 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)
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)

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

Detailed Description

A base class for the lts_dot labelled transition system.

This file contains two functions to efficiently transform

If this preprocessor constant is defined, the program will print some more, and more frequent, progress statistics. Every 10 seconds, also a lower bound on the number of transitions is printed. Additionally, it is counted how often single-block BLC sets are required in the two situations mentioned above.

Typedef Documentation

action_label_set

using mcrl2::lts::detail::action_label_set = typedef boost::container::flat_set<label_type>

Definition at line 37 of file liblts_failures_refinement.h.

anti_chain_type

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

Definition at line 38 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 978 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 55 of file liblts_bisim_gjkw.h.

R_map_t

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

Definition at line 3055 of file liblts_bisim_gjkw.cpp.

set_of_states

using mcrl2::lts::detail::set_of_states = typedef boost::container::flat_set<state_type>

Definition at line 36 of file liblts_failures_refinement.h.

signed_trans_type

using mcrl2::lts::detail::signed_trans_type = typedef std::make_signed_t<trans_type>

type used to store differences between transition counters

Definition at line 124 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 109 of file check_complexity.h.

trans_type

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

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 119 of file check_complexity.h.

Enumeration Type Documentation

t_reach

enum mcrl2::lts::detail::t_reach

Enumerator
unknown
reached
explored

Definition at line 22 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 21 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 849 of file lts_convert.h.

antichain_include()

bool mcrl2::lts::detail::antichain_include ( anti_chain_type &  anti_chain, const detail::state_type &  impl, const detail::set_of_states &  spec  )

inline

Definition at line 477 of file liblts_failures_refinement.h.

antichain_include_inverse()

bool mcrl2::lts::detail::antichain_include_inverse ( anti_chain_type &  anti_chain, const detail::state_type &  impl, const detail::set_of_states &  spec  )

inline

Definition at line 498 of file liblts_failures_refinement.h.

antichain_insert()

bool mcrl2::lts::detail::antichain_insert ( anti_chain_type &  anti_chain, const detail::state_type &  impl, const detail::set_of_states &  spec  )

inline

Definition at line 529 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 20 of file transition.h.

bisimulation_compare()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisimulation_compare	(	const LTS_TYPE &	l1,
		const LTS_TYPE &	l2,
		bool	branching = false,
		bool	preserve_divergences = false,
		bool	generate_counter_examples = false,
		const std::string &	counter_example_file = "",
		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 1177 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 6939 of file liblts_bisim_gj.h.

bisimulation_compare_gj_lazy_BLC()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisimulation_compare_gj_lazy_BLC ( 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_gj_lazy_BLC(). This routine uses the experimental O(m log n) branching bisimulation algorithm published in 2025 by Jan Friso Groote and David N. Jansen, with the variant that only creates BLC sets when necessary. 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.

Returns

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

Definition at line 7442 of file liblts_bisim_gj_lazy_BLC.h.

bisimulation_reduce()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisimulation_reduce	(	LTS_TYPE &	l,
		bool	branching = false,
		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 1158 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 6779 of file liblts_bisim_gj.h.

bisimulation_reduce_gj_lazy_BLC()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisimulation_reduce_gj_lazy_BLC	(	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 7278 of file liblts_bisim_gj_lazy_BLC.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 36 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 561 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	(	state_type	s,
		label_type	e,
		const lts_cache< LTS_TYPE > &	weak_property_cache,
		bool	weak_reduction,
		const LTS_TYPE &	l
	)

Definition at line 455 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 417 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	(	state_type	s,
		const lts_cache< LTS_TYPE > &	weak_property_cache,
		bool	weak_reduction
	)

Definition at line 446 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 158 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 144 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,
		bool	branching = false,
		bool	preserve_divergences = false,
		bool	generate_counter_examples = false,
		const std::string &	counter_example_file = "",
		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 1205 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 experimental O(m log n) branching bisimulation algorithm developed in 2024 by Jan Friso Groote and 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 6894 of file liblts_bisim_gj.h.

destructive_bisimulation_compare_gj_lazy_BLC()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_bisimulation_compare_gj_lazy_BLC	(	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 experimental O(m log n) branching bisimulation algorithm published in 2025 by Jan Friso Groote and David N. Jansen, with the variant that only creates BLC sets when necessary. 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 7395 of file liblts_bisim_gj_lazy_BLC.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 626 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 614 of file liblts_branching_bisim_minimal_depth.h.

destructive_impossible_futures()

template<typename LTS >

bool mcrl2::lts::detail::destructive_impossible_futures	(	LTS &	l1,
		LTS &	l2,
		const lps::exploration_strategy	strategy,
		std::string	counter_example_file,
		bool	generate_counter_example,
		bool	structured_output
	)

Checks impossible futures refinement for the given LTSs.

Impossible futures are defined in the article:

Marc Voorhoeve, Sjouke Mauw. Impossible futures and determinism, Inf. Process. Lett. 80, 2001.

Definition at line 317 of file liblts_impossible_futures.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 829 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 1371 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 71 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 127 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 117 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::ptrdiff_t	d,
		std::vector< transition > &	d_trans,
		LTS_TYPE &	aut
	)

Definition at line 1081 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 104 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 127 of file liblts.cpp.

labelled_transition_system_mark()

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

static

Definition at line 110 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 769 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 778 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 861 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 870 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 822 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 834 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 899 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 909 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 732 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 694 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 631 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 589 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 663 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 668 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 699 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 637 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 594 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 484 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 529 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 379 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 489 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 534 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 453 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 458 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 384 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 288 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 329 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 293 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 334 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 216 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 231 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 170 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 175 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 46 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 307 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 348 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 226 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 189 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 403 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 687 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 718 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 651 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 613 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 508 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 567 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 477 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 713 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 656 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 618 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 682 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 503 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 548 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 472 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 408 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 312 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 353 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 245 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 194 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 221 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<std::size_t Size, typename T >

bool mcrl2::lts::detail::lts_named_cmp	(	const std::array< std::string, Size > &	N,
		T	a,
		T	b
	)

Definition at line 147 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 601 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 607 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 617 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 39 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 122 of file liblts.cpp.

operator!=()

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

inline

Definition at line 83 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 136 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 89 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 73 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 91 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 39 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 818 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 1360 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 802 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 1345 of file liblts_pbisim_grv.h.

probabilistic_transition_mark()

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

static

Definition at line 98 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 132 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 300 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 120 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 134 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 146 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 87 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 625 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 792 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 134 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 45 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 64 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 118 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 128 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 112 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 139 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 152 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 23 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 239 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 99 of file liblts_coupledsim.h.

transition_mark()

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

static

Definition at line 92 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 145 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 88 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 33 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 885 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 58 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 635 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 95 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 32 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 348 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 342 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 355 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

static const std::array< std::string, 5 > mcrl2::lts::detail::extension_strings = { "", "lts", "aut", "fsm", "dot" }

static

Definition at line 73 of file liblts.cpp.

mime_type_strings

static const std::array< std::string, 5 > mcrl2::lts::detail::mime_type_strings

static

Initial value:

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

Definition at line 84 of file liblts.cpp.

NODE_ATK

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

Definition at line 41 of file liblts_coupledsim.h.

NODE_CPL

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

Definition at line 43 of file liblts_coupledsim.h.

NODE_DEF

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

Definition at line 42 of file liblts_coupledsim.h.

type_desc_strings

static const std::array< std::string, 5 > 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)"
                                         }

Definition at line 75 of file liblts.cpp.

type_strings

static const std::array< std::string, 5 > mcrl2::lts::detail::type_strings = { "unknown", "lts", "aut", "fsm", "dot" }

static

Definition at line 71 of file liblts.cpp.