confluence_checker.h File Reference

Go to the source code of this file.

Classes
class	mcrl2::lps::detail::Confluence_Checker< Specification >

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::lps
	The main namespace for the LPS library.
namespace	mcrl2::lps::detail

Functions
process::action_label	mcrl2::lps::detail::make_ctau_act_id ()
	Creates an identifier for the for the ctau action.
process::action	mcrl2::lps::detail::make_ctau_action ()
	Creates the ctau action.
static data::mutable_map_substitution	mcrl2::lps::detail::get_substitutions_from_assignments (const data::assignment_list &a_assignments)
static data::data_expression	mcrl2::lps::detail::get_subst_equation_from_assignments (const data::variable_list &a_variables, data::assignment_list a_assignments_1, data::assignment_list a_assignments_2, data::mutable_map_substitution<> &a_substitutions_1, data::mutable_map_substitution<> &a_substitutions_2)
static data::data_expression	mcrl2::lps::detail::get_equation_from_assignments (const data::variable_list &a_variables, data::assignment_list a_assignments_1, data::assignment_list a_assignments_2)
data::data_expression	mcrl2::lps::detail::get_subst_equation_from_actions (const process::action_list &a_actions, data::mutable_map_substitution<> &a_substitutions)
static data::assignment_list	mcrl2::lps::detail::get_full_assignment_list (data::assignment_list a_assignment_list, const data::variable_list &a_variables)
template<typename ActionSummand >
data::data_expression	mcrl2::lps::detail::get_confluence_condition (const data::data_expression &a_invariant, const ActionSummand &a_summand_1, const ActionSummand &a_summand_2, const data::variable_list &a_variables, const char condition_type)
template<typename Specification >
bool	mcrl2::lps::detail::has_ctau_action (const Specification &a_lps)