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/multi_action.h
10 : /// \brief Multi-action class.
11 :
12 : #ifndef MCRL2_LPS_MULTI_ACTION_H
13 : #define MCRL2_LPS_MULTI_ACTION_H
14 :
15 : #include "mcrl2/core/print.h"
16 : #include "mcrl2/process/process_expression.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace lps
22 : {
23 :
24 : // prototype declaration
25 : bool is_multi_action(const atermpp::aterm_appl& x);
26 :
27 : //--- start generated class multi_action ---//
28 : /// \\brief A timed multi-action
29 : class multi_action: public atermpp::aterm_appl
30 : {
31 : public:
32 :
33 :
34 : /// Move semantics
35 87026 : multi_action(const multi_action&) noexcept = default;
36 73464 : multi_action(multi_action&&) noexcept = default;
37 9139 : multi_action& operator=(const multi_action&) noexcept = default;
38 1692 : multi_action& operator=(multi_action&&) noexcept = default;
39 :
40 139702 : const process::action_list& actions() const
41 : {
42 139702 : return atermpp::down_cast<process::action_list>((*this)[0]);
43 : }
44 :
45 389189 : const data::data_expression& time() const
46 : {
47 389189 : return atermpp::down_cast<data::data_expression>((*this)[1]);
48 : }
49 : //--- start user section multi_action ---//
50 : /// \brief Constructor
51 47394 : explicit multi_action(const process::action_list& actions = process::action_list(),
52 : data::data_expression time = data::undefined_real())
53 47394 : : atermpp::aterm_appl(core::detail::function_symbol_TimedMultAct(), actions, time)
54 : {
55 47394 : assert(data::sort_real::is_real(time.sort()));
56 47394 : }
57 :
58 : /// \brief Constructor.
59 : /// \param term A term
60 4 : explicit multi_action(const atermpp::aterm& term)
61 4 : : atermpp::aterm_appl(term)
62 : {
63 4 : assert(core::detail::check_term_TimedMultAct(*this));
64 4 : }
65 :
66 : /// \brief Constructor
67 419 : explicit multi_action(const process::action& l)
68 838 : : multi_action(process::action_list({ l }),data::undefined_real())
69 419 : {}
70 :
71 : /// \brief Returns true if time is available.
72 : /// \return True if time is available.
73 170482 : bool has_time() const
74 : {
75 170482 : return time() != data::undefined_real();
76 : }
77 :
78 : /// \brief Joins the actions of both multi actions.
79 : /// \pre The time of both multi actions must be equal.
80 2 : multi_action operator+(const multi_action& other) const
81 : {
82 2 : assert(time() == other.time());
83 4 : return multi_action(actions() + other.actions(), time());
84 : }
85 :
86 : /// \brief Returns the multiaction in which the list of actions is sorted.
87 : /// \return A multi-action with a sorted list.
88 2346 : multi_action sort_actions() const
89 : {
90 2346 : if (actions().size()<=1) // There is almost always only one action.
91 : {
92 2334 : return *this;
93 : }
94 24 : return multi_action(atermpp::sort_list(actions()),time());
95 : }
96 :
97 : //--- end user section multi_action ---//
98 : };
99 :
100 : /// \\brief Make_multi_action constructs a new term into a given address.
101 : /// \\ \param t The reference into which the new multi_action is constructed.
102 : template <class... ARGUMENTS>
103 4973 : inline void make_multi_action(atermpp::aterm_appl& t, const ARGUMENTS&... args)
104 : {
105 4973 : atermpp::make_term_appl(t, core::detail::function_symbol_TimedMultAct(), args...);
106 4973 : }
107 :
108 : /// \\brief list of multi_actions
109 : typedef atermpp::term_list<multi_action> multi_action_list;
110 :
111 : /// \\brief vector of multi_actions
112 : typedef std::vector<multi_action> multi_action_vector;
113 :
114 : /// \\brief Test for a multi_action expression
115 : /// \\param x A term
116 : /// \\return True if \\a x is a multi_action expression
117 : inline
118 860 : bool is_multi_action(const atermpp::aterm_appl& x)
119 : {
120 860 : return x.function() == core::detail::function_symbols::TimedMultAct;
121 : }
122 :
123 : // prototype declaration
124 : std::string pp(const multi_action& x);
125 :
126 : /// \\brief Outputs the object to a stream
127 : /// \\param out An output stream
128 : /// \\param x Object x
129 : /// \\return The output stream
130 : inline
131 6 : std::ostream& operator<<(std::ostream& out, const multi_action& x)
132 : {
133 6 : return out << lps::pp(x);
134 : }
135 :
136 : /// \\brief swap overload
137 : inline void swap(multi_action& t1, multi_action& t2)
138 : {
139 : t1.swap(t2);
140 : }
141 : //--- end generated class multi_action ---//
142 :
143 :
144 : // template function overloads
145 : lps::multi_action normalize_sorts(const multi_action& x, const data::sort_specification& sortspec);
146 : lps::multi_action translate_user_notation(const lps::multi_action& x);
147 : std::set<data::variable> find_all_variables(const lps::multi_action& x);
148 : std::set<data::variable> find_free_variables(const lps::multi_action& x);
149 :
150 : /// \cond INTERNAL_DOCS
151 : namespace detail
152 : {
153 :
154 : /// \brief Visits all permutations of the arrays, and calls f for each instance.
155 : /// \pre The range [first, last) contains sorted arrays.
156 : /// \param first Start of a sequence of arrays
157 : /// \param last End of a sequence of arrays
158 : /// \param f A function
159 : template <typename Iter, typename Function>
160 1250 : void forall_permutations(Iter first, Iter last, Function f)
161 : {
162 1250 : if (first == last)
163 : {
164 684 : f();
165 684 : return;
166 : }
167 566 : Iter next = first;
168 566 : ++next;
169 566 : forall_permutations(next, last, f);
170 572 : while (std::next_permutation(first->first, first->second))
171 : {
172 6 : forall_permutations(next, last, f);
173 : }
174 : }
175 :
176 : /// \brief Returns true if the actions in a and b have the same names, and the same sorts.
177 : /// \pre a and b are sorted w.r.t. to the names of the actions.
178 : /// \param a A sequence of actions
179 : /// \param b A sequence of actions
180 : /// \return True if the actions in a and b have the same names, and the same sorts.
181 3021 : inline bool equal_action_signatures(const std::vector<process::action>& a, const std::vector<process::action>& b)
182 : {
183 3021 : if (a.size() != b.size())
184 : {
185 223 : return false;
186 : }
187 2798 : std::vector<process::action>::const_iterator i, j;
188 3371 : for (i = a.begin(), j = b.begin(); i != a.end(); ++i, ++j)
189 : {
190 2693 : if (i->label() != j->label())
191 : {
192 2120 : return false;
193 : }
194 : }
195 678 : return true;
196 : }
197 :
198 : /// \brief Compares action labels
199 : struct compare_action_labels
200 : {
201 : /// \brief Function call operator
202 : /// \param a An action
203 : /// \param b An action
204 : /// \return The function result
205 566 : bool operator()(const process::action& a, const process::action& b) const
206 : {
207 566 : return a.label() < b.label();
208 : }
209 : };
210 :
211 : /// \brief Compares action labels and arguments
212 : struct compare_action_label_arguments
213 : {
214 : /// \brief Function call operator
215 : /// \param a An action
216 : /// \param b An action
217 : /// \return The function result
218 36 : bool operator()(const process::action& a, const process::action& b) const
219 : {
220 36 : if (a.label() != b.label())
221 : {
222 4 : return a.label() < b.label();
223 : }
224 32 : return a < b;
225 : }
226 : };
227 :
228 : /// \brief Used for building an expression for the comparison of data parameters.
229 : struct equal_data_parameters_builder
230 : {
231 : const std::vector<process::action>& a;
232 : const std::vector<process::action>& b;
233 : std::set<data::data_expression>& result;
234 :
235 678 : equal_data_parameters_builder(const std::vector<process::action>& a_,
236 : const std::vector<process::action>& b_,
237 : std::set<data::data_expression>& result_
238 : )
239 678 : : a(a_),
240 678 : b(b_),
241 678 : result(result_)
242 678 : {}
243 :
244 : /// \brief Adds the expression 'a == b' to result.
245 684 : void operator()()
246 : {
247 684 : std::vector<data::data_expression> v;
248 684 : std::vector<process::action>::const_iterator i, j;
249 1270 : for (i = a.begin(), j = b.begin(); i != a.end(); ++i, ++j)
250 : {
251 586 : data::data_expression_list d1 = i->arguments();
252 586 : data::data_expression_list d2 = j->arguments();
253 586 : assert(d1.size() == d2.size());
254 586 : data::data_expression_list::iterator i1 = d1.begin(), i2 = d2.begin();
255 909 : for ( ; i1 != d1.end(); ++i1, ++i2)
256 : {
257 323 : v.push_back(data::lazy::equal_to(*i1, *i2));
258 : }
259 586 : }
260 684 : data::data_expression expr = data::lazy::join_and(v.begin(), v.end());
261 684 : result.insert(expr);
262 684 : }
263 : };
264 :
265 : /// \brief Used for building an expression for the comparison of data parameters.
266 : struct not_equal_multi_actions_builder
267 : {
268 : const std::vector<process::action>& a;
269 : const std::vector<process::action>& b;
270 : std::vector<data::data_expression>& result;
271 :
272 : not_equal_multi_actions_builder(const std::vector<process::action>& a_,
273 : const std::vector<process::action>& b_,
274 : std::vector<data::data_expression>& result_
275 : )
276 : : a(a_),
277 : b(b_),
278 : result(result_)
279 : {}
280 :
281 : /// \brief Adds the expression 'a == b' to result.
282 : void operator()()
283 : {
284 : using namespace data::lazy;
285 :
286 : std::vector<data::data_expression> v;
287 : std::vector<process::action>::const_iterator i, j;
288 : for (i = a.begin(), j = b.begin(); i != a.end(); ++i, ++j)
289 : {
290 : data::data_expression_list d1 = i->arguments();
291 : data::data_expression_list d2 = j->arguments();
292 : assert(d1.size() == d2.size());
293 : data::data_expression_list::iterator i1=d1.begin(), i2=d2.begin();
294 : for ( ; i1 != d1.end(); ++i1, ++i2)
295 : {
296 : v.push_back(data::not_equal_to(*i1, *i2));
297 : }
298 : }
299 : result.push_back(data::lazy::join_or(v.begin(), v.end()));
300 : }
301 : };
302 :
303 : } // namespace detail
304 : /// \endcond
305 :
306 : /// \brief Returns a data expression that expresses under which conditions the
307 : /// multi actions a and b are equal. The multi actions may contain free variables.
308 : /// \param a A sequence of actions
309 : /// \param b A sequence of actions
310 : /// \return Necessary conditions for the equality of a and b
311 3021 : inline data::data_expression equal_multi_actions(const multi_action& a, const multi_action& b)
312 : {
313 : #ifdef MCRL2_EQUAL_MULTI_ACTIONS_DEBUG
314 : mCRL2log(debug) << "\n<equal multi actions>" << std::endl;
315 : mCRL2log(debug) << "a = " << process::pp(a.actions()) << std::endl;
316 : mCRL2log(debug) << "b = " << process::pp(b.actions()) << std::endl;
317 : #endif
318 : using namespace data::lazy;
319 :
320 : // make copies of a and b and sort them
321 3021 : std::vector<process::action> va(a.actions().begin(), a.actions().end()); // protection not needed
322 3021 : std::vector<process::action> vb(b.actions().begin(), b.actions().end()); // protection not needed
323 3021 : std::sort(va.begin(), va.end(), detail::compare_action_label_arguments());
324 3021 : std::sort(vb.begin(), vb.end(), detail::compare_action_label_arguments());
325 :
326 3021 : if (!detail::equal_action_signatures(va, vb))
327 : {
328 : #ifdef MCRL2_EQUAL_MULTI_ACTIONS_DEBUG
329 : mCRL2log(debug) << "different action signatures detected!" << std::endl;
330 : mCRL2log(debug) << "a = " << process::action_list(va.begin(), va.end()) << std::endl;
331 : mCRL2log(debug) << "b = " << process::action_list(vb.begin(), vb.end()) << std::endl;
332 : #endif
333 2343 : return data::sort_bool::false_();
334 : }
335 :
336 : // compute the intervals of a with equal names
337 : typedef std::vector<process::action>::iterator action_iterator;
338 678 : std::vector<std::pair<action_iterator, action_iterator> > intervals;
339 678 : action_iterator first = va.begin();
340 1243 : while (first != va.end())
341 : {
342 565 : action_iterator next = std::upper_bound(first, va.end(), *first, detail::compare_action_labels());
343 565 : intervals.push_back(std::make_pair(first, next));
344 565 : first = next;
345 : }
346 :
347 678 : std::set<data::data_expression> z;
348 678 : detail::equal_data_parameters_builder f(va, vb, z);
349 678 : detail::forall_permutations(intervals.begin(), intervals.end(), f);
350 678 : data::data_expression result = data::lazy::join_or(z.begin(), z.end());
351 678 : return result;
352 3021 : }
353 :
354 : /// \brief Returns a pbes expression that expresses under which conditions the
355 : /// multi actions a and b are not equal. The multi actions may contain free variables.
356 : /// \param a A sequence of actions
357 : /// \param b A sequence of actions
358 : /// \return Necessary conditions for the inequality of a and b
359 : inline data::data_expression not_equal_multi_actions(const multi_action& a, const multi_action& b)
360 : {
361 : using namespace data::lazy;
362 :
363 : // make copies of a and b and sort them
364 : std::vector<process::action> va(a.actions().begin(), a.actions().end());
365 : std::vector<process::action> vb(b.actions().begin(), b.actions().end());
366 : std::sort(va.begin(), va.end(), detail::compare_action_label_arguments());
367 : std::sort(vb.begin(), vb.end(), detail::compare_action_label_arguments());
368 :
369 : if (!detail::equal_action_signatures(va, vb))
370 : {
371 : return data::sort_bool::true_();
372 : }
373 :
374 : // compute the intervals of a with equal names
375 : typedef std::vector<process::action>::iterator action_iterator;
376 : std::vector<std::pair<action_iterator, action_iterator> > intervals;
377 : action_iterator first = va.begin();
378 : while (first != va.end())
379 : {
380 : action_iterator next = std::upper_bound(first, va.end(), *first, detail::compare_action_labels());
381 : intervals.push_back(std::make_pair(first, next));
382 : first = next;
383 : }
384 : std::vector<data::data_expression> z;
385 : detail::not_equal_multi_actions_builder f(va, vb, z);
386 : detail::forall_permutations(intervals.begin(), intervals.end(), f);
387 : data::data_expression result = data::lazy::join_and(z.begin(), z.end());
388 : return result;
389 : }
390 :
391 : } // namespace lps
392 :
393 : } // namespace mcrl2
394 :
395 : namespace std
396 : {
397 : /// \brief specialization of the standard std::hash function for an action_label_string.
398 : template<>
399 : struct hash< mcrl2::lps::multi_action >
400 : {
401 7545 : std::size_t operator()(const mcrl2::lps::multi_action& ma) const
402 : {
403 : std::hash<atermpp::aterm> hasher;
404 7545 : return hasher(ma.actions()) ^ (hasher(ma.time())<<1);
405 : }
406 : };
407 :
408 : } // namespace std
409 :
410 : #endif // MCRL2_LPS_MULTI_ACTION_H
|
