mCRL2
Loading...
Searching...
No Matches
replace_capture_avoiding.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_PROCESS_REPLACE_CAPTURE_AVOIDING_H
13#define MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_H
14
17#include "mcrl2/process/find.h"
18
19namespace mcrl2 {
20
21namespace process {
22
23namespace detail {
24
25template<template<class> class Builder, class Derived, class Substitution>
27 : public data::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
28{
29 typedef data::detail::add_capture_avoiding_replacement <Builder, Derived, Substitution> super;
30 using super::enter;
31 using super::leave;
33 using super::update;
34 using super::sigma;
35
37 {
38 for (auto i = a.begin(); i != a.end(); ++i)
39 {
40 if (i->lhs() == v)
41 {
42 return i;
43 }
44 }
45 return a.end();
46 }
47
49 : super(sigma)
50 { }
51
52 template <class T>
54 {
55 static_cast<Derived&>(*this).enter(x);
57 std::vector <data::assignment> v;
58
59 for (const data::variable& variable: x.identifier().variables())
60 {
61 auto k = find_variable(a, variable);
62 if (k == a.end())
63 {
65 apply(e, variable);
66 if (e != variable)
67 {
68 v.emplace_back(variable, e);
69 }
70 }
71 else
72 {
74 apply(rhs, k->rhs());
75 v.emplace_back(k->lhs(), rhs);
76 }
77 }
79 static_cast<Derived&>(*this).leave(x);
80 }
81
82 template <class T>
83 void apply(T& result, const sum& x)
84 {
85 data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
87 apply(body, x.operand());
88 make_sum(result, v1, body);
89 sigma.remove_fresh_variable_assignments(x.variables());
90 }
91
92 template <class T>
93 void apply(T& result, const stochastic_operator& x)
94 {
95 data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
97 apply(body, x.operand());
99 apply(dist, x.distribution());
100 make_stochastic_operator(result, v1, dist, body);
101 sigma.remove_fresh_variable_assignments(x.variables());
102 }
103};
104
105} // namespace detail
106
107//--- start generated process replace_capture_avoiding code ---//
112template <typename T, typename Substitution>
114 Substitution& sigma,
115 data::set_identifier_generator& id_generator,
116 typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
117)
118{
120 data::detail::apply_replace_capture_avoiding_variables_builder<process::data_expression_builder, process::detail::add_capture_avoiding_replacement>(sigma1).update(x);
121}
122
127template <typename T, typename Substitution>
129 Substitution& sigma,
130 data::set_identifier_generator& id_generator,
131 typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
132)
133{
135 T result;
136 data::detail::apply_replace_capture_avoiding_variables_builder<process::data_expression_builder, process::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
137 return result;
138}
139
143template <typename T, typename Substitution>
145 Substitution& sigma,
146 typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
147)
148{
151 for (const data::variable& v: substitution_variables(sigma))
152 {
153 id_generator.add_identifier(v.name());
154 }
156}
157
161template <typename T, typename Substitution>
163 Substitution& sigma,
164 typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
165)
166{
169 for (const data::variable& v: substitution_variables(sigma))
170 {
171 id_generator.add_identifier(v.name());
172 }
173 return process::replace_variables_capture_avoiding(x, sigma, id_generator);
174}
175//--- end generated process replace_capture_avoiding code ---//
176
177} // namespace process
178
179} // namespace mcrl2
180
181#endif // MCRL2_PROCESS_REPLACE_CAPTURE_AVOIDING_H
Iterator for term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
void add_identifiers(const std::set< core::identifier_string > &ids)
Add a set of identifiers to the context.
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
\brief A data variable
Definition variable.h:28
\brief A process expression
const data::variable_list & variables() const
const data::assignment_list & assignments() const
const process_identifier & identifier() const
\brief The distribution operator
const data::variable_list & variables() const
const data::data_expression & distribution() const
const process_expression & operand() const
\brief The sum operator
const process_expression & operand() const
const data::variable_list & variables() const
add your file description here.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:194
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)
void make_stochastic_operator(atermpp::aterm &t, const ARGUMENTS &... args)
void make_process_instance_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
add your file description here.
add your file description here.
void apply(atermpp::term_list< T > &result, const assignment_list &x)
capture_avoiding_substitution_updater< Substitution > & sigma
data::detail::add_capture_avoiding_replacement< Builder, Derived, Substitution > super
capture_avoiding_substitution_updater< Substitution > & sigma
void apply(T &result, const process::process_instance_assignment &x)
void apply(T &result, const stochastic_operator &x)
add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater< Substitution > &sigma)
data::assignment_list::const_iterator find_variable(const data::assignment_list &a, const data::variable &v) const