The main LTS namespace. More...

Namespaces
namespace	detail
	A base class for the lts_dot labelled transition system.

Classes
class	action_label_lts
	A class containing the values for action labels for the .lts format. More...

class	action_label_string
	This class contains strings to be used as values for action labels in lts's. More...

struct	fsm_writer

class	lts
	A class that contains a labelled transition system. More...

class	lts_aut_builder

class	lts_aut_disk_builder

class	lts_aut_t
	A simple labelled transition format with only strings as action labels. More...

struct	lts_builder

class	lts_default_base

class	lts_dot_builder

class	lts_dot_t
	A class to contain labelled transition systems in graphviz format. More...

class	lts_fsm_builder

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

class	lts_lts_builder

class	lts_lts_disk_builder

class	lts_lts_t
	This class contains labelled transition systems in .lts format. More...

class	lts_none_builder

class	probabilistic_lts
	A class that contains a labelled transition system. More...

class	probabilistic_lts_aut_t
	A simple labelled transition format with only strings as action labels. More...

class	probabilistic_lts_dot_t
	A class to contain labelled transition systems in graphviz format. More...

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

class	probabilistic_lts_lts_t
	This class contains probabilistic labelled transition systems in .lts format. More...

class	probabilistic_state
	A class that contains a probabilistic state. More...

struct	refinement_statistics

class	signature
	Base class for signature computation. More...

class	signature_bisim
	Class for computing the signature for strong bisimulation. More...

class	signature_branching_bisim
	Class for computing the signature for branching bisimulation. More...

class	signature_divergence_preserving_branching_bisim
	Class for computing the signature for divergence preserving branching bisimulation. More...

class	sigref
	Signature based reductions for labelled transition systems. More...

class	state_label_dot
	This class contains labels for states in dot format. More...

class	state_label_empty
	Contains empty state values, used for lts's without state valued. More...

class	state_label_fsm
	This class contains state labels for the fsm format. More...

class	state_label_lts
	This class contains state labels for an labelled transition system in .lts format. More...

struct	state_space_generator

class	stochastic_lts_aut_builder

struct	stochastic_lts_builder

class	stochastic_lts_fsm_builder

class	stochastic_lts_lts_builder

class	stochastic_lts_none_builder

class	trace
	This class contains a trace consisting of a sequence of (timed) actions possibly with intermediate states. More...

class	transition
	A class containing triples, source label and target representing transitions. More...

class	tree_set_store

Typedefs
typedef std::pair< transition::size_type, transition::size_type >	outgoing_pair_t
	Type for exploring transitions per state.

typedef detail::indexed_sorted_vector_for_transitions< outgoing_pair_t >	outgoing_transitions_per_state_t

typedef std::multimap< std::pair< transition::size_type, transition::size_type >, transition::size_type >	outgoing_transitions_per_state_action_t
	Type for exploring transitions per state and action.

typedef std::set< std::pair< std::size_t, std::size_t > >	signature_t
	A signature is a pair of an action label and a block.

Enumerations
enum class	refinement_type { trace , failures , failures_divergence }

enum	lts_equivalence { lts_eq_none , lts_eq_bisim , lts_eq_bisim_gv , lts_eq_bisim_gjkw , lts_eq_bisim_gj , lts_eq_bisim_sigref , lts_eq_branching_bisim , lts_eq_branching_bisim_gv , lts_eq_branching_bisim_gjkw , lts_eq_branching_bisim_gj , lts_eq_branching_bisim_sigref , lts_eq_divergence_preserving_branching_bisim , lts_eq_divergence_preserving_branching_bisim_gv , lts_eq_divergence_preserving_branching_bisim_gjkw , lts_eq_divergence_preserving_branching_bisim_gj , lts_eq_divergence_preserving_branching_bisim_sigref , lts_eq_weak_bisim , lts_eq_divergence_preserving_weak_bisim , lts_eq_sim , lts_eq_ready_sim , lts_eq_trace , lts_eq_weak_trace , lts_eq_coupled_sim , lts_red_tau_star , lts_red_determinisation }
	LTS equivalence relations. More...

enum	data_file_type_t { none_e , data_e , lps_e , mcrl2_e }
	Type for data files that contain extra information for an lts in .aut or .fsm format. Typically this is a data_specification (data_e), a linear process (lps_e) or an .mcrl2 file. The value none_e indicates that no information is available. More...

enum	lts_preorder { lts_pre_none , lts_pre_sim , lts_pre_ready_sim , lts_pre_trace , lts_pre_weak_trace , lts_pre_trace_anti_chain , lts_pre_weak_trace_anti_chain , lts_pre_failures_refinement , lts_pre_weak_failures_refinement , lts_pre_failures_divergence_refinement , lts_preorder_min = lts_pre_none , lts_preorder_max = lts_pre_failures_divergence_refinement }
	LTS preorder relations. More...

enum	lts_probabilistic_equivalence { lts_probabilistic_eq_none , lts_probabilistic_bisim_bem , lts_probabilistic_bisim_grv }
	LTS equivalence relations. More...

enum	lts_probabilistic_preorder { lts_probabilistic_pre_none }
	LTS preorder relations. More...

enum	lts_type { lts_none , lts_lts , lts_aut , lts_fsm , lts_dot , lts_lts_probabilistic , lts_aut_probabilistic , lts_fsm_probabilistic , lts_type_min =lts_none , lts_type_max =lts_dot }
	The enumerated type lts_type contains an index for every type type of labelled transition system that is supported by the system. More...

enum	transition_sort_style { src_lbl_tgt , lbl_tgt_src , tgt_lbl_src , tgt_src_lbl , tgt_lbl , target }
	Transition sort styles. More...

Functions
std::string	pp (const action_label_string &l)

template<typename T >
void	report_statistics (refinement_statistics< T > &stats)
	Print a message to debugging containing information about the given statistics.

template<typename LTS_TYPE >
std::pair< std::size_t, bool >	reduce (LTS_TYPE &lts, const bool weak_reduction, const bool preserve_divergence, std::size_t l2_init)
	Preprocess the LTS for destructive refinement checking.

template<class LTS_TYPE , class COUNTER_EXAMPLE_CONSTRUCTOR = detail::dummy_counter_example_constructor>
bool	destructive_refinement_checker (LTS_TYPE &l1, LTS_TYPE &l2, const refinement_type refinement, const bool weak_reduction, const lps::exploration_strategy strategy, const bool preprocess=true, COUNTER_EXAMPLE_CONSTRUCTOR generate_counter_example=detail::dummy_counter_example_constructor())
	This function checks using algorithms in the paper mentioned above whether transition system l1 is included in transition system l2, in the sense of trace inclusions, failures inclusion and divergence failures inclusion.

template<class LTS_TYPE >
void	scc_reduce (LTS_TYPE &l, const bool preserve_divergence_loops=false)

lps::specification	transform_lts2lps (const lts_lts_t &l)
	transform an lts in lts format into a linear process.

lps::specification	transform_lts2lps (const lts_aut_t &l1, const data_specification &data, const process::action_label_list &action_labels, const variable_list &process_parameters)
	transform an lts in aut format into a linear process.

lps::specification	transform_lts2lps (const lts_fsm_t &l1, const data_specification &data, const process::action_label_list &action_labels, const variable_list &process_parameters)
	transform an lts in fsm format into a linear process.

template<class LTS_TYPE >
void	reduce (LTS_TYPE &l, lts_equivalence eq)
	Applies a reduction algorithm to this LTS.

