mcrl2::lps::detail::Confluence_Checker

Include file:

#include "mcrl2/lps/confluence_checker.h

class mcrl2::lps::detail::Confluence_Checker

Private types

type mcrl2::lps::detail::Confluence_Checker::action_summand_type

typedef for process_type::action_summand_type

type mcrl2::lps::detail::Confluence_Checker::action_summand_vector_type

typedef for std::vector< action_summand_type >

type mcrl2::lps::detail::Confluence_Checker::process_type

typedef for Specification::process_type

Private attributes

data::detail::BDD2Dot mcrl2::lps::detail::Confluence_Checker::f_bdd2dot

Class that prints BDDs in dot format.

data::detail::BDD_Prover mcrl2::lps::detail::Confluence_Checker::f_bdd_prover

BDD based prover.

bool mcrl2::lps::detail::Confluence_Checker::f_check_all

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 whena summand is encountered that is not confluent with the tau summand at hand.

std::string mcrl2::lps::detail::Confluence_Checker::f_conditions

Confluence types for which the tool should check.

bool mcrl2::lps::detail::Confluence_Checker::f_counter_example

Flag indicating whether or not counter examples are printed.

Disjointness_Checker mcrl2::lps::detail::Confluence_Checker::f_disjointness_checker

Class that can check if two summands are disjoint.

std::string mcrl2::lps::detail::Confluence_Checker::f_dot_file_name

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

bool mcrl2::lps::detail::Confluence_Checker::f_generate_invariants

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.

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

An integer array, storing intermediate results per summand.

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

Class that checks if an invariant holds for an LPS.

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

A linear process specification.

bool mcrl2::lps::detail::Confluence_Checker::f_no_sums

Do not rewrite summands with sum operators.

std::size_t mcrl2::lps::detail::Confluence_Checker::f_number_of_summands

The number of summands of the current LPS.

data::set_identifier_generator mcrl2::lps::detail::Confluence_Checker::f_set_identifier_generator

Identifier generator to allow variables to be uniquely renamed.

Private member functions

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.

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 print_counter_example()

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

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 uniquely_rename_summutation_variables(action_summand_type &summand)

Public member functions

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.

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