12#ifndef MCRL2_LPS_CONFLUENCE_H
13#define MCRL2_LPS_CONFLUENCE_H
44 std::vector<data::data_expression> conjuncts;
47 for (; xi != x.
end(); ++xi, ++yi)
57 return (i < j) ? std::make_pair(i, j) : std::make_pair(j, i);
70template <
typename Summand>
74 return empty_distribution;
87 std::set<data::variable> result;
92 if (a.lhs() != a.rhs())
103 std::set<data::variable> result;
106 result.insert(a.lhs());
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)
123 result.emplace_back(*vi, *ei);
139 template <
typename ActionSummand>
141 :
variables(summand.summation_variables()),
159 std::ostringstream out;
175 return has_empty_intersection(summand1.
used, summand2.
changed)
176 && has_empty_intersection(summand2.
used, summand1.
changed)
194template <
typename Specification>
221 assert(summand_j.
is_tau());
287 assert(summand_j.
is_tau());
339 assert(summand_j.
is_tau());
386 assert(summand_j.
is_tau());
414 mutable std::map<std::pair<std::size_t, std::size_t>,
bool>
m_cache;
427 return found->second ?
yes :
no;
432 void cache_store(std::size_t i, std::size_t j,
bool confluent)
const
442 x =
m_rewr(R_one_point(R_quantifiers_inside(x)));
451 const auto& x_ = atermpp::down_cast<data::forall>(x);
478 template <
typename ConfluenceCondition>
479 std::pair<bool, std::size_t>
is_confluent(std::size_t j, ConfluenceCondition confluence_condition,
bool check_disjointness)
const
482 for (std::size_t i = 0; i <
m_summands.size(); i++)
495 else if (value ==
no)
501 if (check_disjointness &&
disjoint(summand_i, summand_j))
509 bool confluent =
is_true(condition);
526 bool check_disjointness =
true;
532 bool check_disjointness =
true;
538 bool check_disjointness =
false;
544 bool check_disjointness =
false;
548 template <
typename Specification>
551 std::vector<std::size_t> result;
558 for (
const auto& summand: lpsspec.process().action_summands())
564 std::size_t tau_summand_count = 0;
565 for (std::size_t j = 0; j < n; j++)
568 if (!summand_j.is_tau())
573 mCRL2log(
log::info) <<
"summand " << (j + 1) <<
" of " << n <<
" (condition = " << confluence_type <<
"): ";
575 std::size_t violating_index;
576 switch (confluence_type)
587 default:
throw mcrl2::runtime_error(
"Unknown confluence type " + std::to_string(confluence_type));
600 mCRL2log(
log::info) << result.size() <<
" of " << tau_summand_count <<
" tau summands were found to be confluent";
605 template <
typename Specification>
606 void run(Specification& lpsspec,
char confluence_type,
bool use_smt_solver =
false)
620 auto& summands = lpsspec.process().action_summands();
621 for (std::size_t i: I)
623 summands[i].multi_action() = ctau;
size_type size() const
Returns the size of the term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
const Term & front() const
Returns the first element of the list.
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
bool empty() const
Returns true if the list's size is 0.
void add_identifiers(const std::set< core::identifier_string > &ids)
Add a set of identifiers to the context.
Generic substitution function.
Rewriter that operates on data expressions.
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
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
std::pair< bool, std::size_t > is_trivial_confluent(std::size_t j) const
bool is_true_smt(const data::data_expression &x) const
std::unique_ptr< smt::smt_solver > m_solver
std::vector< confluence_summand > m_summands
bool is_true(const data::data_expression &x) const
bool is_true_rewriter(data::data_expression x) const
void cache_store(std::size_t i, std::size_t j, bool confluent) const
std::pair< bool, std::size_t > is_confluent(std::size_t j, ConfluenceCondition confluence_condition, bool check_disjointness) const
void run(Specification &lpsspec, char confluence_type, bool use_smt_solver=false)
Applies confluent reduction to an LPS.
data::mutable_indexed_substitution m_sigma
std::map< std::pair< std::size_t, std::size_t >, bool > m_cache
data::variable_list m_process_parameters
std::pair< bool, std::size_t > is_square_confluent(std::size_t j) const
cache_result cache_lookup(std::size_t i, std::size_t j) const
std::vector< std::size_t > compute_confluent_summands(const Specification &lpsspec, char confluence_type)
std::pair< bool, std::size_t > is_triangular_confluent(std::size_t j) const
\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.
Standard exception class for reporting runtime errors.
This file contains some functions that are present in all libraries except the data library....
add your file description here.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
const atermpp::function_symbol & function_symbol_ActId()
const atermpp::function_symbol & function_symbol_Action()
const function_symbol & not_()
Constructor for function symbol !.
std::set< data::variable > find_all_variables(const data::data_expression &x)
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_()
bool is_true(const data_expression &x)
Test if x is true.
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_()
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)
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
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
data_expression join_and(FwdIt first, FwdIt last)
Returns and applied to the sequence of data expressions [first, last)
std::pair< std::size_t, std::size_t > make_sorted_pair(std::size_t i, std::size_t j)
data::data_expression make_and(const data::data_expression &x1, const data::data_expression &x2, const data::data_expression &x3)
process::action make_ctau_action()
Creates the ctau action.
const stochastic_distribution & summand_distribution(const Summand &)
bool has_ctau_action(const Specification &lpsspec)
bool disjoint(const confluence_summand &summand1, const confluence_summand &summand2)
Indicates whether or not two summands are disjoint.
std::set< data::variable > changed_variables(const action_summand &summand)
process::action_label make_ctau_act_id()
Creates an identifier for the ctau action.
void find_identifiers(const T &x, OutputIterator o)
std::string print_confluence_summand(const confluence_summand &summand, const data::variable_list &process_parameters)
data::assignment_list make_assignment_list(const data::variable_list &variables, const data::data_expression_list &expressions)
std::set< data::variable > used_read_variables(const action_summand &summand)
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)
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...
Function object that computes the condition for commutative confluence.
data::variable_list make_fresh_variables(const data::variable_list &e) const
commutative_confluence_condition(const data::variable_list &process_parameters_, data::mutable_indexed_substitution<> &sigma_, data::set_identifier_generator &generator_)
data::set_identifier_generator & generator
data::mutable_indexed_substitution & sigma
data::data_expression operator()(const confluence_summand &summand_i, const confluence_summand &summand_j) const
const data::variable_list & process_parameters
data::variable_list variables
std::set< data::variable > changed
data::data_expression condition
stochastic_distribution distribution
data::data_expression_list next_state
lps::multi_action multi_action
confluence_summand(const ActionSummand &summand, const data::variable_list &process_parameters)
std::set< data::variable > used
Function object that computes the condition for square confluence.
const data::variable_list & process_parameters
data::mutable_indexed_substitution & sigma
data::data_expression operator()(const confluence_summand &summand_i, const confluence_summand &summand_j) const
square_confluence_condition(const data::variable_list &process_parameters_, data::mutable_indexed_substitution<> &sigma_)
Function object that computes the condition for triangular confluence.
data::data_expression operator()(const confluence_summand &summand_i, const confluence_summand &summand_j) const
triangular_confluence_condition(const data::variable_list &process_parameters_, data::mutable_indexed_substitution<> &sigma_)
data::mutable_indexed_substitution & sigma
const data::variable_list & process_parameters
Function object that computes the condition for triangular confluence.
data::data_expression operator()(const confluence_summand &summand_i, const confluence_summand &summand_j) const
data::mutable_indexed_substitution & sigma
trivial_confluence_condition(data::mutable_indexed_substitution<> &sigma_)
add your file description here.