template<class LTS_TYPE >
bool	destructive_compare (LTS_TYPE &l1, LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file=std::string(), const bool structured_output=false)
	Checks whether this LTS is equivalent to another LTS.

template<class LTS_TYPE >
bool	compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_equivalence eq, const bool generate_counter_examples=false, const std::string &counter_example_file="", const bool structured_output=false)
	Checks whether this LTS is equivalent to another LTS.

template<class LTS_TYPE >
bool	destructive_compare (LTS_TYPE &l1, LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, const std::string &counter_example_file="", const bool structured_output=false, const lps::exploration_strategy strategy=lps::es_breadth, const bool preprocess=true)
	Checks whether this LTS is smaller than another LTS according to a preorder.

template<class LTS_TYPE >
bool	compare (const LTS_TYPE &l1, const LTS_TYPE &l2, const lts_preorder pre, const bool generate_counter_example, const std::string &counter_example_file="", const bool structured_output=false, const lps::exploration_strategy strategy=lps::es_breadth, const bool preprocess=true)
	Checks whether this LTS is smaller than another LTS according to a preorder.

template<class LTS_TYPE >
void	determinise (LTS_TYPE &l)
	Determinises this LTS.

template<class SL , class AL , class BASE >
bool	reachability_check (lts< SL, AL, BASE > &l, bool remove_unreachable=false)
	Checks whether all states in this LTS are reachable from the initial state and remove unreachable states if required.

template<class SL , class AL , class PROBABILISTIC_STATE , class BASE >
bool	reachability_check (probabilistic_lts< SL, AL, PROBABILISTIC_STATE, BASE > &l, bool remove_unreachable=false)
	Checks whether all states in a probabilistic LTS are reachable from the initial state and remove unreachable states if required.

template<class LTS_TYPE >
bool	is_deterministic (const LTS_TYPE &l)
	Checks whether this LTS is deterministic.

template<class LTS_TYPE >
void	merge (LTS_TYPE &l1, const LTS_TYPE &l2)
	Merge the second lts into the first lts.

lps::state	remove_time_stamp (const lps::state &s)
	Removes the last element from state s.

std::unique_ptr< lts_builder >	create_lts_builder (const lps::specification &lpsspec, const lps::explorer_options &options, lts_type output_format, const std::string &output_filename="")

std::string	pp (const state_label_dot &l)
	Pretty print function for a state_label_dot. Only prints the label field.

lts_equivalence	parse_equivalence (std::string const &s)
	Determines the equivalence from a string.

std::istream &	operator>> (std::istream &is, lts_equivalence &eq)

std::string	print_equivalence (const lts_equivalence eq)
	Gives the short name of an equivalence.

std::ostream &	operator<< (std::ostream &os, const lts_equivalence eq)

std::string	description (const lts_equivalence eq)
	Gives a description of an equivalence.

std::string	pp (const state_label_fsm &label)
	Pretty print an fsm state label.

template<class LTS_TYPE >
void	load_lts (LTS_TYPE &result, const std::string &infilename, lts_type type, const data_file_type_t extra_data_file_type=none_e, const std::string &extra_data_file_name="")
	Loads an lts of the indicated type, transforms it to an lts of the form lts_lts_t using the additional data parameters.

void	load_lts_as_fsm_file (const std::string &path, lts_fsm_t &l)
	Read a labelled transition system and return it in fsm format.

atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, lts_lts_t &lts)
	Read a (probabilistic) LTS from the given stream.

atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, probabilistic_lts_lts_t &lts)

atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const lts_lts_t &lts)
	Write a (probabilistic) LTS to the given stream at once.

atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const probabilistic_lts_lts_t &lts)

void	write_lts_header (atermpp::aterm_ostream &stream, const data::data_specification &data, const data::variable_list &parameters, const process::action_label_list &action_labels)
	Writes the start of an LTS stream.

void	write_transition (atermpp::aterm_ostream &stream, std::size_t from, const lps::multi_action &label, std::size_t to)
	Write a transition to the LTS stream.

void	write_transition (atermpp::aterm_ostream &stream, std::size_t from, const lps::multi_action &label, const probabilistic_lts_lts_t::probabilistic_state_t &to)

void	write_state_label (atermpp::aterm_ostream &stream, const state_label_lts &label)
	Write a state label to the LTS stream.

void	write_initial_state (atermpp::aterm_ostream &stream, std::size_t index)
	Write the initial state to the LTS stream.

std::string	pp (const state_label_lts &label)
	Pretty print a state value of this LTS.

std::string	pp (const action_label_lts &l)
	Print the action label to string.

action_label_lts	parse_lts_action (const std::string &multi_action_string, const data::data_specification &data_spec, lps::multi_action_type_checker &typechecker)
	Parse a string into an action label.

lts_preorder	parse_preorder (std::string const &s)
	Determines the preorder from a string.

std::istream &	operator>> (std::istream &is, lts_preorder &eq)

std::string	print_preorder (const lts_preorder pre)
	Gives the short name of a preorder.

std::ostream &	operator<< (std::ostream &os, const lts_preorder pre)

std::string	description (const lts_preorder pre)
	Gives a description of a preorder.

lts_probabilistic_equivalence	parse_probabilistic_equivalence (const std::string &s)
	Determines the equivalence from a string.

std::istream &	operator>> (std::istream &is, lts_probabilistic_equivalence &eq)

std::string	print_probabilistic_equivalence (const lts_probabilistic_equivalence &eq)
	Gives the short name of an equivalence.

std::ostream &	operator<< (std::ostream &os, const lts_probabilistic_equivalence &eq)

std::string	description (const lts_probabilistic_equivalence &eq)
	Gives a description of an equivalence.

lts_probabilistic_preorder	parse_probabilistic_preorder (std::string const &s)
	Determines the probabilistic preorder from a string.

std::istream &	operator>> (std::istream &is, lts_probabilistic_preorder &eq)

std::string	print_probabilistic_preorder (const lts_probabilistic_preorder &pre)
	Gives the short name of an preorder.

std::ostream &	operator<< (std::ostream &os, const lts_probabilistic_preorder &pre)

std::string	description (const lts_probabilistic_preorder &pre)
	Gives a description of an preorder.

void	sort_transitions (std::vector< transition > &transitions, const std::set< transition::size_type > &hidden_label_set, transition_sort_style ts=src_lbl_tgt)
	Sorts the transitions using a sort style.

std::string	ptr (const transition t)
	Sorts the transitions on labels. Action with the tau label are put first.

void	group_transitions_on_label (const std::vector< transition >::iterator begin, const std::vector< transition >::iterator end, std::function< std::size_t(const transition &)> get_label, const std::size_t tau_label_index, std::vector< std::pair< std::size_t, std::size_t > > &count_sum_transitions_per_action, std::vector< std::size_t > &todo_stack)

void	group_transitions_on_label (std::vector< transition > &transitions, std::function< std::size_t(const transition &)> get_label, const std::size_t number_of_labels, const std::size_t tau_label_index)

void	group_transitions_on_label_tgt (std::vector< transition > &transitions, const std::size_t number_of_labels, const std::size_t tau_label_index, const std::size_t number_of_states)

void	sort_transitions (std::vector< transition > &transitions, transition_sort_style ts=src_lbl_tgt)
	Sorts the transitions using a sort style.

std::size_t	label (const outgoing_pair_t &p)
	Label of a pair of a label and target state.

