mCRL2
Loading...
Searching...
No Matches
confluence.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_LPS_CONFLUENCE_H
13#define MCRL2_LPS_CONFLUENCE_H
14
15#include "mcrl2/data/rewriter.h"
21#include "mcrl2/smt/solver.h"
22
23namespace mcrl2 {
24
25namespace lps {
26
27namespace detail {
28
29inline
31{
32 return and_(x1, data::and_(x2, x3));
33}
34
35inline
37{
38 return and_(data::and_(x1, x2), data::and_(x3, x4));
39}
40
41inline
43{
44 std::vector<data::data_expression> conjuncts;
45 auto xi = x.begin();
46 auto yi = y.begin();
47 for (; xi != x.end(); ++xi, ++yi)
48 {
49 conjuncts.push_back(data::equal_to(*xi, *yi));
50 }
51 return data::join_and(conjuncts.begin(), conjuncts.end());
52}
53
54inline
55std::pair<std::size_t, std::size_t> make_sorted_pair(std::size_t i, std::size_t j)
56{
57 return (i < j) ? std::make_pair(i, j) : std::make_pair(j, i);
58}
59
60inline
62{
63 std::set<data::variable> freevars = data::find_free_variables(x);
64 return data::make_forall_(data::variable_list(freevars.begin(), freevars.end()), x);
65}
66
67} // namespace detail
68
69// TODO: reuse this code
70template <typename Summand>
71const stochastic_distribution& summand_distribution(const Summand& /* summand */)
72{
73 static stochastic_distribution empty_distribution;
74 return empty_distribution;
75}
76
77// TODO: reuse this code
78template <>
80{
81 return summand.distribution();
82}
83
84inline
85std::set<data::variable> used_read_variables(const action_summand& summand)
86{
87 std::set<data::variable> result;
88 data::find_all_variables(summand.condition(), std::inserter(result, result.end()));
89 data::find_all_variables(summand.multi_action(), std::inserter(result, result.end()));
90 for (const auto& a : summand.assignments())
91 {
92 if (a.lhs() != a.rhs())
93 {
94 data::find_all_variables(a.rhs(), std::inserter(result, result.end()));
95 }
96 }
97 return result;
98}
99
100inline
101std::set<data::variable> changed_variables(const action_summand& summand)
102{
103 std::set<data::variable> result;
104 for (const auto& a: summand.assignments())
105 {
106 result.insert(a.lhs());
107 }
108 return result;
109}
110
111// This is an alternative version of data::make_assignment_list that removes trivial assignments
112inline
114{
115 assert(variables.size() == expressions.size());
116 std::vector<data::assignment> result;
117 auto vi = variables.begin();
118 auto ei = expressions.begin();
119 for (; vi != variables.end(); ++vi, ++ei)
120 {
121 if (*vi != *ei)
122 {
123 result.emplace_back(*vi, *ei);
124 }
125 }
126 return data::assignment_list(result.begin(), result.end());
127}
128
130{
136 std::set<data::variable> changed;
137 std::set<data::variable> used;
138
139 template <typename ActionSummand>
140 confluence_summand(const ActionSummand& summand, const data::variable_list& process_parameters)
141 : variables(summand.summation_variables()),
142 condition(summand.condition()),
143 multi_action(summand.multi_action().actions(), summand.multi_action().time()),
145 next_state(summand.next_state(process_parameters)),
146 changed(changed_variables(summand)),
147 used(used_read_variables(summand))
148 {}
149
150 bool is_tau() const
151 {
152 return multi_action.actions().empty();
153 }
154};
155
156inline
157std::string print_confluence_summand(const confluence_summand& summand, const data::variable_list& process_parameters)
158{
159 std::ostringstream out;
161 summand.variables,
162 summand.condition,
163 summand.multi_action,
164 make_assignment_list(process_parameters, summand.next_state),
165 summand.distribution
166 );
167 return out.str();
168}
169
171inline
172bool disjoint(const confluence_summand& summand1, const confluence_summand& summand2)
173{
175 return has_empty_intersection(summand1.used, summand2.changed)
176 && has_empty_intersection(summand2.used, summand1.changed)
177 && has_empty_intersection(summand1.changed, summand2.changed);
178}
179
182{
184 return process::action_label(ctau_act_id);
185}
186
189{
191 return process::action(ctau_action);
192}
193
194template <typename Specification>
195bool has_ctau_action(const Specification& lpsspec)
196{
198 return contains(lpsspec.action_labels(), make_ctau_act_id());
199}
200
205{
208 data::set_identifier_generator& generator; // used to generate unique variable names
209
211 : process_parameters(process_parameters_), sigma(sigma_), generator(generator_)
212 {}
213
215 {
216 return data::variable_list(e.begin(), e.end(), [&](const data::variable& v) { return data::variable(generator(v.name()), v.sort()); });
217 }
218
220 {
221 assert(summand_j.is_tau());
222
224
225 const auto& d = process_parameters;
226
227 const auto& ci = summand_j.condition;
228 const auto& gi = summand_j.next_state;
229 const auto& ei = summand_i.variables;
231
232 const auto& cj = summand_i.condition;
233 const auto& gj = summand_i.next_state;
234 const auto& ej = summand_i.variables;
236
237 data::add_assignments(sigma, d, gi); // sigma = [d := gi]
238 data::add_assignments(sigma, ej, ej1); // sigma = [d := gi, ej := ej']
241
242 data::remove_assignments(sigma, ej); // sigma = [d := gi]
243 data::add_assignments(sigma, d, gj); // sigma = [d := gj]
244 data::add_assignments(sigma, ei, ei1); // sigma = [d := gj, ei := ei']
247
248 if (summand_i.is_tau())
249 {
250 result = imp(data::and_(ci, cj),
251 data::make_exists_(ei1 + ej1,
252 or_(detail::equal_to(gi, gj), detail::make_and(ci_gj_ei1, cj_gi_ej1, detail::equal_to(gj_gi_ej1, gi_gj_ei1)))
253 )
254 );
255 }
256 else
257 {
258 const auto& fi = summand_i.multi_action.actions().front().arguments();
260 result = imp(data::and_(ci, cj),
261 data::make_exists_(ei1 + ej1,
262 detail::make_and(ci_gj_ei1, cj_gi_ej1, detail::equal_to(fi, fi_gj_ei1), detail::equal_to(gj_gi_ej1, gi_gj_ei1))
263 )
264 );
265 }
266
267 data::remove_assignments(sigma, ei); // sigma = [d := gj]
268 data::remove_assignments(sigma, d); // sigma = []
269 return detail::make_forall_(result);
270 }
271};
272
277{
280
282 : process_parameters(process_parameters_), sigma(sigma_)
283 {}
284
286 {
287 assert(summand_j.is_tau());
288
290
291 const auto& d = process_parameters;
292
293 const auto& ci = summand_j.condition;
294 const auto& gi = summand_j.next_state;
295
296 const auto& cj = summand_i.condition;
297 const auto& gj = summand_i.next_state;
298
302
306
307 if (summand_i.is_tau())
308 {
310 result = imp(data::and_(ci, cj), or_(detail::equal_to(gi, gj), detail::make_and(ci_gj, cj_gi, detail::equal_to(gj_gi, gi_gj))));
311 }
312 else
313 {
314 const auto& fi = summand_i.multi_action.actions().front().arguments();
317 result = imp(data::and_(ci, cj), detail::make_and(ci_gj, cj_gi, detail::equal_to(fi, fi_gj), detail::equal_to(gj_gi, gi_gj)));
318 }
319
320 return detail::make_forall_(result);
321 }
322};
323
328{
331
333 : process_parameters(process_parameters_), sigma(sigma_)
334 {}
335
336 inline
338 {
339 assert(summand_j.is_tau());
340
342
343 const auto& d = process_parameters;
344
345 const auto& ci = summand_i.condition;
346 const auto& gi = summand_i.next_state;
347
348 const auto& cj = summand_j.condition;
349 const auto& gj = summand_j.next_state;
350
354
355 if (summand_i.is_tau())
356 {
358 result = imp(and_(ci, cj), and_(ci_gj, detail::equal_to(gi_gj, gi)));
359 }
360 else
361 {
362 const auto& fi = summand_i.multi_action.actions().front().arguments();
365 result = imp(and_(ci, cj), detail::make_and(ci_gj, detail::equal_to(fi, fi_gj), detail::equal_to(gi_gj, gi)));
366 }
367
368 return detail::make_forall_(result);
369 }
370};
371
376{
378
380 : sigma(sigma_)
381 {}
382
383 inline
385 {
386 assert(summand_j.is_tau());
387
389
390 data::data_expression aj_is_tau = summand_i.is_tau() ? data::true_() : data::false_();
391
392 const auto& ci = summand_i.condition;
393 const auto& gi = summand_i.next_state;
394
395 const auto& cj = summand_j.condition;
396 const auto& gj = summand_j.next_state;
397
398 result = imp(and_(cj, ci), and_(aj_is_tau, detail::equal_to(gj, gi)));
399
400 return detail::make_forall_(result);
401 }
402};
403
405{
406 protected:
407 std::vector<confluence_summand> m_summands;
411 std::unique_ptr<smt::smt_solver> m_solver;
412
413 // cache for the value of is_confluent for pairs (i, j) with i <= j, and i and j both tau-summands
414 mutable std::map<std::pair<std::size_t, std::size_t>, bool> m_cache;
415
417 {
419 };
420
421 cache_result cache_lookup(std::size_t i, std::size_t j) const
422 {
423 // check if the combination (i, j) is already in the cache
424 auto found = m_cache.find(detail::make_sorted_pair(i, j));
425 if (found != m_cache.end())
426 {
427 return found->second ? yes : no;
428 }
429 return indeterminate;
430 }
431
432 void cache_store(std::size_t i, std::size_t j, bool confluent) const
433 {
434 m_cache[detail::make_sorted_pair(i, j)] = confluent;
435 }
436
437 // check if x is a tautology using the data rewriter
439 {
441 data::quantifiers_inside_rewriter R_quantifiers_inside;
442 x = m_rewr(R_one_point(R_quantifiers_inside(x)));
443 return data::is_true(x);
444 }
445
446 // check if x is a tautology using an smt solver
448 {
449 if (data::is_forall(x))
450 {
451 const auto& x_ = atermpp::down_cast<data::forall>(x);
452 bool result = true;
453 switch (m_solver->solve(x_.variables(), data::sort_bool::not_(x_.body())))
454 {
455 case smt::answer::SAT: result = true; break;
456 case smt::answer::UNSAT: result = false; break;
457 // since the formula is negated, we over-approximate unknown results
458 // the result of this function will then be an under-approximation
459 case smt::answer::UNKNOWN: result = true; break;
460 }
461 return !result;
462 }
463 else
464 {
465 // x has no free variables, so just evaluate the expression
466 return data::is_true(m_rewr(x));
467 }
468 }
469
470 // check if x evaluates true
471 bool is_true(const data::data_expression& x) const
472 {
473 return m_solver ? is_true_smt(x) : is_true_rewriter(x);
474 }
475
476 // Returns whether the tau summand with index j is confluent. If not, the second value returned is
477 // the index of the summand for which a violation was detected.
478 template <typename ConfluenceCondition>
479 std::pair<bool, std::size_t> is_confluent(std::size_t j, ConfluenceCondition confluence_condition, bool check_disjointness) const
480 {
481 const confluence_summand& summand_j = m_summands[j];
482 for (std::size_t i = 0; i < m_summands.size(); i++)
483 {
484 const confluence_summand& summand_i = m_summands[i];
485
486 // check if the value for (i, j) is already in the cache
487 if (summand_j.is_tau())
488 {
489 auto value = cache_lookup(i, j);
490 if (value == yes)
491 {
492 mCRL2log(log::info) << '.';
493 continue;
494 }
495 else if (value == no)
496 {
497 return { false, i };
498 }
499 }
500
501 if (check_disjointness && disjoint(summand_i, summand_j))
502 {
503 cache_store(i, j, true);
504 mCRL2log(log::info) << ':';
505 continue;
506 }
507
508 data::data_expression condition = confluence_condition(summand_i, summand_j);
509 bool confluent = is_true(condition);
510 cache_store(i, j, confluent);
511 if (confluent)
512 {
513 mCRL2log(log::info) << '+';
514 }
515 else
516 {
517 return { false, i };
518 }
519 }
520 return { true, 0 };
521 }
522
523 public:
524 std::pair<bool, std::size_t> is_commutative_confluent(std::size_t j, data::set_identifier_generator& generator) const
525 {
526 bool check_disjointness = true;
527 return is_confluent(j, commutative_confluence_condition(m_process_parameters, m_sigma, generator), check_disjointness);
528 }
529
530 std::pair<bool, std::size_t> is_square_confluent(std::size_t j) const
531 {
532 bool check_disjointness = true;
534 }
535
536 std::pair<bool, std::size_t> is_triangular_confluent(std::size_t j) const
537 {
538 bool check_disjointness = false;
540 }
541
542 std::pair<bool, std::size_t> is_trivial_confluent(std::size_t j) const
543 {
544 bool check_disjointness = false;
545 return is_confluent(j, trivial_confluence_condition(m_sigma), check_disjointness);
546 }
547
548 template <typename Specification>
549 std::vector<std::size_t> compute_confluent_summands(const Specification& lpsspec, char confluence_type)
550 {
551 std::vector<std::size_t> result;
552
553 m_cache.clear();
554 m_summands.clear();
555 m_process_parameters = lpsspec.process().process_parameters();
556 m_rewr = data::rewriter(lpsspec.data());
557
558 for (const auto& summand: lpsspec.process().action_summands())
559 {
560 m_summands.emplace_back(summand, m_process_parameters);
561 }
562
563 std::size_t n = m_summands.size();
564 std::size_t tau_summand_count = 0;
565 for (std::size_t j = 0; j < n; j++)
566 {
567 const auto& summand_j = m_summands[j];
568 if (!summand_j.is_tau())
569 {
570 continue;
571 }
572 tau_summand_count++;
573 mCRL2log(log::info) << "summand " << (j + 1) << " of " << n << " (condition = " << confluence_type << "): ";
574 bool confluent;
575 std::size_t violating_index;
576 switch (confluence_type)
577 {
578 case 'Q':
579 {
581 generator.add_identifiers(lps::find_identifiers(lpsspec));
582 std::tie(confluent, violating_index) = is_commutative_confluent(j, generator); break;
583 }
584 case 'C': std::tie(confluent, violating_index) = is_square_confluent(j); break;
585 case 'T': std::tie(confluent, violating_index) = is_triangular_confluent(j); break;
586 case 'Z': std::tie(confluent, violating_index) = is_trivial_confluent(j); break;
587 default: throw mcrl2::runtime_error("Unknown confluence type " + std::to_string(confluence_type));
588 }
589 if (confluent)
590 {
591 result.push_back(j);
592 mCRL2log(log::info) << "Confluent with all summands";
593 }
594 else
595 {
596 mCRL2log(log::info) << "Not confluent with summand " << (violating_index + 1);
597 }
598 mCRL2log(log::info) << std::endl;
599 }
600 mCRL2log(log::info) << result.size() << " of " << tau_summand_count << " tau summands were found to be confluent";
601 return result;
602 }
603
605 template <typename Specification>
606 void run(Specification& lpsspec, char confluence_type, bool use_smt_solver = false)
607 {
608 if (has_ctau_action(lpsspec))
609 {
610 throw mcrl2::runtime_error("An action named \'ctau\' already exists.\n");
611 }
612
613 if (use_smt_solver)
614 {
615 m_solver = std::unique_ptr<smt::smt_solver>(new smt::smt_solver(lpsspec.data()));
616 }
617
619 std::vector<std::size_t> I = compute_confluent_summands(lpsspec, confluence_type);
620 auto& summands = lpsspec.process().action_summands();
621 for (std::size_t i: I)
622 {
623 summands[i].multi_action() = ctau;
624 }
625 }
626};
627
628} // namespace lps
629
630} // namespace mcrl2
631
632#endif // MCRL2_LPS_CONFLUENCE_H
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
void add_identifiers(const std::set< core::identifier_string > &ids)
Add a set of identifiers to the context.
Rewriter that operates on data expressions.
Definition rewriter.h:81
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
\brief A data variable
Definition variable.h:28
LPS summand containing a multi-action.
const lps::multi_action & multi_action() const
Returns the multi-action of this summand.
const data::assignment_list & assignments() const
Returns the sequence of assignments.
std::pair< bool, std::size_t > is_commutative_confluent(std::size_t j, data::set_identifier_generator &generator) const
Definition confluence.h:524
std::pair< bool, std::size_t > is_trivial_confluent(std::size_t j) const
Definition confluence.h:542
bool is_true_smt(const data::data_expression &x) const
Definition confluence.h:447
std::unique_ptr< smt::smt_solver > m_solver
Definition confluence.h:411
std::vector< confluence_summand > m_summands
Definition confluence.h:407
bool is_true(const data::data_expression &x) const
Definition confluence.h:471
bool is_true_rewriter(data::data_expression x) const
Definition confluence.h:438
void cache_store(std::size_t i, std::size_t j, bool confluent) const
Definition confluence.h:432
std::pair< bool, std::size_t > is_confluent(std::size_t j, ConfluenceCondition confluence_condition, bool check_disjointness) const
Definition confluence.h:479
void run(Specification &lpsspec, char confluence_type, bool use_smt_solver=false)
Applies confluent reduction to an LPS.
Definition confluence.h:606
data::mutable_indexed_substitution m_sigma
Definition confluence.h:410
std::map< std::pair< std::size_t, std::size_t >, bool > m_cache
Definition confluence.h:414
data::variable_list m_process_parameters
Definition confluence.h:408
std::pair< bool, std::size_t > is_square_confluent(std::size_t j) const
Definition confluence.h:530
cache_result cache_lookup(std::size_t i, std::size_t j) const
Definition confluence.h:421
std::vector< std::size_t > compute_confluent_summands(const Specification &lpsspec, char confluence_type)
Definition confluence.h:549
std::pair< bool, std::size_t > is_triangular_confluent(std::size_t j) const
Definition confluence.h:536
\brief A timed multi-action
const process::action_list & actions() const
LPS summand containing a multi-action.
const stochastic_distribution & distribution() const
Returns the distribution of this summand.
\brief A stochastic distribution
const data::data_expression & condition() const
Returns the condition expression.
Definition summand.h:60
\brief An action label
Standard exception class for reporting runtime errors.
Definition exception.h:27
This file contains some functions that are present in all libraries except the data library....
The class rewriter.
add your file description here.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
const atermpp::function_symbol & function_symbol_ActId()
const atermpp::function_symbol & function_symbol_Action()
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:94
data_expression make_exists_(const data::variable_list &v, const data_expression &x)
Make an existential quantification. It checks for an empty variable list, which is not allowed.
data_expression make_forall_(const data::variable_list &v, const data_expression &x)
Make a universal quantification. It checks for an empty variable list, which is not allowed.
data_expression and_(const data_expression &x, const data_expression &y)
const data_expression & false_()
Definition consistency.h:99
bool is_true(const data_expression &x)
Test if x is true.
Definition consistency.h:29
void add_assignments(data::mutable_indexed_substitution<> &sigma, const VariableSequence &v, const DataExpressionSequence &e)
Adds assignments [v := e] to the substitution sigma for each variable in v.
const data_expression & true_()
Definition consistency.h:92
void remove_assignments(data::mutable_indexed_substitution<> &sigma, const VariableSequence &v)
Removes assignments to variables in v from the substitution sigma.
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
atermpp::term_list< variable > variable_list
\brief list of variables
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
data_expression join_and(FwdIt first, FwdIt last)
Returns and applied to the sequence of data expressions [first, last)
Definition join.h:40
std::pair< std::size_t, std::size_t > make_sorted_pair(std::size_t i, std::size_t j)
Definition confluence.h:55
data::data_expression make_and(const data::data_expression &x1, const data::data_expression &x2, const data::data_expression &x3)
Definition confluence.h:30
process::action make_ctau_action()
Creates the ctau action.
Definition confluence.h:188
const stochastic_distribution & summand_distribution(const Summand &)
Definition confluence.h:71
bool has_ctau_action(const Specification &lpsspec)
Definition confluence.h:195
bool disjoint(const confluence_summand &summand1, const confluence_summand &summand2)
Indicates whether or not two summands are disjoint.
Definition confluence.h:172
std::set< data::variable > changed_variables(const action_summand &summand)
Definition confluence.h:101
process::action_label make_ctau_act_id()
Creates an identifier for the ctau action.
Definition confluence.h:181
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:96
std::string print_confluence_summand(const confluence_summand &summand, const data::variable_list &process_parameters)
Definition confluence.h:157
data::assignment_list make_assignment_list(const data::variable_list &variables, const data::data_expression_list &expressions)
Definition confluence.h:113
std::set< data::variable > used_read_variables(const action_summand &summand)
Definition confluence.h:85
@ UNKNOWN
Definition answer.h:24
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
Definition indexed_set.h:86
bool has_empty_intersection(InputIterator1 first1, InputIterator1 last1, InputIterator2 first2, InputIterator2 last2)
Returns true if the sorted ranges [first1, ..., last1) and [first2, ..., last2) have an empty interse...
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Function object that computes the condition for commutative confluence.
Definition confluence.h:205
data::variable_list make_fresh_variables(const data::variable_list &e) const
Definition confluence.h:214
commutative_confluence_condition(const data::variable_list &process_parameters_, data::mutable_indexed_substitution<> &sigma_, data::set_identifier_generator &generator_)
Definition confluence.h:210
data::set_identifier_generator & generator
Definition confluence.h:208
data::mutable_indexed_substitution & sigma
Definition confluence.h:207
data::data_expression operator()(const confluence_summand &summand_i, const confluence_summand &summand_j) const
Definition confluence.h:219
const data::variable_list & process_parameters
Definition confluence.h:206
data::variable_list variables
Definition confluence.h:131
std::set< data::variable > changed
Definition confluence.h:136
data::data_expression condition
Definition confluence.h:132
stochastic_distribution distribution
Definition confluence.h:134
data::data_expression_list next_state
Definition confluence.h:135
lps::multi_action multi_action
Definition confluence.h:133
confluence_summand(const ActionSummand &summand, const data::variable_list &process_parameters)
Definition confluence.h:140
std::set< data::variable > used
Definition confluence.h:137
Function object that computes the condition for square confluence.
Definition confluence.h:277
const data::variable_list & process_parameters
Definition confluence.h:278
data::mutable_indexed_substitution & sigma
Definition confluence.h:279
data::data_expression operator()(const confluence_summand &summand_i, const confluence_summand &summand_j) const
Definition confluence.h:285
square_confluence_condition(const data::variable_list &process_parameters_, data::mutable_indexed_substitution<> &sigma_)
Definition confluence.h:281
Function object that computes the condition for triangular confluence.
Definition confluence.h:328
data::data_expression operator()(const confluence_summand &summand_i, const confluence_summand &summand_j) const
Definition confluence.h:337
triangular_confluence_condition(const data::variable_list &process_parameters_, data::mutable_indexed_substitution<> &sigma_)
Definition confluence.h:332
data::mutable_indexed_substitution & sigma
Definition confluence.h:330
const data::variable_list & process_parameters
Definition confluence.h:329
Function object that computes the condition for triangular confluence.
Definition confluence.h:376
data::data_expression operator()(const confluence_summand &summand_i, const confluence_summand &summand_j) const
Definition confluence.h:384
data::mutable_indexed_substitution & sigma
Definition confluence.h:377
trivial_confluence_condition(data::mutable_indexed_substitution<> &sigma_)
Definition confluence.h:379
add your file description here.