#include <confluence_checker.h>

Public Member Functions
	Confluence_Checker (Specification &a_lps, data::rewriter::strategy a_rewrite_strategy=data::jitty, int a_time_limit=0, bool a_path_eliminator=false, data::detail::smt_solver_type a_solver_type=data::detail::solver_type_cvc, bool a_apply_induction=false, bool a_check_all=false, bool a_no_sums=false, std::string a_conditions="c", bool a_counter_example=false, bool a_generate_invariants=false, std::string const &a_dot_file_name=std::string())
	Constructor that initializes Confluence_Checker::f_lps, Confluence_Checker::f_bdd_prover,.

void	check_confluence_and_mark (const data::data_expression &a_invariant, const std::size_t a_summand_number)
	Check the confluence of the LPS Confluence_Checker::f_lps. precondition: the argument passed as parameter a_invariant is an expression of sort Bool in internal mCRL2 format precondition: the argument passed as parameter a_summand_number corresponds with a summand of the LPS for which confluence must be checked (lowest summand has number 1). If this number is 0 confluence for all summands is checked.

Private Types
typedef Specification::process_type	process_type

typedef process_type::action_summand_type	action_summand_type

typedef std::vector< action_summand_type >	action_summand_vector_type

Private Member Functions
void	save_dot_file (std::size_t a_summand_number_1, std::size_t a_summand_number_2)
	Writes a dot file of the BDD created when checking the confluence of summands a_summand_number_1 and a_summand_number_2.

void	print_counter_example ()
	Outputs a path in the BDD corresponding to the condition at hand that leads to a node labelled false.

bool	check_summands (const data::data_expression &a_invariant, const action_summand_type a_summand_1, const std::size_t a_summand_number_1, const action_summand_type a_summand_2, const std::size_t a_summand_number_2, const char a_condition_type)
	Checks the confluence of summand a_summand_1 and a_summand_2.

void	check_confluence_and_mark_summand (action_summand_type &a_summand, const std::size_t a_summand_number, const data::data_expression &a_invariant, const char a_condition_type, bool &a_is_marked)
	Checks and updates the confluence of summand a_summand concerning all other tau-summands.

void	uniquely_rename_summutation_variables (action_summand_type &summand)

Private Attributes
Disjointness_Checker	f_disjointness_checker
	Class that can check if two summands are disjoint.

Invariant_Checker< Specification >	f_invariant_checker
	Class that checks if an invariant holds for an LPS.

data::detail::BDD_Prover	f_bdd_prover
	BDD based prover.

data::detail::BDD2Dot	f_bdd2dot
	Class that prints BDDs in dot format.

Specification &	f_lps
	A linear process specification.

bool	f_check_all
	Flag indicating whether or not the tau actions of confluent tau summands are renamed to ctau.

bool	f_no_sums
	Do not rewrite summands with sum operators.

std::string	f_conditions
	Confluence types for which the tool should check.

bool	f_counter_example
	Flag indicating whether or not counter examples are printed.

std::string	f_dot_file_name
	The prefix for the names of the files written in dot format.

bool	f_generate_invariants
	Flag indicating whether or not invariants are generated and checked each time a.

std::size_t	f_number_of_summands
	The number of summands of the current LPS.

std::vector< std::size_t >	f_intermediate
	An integer array, storing intermediate results per summand.

data::set_identifier_generator	f_set_identifier_generator
	Identifier generator to allow variables to be uniquely renamed.

Detailed Description

template<typename Specification>
class mcrl2::lps::detail::Confluence_Checker< Specification >

Definition at line 158 of file confluence_checker.h.

Member Typedef Documentation

◆ action_summand_type

template<typename Specification >

typedef process_type::action_summand_type mcrl2::lps::detail::Confluence_Checker< Specification >::action_summand_type

private

Definition at line 161 of file confluence_checker.h.

◆ action_summand_vector_type

template<typename Specification >

typedef std::vector<action_summand_type> mcrl2::lps::detail::Confluence_Checker< Specification >::action_summand_vector_type

private

Definition at line 162 of file confluence_checker.h.

◆ process_type

template<typename Specification >

typedef Specification::process_type mcrl2::lps::detail::Confluence_Checker< Specification >::process_type

private