std::size_t	to (const outgoing_pair_t &p)
	Target state of a label state pair.

std::size_t	from (const outgoing_transitions_per_state_action_t::const_iterator &i)
	From state of an iterator exploring transitions per outgoing state and action.

std::size_t	label (const outgoing_transitions_per_state_action_t::const_iterator &i)
	Label of an iterator exploring transitions per outgoing state and action.

std::size_t	to (const outgoing_transitions_per_state_action_t::const_iterator &i)
	To state of an iterator exploring transitions per outgoing state and action.

outgoing_transitions_per_state_action_t	transitions_per_outgoing_state_action_pair (const std::vector< transition > &trans)
	Provide the transitions as a multimap accessible per from state and label.

outgoing_transitions_per_state_action_t	transitions_per_outgoing_state_action_pair (const std::vector< transition > &trans, const std::set< transition::size_type > &hide_label_set)
	Provide the transitions as a multimap accessible per from state and label.

outgoing_transitions_per_state_action_t	transitions_per_outgoing_state_action_pair_reversed (const std::vector< transition > &trans)
	Provide the transitions as a multimap accessible per from state and label, ordered backwardly.

outgoing_transitions_per_state_action_t	transitions_per_outgoing_state_action_pair_reversed (const std::vector< transition > &trans, const std::set< transition::size_type > &hide_label_set)
	Provide the transitions as a multimap accessible per from state and label, ordered backwardly.

void	parse_fsm_specification (std::istream &from, probabilistic_lts_fsm_t &result)

void	parse_fsm_specification (const std::string &text, probabilistic_lts_fsm_t &result)

template<class STATE , class PROBABILITY >
std::string	pp (const probabilistic_state< STATE, PROBABILITY > &l)

template<class STATE , class PROBABILITY >
std::ostream &	operator<< (std::ostream &out, const probabilistic_state< STATE, PROBABILITY > &l)
	Pretty print to an outstream.

std::string	pp (const state_label_empty &)

std::ostream &	operator<< (std::ostream &out, const lps::state &s)

const lps::state &	first_state (const lps::state &s)

const lps::state &	first_state (const lps::stochastic_state &s)

std::unique_ptr< stochastic_lts_builder >	create_stochastic_lts_builder (const lps::stochastic_specification &lpsspec, const lps::explorer_options &options, lts_type output_format)

atermpp::aterm_ostream &	operator<< (atermpp::aterm_ostream &stream, const probabilistic_lts_lts_t::probabilistic_state_t &state)
	Converts a probabilistic state into an aterm that encodes it.

atermpp::aterm_istream &	operator>> (atermpp::aterm_istream &stream, probabilistic_lts_lts_t::probabilistic_state_t &state)

Variables
static const std::size_t	const_tau_label_index =0

Detailed Description

The main LTS namespace.

The namespace for traces.

This namespace contains all data structures and members of the LTS library.

The namespace trace contains all data structures and members of the trace library.

Typedef Documentation

◆ outgoing_pair_t

typedef std::pair<transition::size_type, transition::size_type> mcrl2::lts::outgoing_pair_t

Type for exploring transitions per state.

Definition at line 593 of file lts_utilities.h.

◆ outgoing_transitions_per_state_action_t

typedef std::multimap<std::pair<transition::size_type, transition::size_type>, transition::size_type> mcrl2::lts::outgoing_transitions_per_state_action_t

Type for exploring transitions per state and action.

Definition at line 614 of file lts_utilities.h.

◆ outgoing_transitions_per_state_t

typedef detail::indexed_sorted_vector_for_transitions< outgoing_pair_t > mcrl2::lts::outgoing_transitions_per_state_t

Definition at line 595 of file lts_utilities.h.

◆ signature_t

typedef std::set<std::pair<std::size_t, std::size_t> > mcrl2::lts::signature_t

A signature is a pair of an action label and a block.

Definition at line 25 of file sigref.h.

Enumeration Type Documentation

◆ data_file_type_t

enum mcrl2::lts::data_file_type_t

Type for data files that contain extra information for an lts in .aut or .fsm format. Typically this is a data_specification (data_e), a linear process (lps_e) or an .mcrl2 file. The value none_e indicates that no information is available.

Enumerator
none_e
data_e
lps_e
mcrl2_e

Definition at line 33 of file lts_io.h.

◆ lts_equivalence

enum mcrl2::lts::lts_equivalence

LTS equivalence relations.

This enumerated type defines equivalence relations on LTSs. They can be used to reduce an LTS or decide whether two LTSs are equivalent.

Enumerator
lts_eq_none	Unknown or no equivalence
lts_eq_bisim	Strong bisimulation equivalence using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
lts_eq_bisim_gv	Strong bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]
lts_eq_bisim_gjkw	Strong bisimulation equivalence using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
lts_eq_bisim_gj	Strong bisimulation equivalence using an O(m log n) experimental algorithm [Groote/Jansen 2024]
lts_eq_bisim_sigref	Strong bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003]
lts_eq_branching_bisim	Branching bisimulation equivalence using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
lts_eq_branching_bisim_gv	Branching bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]
lts_eq_branching_bisim_gjkw	Branching bisimulation equivalence using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017
lts_eq_branching_bisim_gj	Branching bisimulation equivalence using the expremental O(m log n) algorithm [Groote/Jansen 2024]
lts_eq_branching_bisim_sigref	Branching bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003]
lts_eq_divergence_preserving_branching_bisim	Divergence-preserving branching bisimulation equivalence using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
lts_eq_divergence_preserving_branching_bisim_gv	Divergence-preserving branching bisimulation equivalence using the O(mn) algorithm [Groote/Vaandrager 1990]
lts_eq_divergence_preserving_branching_bisim_gjkw	Divergence-preserving branching bisimulation equivalence using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
lts_eq_divergence_preserving_branching_bisim_gj	Divergence-preserving branching bisimulation equivalence using the O(m log n) experimental algorithm [Groote/Jansen 2024]
lts_eq_divergence_preserving_branching_bisim_sigref
lts_eq_weak_bisim	Divergence-preserving branching bisimulation equivalence using the signature refinement algorithm [Blom/Orzan 2003] Weak bisimulation equivalence
lts_eq_divergence_preserving_weak_bisim	Divergence-preserving weak bisimulation equivalence
lts_eq_sim	Strong simulation equivalence
lts_eq_ready_sim	Strong ready-simulation equivalence
lts_eq_trace	Strong trace equivalence
lts_eq_weak_trace	Weak trace equivalence
lts_eq_coupled_sim
lts_red_tau_star	Coupled Similarity TODO Tau star reduction
lts_red_determinisation	Used for a determinisation reduction

Definition at line 33 of file lts_equivalence.h.

◆ lts_preorder

enum mcrl2::lts::lts_preorder

LTS preorder relations.

This enumerated type defines preorder relations on LTSs. They can be used to decide whether one LTS is behaviourally contained in another LTS.

Enumerator
lts_pre_none	Unknown or no preorder
lts_pre_sim	Strong simulation preorder
lts_pre_ready_sim	Strong ready simulation preorder
lts_pre_trace	Strong trace preorder
lts_pre_weak_trace	Weak trace preorder
lts_pre_trace_anti_chain	Trace preorder based on anti chains
lts_pre_weak_trace_anti_chain	Weak trace preorder based on anti chains
lts_pre_failures_refinement	Failures refinement based on anti chains
lts_pre_weak_failures_refinement	Weak failures refinement based on anti chains
lts_pre_failures_divergence_refinement	Failures divergence refinement based on anti chains, which is automatically weak
lts_preorder_min
lts_preorder_max

