confluence.h File Reference

add your file description here. More...

Go to the source code of this file.

Classes
struct	mcrl2::lps::confluence_summand
struct	mcrl2::lps::commutative_confluence_condition
	Function object that computes the condition for commutative confluence. More...
struct	mcrl2::lps::square_confluence_condition
	Function object that computes the condition for square confluence. More...
struct	mcrl2::lps::triangular_confluence_condition
	Function object that computes the condition for triangular confluence. More...
struct	mcrl2::lps::trivial_confluence_condition
	Function object that computes the condition for triangular confluence. More...
class	mcrl2::lps::confluence_checker

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
data::data_expression	mcrl2::lps::detail::make_and (const data::data_expression &x1, const data::data_expression &x2, const data::data_expression &x3)
data::data_expression	mcrl2::lps::detail::make_and (const data::data_expression &x1, const data::data_expression &x2, const data::data_expression &x3, const data::data_expression &x4)
data::data_expression	mcrl2::lps::detail::equal_to (const data::data_expression_list &x, const data::data_expression_list &y)
std::pair< std::size_t, std::size_t >	mcrl2::lps::detail::make_sorted_pair (std::size_t i, std::size_t j)
data::data_expression	mcrl2::lps::detail::make_forall_ (const data::data_expression &x)
template<typename Summand >
const stochastic_distribution &	mcrl2::lps::summand_distribution (const Summand &)
template<>
const stochastic_distribution &	mcrl2::lps::summand_distribution (const lps::stochastic_action_summand &summand)
std::set< data::variable >	mcrl2::lps::used_read_variables (const action_summand &summand)
std::set< data::variable >	mcrl2::lps::changed_variables (const action_summand &summand)
data::assignment_list	mcrl2::lps::make_assignment_list (const data::variable_list &variables, const data::data_expression_list &expressions)
std::string	mcrl2::lps::print_confluence_summand (const confluence_summand &summand, const data::variable_list &process_parameters)
bool	mcrl2::lps::disjoint (const confluence_summand &summand1, const confluence_summand &summand2)
	Indicates whether or not two summands are disjoint.
process::action_label	mcrl2::lps::make_ctau_act_id ()
	Creates an identifier for the ctau action.
process::action	mcrl2::lps::make_ctau_action ()
	Creates the ctau action.
template<typename Specification >
bool	mcrl2::lps::has_ctau_action (const Specification &lpsspec)

Detailed Description

add your file description here.

Definition in file confluence.h.