Definition at line 160 of file confluence_checker.h.

Constructor & Destructor Documentation

◆ Confluence_Checker()

template<typename Specification >

mcrl2::lps::detail::Confluence_Checker< Specification >::Confluence_Checker	(	Specification &	a_lps,
		data::rewriter::strategy	a_rewrite_strategy = `data::jitty`,
		int	a_time_limit = `0`,
		bool	a_path_eliminator = `false`,
		data::detail::smt_solver_type	a_solver_type = `data::detail::solver_type_cvc`,
		bool	a_apply_induction = `false`,
		bool	a_check_all = `false`,
		bool	a_no_sums = `false`,
		std::string	a_conditions = `"c"`,
		bool	a_counter_example = `false`,
		bool	a_generate_invariants = `false`,
		std::string const &	a_dot_file_name = `std::string()`
	)

Constructor that initializes Confluence_Checker::f_lps, Confluence_Checker::f_bdd_prover,.

Confluence_Checker::f_generate_invariants and Confluence_Checker::f_dot_file_name. precondition: the argument passed as parameter a_lps is a valid mCRL2 LPS precondition: the argument passed as parameter a_time_limit is greater than or equal to 0. If the argument is equal to 0, no time limit will be enforced

Definition at line 833 of file confluence_checker.h.

Member Function Documentation

◆ check_confluence_and_mark()

template<typename Specification >

void mcrl2::lps::detail::Confluence_Checker< Specification >::check_confluence_and_mark	(	const data::data_expression &	a_invariant,
		const std::size_t	a_summand_number
	)

Check the confluence of the LPS Confluence_Checker::f_lps. precondition: the argument passed as parameter a_invariant is an expression of sort Bool in internal mCRL2 format precondition: the argument passed as parameter a_summand_number corresponds with a summand of the LPS for which confluence must be checked (lowest summand has number 1). If this number is 0 confluence for all summands is checked.

Definition at line 884 of file confluence_checker.h.

◆ check_confluence_and_mark_summand()

template<typename Specification >

void mcrl2::lps::detail::Confluence_Checker< Specification >::check_confluence_and_mark_summand	(	action_summand_type &	a_summand,
		const std::size_t	a_summand_number,
		const data::data_expression &	a_invariant,
		const char	a_condition_type,
		bool &	a_is_marked
	)

private

Checks and updates the confluence of summand a_summand concerning all other tau-summands.

Definition at line 747 of file confluence_checker.h.

◆ check_summands()

template<typename Specification >

bool mcrl2::lps::detail::Confluence_Checker< Specification >::check_summands	(	const data::data_expression &	a_invariant,
		const action_summand_type	a_summand_1,
		const std::size_t	a_summand_number_1,
		const action_summand_type	a_summand_2,
		const std::size_t	a_summand_number_2,
		const char	a_condition_type
	)

private

Checks the confluence of summand a_summand_1 and a_summand_2.

Definition at line 666 of file confluence_checker.h.

◆ print_counter_example()

template<typename Specification >

void mcrl2::lps::detail::Confluence_Checker< Specification >::print_counter_example

private

Outputs a path in the BDD corresponding to the condition at hand that leads to a node labelled false.

Definition at line 585 of file confluence_checker.h.

◆ save_dot_file()

template<typename Specification >

void mcrl2::lps::detail::Confluence_Checker< Specification >::save_dot_file	(	std::size_t	a_summand_number_1,
		std::size_t	a_summand_number_2
	)

private

Writes a dot file of the BDD created when checking the confluence of summands a_summand_number_1 and a_summand_number_2.

Definition at line 574 of file confluence_checker.h.

◆ uniquely_rename_summutation_variables()

template<typename Specification >

void mcrl2::lps::detail::Confluence_Checker< Specification >::uniquely_rename_summutation_variables ( action_summand_type & summand )

private

Definition at line 597 of file confluence_checker.h.

Member Data Documentation

◆ f_bdd2dot

template<typename Specification >

data::detail::BDD2Dot mcrl2::lps::detail::Confluence_Checker< Specification >::f_bdd2dot

private

Class that prints BDDs in dot format.

Definition at line 175 of file confluence_checker.h.

◆ f_bdd_prover

template<typename Specification >

