mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | List of all members
mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data Class Reference

#include <partial_order_reduction.h>

Public Member Functions

 summand_relations_data (partial_order_reduction_algorithm &p, const std::size_t k, const std::size_t k1)
 
bool can_enable ()
 
tribool left_accords_data (bool affect_set, bool needs_yes)
 
tribool square_accords_data (bool affect_set, bool needs_yes)
 
tribool triangle_accords_data (bool affect_set, bool needs_yes)
 

Private Member Functions

data::data_expression make_exists_if_strong (const data::variable_list &vars, const data::data_expression &body)
 
data::data_expression left_accords_antecedent ()
 
data::data_expression left_accords_consequent ()
 
data::data_expression coenabled_antecedent ()
 
data::data_expression square_accords_consequent ()
 
data::data_expression triangle_accords_consequent_weak ()
 
data::data_expression triangle_accords_consequent ()
 
tribool accords_data (bool affect_set, bool needs_yes, const std::function< data::data_expression()> &make_antecedent, const std::function< data::data_expression()> &make_consequent)
 

Private Attributes

partial_order_reduction_algorithm & parent
 
bool compute_weak_conditions
 
data::set_identifier_generator id_gen
 
data::variable_list qvars1_k
 
data::data_expression condition1_k
 
data::data_expression_list updates1_k
 
data::variable_list qvars1_k1
 
data::data_expression condition1_k1
 
data::data_expression_list updates1_k1
 
data::variable_list qvars2_k
 
data::data_expression condition2_k
 
data::data_expression_list updates2_k
 
data::variable_list qvars2_k1
 
data::data_expression condition2_k1
 
data::data_expression_list updates2_k1
 
data::mutable_indexed_substitution sigma_k
 
data::mutable_indexed_substitution sigma_k1
 
data::variable_list combined_quantified_vars
 

Detailed Description

Definition at line 302 of file partial_order_reduction.h.

Constructor & Destructor Documentation

◆ summand_relations_data()

mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::summand_relations_data ( partial_order_reduction_algorithm &  p,
const std::size_t  k,
const std::size_t  k1 
)
inline

Definition at line 419 of file partial_order_reduction.h.

Member Function Documentation

◆ accords_data()

tribool mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::accords_data ( bool  affect_set,
bool  needs_yes,
const std::function< data::data_expression()> &  make_antecedent,
const std::function< data::data_expression()> &  make_consequent 
)
inlineprivate

Definition at line 390 of file partial_order_reduction.h.

◆ can_enable()

bool mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::can_enable ( )
inline

Definition at line 459 of file partial_order_reduction.h.

◆ coenabled_antecedent()

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::coenabled_antecedent ( )
inlineprivate

Definition at line 354 of file partial_order_reduction.h.

◆ left_accords_antecedent()

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::left_accords_antecedent ( )
inlineprivate

Definition at line 337 of file partial_order_reduction.h.

◆ left_accords_consequent()

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::left_accords_consequent ( )
inlineprivate

Definition at line 342 of file partial_order_reduction.h.

◆ left_accords_data()

tribool mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::left_accords_data ( bool  affect_set,
bool  needs_yes 
)
inline

Definition at line 477 of file partial_order_reduction.h.

◆ make_exists_if_strong()

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::make_exists_if_strong ( const data::variable_list &  vars,
const data::data_expression &  body 
)
inlineprivate

Definition at line 332 of file partial_order_reduction.h.

◆ square_accords_consequent()

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::square_accords_consequent ( )
inlineprivate

Definition at line 359 of file partial_order_reduction.h.

◆ square_accords_data()

tribool mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::square_accords_data ( bool  affect_set,
bool  needs_yes 
)
inline

Definition at line 484 of file partial_order_reduction.h.

◆ triangle_accords_consequent()

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::triangle_accords_consequent ( )
inlineprivate

Definition at line 380 of file partial_order_reduction.h.

◆ triangle_accords_consequent_weak()

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::triangle_accords_consequent_weak ( )
inlineprivate

Definition at line 371 of file partial_order_reduction.h.

◆ triangle_accords_data()

tribool mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::triangle_accords_data ( bool  affect_set,
bool  needs_yes 
)
inline

Definition at line 491 of file partial_order_reduction.h.

Member Data Documentation

◆ combined_quantified_vars

data::variable_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::combined_quantified_vars
private

Definition at line 328 of file partial_order_reduction.h.

◆ compute_weak_conditions

bool mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::compute_weak_conditions
private

Definition at line 306 of file partial_order_reduction.h.

◆ condition1_k

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::condition1_k
private

Definition at line 310 of file partial_order_reduction.h.

◆ condition1_k1

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::condition1_k1
private

Definition at line 314 of file partial_order_reduction.h.

◆ condition2_k

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::condition2_k
private

Definition at line 318 of file partial_order_reduction.h.

◆ condition2_k1

data::data_expression mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::condition2_k1
private

Definition at line 322 of file partial_order_reduction.h.

◆ id_gen

data::set_identifier_generator mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::id_gen
private

Definition at line 307 of file partial_order_reduction.h.

◆ parent

partial_order_reduction_algorithm& mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::parent
private

Definition at line 305 of file partial_order_reduction.h.

◆ qvars1_k

data::variable_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::qvars1_k
private

Definition at line 309 of file partial_order_reduction.h.

◆ qvars1_k1

data::variable_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::qvars1_k1
private

Definition at line 313 of file partial_order_reduction.h.

◆ qvars2_k

data::variable_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::qvars2_k
private

Definition at line 317 of file partial_order_reduction.h.

◆ qvars2_k1

data::variable_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::qvars2_k1
private

Definition at line 321 of file partial_order_reduction.h.

◆ sigma_k

data::mutable_indexed_substitution mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::sigma_k
private

Definition at line 325 of file partial_order_reduction.h.

◆ sigma_k1

data::mutable_indexed_substitution mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::sigma_k1
private

Definition at line 326 of file partial_order_reduction.h.

◆ updates1_k

data::data_expression_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::updates1_k
private

Definition at line 311 of file partial_order_reduction.h.

◆ updates1_k1

data::data_expression_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::updates1_k1
private

Definition at line 315 of file partial_order_reduction.h.

◆ updates2_k

data::data_expression_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::updates2_k
private

Definition at line 319 of file partial_order_reduction.h.

◆ updates2_k1

data::data_expression_list mcrl2::pbes_system::partial_order_reduction_algorithm::summand_relations_data::updates2_k1
private

Definition at line 323 of file partial_order_reduction.h.

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