Definition at line 31 of file lts_preorder.h.

◆ lts_probabilistic_equivalence

enum mcrl2::lts::lts_probabilistic_equivalence

LTS equivalence relations.

This enumerated type defines equivalence relations on LTSs. They can be used to reduce an LTS or decide whether two LTSs are equivalent.

Enumerator
lts_probabilistic_eq_none	Unknown or no equivalence
lts_probabilistic_bisim_bem	Probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm [Bier]
lts_probabilistic_bisim_grv	Probabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera Verduzco and de Vink

Definition at line 31 of file lts_probabilistic_equivalence.h.

◆ lts_probabilistic_preorder

enum mcrl2::lts::lts_probabilistic_preorder

LTS preorder relations.

This enumerated type defines equivalence relations on LTSs. They can be used to reduce an LTS or decide whether two LTSs are equivalent.

Enumerator
lts_probabilistic_pre_none	Unknown or no preorder

Definition at line 136 of file lts_probabilistic_equivalence.h.

◆ lts_type

enum mcrl2::lts::lts_type

The enumerated type lts_type contains an index for every type type of labelled transition system that is supported by the system.

Every type has an associated labelled transition format. E.g. for lts_lts the type of the lts is lts_lts_t. Similarly, lts_aut_t, etc. are available. Files in which the lts's are stored have the name file.lts, file.aut, etc.

Enumerator
lts_none	unknown or no format
lts_lts	mCRL2 SVC format
lts_aut	Aldébaran format (CADP)
lts_fsm	FSM format
lts_dot	GraphViz format
lts_lts_probabilistic
lts_aut_probabilistic
lts_fsm_probabilistic
lts_type_min
lts_type_max

Definition at line 36 of file lts_type.h.

◆ refinement_type

enum class mcrl2::lts::refinement_type

strong

Enumerator
trace
failures
failures_divergence

Definition at line 191 of file liblts_failures_refinement.h.

◆ transition_sort_style

enum mcrl2::lts::transition_sort_style

Transition sort styles.

This enumerated type defines sort styles for transitions. They can be used to sort the transitions of an LTS based on various criteria.

Enumerator
src_lbl_tgt	Sort first on source state, then on label, then on target state
lbl_tgt_src	Sort first on label, then on target state, then on source state
tgt_lbl_src	Sort first on target state, then on label, then on source state
tgt_src_lbl	Sort first on target state, then on the source state, and finally on label
tgt_lbl	Sort first on target state, then on label
target	Sort on target only

Definition at line 33 of file transition.h.

Function Documentation

◆ compare() [1/2]

template<class LTS_TYPE >

bool mcrl2::lts::compare	(	const LTS_TYPE &	l1,
		const LTS_TYPE &	l2,
		const lts_equivalence	eq,
		const bool	generate_counter_examples = `false`,
		const std::string &	counter_example_file = `""`,
		const bool	structured_output = `false`
	)

Checks whether this LTS is equivalent to another LTS.

The input labelled transition systems are duplicated in memory to carry out the comparison. When space efficiency is a concern, one can consider to use destructive_compare.

Parameters

[in]	l1	The first LTS to compare.
[in]	l2	The second LTS to compare.
[in]	eq	The equivalence with respect to which the LTSs will be compared.
[in]	generate_counter_examples	Whether to generate a counter example
[in]	counter_example_file	The file to store the counter example in

Return values

true	if the LTSs are found to be equivalent.
false	otherwise.

Definition at line 850 of file lts_algorithm.h.

◆ compare() [2/2]

template<class LTS_TYPE >

bool mcrl2::lts::compare	(	const LTS_TYPE &	l1,
		const LTS_TYPE &	l2,
		const lts_preorder	pre,
		const bool	generate_counter_example,
		const std::string &	counter_example_file = `""`,
		const bool	structured_output = `false`,
		const lps::exploration_strategy	strategy = `lps::es_breadth`,
		const bool	preprocess = `true`
	)

Checks whether this LTS is smaller than another LTS according to a preorder.

Parameters

[in]	l1	The first LTS to be compared.
[in]	l2	The second LTS to be compared.
[in]	pre	The preorder with respect to which the LTSs will be compared.
[in]	generate_counter_examples	Whether to generate a counter example
[in]	counter_example_file	The file to store the counter example in
[in]	strategy	Choose breadth-first or depth-first for exploration strategy of the antichain algorithms.
[in]	preprocess	Whether to allow preprocessing of the given LTSs.

Return values

true	if this LTS is smaller than LTS l according to preorder pre.
false	otherwise.

Definition at line 865 of file lts_algorithm.h.

◆ create_lts_builder()

std::unique_ptr< lts_builder > mcrl2::lts::create_lts_builder	(	const lps::specification &	lpsspec,
		const lps::explorer_options &	options,
		lts_type	output_format,
		const std::string &	output_filename = `""`
	)

inline

Definition at line 332 of file lts_builder.h.

◆ create_stochastic_lts_builder()

std::unique_ptr< stochastic_lts_builder > mcrl2::lts::create_stochastic_lts_builder	(	const lps::stochastic_specification &	lpsspec,
		const lps::explorer_options &	options,
		lts_type	output_format
	)

inline

Definition at line 308 of file stochastic_lts_builder.h.

◆ description() [1/4]

std::string mcrl2::lts::description ( const lts_equivalence eq )

inline

Gives a description of an equivalence.

Parameters

[in] eq The equivalence type.

Returns: A string describing the equivalence specified by eq.

Definition at line 313 of file lts_equivalence.h.

◆ description() [2/4]

std::string mcrl2::lts::description ( const lts_preorder pre )

inline

Gives a description of a preorder.

Parameters

[in] pre The preorder type.

Returns: A string describing the preorder specified by eq.

Definition at line 169 of file lts_preorder.h.

◆ description() [3/4]

std::string mcrl2::lts::description ( const lts_probabilistic_equivalence & eq )

inline

Gives a description of an equivalence.

Parameters

[in] eq The equivalence type.

Returns: A string describing the equivalence specified by eq.

Definition at line 116 of file lts_probabilistic_equivalence.h.

◆ description() [4/4]

std::string mcrl2::lts::description ( const lts_probabilistic_preorder & pre )

inline

Gives a description of an preorder.

Parameters

[in] pre The preorder type.

Returns: A string describing the preorder specified by pre.

Definition at line 206 of file lts_probabilistic_equivalence.h.

◆ destructive_compare() [1/2]

template<class LTS_TYPE >

bool mcrl2::lts::destructive_compare	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		const lts_equivalence	eq,
		const bool	generate_counter_examples = `false`,
		const std::string &	counter_example_file = `std::string()`,
		const bool	structured_output = `false`
	)

Checks whether this LTS is equivalent to another LTS.

Parameters

[in]	l1	The first LTS that will be compared.
[in]	l2	The second LTS that will be compared.
[in]	eq	The equivalence with respect to which the LTSs will be compared.
[in]	generate_counter_examples	Whether to generate a counter example
[in]	counter_example_file	The file to store the counter example in

Return values

true	if the LTSs are found to be equivalent.
false	otherwise.

Warning: This function alters the internal data structure of both LTSs for efficiency reasons. After comparison, this LTS is equivalent to the original LTS by equivalence eq, and similarly for the LTS l.

Definition at line 69 of file lts_algorithm.h.

