mcrl2/lps/confluence_checker.h¶

Include file:

#include "mcrl2/lps/confluence_checker.h"

Classes¶

mcrl2::lps::detail::Confluence_Checker

Functions¶

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)¶

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)¶

static data::assignment_list mcrl2::lps::detail::get_full_assignment_list(data::assignment_list a_assignment_list, const data::variable_list &a_variables)¶

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::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::mutable_map_substitution mcrl2::lps::detail::get_substitutions_from_assignments(const data::assignment_list &a_assignments)¶

bool mcrl2::lps::detail::has_ctau_action(const Specification &a_lps)¶

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.