mcrl2/lps/confluence.h

Include file:

#include "mcrl2/lps/confluence.h"

add your file description here.

Classes

• mcrl2::lps::commutative_confluence_condition
• mcrl2::lps::confluence_checker
• mcrl2::lps::confluence_summand
• mcrl2::lps::square_confluence_condition
• mcrl2::lps::triangular_confluence_condition
• mcrl2::lps::trivial_confluence_condition

Functions

std::set<data::variable> mcrl2::lps::changed_variables(const action_summand &summand)

bool mcrl2::lps::disjoint(const confluence_summand &summand1, const confluence_summand &summand2)

Indicates whether or not two summands are disjoint.

bool mcrl2::lps::has_ctau_action(const Specification &lpsspec)

data::assignment_list mcrl2::lps::make_assignment_list(const data::variable_list &variables, const data::data_expression_list &expressions)

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.

std::string mcrl2::lps::print_confluence_summand(const confluence_summand &summand, const data::variable_list &process_parameters)

const stochastic_distribution &summand_distribution(const lps::stochastic_action_summand &summand)

const stochastic_distribution &summand_distribution(const Summand&)

std::set<data::variable> mcrl2::lps::used_read_variables(const action_summand &summand)

Functions

data::data_expression mcrl2::lps::detail::equal_to(const data::data_expression_list &x, const data::data_expression_list &y)

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::make_forall_(const data::data_expression &x)

std::pair<std::size_t, std::size_t> mcrl2::lps::detail::make_sorted_pair(std::size_t i, std::size_t j)