◆ destructive_compare() [2/2]

template<class LTS_TYPE >

bool mcrl2::lts::destructive_compare	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		const lts_preorder	pre,
		const bool	generate_counter_example,
		const std::string &	counter_example_file = `""`,
		const bool	structured_output = `false`,
		const lps::exploration_strategy	strategy = `lps::es_breadth`,
		const bool	preprocess = `true`
	)

Checks whether this LTS is smaller than another LTS according to a preorder.

Parameters

[in]	l1	The first LTS to be compared.
[in]	l2	The second LTS to be compared.
[in]	pre	The preorder with respect to which the LTSs will be compared.
[in]	generate_counter_examples	Whether to generate a counter example
[in]	counter_example_file	The file to store the counter example in
[in]	strategy	Choose breadth-first or depth-first for exploration strategy of the antichain algorithms.
[in]	preprocess	Whether to allow preprocessing of the given LTSs.

Return values

true	if LTS l1 is smaller than LTS l2 according to preorder pre.
false	otherwise.

Warning: This function alters the internal data structure of both LTSs for efficiency reasons. After comparison, this LTS is equivalent to the original LTS by equivalence eq, and similarly for the LTS l, where eq is the equivalence induced by the preorder pre (i.e. $eq = pre \cap pre^{-1}$ ).

Definition at line 873 of file lts_algorithm.h.

◆ destructive_refinement_checker()

template<class LTS_TYPE , class COUNTER_EXAMPLE_CONSTRUCTOR = detail::dummy_counter_example_constructor>

bool mcrl2::lts::destructive_refinement_checker	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		const refinement_type	refinement,
		const bool	weak_reduction,
		const lps::exploration_strategy	strategy,
		const bool	preprocess = `true`,
		COUNTER_EXAMPLE_CONSTRUCTOR	generate_counter_example = `detail::dummy_counter_example_constructor()`
	)

This function checks using algorithms in the paper mentioned above whether transition system l1 is included in transition system l2, in the sense of trace inclusions, failures inclusion and divergence failures inclusion.

Parameters

weak_reduction	Remove inert tau loops.
strategy	Choose between breadth and depth first.
preprocess	Uses (divergence preserving) branching bisimulation and tau scc reduction to reduce the input LTSs.
generate_counter_example	If set, a labelled transition system is generated that can act as a counterexample. It consists of a trace, followed by outgoing transitions representing a refusal set.

Definition at line 260 of file liblts_failures_refinement.h.

◆ determinise()

template<class LTS_TYPE >

void mcrl2::lts::determinise ( LTS_TYPE & l )

Determinises this LTS.

Definition at line 1067 of file lts_algorithm.h.

◆ first_state() [1/2]

const lps::state & mcrl2::lts::first_state ( const lps::state & s )

inline

Definition at line 28 of file state_space_generator.h.

◆ first_state() [2/2]

const lps::state & mcrl2::lts::first_state ( const lps::stochastic_state & s )

inline

Definition at line 34 of file state_space_generator.h.

◆ from()

std::size_t mcrl2::lts::from ( const outgoing_transitions_per_state_action_t::const_iterator & i )

inline

From state of an iterator exploring transitions per outgoing state and action.

Definition at line 617 of file lts_utilities.h.

◆ group_transitions_on_label() [1/2]

void mcrl2::lts::group_transitions_on_label	(	const std::vector< transition >::iterator	begin,
		const std::vector< transition >::iterator	end,
		std::function< std::size_t(const transition &)>	get_label,
		const std::size_t	tau_label_index,
		std::vector< std::pair< std::size_t, std::size_t > > &	count_sum_transitions_per_action,
		std::vector< std::size_t > &	todo_stack
	)

inline

Definition at line 93 of file lts_utilities.h.

◆ group_transitions_on_label() [2/2]

void mcrl2::lts::group_transitions_on_label	(	std::vector< transition > &	transitions,
		std::function< std::size_t(const transition &)>	get_label,
		const std::size_t	number_of_labels,
		const std::size_t	tau_label_index
	)

inline

Definition at line 195 of file lts_utilities.h.

◆ group_transitions_on_label_tgt()

void mcrl2::lts::group_transitions_on_label_tgt	(	std::vector< transition > &	transitions,
		const std::size_t	number_of_labels,
		const std::size_t	tau_label_index,
		const std::size_t	number_of_states
	)

inline

Definition at line 378 of file lts_utilities.h.

◆ is_deterministic()

template<class LTS_TYPE >

bool mcrl2::lts::is_deterministic ( const LTS_TYPE & l )

Checks whether this LTS is deterministic.

Return values

true	if this LTS is deterministic;
false	otherwise.

Definition at line 1000 of file lts_algorithm.h.

◆ label() [1/2]

std::size_t mcrl2::lts::label ( const outgoing_pair_t & p )

inline

Label of a pair of a label and target state.

Definition at line 598 of file lts_utilities.h.

◆ label() [2/2]

std::size_t mcrl2::lts::label ( const outgoing_transitions_per_state_action_t::const_iterator & i )

inline

Label of an iterator exploring transitions per outgoing state and action.

Definition at line 623 of file lts_utilities.h.

◆ load_lts()

template<class LTS_TYPE >

void mcrl2::lts::load_lts	(	LTS_TYPE &	result,
		const std::string &	infilename,
		lts_type	type,
		const data_file_type_t	extra_data_file_type = `none_e`,
		const std::string &	extra_data_file_name = `""`
	)

inline

Loads an lts of the indicated type, transforms it to an lts of the form lts_lts_t using the additional data parameters.

The file can refer to any file in lts, aut, fsm, or dot format. After reading it is is translated into .lts format. For this a file is read with the name extra_data_file, which is interpreted as a data specification if extra_data_file_type has type data_e, a linear process specification if it has value lps_e, and an mcrl2 file if it has value mcrl2_e.

Parameters

[out]	result	The lts in which the transition system is put.
[in]	infilename	The name of the file containing the lts.
[in]	type	The type of the lts file, i.e. .lts, .fsm, .dot or .aut.
[in]	extra_data_file_type	The type of the file containing extra information, such as a data specification.
[in]	extra_data_file_name	The name of the file containing extra information.

Definition at line 202 of file lts_io.h.

◆ load_lts_as_fsm_file()

void mcrl2::lts::load_lts_as_fsm_file	(	const std::string &	path,
		lts_fsm_t &	l
	)

inline

Read a labelled transition system and return it in fsm format.

The file can refer to any file in lts, aut, fsm, or dot format. After reading it is is attempted to translate it into fsm format.

Parameters

[in]	path	A string with the name of the file.
[out]	l	The lts in which the transition system is put.

Definition at line 253 of file lts_io.h.

◆ merge()

template<class LTS_TYPE >

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

Merge the second lts into the first lts.

Parameters

[in,out]	l1	The transition system in which l2 is merged.
[in]	l2	The second transition system, which remains unchanged

Definition at line 617 of file lts_algorithm.h.

◆ operator<<() [1/9]

atermpp::aterm_ostream & mcrl2::lts::operator<<	(	atermpp::aterm_ostream &	stream,
		const lts_lts_t &	lts
	)

Write a (probabilistic) LTS to the given stream at once.

Definition at line 439 of file liblts_lts.cpp.

◆ operator<<() [2/9]

atermpp::aterm_ostream & mcrl2::lts::operator<<	(	atermpp::aterm_ostream &	stream,
		const probabilistic_lts_lts_t &	lts
	)