data::detail::BDD_Prover mcrl2::lps::detail::Confluence_Checker< Specification >::f_bdd_prover

private

BDD based prover.

Definition at line 172 of file confluence_checker.h.

◆ f_check_all

template<typename Specification >

bool mcrl2::lps::detail::Confluence_Checker< Specification >::f_check_all

private

Flag indicating whether or not the tau actions of confluent tau summands are renamed to ctau.

Flag indicating whether or not the process of checking the confluence of a summand stops when

a summand is encountered that is not confluent with the tau summand at hand.

Definition at line 185 of file confluence_checker.h.

◆ f_conditions

template<typename Specification >

std::string mcrl2::lps::detail::Confluence_Checker< Specification >::f_conditions

private

Confluence types for which the tool should check.

Definition at line 191 of file confluence_checker.h.

◆ f_counter_example

template<typename Specification >

bool mcrl2::lps::detail::Confluence_Checker< Specification >::f_counter_example

private

Flag indicating whether or not counter examples are printed.

Definition at line 194 of file confluence_checker.h.

◆ f_disjointness_checker

template<typename Specification >

Disjointness_Checker mcrl2::lps::detail::Confluence_Checker< Specification >::f_disjointness_checker

private

Class that can check if two summands are disjoint.

Definition at line 166 of file confluence_checker.h.

◆ f_dot_file_name

template<typename Specification >

std::string mcrl2::lps::detail::Confluence_Checker< Specification >::f_dot_file_name

private

The prefix for the names of the files written in dot format.

Definition at line 197 of file confluence_checker.h.

◆ f_generate_invariants

template<typename Specification >

bool mcrl2::lps::detail::Confluence_Checker< Specification >::f_generate_invariants

private

Flag indicating whether or not invariants are generated and checked each time a.

summand is encountered that is not confluent with the tau summand at hand.

Definition at line 201 of file confluence_checker.h.

◆ f_intermediate

template<typename Specification >

std::vector<std::size_t> mcrl2::lps::detail::Confluence_Checker< Specification >::f_intermediate

private

An integer array, storing intermediate results per summand.

Definition at line 207 of file confluence_checker.h.

◆ f_invariant_checker

template<typename Specification >

Invariant_Checker<Specification> mcrl2::lps::detail::Confluence_Checker< Specification >::f_invariant_checker

private

Class that checks if an invariant holds for an LPS.

Definition at line 169 of file confluence_checker.h.

◆ f_lps

template<typename Specification >

Specification& mcrl2::lps::detail::Confluence_Checker< Specification >::f_lps

private

A linear process specification.

Definition at line 178 of file confluence_checker.h.

◆ f_no_sums

template<typename Specification >

bool mcrl2::lps::detail::Confluence_Checker< Specification >::f_no_sums

private

Do not rewrite summands with sum operators.

Definition at line 188 of file confluence_checker.h.

◆ f_number_of_summands

template<typename Specification >

std::size_t mcrl2::lps::detail::Confluence_Checker< Specification >::f_number_of_summands

private

The number of summands of the current LPS.

Definition at line 204 of file confluence_checker.h.

◆ f_set_identifier_generator

template<typename Specification >

data::set_identifier_generator mcrl2::lps::detail::Confluence_Checker< Specification >::f_set_identifier_generator

private

Identifier generator to allow variables to be uniquely renamed.

Definition at line 210 of file confluence_checker.h.

The documentation for this class was generated from the following file:

lps/include/mcrl2/lps/confluence_checker.h

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ action_summand_type

◆ action_summand_vector_type

◆ process_type

Constructor & Destructor Documentation

◆ Confluence_Checker()

Member Function Documentation

◆ check_confluence_and_mark()

◆ check_confluence_and_mark_summand()

◆ check_summands()

◆ print_counter_example()

◆ save_dot_file()

◆ uniquely_rename_summutation_variables()

Member Data Documentation

◆ f_bdd2dot

◆ f_bdd_prover

◆ f_check_all

◆ f_conditions

◆ f_counter_example

◆ f_disjointness_checker

◆ f_dot_file_name

◆ f_generate_invariants

◆ f_intermediate

◆ f_invariant_checker

◆ f_lps

◆ f_no_sums

◆ f_number_of_summands

◆ f_set_identifier_generator