Line data Source code
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 : //
9 : /// \file mcrl2/lps/constelm.h
10 : /// \brief Add your file description here.
11 :
12 : #ifndef MCRL2_LPS_CONSTELM_H
13 : #define MCRL2_LPS_CONSTELM_H
14 :
15 : #include "mcrl2/lps/detail/lps_algorithm.h"
16 :
17 : namespace mcrl2
18 : {
19 :
20 : namespace lps
21 : {
22 :
23 : /// \brief Algorithm class for elimination of constant parameters
24 : template <typename DataRewriter, typename Specification = specification>
25 : class constelm_algorithm: public lps::detail::lps_algorithm<Specification>
26 : {
27 : typedef typename lps::detail::lps_algorithm<Specification> super;
28 :
29 : protected:
30 : /// \brief If true, then the algorithm is allowed to instantiate free variables
31 : /// as a side effect.
32 : bool m_instantiate_global_variables;
33 :
34 : /// \brief If true, conditions are not evaluated and assumed to be true.
35 : bool m_ignore_conditions;
36 :
37 : /// \brief Maps process parameters to their index.
38 : std::map<data::variable, std::size_t> m_index_of;
39 :
40 : /// \brief The rewriter used by the constelm algorithm.
41 : const DataRewriter& R;
42 :
43 727 : void LOG_CONSTANT_PARAMETERS(const data::mutable_map_substitution<>& sigma, const std::string& msg = "")
44 : {
45 727 : if (mCRL2logEnabled(log::verbose))
46 : {
47 0 : mCRL2log(log::verbose) << msg;
48 0 : for (const auto& i : sigma)
49 : {
50 0 : mCRL2log(log::verbose) << data::pp(i.first) << " := " << data::pp(i.second) << std::endl;
51 : }
52 : }
53 727 : }
54 :
55 1359 : void LOG_PARAMETER_CHANGE(const data::data_expression& d_j,
56 : const data::data_expression& Rd_j,
57 : const data::data_expression& Rg_ij,
58 : const data::mutable_map_substitution<>& sigma,
59 : const std::string& msg = ""
60 : )
61 : {
62 1359 : if (mCRL2logEnabled(log::debug))
63 : {
64 0 : mCRL2log(log::debug) << msg
65 : << data::pp(d_j) << "\n"
66 0 : << " value before: " << Rd_j << "\n"
67 0 : << " value after: " << Rg_ij << "\n"
68 0 : << " replacements: " << sigma << std::endl;
69 : }
70 1359 : }
71 :
72 241 : void LOG_CONDITION(const data::data_expression& cond,
73 : const data::data_expression& c_i,
74 : const data::mutable_map_substitution<>& sigma,
75 : const std::string& msg = ""
76 : )
77 :
78 : {
79 241 : if (mCRL2logEnabled(log::debug))
80 : {
81 0 : mCRL2log(log::debug) << msg
82 : << cond
83 0 : << sigma
84 0 : << " -> "
85 0 : << c_i << std::endl;
86 : }
87 241 : }
88 :
89 : // returns true if x contains free variables that are not in global_variables
90 942 : bool is_constant(const data::data_expression& x, const std::set<data::variable>& global_variables) const
91 : {
92 : using utilities::detail::contains;
93 :
94 1179 : for (const data::variable& v: find_free_variables(x))
95 : {
96 237 : if (!contains(global_variables, v))
97 : {
98 75 : return false;
99 : }
100 : }
101 867 : return true;
102 : }
103 :
104 : public:
105 :
106 : /// \brief Constructor
107 727 : constelm_algorithm(Specification& spec, const DataRewriter& R_)
108 : : lps::detail::lps_algorithm<Specification>(spec),
109 727 : m_instantiate_global_variables(false),
110 727 : m_ignore_conditions(false),
111 727 : R(R_)
112 727 : {}
113 :
114 : /// \brief Computes constant parameters
115 : /// \param instantiate_global_variables If true, the algorithm is allowed to instantiate free variables
116 : /// as a side effect
117 : /// \param ignore_conditions If true, the algorithm is allowed to ignore the conditions in the LPS.
118 727 : data::mutable_map_substitution<> compute_constant_parameters(bool instantiate_global_variables = false, bool ignore_conditions = false)
119 : {
120 : using utilities::detail::contains;
121 :
122 727 : data::mutable_map_substitution<> sigma;
123 :
124 727 : m_instantiate_global_variables = instantiate_global_variables;
125 727 : m_ignore_conditions = ignore_conditions;
126 727 : data::data_expression_list initial_state = super::m_spec.initial_process().expressions();
127 727 : data::data_expression_vector r(initial_state.begin(), initial_state.end());
128 :
129 : // essential: rewrite the initial state vector r to normal form. Essential
130 : // because this value is used in W below, and assigned to the right hand side of a substitution, which
131 : // must be a normal form.
132 727 : lps::rewrite(r, R);
133 :
134 727 : auto& process = super::m_spec.process();
135 727 : const std::set<data::variable>& global_variables = super::m_spec.global_variables();
136 727 : const data::variable_list& d = process.process_parameters();
137 727 : const data::data_expression_list& e = super::m_spec.initial_process().expressions();
138 :
139 : // initialize m_index_of
140 727 : unsigned index = 0;
141 2396 : for (const data::variable& v: d)
142 : {
143 942 : m_index_of[v] = index++;
144 : }
145 :
146 727 : std::set<data::variable> G(d.begin(), d.end());
147 727 : std::set<data::variable> dG;
148 727 : auto di = d.begin();
149 727 : auto ei = e.begin();
150 1669 : for (; di != d.end(); ++di, ++ei)
151 : {
152 : // The rewriter requires that the right hand sides of a substitution are in normal form.
153 942 : data::data_expression rhs = R(*ei);
154 942 : if (is_constant(rhs, global_variables))
155 : {
156 867 : sigma[*di] = rhs;
157 : }
158 : else
159 : {
160 75 : G.erase(*di);
161 : }
162 : }
163 :
164 : // undo contains undo information of instantiations of free variables
165 727 : std::map<data::variable, std::set<data::variable> > undo;
166 :
167 : do
168 : {
169 1167 : dG.clear();
170 3376 : for (const auto& summand: process.action_summands())
171 : {
172 2209 : const data::data_expression& c_i = summand.condition();
173 2209 : if (m_ignore_conditions || (R(c_i, sigma) != data::sort_bool::false_()))
174 : {
175 5155 : for (const data::variable& j: G)
176 : {
177 1828 : if (dG.find(j) != dG.end())
178 : {
179 469 : continue;
180 : }
181 1359 : std::size_t index_j = m_index_of[j];
182 1359 : const data::variable& d_j = j;
183 1359 : data::data_expression g_ij = super::next_state(summand, d_j);
184 :
185 1359 : if (R(g_ij, sigma) != R(d_j, sigma))
186 : {
187 821 : LOG_PARAMETER_CHANGE(d_j, R(d_j, sigma), R(g_ij, sigma), sigma, "POSSIBLE CHANGE FOR PARAMETER ");
188 821 : data::data_expression z = R(g_ij, sigma);
189 821 : if (is_variable(z) && contains(global_variables, atermpp::down_cast<data::variable>(z)))
190 : {
191 177 : sigma[atermpp::down_cast<data::variable>(z)] = r[index_j];
192 177 : undo[d_j].insert(atermpp::down_cast<data::variable>(z));
193 : }
194 : else
195 : {
196 644 : dG.insert(d_j);
197 644 : sigma[d_j] = d_j; // erase d_j
198 680 : for (const data::variable& w: undo[d_j])
199 : {
200 36 : sigma[w] = w; // erase *w
201 : }
202 644 : undo[d_j].clear();
203 : }
204 821 : }
205 : else
206 : {
207 538 : LOG_PARAMETER_CHANGE(d_j, R(d_j, sigma), R(g_ij, sigma), sigma, "NO CHANGE FOR PARAMETER ");
208 : }
209 : }
210 : }
211 : else
212 : {
213 241 : LOG_CONDITION(summand.condition(), R(c_i, sigma), sigma, "CONDITION IS FALSE: ");
214 : }
215 : }
216 1811 : for (const data::variable& v: dG)
217 : {
218 644 : G.erase(v);
219 : }
220 : }
221 1167 : while (!dG.empty());
222 :
223 1454 : return sigma;
224 727 : }
225 :
226 : /// \brief Applies the substitution computed by compute_constant_parameters
227 727 : void remove_parameters(data::mutable_map_substitution<>& sigma)
228 : {
229 727 : LOG_CONSTANT_PARAMETERS(sigma, "Removing the following constant parameters:\n");
230 :
231 : // N.B. The order of removing constant parameters and rewriting has been reversed
232 : // as requested by Jan Friso Groote. This may lead to some gain in performance (13%
233 : // in the case of 6x6 othello). Note that due to this change the intermediate result
234 : // after removing parameters may not be a valid LPS.
235 :
236 : // remove the constant parameters from the specification spec
237 727 : std::set<data::variable> constant_parameters;
238 1091 : for (const auto& i: sigma)
239 : {
240 364 : constant_parameters.insert(i.first);
241 : }
242 727 : lps::remove_parameters(super::m_spec, constant_parameters);
243 :
244 : // rewrite the specification with substitution sigma
245 727 : lps::rewrite(super::m_spec, R, sigma);
246 727 : }
247 :
248 : /// \brief Runs the constelm algorithm
249 : /// \param instantiate_global_variables If true, the algorithm is allowed to instantiate free variables
250 : /// as a side effect
251 : /// \param ignore_conditions If true, the algorithm is allowed to ignore the conditions in the LPS.
252 12 : void run(bool instantiate_global_variables = false, bool ignore_conditions = false)
253 : {
254 12 : data::mutable_map_substitution<> sigma = compute_constant_parameters(instantiate_global_variables, ignore_conditions);
255 12 : remove_parameters(sigma);
256 12 : };
257 : };
258 :
259 : /// \brief Removes zero or more constant parameters from the specification spec.
260 : /// \param spec A linear process specification
261 : /// \param R A data rewriter
262 : /// \param instantiate_global_variables If true, free variables may be instantiated as a side effect of the algorithm
263 : template <typename DataRewriter, typename Specification>
264 12 : void constelm(Specification& spec, const DataRewriter& R, bool instantiate_global_variables = false)
265 : {
266 12 : constelm_algorithm<DataRewriter, Specification> algorithm(spec, R);
267 12 : algorithm.run(instantiate_global_variables);
268 12 : }
269 :
270 : } // namespace lps
271 :
272 : } // namespace mcrl2
273 :
274 : #endif // MCRL2_LPS_CONSTELM_H
|