Definition at line 445 of file liblts_lts.cpp.

◆ operator<<() [3/9]

atermpp::aterm_ostream & mcrl2::lts::operator<<	(	atermpp::aterm_ostream &	stream,
		const probabilistic_lts_lts_t::probabilistic_state_t &	state
	)

Converts a probabilistic state into an aterm that encodes it.

Definition at line 23 of file liblts_lts.cpp.

◆ operator<<() [4/9]

std::ostream & mcrl2::lts::operator<<	(	std::ostream &	os,
		const lts_equivalence	eq
	)

inline

Definition at line 303 of file lts_equivalence.h.

◆ operator<<() [5/9]

std::ostream & mcrl2::lts::operator<<	(	std::ostream &	os,
		const lts_preorder	pre
	)

inline

Definition at line 158 of file lts_preorder.h.

◆ operator<<() [6/9]

std::ostream & mcrl2::lts::operator<<	(	std::ostream &	os,
		const lts_probabilistic_equivalence &	eq
	)

inline

Definition at line 106 of file lts_probabilistic_equivalence.h.

◆ operator<<() [7/9]

std::ostream & mcrl2::lts::operator<<	(	std::ostream &	os,
		const lts_probabilistic_preorder &	pre
	)

inline

Definition at line 196 of file lts_probabilistic_equivalence.h.

◆ operator<<() [8/9]

std::ostream & mcrl2::lts::operator<<	(	std::ostream &	out,
		const lps::state &	s
	)

inline

Definition at line 22 of file state_space_generator.h.

◆ operator<<() [9/9]

template<class STATE , class PROBABILITY >

std::ostream & mcrl2::lts::operator<<	(	std::ostream &	out,
		const probabilistic_state< STATE, PROBABILITY > &	l
	)

inline

Pretty print to an outstream.

Definition at line 356 of file probabilistic_state.h.

◆ operator>>() [1/7]

atermpp::aterm_istream & mcrl2::lts::operator>>	(	atermpp::aterm_istream &	stream,
		lts_lts_t &	lts
	)

Read a (probabilistic) LTS from the given stream.

Definition at line 427 of file liblts_lts.cpp.

◆ operator>>() [2/7]

atermpp::aterm_istream & mcrl2::lts::operator>>	(	atermpp::aterm_istream &	stream,
		probabilistic_lts_lts_t &	lts
	)

Definition at line 433 of file liblts_lts.cpp.

◆ operator>>() [3/7]

atermpp::aterm_istream & mcrl2::lts::operator>>	(	atermpp::aterm_istream &	stream,
		probabilistic_lts_lts_t::probabilistic_state_t &	state
	)

Definition at line 53 of file liblts_lts.cpp.

◆ operator>>() [4/7]

std::istream & mcrl2::lts::operator>>	(	std::istream &	is,
		lts_equivalence &	eq
	)

inline

Definition at line 216 of file lts_equivalence.h.

◆ operator>>() [5/7]

std::istream & mcrl2::lts::operator>>	(	std::istream &	is,
		lts_preorder &	eq
	)

inline

Definition at line 107 of file lts_preorder.h.

◆ operator>>() [6/7]

std::istream & mcrl2::lts::operator>>	(	std::istream &	is,
		lts_probabilistic_equivalence &	eq
	)

inline

Definition at line 69 of file lts_probabilistic_equivalence.h.

◆ operator>>() [7/7]

std::istream & mcrl2::lts::operator>>	(	std::istream &	is,
		lts_probabilistic_preorder &	eq
	)

inline

Definition at line 163 of file lts_probabilistic_equivalence.h.

◆ parse_equivalence()

lts_equivalence mcrl2::lts::parse_equivalence ( std::string const & s )

inline

Determines the equivalence from a string.

The following strings may be used:

"none" for identity equivalence;
"bisim" for strong bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
"bisim-gv" for strong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
"bisim-sig" for strong bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
"branching-bisim" for branching bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
"branching-bisim-gv" for branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
"branching-bisim-sig" for branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
"dpbranching-bisim" for divergence-preserving branching bisimilarity using the O(m log n) algorithm [Groote/Jansen/Keiren/Wijs 2017];
"dpbranching-bisim-gv" for divergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990];
"dpbranching-bisim-sig" for divergence-preserving branching bisimilarity using the signature refinement algorithm [Blom/Orzan 2003];
"weak-bisim" for weak bisimilarity;
"dpweak-bisim" for divergence-preserving weak bisimilarity;
"sim" for strong simulation equivalence;
"trace" for strong trace equivalence;
"weak-trace" for weak trace equivalence;
"determinisation" for a determinisation reduction.

Parameters

[in] s The string specifying the equivalence.

Returns: The equivalence type specified by s. If s is none of the above values then lts_eq_none is returned.

Definition at line 100 of file lts_equivalence.h.

◆ parse_fsm_specification() [1/2]

void mcrl2::lts::parse_fsm_specification	(	const std::string &	text,
		probabilistic_lts_fsm_t &	result
	)

inline

Definition at line 176 of file parse.h.

◆ parse_fsm_specification() [2/2]

void mcrl2::lts::parse_fsm_specification	(	std::istream &	from,
		probabilistic_lts_fsm_t &	result
	)

inline

Definition at line 169 of file parse.h.

◆ parse_lts_action()

action_label_lts mcrl2::lts::parse_lts_action	(	const std::string &	multi_action_string,
		const data::data_specification &	data_spec,
		lps::multi_action_type_checker &	typechecker
	)

inline

Parse a string into an action label.

The string is typechecked against the data specification and list of declared actions. If parsing or type checking fails, an mcrl2::runtime_error is thrown.

Parameters

[in]	multi_action_string	The string to be parsed.
[in]	data_spec	The data specification used for parsing.
[in]	act_decls	Action declarations.

Returns: The parsed and type checked multi action.

Definition at line 208 of file lts_lts.h.

◆ parse_preorder()

lts_preorder mcrl2::lts::parse_preorder ( std::string const & s )

inline

Determines the preorder from a string.

The following strings may be used:

"sim" for strong simulation preorder;
"trace" for strong trace preorder;
"weak-trace" for weak trace preorder.

Parameters

[in] s The string specifying the preorder.

Returns: The preorder type specified by s. If s is none of the above values then lts_pre_none is returned.

Definition at line 57 of file lts_preorder.h.

◆ parse_probabilistic_equivalence()

lts_probabilistic_equivalence mcrl2::lts::parse_probabilistic_equivalence ( const std::string & s )

inline

Determines the equivalence from a string.

The following strings may be used:

"none" for identity equivalence;
"pbisim" for Probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm [Bier];

Parameters

[in] s The string specifying the equivalence.

Returns: The equivalence type specified by s. If s is none of the above values then lts_probabilistic_eq_none is returned.

Definition at line 47 of file lts_probabilistic_equivalence.h.

◆ parse_probabilistic_preorder()

lts_probabilistic_preorder mcrl2::lts::parse_probabilistic_preorder ( std::string const & s )

inline

Determines the probabilistic preorder from a string.

The following strings may be used:

"none" for identity preorder;

Parameters

[in] s The string specifying the equivalence.

Returns: The equivalence type specified by s. If s is none of the above values then lts_probabilistic_pre_none is returned.

Definition at line 149 of file lts_probabilistic_equivalence.h.

◆ pp() [1/7]

std::string mcrl2::lts::pp ( const action_label_lts & l )

inline

Print the action label to string.

