mCRL2
Loading...
Searching...
No Matches
multi_action.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_MULTI_ACTION_H
13#define MCRL2_LPS_MULTI_ACTION_H
14
15#include "mcrl2/core/print.h"
17
18namespace mcrl2
19{
20
21namespace lps
22{
23
24// prototype declaration
26
27//--- start generated class multi_action ---//
30{
31 public:
32
33
35 multi_action(const multi_action&) noexcept = default;
36 multi_action(multi_action&&) noexcept = default;
37 multi_action& operator=(const multi_action&) noexcept = default;
38 multi_action& operator=(multi_action&&) noexcept = default;
39
40 const process::action_list& actions() const
41 {
42 return atermpp::down_cast<process::action_list>((*this)[0]);
43 }
44
46 {
47 return atermpp::down_cast<data::data_expression>((*this)[1]);
48 }
49//--- start user section multi_action ---//
53 : atermpp::aterm_appl(core::detail::function_symbol_TimedMultAct(), actions, time)
54 {
56 }
57
60 explicit multi_action(const atermpp::aterm& term)
61 : atermpp::aterm_appl(term)
62 {
64 }
65
67 explicit multi_action(const process::action& l)
68 : multi_action(process::action_list({ l }),data::undefined_real())
69 {}
70
73 bool has_time() const
74 {
75 return time() != data::undefined_real();
76 }
77
81 {
82 assert(time() == other.time());
83 return multi_action(actions() + other.actions(), time());
84 }
85
89 {
90 if (actions().size()<=1) // There is almost always only one action.
91 {
92 return *this;
93 }
95 }
96
97 //--- end user section multi_action ---//
98};
99
102template <class... ARGUMENTS>
103inline void make_multi_action(atermpp::aterm_appl& t, const ARGUMENTS&... args)
104{
106}
107
110
112typedef std::vector<multi_action> multi_action_vector;
113
117inline
119{
121}
122
123// prototype declaration
124std::string pp(const multi_action& x);
125
130inline
131std::ostream& operator<<(std::ostream& out, const multi_action& x)
132{
133 return out << lps::pp(x);
134}
135
137inline 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
145lps::multi_action normalize_sorts(const multi_action& x, const data::sort_specification& sortspec);
147std::set<data::variable> find_all_variables(const lps::multi_action& x);
148std::set<data::variable> find_free_variables(const lps::multi_action& x);
149
151namespace detail
152{
153
159template <typename Iter, typename Function>
160void forall_permutations(Iter first, Iter last, Function f)
161{
162 if (first == last)
163 {
164 f();
165 return;
166 }
167 Iter next = first;
168 ++next;
169 forall_permutations(next, last, f);
170 while (std::next_permutation(first->first, first->second))
171 {
172 forall_permutations(next, last, f);
173 }
174}
175
181inline bool equal_action_signatures(const std::vector<process::action>& a, const std::vector<process::action>& b)
182{
183 if (a.size() != b.size())
184 {
185 return false;
186 }
187 std::vector<process::action>::const_iterator i, j;
188 for (i = a.begin(), j = b.begin(); i != a.end(); ++i, ++j)
189 {
190 if (i->label() != j->label())
191 {
192 return false;
193 }
194 }
195 return true;
196}
197
199struct compare_action_labels
200{
205 bool operator()(const process::action& a, const process::action& b) const
206 {
207 return a.label() < b.label();
208 }
209};
210
212struct compare_action_label_arguments
213{
218 bool operator()(const process::action& a, const process::action& b) const
219 {
220 if (a.label() != b.label())
221 {
222 return a.label() < b.label();
223 }
224 return a < b;
225 }
226};
227
229struct 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 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 : a(a_),
240 b(b_),
241 result(result_)
242 {}
243
245 void operator()()
246 {
247 std::vector<data::data_expression> v;
248 std::vector<process::action>::const_iterator i, j;
249 for (i = a.begin(), j = b.begin(); i != a.end(); ++i, ++j)
250 {
251 data::data_expression_list d1 = i->arguments();
252 data::data_expression_list d2 = j->arguments();
253 assert(d1.size() == d2.size());
254 data::data_expression_list::iterator i1 = d1.begin(), i2 = d2.begin();
255 for ( ; i1 != d1.end(); ++i1, ++i2)
256 {
257 v.push_back(data::lazy::equal_to(*i1, *i2));
258 }
259 }
260 data::data_expression expr = data::lazy::join_and(v.begin(), v.end());
261 result.insert(expr);
262 }
263};
264
266struct 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
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
305
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 std::vector<process::action> va(a.actions().begin(), a.actions().end()); // protection not needed
322 std::vector<process::action> vb(b.actions().begin(), b.actions().end()); // protection not needed
323 std::sort(va.begin(), va.end(), detail::compare_action_label_arguments());
324 std::sort(vb.begin(), vb.end(), detail::compare_action_label_arguments());
325
326 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
334 }
335
336 // compute the intervals of a with equal names
337 typedef std::vector<process::action>::iterator action_iterator;
338 std::vector<std::pair<action_iterator, action_iterator> > intervals;
339 action_iterator first = va.begin();
340 while (first != va.end())
341 {
342 action_iterator next = std::upper_bound(first, va.end(), *first, detail::compare_action_labels());
343 intervals.push_back(std::make_pair(first, next));
344 first = next;
345 }
346
347 std::set<data::data_expression> z;
348 detail::equal_data_parameters_builder f(va, vb, z);
349 detail::forall_permutations(intervals.begin(), intervals.end(), f);
350 data::data_expression result = data::lazy::join_or(z.begin(), z.end());
351 return result;
352}
353
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
395namespace std
396{
398template<>
399struct hash< mcrl2::lps::multi_action >
400{
401 std::size_t operator()(const mcrl2::lps::multi_action& ma) const
402 {
403 std::hash<atermpp::aterm> hasher;
404 return hasher(ma.actions()) ^ (hasher(ma.time())<<1);
405 }
406};
407
408} // namespace std
409
410#endif // MCRL2_LPS_MULTI_ACTION_H
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
size_type size() const
Returns the number of arguments of this term.
Definition aterm_appl.h:181
const function_symbol & function() const
Returns the function symbol belonging to an aterm_appl.
Definition aterm_appl.h:174
A list of aterm objects.
Definition aterm_list.h:23
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:281
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:274
void swap(unprotected_aterm &t) noexcept
Swaps this term with its argument.
Definition aterm.h:156
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
const_iterator end() const
const_iterator begin() const
\brief A timed multi-action
multi_action(const multi_action &) noexcept=default
Move semantics.
multi_action(const atermpp::aterm &term)
Constructor.
bool has_time() const
Returns true if time is available.
const process::action_list & actions() const
multi_action(const process::action &l)
Constructor.
multi_action operator+(const multi_action &other) const
Joins the actions of both multi actions.
multi_action sort_actions() const
Returns the multiaction in which the list of actions is sorted.
const data::data_expression & time() const
multi_action(multi_action &&) noexcept=default
multi_action(const process::action_list &actions=process::action_list(), data::data_expression time=data::undefined_real())
Constructor.
Functions for pretty printing ATerms.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
The main namespace for the aterm++ library.
Definition algorithm.h:21
term_list< Term > sort_list(const term_list< Term > &l, const std::function< bool(const Term &, const Term &)> &ordering=[](const Term &t1, const Term &t2){ return t1< t2;})
Returns the list with the elements sorted according to the <-operator on the addresses of terms.
void make_term_appl(Term &target, const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
Constructor an aterm_appl in a variable based on a function symbol and an forward iterator providing ...
Definition aterm_appl.h:239
const atermpp::function_symbol & function_symbol_TimedMultAct()
bool check_term_TimedMultAct(const Term &t)
data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns and applied to the sequence of data expressions [first, last)
data_expression join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)
Returns or applied to the sequence of data expressions [first, last)
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real.h:58
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:62
std::vector< multi_action > multi_action_vector
\brief vector of multi_actions
void make_multi_action(atermpp::aterm_appl &t, const ARGUMENTS &... args)
std::string pp(const action_summand &x)
Definition lps.cpp:26
std::ostream & operator<<(std::ostream &out, const action_summand &x)
atermpp::term_list< multi_action > multi_action_list
\brief list of multi_actions
lps::multi_action normalize_sorts(const multi_action &x, const data::sort_specification &sortspec)
Definition lps.cpp:38
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
void swap(action_summand &t1, action_summand &t2)
\brief swap overload
data::data_expression equal_multi_actions(const multi_action &a, const multi_action &b)
Returns a data expression that expresses under which conditions the multi actions a and b are equal....
data::data_expression not_equal_multi_actions(const multi_action &a, const multi_action &b)
Returns a pbes expression that expresses under which conditions the multi actions a and b are not equ...
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:48
lps::multi_action translate_user_notation(const lps::multi_action &x)
Definition lps.cpp:41
bool is_multi_action(const atermpp::aterm_appl &x)
std::string pp(const action_label &x)
Definition process.cpp:36
atermpp::term_list< action > action_list
\brief list of actions
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
add your file description here.
static const atermpp::function_symbol TimedMultAct
std::size_t operator()(const mcrl2::lps::multi_action &ma) const
#define hash(l, r, m)
Definition tree_set.cpp:23