liblts_tau_star_reduce.h File Reference

Go to the source code of this file.

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::lts
	The main LTS namespace.
namespace	mcrl2::lts::detail
	A base class for the lts_dot labelled transition system.

Enumerations
enum	mcrl2::lts::detail::t_reach { mcrl2::lts::detail::unknown , mcrl2::lts::detail::reached , mcrl2::lts::detail::explored }

Functions
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.
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)
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.
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)