Definition at line 195 of file lts_lts.h.

◆ pp() [2/7]

std::string mcrl2::lts::pp ( const action_label_string & l )

inline

Definition at line 193 of file action_label_string.h.

◆ pp() [3/7]

template<class STATE , class PROBABILITY >

std::string mcrl2::lts::pp ( const probabilistic_state< STATE, PROBABILITY > & l )

inline

Definition at line 323 of file probabilistic_state.h.

◆ pp() [4/7]

std::string mcrl2::lts::pp ( const state_label_dot & l )

inline

Pretty print function for a state_label_dot. Only prints the label field.

Definition at line 101 of file lts_dot.h.

◆ pp() [5/7]

std::string mcrl2::lts::pp ( const state_label_empty & )

inline

Definition at line 57 of file state_label_empty.h.

◆ pp() [6/7]

std::string mcrl2::lts::pp ( const state_label_fsm & label )

inline

Pretty print an fsm state label.

Definition at line 71 of file lts_fsm.h.

◆ pp() [7/7]

std::string mcrl2::lts::pp ( const state_label_lts & label )

inline

Pretty print a state value of this LTS.

The label is printed as (t1,...,tn) if it consists of a single label. Otherwise the labels are printed with square brackets surrounding it.

Parameters

[in] label The state value to pretty print.

Returns: The pretty-printed representation of value.

Definition at line 101 of file lts_lts.h.

◆ print_equivalence()

std::string mcrl2::lts::print_equivalence ( const lts_equivalence eq )

inline

Gives the short name of an equivalence.

Parameters

[in] eq The equivalence type.

Returns: A short string representing the equivalence specified by eq. The returned value is one of the strings listed for parse_equivalence.

Definition at line 236 of file lts_equivalence.h.

◆ print_preorder()

std::string mcrl2::lts::print_preorder ( const lts_preorder pre )

inline

Gives the short name of a preorder.

Parameters

[in] pre The preorder type.

Returns: A short string representing the preorder specified by pre. The returned value is one of the strings listed for parse_preorder.

Definition at line 128 of file lts_preorder.h.

◆ print_probabilistic_equivalence()

std::string mcrl2::lts::print_probabilistic_equivalence ( const lts_probabilistic_equivalence & eq )

inline

Gives the short name of an equivalence.

Parameters

[in] eq The equivalence type.

Returns: A short string representing the equivalence specified by eq. The returned value is one of the strings listed for parse_equivalence.

Definition at line 89 of file lts_probabilistic_equivalence.h.

◆ print_probabilistic_preorder()

std::string mcrl2::lts::print_probabilistic_preorder ( const lts_probabilistic_preorder & pre )

inline

Gives the short name of an preorder.

Parameters

[in] pre The preorder type.

Returns: A short string representing the preorder specified by pre. The returned value is one of the strings listed for parse_preorder.

Definition at line 183 of file lts_probabilistic_equivalence.h.

◆ ptr()

std::string mcrl2::lts::ptr ( const transition t )

inline

Sorts the transitions on labels. Action with the tau label are put first.

This function is linear in time, but it uses that the labels have a limited range, i.e., it is also linear in time and space in the largest used index of a label. This function does not employ the hidden label set.

Parameters

[in/out] transitions A vector of transitions to be sorted.

Definition at line 88 of file lts_utilities.h.

◆ reachability_check() [1/2]

template<class SL , class AL , class BASE >

bool mcrl2::lts::reachability_check	(	lts< SL, AL, BASE > &	l,
		bool	remove_unreachable = `false`
	)

Checks whether all states in this LTS are reachable from the initial state and remove unreachable states if required.

Runs in O(num_states * num_transitions) time.

Parameters

[in]	l	The LTS on which reachability is checked.
[in]	remove_unreachable	Indicates whether all unreachable states should be removed from the LTS. This option does not influence the return value; the return value is with respect to the original LTS.

Return values

true	if all states are reachable from the initial state;
false	otherwise.

Definition at line 341 of file lts_algorithm.h.

◆ reachability_check() [2/2]

template<class SL , class AL , class PROBABILISTIC_STATE , class BASE >

bool mcrl2::lts::reachability_check	(	probabilistic_lts< SL, AL, PROBABILISTIC_STATE, BASE > &	l,
		bool	remove_unreachable = `false`
	)

Checks whether all states in a probabilistic LTS are reachable from the initial state and remove unreachable states if required.

Runs in O(num_states * num_transitions) time.

Parameters

[in]	l	The LTS on which reachability is checked.
[in]	remove_unreachable	Indicates whether all unreachable states should be removed from the LTS. This option does not influence the return value; the return value is with respect to the original LTS.

Return values

true	if all states are reachable from the initial state;
false	otherwise.

Definition at line 450 of file lts_algorithm.h.

◆ reduce() [1/2]

template<class LTS_TYPE >

void mcrl2::lts::reduce	(	LTS_TYPE &	l,
		lts_equivalence	eq
	)

Applies a reduction algorithm to this LTS.

Parameters

[in]	l	A labelled transition system that must be reduced.
[in]	eq	The equivalence with respect to which the LTS will be reduced.

Definition at line 629 of file lts_algorithm.h.

◆ reduce() [2/2]

template<typename LTS_TYPE >

std::pair< std::size_t, bool > mcrl2::lts::reduce	(	LTS_TYPE &	lts,
		const bool	weak_reduction,
		const bool	preserve_divergence,
		std::size_t	l2_init
	)

Preprocess the LTS for destructive refinement checking.

Parameters

lts	The lts to preprocess.
init	The initial state of the right LTS that was merged.

Returns: A pair where the first element is the state number of init in the reduced lts and the second value indicate whether this state in equal to lts.initial_state.

Definition at line 226 of file liblts_failures_refinement.h.

◆ remove_time_stamp()

lps::state mcrl2::lts::remove_time_stamp ( const lps::state & s )

inline

Removes the last element from state s.

Definition at line 25 of file lts_builder.h.

◆ report_statistics()

template<typename T >

void mcrl2::lts::report_statistics ( refinement_statistics< T > & stats )

Print a message to debugging containing information about the given statistics.

Definition at line 211 of file liblts_failures_refinement.h.

◆ scc_reduce()

template<class LTS_TYPE >

void mcrl2::lts::scc_reduce	(	LTS_TYPE &	l,
		const bool	preserve_divergence_loops = `false`
	)

Definition at line 362 of file liblts_scc.h.

◆ sort_transitions() [1/2]

void mcrl2::lts::sort_transitions	(	std::vector< transition > &	transitions,
		const std::set< transition::size_type > &	hidden_label_set,
		transition_sort_style	ts = `src_lbl_tgt`
	)

inline

Sorts the transitions using a sort style.

Parameters

	[in/out]	transitions A vector of transitions to be sorted.
[in]	hidden_label_set	A set that tells which actions are to be interpreted as being hidden. Sorting takes place after mapping hidden actions to zero.
[in]	ts	The sort style to use.

Definition at line 36 of file lts_utilities.h.

◆ sort_transitions() [2/2]

void mcrl2::lts::sort_transitions	(	std::vector< transition > &	transitions,
		transition_sort_style	ts = `src_lbl_tgt`
	)

inline

Sorts the transitions using a sort style.

Parameters

	[in/out]	transitions A vector of transitions to be sorted.
[in]	ts	The sort style to use.

Definition at line 485 of file lts_utilities.h.

◆ to() [1/2]

std::size_t mcrl2::lts::to ( const outgoing_pair_t & p )

inline

Target state of a label state pair.

Definition at line 604 of file lts_utilities.h.

◆ to() [2/2]

std::size_t mcrl2::lts::to ( const outgoing_transitions_per_state_action_t::const_iterator & i )

inline

To state of an iterator exploring transitions per outgoing state and action.

Definition at line 629 of file lts_utilities.h.

◆ transform_lts2lps() [1/3]

lps::specification mcrl2::lts::transform_lts2lps	(	const lts_aut_t &	l1,
		const data_specification &	data,
		const process::action_label_list &	action_labels,
		const variable_list &	process_parameters
	)

transform an lts in aut format into a linear process.

Parameters

l1	A labelled transition system in aut format.
data	A separate data specification.
action_labels	A list containing the action labels used in the lts.
process_parameters	The process parameters of the current process.

Returns: The function returns a linear process with the same behaviour as the lts.

Definition at line 73 of file lts2lps.h.

◆ transform_lts2lps() [2/3]

lps::specification mcrl2::lts::transform_lts2lps	(	const lts_fsm_t &	l1,
		const data_specification &	data,
		const process::action_label_list &	action_labels,
		const variable_list &	process_parameters
	)

transform an lts in fsm format into a linear process.

Parameters

l1	A labelled transition system in fsm format.
data	A separate data specification.
action_labels	A list containing the action labels used in the lts.
process_parameters	The process parameters of the current process. XXXXX Is this needed????

Returns: The function returns a linear process with the same behaviour as the lts.

Definition at line 90 of file lts2lps.h.

◆ transform_lts2lps() [3/3]

lps::specification mcrl2::lts::transform_lts2lps ( const lts_lts_t & l )

transform an lts in lts format into a linear process.

Parameters

l	A labelled transition system in lts format.

Returns: The function returns a linear process with the same behaviour as the lts.

Definition at line 32 of file lts2lps.h.

◆ transitions_per_outgoing_state_action_pair() [1/2]

outgoing_transitions_per_state_action_t mcrl2::lts::transitions_per_outgoing_state_action_pair ( const std::vector< transition > & trans )

inline

Provide the transitions as a multimap accessible per from state and label.

Definition at line 635 of file lts_utilities.h.

◆ transitions_per_outgoing_state_action_pair() [2/2]

outgoing_transitions_per_state_action_t mcrl2::lts::transitions_per_outgoing_state_action_pair	(	const std::vector< transition > &	trans,
		const std::set< transition::size_type > &	hide_label_set
	)

inline

Provide the transitions as a multimap accessible per from state and label.

Definition at line 647 of file lts_utilities.h.

◆ transitions_per_outgoing_state_action_pair_reversed() [1/2]

outgoing_transitions_per_state_action_t mcrl2::lts::transitions_per_outgoing_state_action_pair_reversed ( const std::vector< transition > & trans )

inline

Provide the transitions as a multimap accessible per from state and label, ordered backwardly.

Definition at line 661 of file lts_utilities.h.

◆ transitions_per_outgoing_state_action_pair_reversed() [2/2]

outgoing_transitions_per_state_action_t mcrl2::lts::transitions_per_outgoing_state_action_pair_reversed	(	const std::vector< transition > &	trans,
		const std::set< transition::size_type > &	hide_label_set
	)

inline

Provide the transitions as a multimap accessible per from state and label, ordered backwardly.

Definition at line 673 of file lts_utilities.h.

◆ write_initial_state()

void mcrl2::lts::write_initial_state	(	atermpp::aterm_ostream &	stream,
		std::size_t	index
	)

Write the initial state to the LTS stream.

Definition at line 496 of file liblts_lts.cpp.

◆ write_lts_header()

void mcrl2::lts::write_lts_header	(	atermpp::aterm_ostream &	stream,
		const data::data_specification &	data,
		const data::variable_list &	parameters,
		const process::action_label_list &	action_labels
	)

Writes the start of an LTS stream.

Definition at line 451 of file liblts_lts.cpp.

◆ write_state_label()

void mcrl2::lts::write_state_label	(	atermpp::aterm_ostream &	stream,
		const state_label_lts &	label
	)

Write a state label to the LTS stream.

Definition at line 490 of file liblts_lts.cpp.

◆ write_transition() [1/2]

void mcrl2::lts::write_transition	(	atermpp::aterm_ostream &	stream,
		std::size_t	from,
		const lps::multi_action &	label,
		const probabilistic_lts_lts_t::probabilistic_state_t &	to
	)

Definition at line 474 of file liblts_lts.cpp.

◆ write_transition() [2/2]

void mcrl2::lts::write_transition	(	atermpp::aterm_ostream &	stream,
		std::size_t	from,
		const lps::multi_action &	label,
		std::size_t	to
	)

Write a transition to the LTS stream.

Definition at line 466 of file liblts_lts.cpp.

Variable Documentation

◆ const_tau_label_index

const std::size_t mcrl2::lts::const_tau_label_index =0

static

Definition at line 27 of file transition.h.

Namespaces

Classes

Typedefs

Enumerations

Functions

Variables

Detailed Description

Typedef Documentation

◆ outgoing_pair_t

◆ outgoing_transitions_per_state_action_t

◆ outgoing_transitions_per_state_t

◆ signature_t

Enumeration Type Documentation

◆ data_file_type_t

◆ lts_equivalence

◆ lts_preorder

◆ lts_probabilistic_equivalence

◆ lts_probabilistic_preorder

◆ lts_type

◆ refinement_type

◆ transition_sort_style

Function Documentation

◆ compare() [1/2]

◆ compare() [2/2]

◆ create_lts_builder()

◆ create_stochastic_lts_builder()

◆ description() [1/4]

◆ description() [2/4]

◆ description() [3/4]

◆ description() [4/4]

◆ destructive_compare() [1/2]

◆ destructive_compare() [2/2]

◆ destructive_refinement_checker()

◆ determinise()

◆ first_state() [1/2]

◆ first_state() [2/2]

◆ from()

◆ group_transitions_on_label() [1/2]

◆ group_transitions_on_label() [2/2]

◆ group_transitions_on_label_tgt()

◆ is_deterministic()

◆ label() [1/2]

◆ label() [2/2]

◆ load_lts()

◆ load_lts_as_fsm_file()

◆ merge()

◆ operator<<() [1/9]

◆ operator<<() [2/9]

◆ operator<<() [3/9]

◆ operator<<() [4/9]

◆ operator<<() [5/9]

◆ operator<<() [6/9]

◆ operator<<() [7/9]

◆ operator<<() [8/9]

◆ operator<<() [9/9]

◆ operator>>() [1/7]

◆ operator>>() [2/7]

◆ operator>>() [3/7]

◆ operator>>() [4/7]

◆ operator>>() [5/7]

◆ operator>>() [6/7]

◆ operator>>() [7/7]

◆ parse_equivalence()

◆ parse_fsm_specification() [1/2]

◆ parse_fsm_specification() [2/2]

◆ parse_lts_action()

◆ parse_preorder()

◆ parse_probabilistic_equivalence()

◆ parse_probabilistic_preorder()

◆ pp() [1/7]

◆ pp() [2/7]

◆ pp() [3/7]

◆ pp() [4/7]

◆ pp() [5/7]

◆ pp() [6/7]

◆ pp() [7/7]

◆ print_equivalence()

◆ print_preorder()

◆ print_probabilistic_equivalence()

◆ print_probabilistic_preorder()