mCRL2
Loading...
Searching...
No Matches
typecheck.h
Go to the documentation of this file.
1// Author(s): Jan Friso Groote
2// Wieger Wesselink 2015 -
3// Copyright: see the accompanying file COPYING or copy at
4// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
5//
6// Distributed under the Boost Software License, Version 1.0.
7// (See accompanying file LICENSE_1_0.txt or copy at
8// http://www.boost.org/LICENSE_1_0.txt)
9//
12
13#ifndef MCRL2_PROCESS_TYPECHECK_H
14#define MCRL2_PROCESS_TYPECHECK_H
15
16#include <algorithm>
20
21namespace mcrl2
22{
23
24namespace process
25{
26
27inline
29 const data::data_expression_list& parameters,
30 data::data_type_checker& typechecker,
31 const data::detail::variable_context& variable_context,
32 const detail::action_context& action_context
33 )
34{
35 std::string msg = "action";
36 data::sorts_list parameter_list = action_context.matching_action_sorts(name, parameters);
37 auto p = process::detail::match_action_parameters(parameters, parameter_list, variable_context, name, msg, typechecker);
38 return action(action_label(name, p.second), p.first);
39}
40
41// returns the intersection of the 2 type list lists
42inline
44{
45 data::sorts_list result;
46 for (const data::sort_expression_list& s: sorts2)
47 {
48 if (std::find(sorts1.begin(), sorts1.end(), s) != sorts1.end())
49 {
50 result.push_front(s);
51 }
52 }
53 return atermpp::reverse(result);
54}
55
56inline
57std::ostream& operator<<(std::ostream& out, const data::sorts_list& x)
58{
59 out << "[";
60 for (auto i = x.begin(); i != x.end(); ++i)
61 {
62 if (i != x.begin())
63 {
64 out << ", ";
65 }
66 out << *i;
67 }
68 return out;
69}
70
71namespace detail
72{
73
75
76// returns true if a is in A
77inline
79{
80 for (const action_name_multiset& i: A)
81 {
82 if (equal_multi_actions(a, i.names()))
83 {
84 return true;
85 }
86 }
87 return false;
88}
89
90// returns true if the two multiactions are equal.
91inline
93{
94 if (a1.size() != a2.size())
95 {
96 return false;
97 }
98 if (a1.empty())
99 {
100 return true;
101 }
102 core::identifier_string Act1 = a1.front();
103 a1 = a1.tail();
104
105 //remove Act1 once from a2. if not there -- return ATfalse.
107 for (; !a2.empty(); a2 = a2.tail())
108 {
109 core::identifier_string Act2 = a2.front();
110 if (Act1 == Act2)
111 {
112 a2 = atermpp::reverse(NewMAct2) + a2.tail();
113 return equal_multi_actions(a1, a2);
114 }
115 else
116 {
117 NewMAct2.push_front(Act2);
118 }
119 }
120 return false;
121}
122
123inline
124std::ostream& operator<<(std::ostream& out, const std::pair<core::identifier_string, data::sort_expression_list>& x)
125{
126 return out << "(" << x.first << ", " << x.second << ")";
127}
128
129struct typecheck_builder: public process_expression_builder<typecheck_builder>
130{
132 using super::apply;
133
139
141 const data::detail::variable_context& variable_context,
144 const process_identifier* current_equation = nullptr
145 )
146 : m_data_type_checker(data_typechecker),
147 m_variable_context(variable_context),
150 m_current_equation(current_equation)
151 {}
152
154 {
156 }
157
159 {
161 {
162 throw mcrl2::runtime_error("Undefined action " + core::pp(a) + " (typechecking " + core::pp(x) + ")");
163 }
164 }
165
167 {
168 std::set<core::identifier_string> actions;
169 for (const core::identifier_string& a: act_list)
170 {
172 if (!actions.insert(a).second) // The action was already in the set.
173 {
174 mCRL2log(log::warning) << "Used action " << a << " twice (typechecking " << x << ")" << std::endl;
175 }
176 }
177 }
178
179 template <typename Container>
180 void check_not_empty(const Container& c, const std::string& msg, const process_expression& x)
181 {
182 if (c.empty())
183 {
184 mCRL2log(log::warning) << msg << " (typechecking " << x << ")" << std::endl;
185 }
186 }
187
188 template <typename T>
189 void check_not_equal(const T& first, const T& second, const std::string& msg, const process_expression& x)
190 {
191 if (first == second)
192 {
193 mCRL2log(log::warning) << msg << " " << first << "(typechecking " << x << ")" << std::endl;
194 }
195 }
196
198 {
199 std::set<data::sort_expression_list> v1(s1.begin(), s1.end());
200 std::set<data::sort_expression_list> v2(s2.begin(), s2.end());
202 }
203
205 {
207 {
208 throw mcrl2::runtime_error("renaming action " + core::pp(a) + " into action " + core::pp(b) + ": these two have no common type (typechecking " + process::pp(x) + ")");
209 }
210 }
211
212 static std::map<core::identifier_string, data::data_expression> make_assignment_map(const data::untyped_identifier_assignment_list& assignments)
213 {
214 std::map<core::identifier_string, data::data_expression> result;
215 for (const data::untyped_identifier_assignment& a: assignments)
216 {
217 auto i = result.find(a.lhs());
218 if (i != result.end()) // An data::assignment of the shape x := t already exists, this is not OK.
219 {
220 throw mcrl2::runtime_error("Double data::assignment to data::variable " + core::pp(a.lhs()) + " (detected assigned values are " + data::pp(i->second) + " and " + core::pp(a.rhs()) + ")");
221 }
222 result[a.lhs()]=a.rhs();
223 }
224 return result;
225 }
226
228 {
229 return m_action_context.is_declared(name);
230 }
231
233 {
234 return m_process_context.is_declared(name);
235 }
236
238 {
240 }
241
243 {
244 std::string msg = "process";
245 data::sorts_list parameter_list = m_process_context.matching_process_sorts(name, parameters);
246 auto p = process::detail::match_action_parameters(parameters, parameter_list, m_variable_context, name, msg, m_data_type_checker);
247 return m_process_context.make_process_instance(name, p.second, p.first);
248 }
249
251 {
252 if (x.assignments().empty())
253 {
254 return core::pp(x.name()) + "()";
255 }
256 else
257 {
259 }
260 }
261
262 // Checks if in the equation P(..) = Q(assignments) all formal parameters of Q have been assigned a value,
263 // either directly via an assignment in assignments, or indirectly via a formal parameter of P.
264 void check_assignments(const process_identifier& P, const process_identifier& Q, const std::vector<data::assignment>& assignments, const untyped_process_assignment& x) const
265 {
266 std::set<data::variable> Q_variables;
267 for (const data::assignment& a: assignments)
268 {
269 Q_variables.insert(a.lhs());
270 }
271 for (const data::variable& v: P.variables())
272 {
273 Q_variables.insert(v);
274 }
275 for (const data::variable& v: Q.variables())
276 {
277 if (Q_variables.find(v) == Q_variables.end())
278 {
279 throw mcrl2::runtime_error("Process parameter " + core::pp(v.name()) + " has not been assigned a value in the process call with short-hand assignments " + print_untyped_process_assignment(x) + ".");
280 }
281 }
282 }
283
284 template <class T>
285 void apply(T& result, const untyped_process_assignment& x)
286 {
287 mCRL2log(log::debug) << "typechecking a process call with short-hand assignments " << x << "" << std::endl;
288 if (!is_process_name(x.name()))
289 {
290 throw mcrl2::runtime_error("Could not find a matching declaration for action or process expression " + print_untyped_process_assignment(x) + ".");
291 }
292
294 const data::variable_list& formal_parameters = P.variables();
295
296 // This checks for duplicate left hand sides.
297 std::map<core::identifier_string, data::data_expression> assignment_map = make_assignment_map(x.assignments());
298
299 std::map<core::identifier_string, data::variable> formal_parameter_map;
300 for (const data::variable& v: formal_parameters)
301 {
302 formal_parameter_map[v.name()] = v;
303 }
304
305 // Typecheck the right hand sides of the assignments
306 std::vector<data::assignment> assignments;
308 {
309 try
310 {
311 data::variable v = formal_parameter_map[a.lhs()];
312 formal_parameter_map.erase(v.name());
314 assignments.emplace_back(v, e);
315 }
316 catch (const mcrl2::runtime_error& e)
317 {
318 throw mcrl2::runtime_error(std::string(e.what()) + "\nType error occurred while typechecking the process call with short-hand assignments " + process::pp(x));
319 }
320 }
321
322 // Check if all formal parameters have been assigned a value
324 {
325 check_assignments(*m_current_equation, P, assignments, x);
326 }
327
328 // Check that for any non explicitly stated assignment x:=x, the rhs is well defined.
329 for (const auto& [name, var]: formal_parameter_map)
330 {
331 try
332 {
334 }
335 catch (const mcrl2::runtime_error& e)
336 {
337 throw mcrl2::runtime_error(std::string(e.what()) + "\nIn implicitly stated assignment " + pp(var) + "=" + pp(var) + " in process " + pp(P) + "(" + data::pp(assignments) + ")\n");
338 }
339 }
340
341 make_process_instance_assignment(result, P, data::assignment_list(assignments.begin(), assignments.end()));
342 }
343
344 template <class T>
345 void apply(T& result, const data::untyped_data_parameter& x)
346 {
347 if (is_action_name(x.name()))
348 {
349 result = typecheck_action(x.name(), x.arguments());
350 }
351 else if (is_process_name(x.name()))
352 {
353 result = typecheck_process_instance(x.name(), x.arguments());
354 }
355 else
356 {
357 throw mcrl2::runtime_error("Could not find a matching declaration for action or process expression " + core::pp(x.name()) + core::detail::print_arguments(x.arguments()) + ".");
358 }
359 }
360
361 // This case is necessary for actionrename
362 template <class T>
363 void apply(T& result, const process::action& x)
364 {
365 result = typecheck_action(x.label().name(), x.arguments());
366 }
367
368 template <class T>
369 void apply(T& result, const process::hide& x)
370 {
371 check_not_empty(x.hide_set(), "Hiding empty set of actions", x);
373 process::make_hide(result,
374 x.hide_set(),
375 [&](process_expression& result){ (*this).apply(result, x.operand()); } );
376 }
377
378 template <class T>
379 void apply(T& result, const process::block& x)
380 {
381 check_not_empty(x.block_set(), "Blocking empty set of actions", x);
383 make_block(result, x.block_set(), [&]( process_expression& result){ (*this).apply(result, x.operand()); });
384 }
385
386 template <class T>
387 void apply(T& result, const process::rename& x)
388 {
389 check_not_empty(x.rename_set(), "Renaming empty set of actions", x);
390
391 std::set<core::identifier_string> actions;
392 for (const rename_expression& r: x.rename_set())
393 {
394 check_not_equal(r.source(), r.target(), "Renaming action into itself:", x);
395 check_action_declared(r.source(), x);
396 check_action_declared(r.target(), x);
397 check_rename_common_type(r.source(), r.target(), x);
398 if (!actions.insert(r.source()).second) // The element was already in the set.
399 {
400 throw mcrl2::runtime_error("renaming action " + core::pp(r.source()) + " twice (typechecking " + process::pp(x) + ")");
401 }
402 }
403 make_rename(result, x.rename_set(), [&](process_expression& r){ (*this).apply(r, x.operand()); } );
404 }
405
406 //comm: like renaming multiactions (with the same parameters) to action/tau
407 template <class T>
408 void apply(T& result, const process::comm& x)
409 {
410 check_not_empty(x.comm_set(), "synchronizing empty set of (multi)actions", x);
411
412 std::multiset<core::identifier_string> left_hand_side_actions;
413 for (const communication_expression& c: x.comm_set())
414 {
415 const core::identifier_string_list& cnames = c.action_name().names();
416 assert(!cnames.empty());
417
418 if (cnames.size() == 1)
419 {
420 throw mcrl2::runtime_error("using synchronization as renaming/hiding of action " + core::pp(cnames.front()) + " into " + core::pp(c.name()) + " (typechecking " + process::pp(x) + ")");
421 }
422
423 //Actions must be declared
424 data::sorts_list c_sorts;
425 if (!m_action_context.is_declared(c.name()))
426 {
427 throw mcrl2::runtime_error("synchronizing to an undefined action " + core::pp(c.name()) + " (typechecking " + process::pp(x) + ")");
428 }
429 c_sorts = action_sorts(c.name());
430
431 for (const core::identifier_string& a: cnames)
432 {
434 {
435 throw mcrl2::runtime_error("synchronizing an undefined action " + core::pp(a) + " in (multi)action " + core::pp(cnames) + " (typechecking " + process::pp(x) + ")");
436 }
437 c_sorts = sorts_list_intersection(c_sorts, action_sorts(a));
438 if (c_sorts.empty())
439 {
440 throw mcrl2::runtime_error("synchronizing action " + core::pp(a) + " from (multi)action " + core::pp(cnames) +
441 " into action " + core::pp(c.name()) + ": these have no common type (typechecking " + process::pp(x) + ")");
442 }
443 }
444
445 //the multiactions in the lhss of comm should not intersect.
446 //but there can be multiple of the same actions in cnames.
447 std::set < core::identifier_string > this_left_hand_sides;
448 for (const core::identifier_string& a: cnames)
449 {
450 if (this_left_hand_sides.count(a)==0 && left_hand_side_actions.find(a) != left_hand_side_actions.end())
451 {
452 throw mcrl2::runtime_error("synchronizing action " + core::pp(a) + " in different ways (typechecking " + process::pp(x) + ")");
453 }
454 else
455 {
456 left_hand_side_actions.insert(a);
457 this_left_hand_sides.insert(a);
458 }
459 }
460 }
461
462 //the multiactions in the rhs of comm should not intersect with an action in the a lhs of
463 //all other rules. So, {a|a->a} is allowed, but {a|b->c, c|a->d} is not.
464 for (const communication_expression& c: x.comm_set())
465 {
466 // Count how many actions in the rhs occur at the left
467 std::size_t number_of_rhs_in_lhs=0;
468 for (const core::identifier_string& lhs_action: c.action_name().names())
469 {
470 if (lhs_action==c.name())
471 {
472 number_of_rhs_in_lhs++;
473 }
474 }
475 assert(left_hand_side_actions.count(c.name())>=number_of_rhs_in_lhs);
476 if (left_hand_side_actions.count(c.name())-number_of_rhs_in_lhs>0) // There are more actions x.name() in the lhss than just in this lhs.
477 {
478 throw mcrl2::runtime_error("action " + core::pp(c.name()) +
479 " occurs at the left and the right in a communication (typechecking " + process::pp(x) + ")");
480 }
481 }
482 make_comm(result, x.comm_set(), [&](process_expression& r){ (*this).apply(r, x.operand()); } );
483 }
484
485 template <class T>
486 void apply(T& result, const process::allow& x)
487 {
488 check_not_empty(x.allow_set(), "Allowing empty set of (multi) actions", x);
490 for (const action_name_multiset& A: x.allow_set())
491 {
492 //Actions must be declared
493 for (const core::identifier_string& a: A.names())
494 {
496 {
497 throw mcrl2::runtime_error("allowing an undefined action " + core::pp(a) + " in (multi)action " + core::pp(A.names()) + " (typechecking " + process::pp(x) + ")");
498 }
499 }
500 if (multi_actions_contains(A.names(), MActs))
501 {
502 mCRL2log(log::warning) << "allowing (multi)action " << A.names() << " twice (typechecking " << x << ")" << std::endl;
503 }
504 else
505 {
507 }
508 }
509 make_allow(result, x.allow_set(), [&](process_expression& r){ (*this).apply(r, x.operand()); } );
510 }
511
512 template <class T>
513 void apply(T& result, const process::at& x)
514 {
516 make_at(result, [&](process_expression& r){ (*this).apply(r, x.operand()); }, new_time);
517 }
518
519 template <class T>
520 void apply(T& result, const process::if_then& x)
521 {
523 make_if_then(result, condition, [&](process_expression& r){ (*this).apply(r, x.then_case()); } );
524 }
525
526 template <class T>
527 void apply(T& result, const process::if_then_else& x)
528 {
530 make_if_then_else(result,
531 condition,
532 [&](process_expression& r){ (*this).apply(r, x.then_case()); },
533 [&](process_expression& r){ (*this).apply(r, x.else_case()); } );
534 }
535
536 template <class T>
537 void apply(T& result, const process::sum& x)
538 {
539 try
540 {
541 auto m_variable_context_copy = m_variable_context;
543 process_expression operand;
544 (*this).apply(operand, x.operand());
545 m_variable_context = m_variable_context_copy;
546 make_sum(result, x.variables(), operand);
547 }
548 catch (mcrl2::runtime_error& e)
549 {
550 throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + process::pp(x));
551 }
552 }
553
554 template <class T>
555 void apply(T& result, const process::stochastic_operator& x)
556 {
557 try
558 {
559 auto m_variable_context_copy = m_variable_context;
562 process_expression operand;
563 (*this).apply(operand, x.operand());
564 m_variable_context = m_variable_context_copy;
565 make_stochastic_operator(result, x.variables(), distribution, operand);
566 }
567 catch (mcrl2::runtime_error& e)
568 {
569 throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + process::pp(x));
570 }
571 }
572};
573
574inline
576 data::data_type_checker& data_typechecker,
577 const data::detail::variable_context& variables,
578 const detail::process_context& process_identifiers,
580 const process_identifier* current_equation = nullptr
581 )
582{
583 return typecheck_builder(data_typechecker, variables, process_identifiers, action_context, current_equation);
584}
585
586} // namespace detail
587
589{
590 protected:
595
596 static std::vector<process_identifier> equation_identifiers(const std::vector<process_equation>& equations)
597 {
598 std::vector<process_identifier> result;
599 for (const process_equation& eqn: equations)
600 {
601 result.push_back(eqn.identifier());
602 }
603 return result;
604 }
605
606 public:
607 template <typename VariableContainer, typename ActionLabelContainer, typename ProcessIdentifierContainer>
609 const VariableContainer& variables,
610 const ActionLabelContainer& action_labels,
611 const ProcessIdentifierContainer& process_identifiers
612 )
613 : m_data_type_checker(dataspec)
614 {
618 }
619
622 : m_data_type_checker(dataspec)
623 {}
624
630 process_expression operator()(const process_expression& x, const process_identifier* current_equation = nullptr)
631 {
633 }
634
637 {
638 mCRL2log(log::verbose) << "type checking process specification..." << std::endl;
639
640 // reset the context
642
644
651
652 // typecheck the equations
653 for (process_equation& eqn: procspec.equations())
654 {
656 variable_context.add_context_variables(eqn.identifier().variables(), m_data_type_checker);
657 eqn = process_equation(eqn.identifier(), eqn.formal_parameters(), typecheck_process_expression(variable_context, eqn.expression(), &eqn.identifier()));
658 }
659
660 // typecheck the initial state
662
663 // typecheck the data specification
665 procspec.data().translate_user_notation();
666
667
668 mCRL2log(log::debug) << "type checking process specification finished" << std::endl;
669 }
670
671 protected:
673 {
674 process_expression result;
676 return result;
677 }
678};
679
686inline
688{
689 process_type_checker type_checker;
690 type_checker(proc_spec);
691}
692
701template <typename VariableContainer, typename ActionLabelContainer, typename ProcessIdentifierContainer>
703 const VariableContainer& variables = VariableContainer(),
705 const ActionLabelContainer& action_labels = ActionLabelContainer(),
706 const ProcessIdentifierContainer& process_identifiers = ProcessIdentifierContainer(),
707 const process_identifier* current_equation = nullptr
708 )
709{
710 process_type_checker type_checker(dataspec, variables, action_labels, process_identifiers);
711 return type_checker(x, current_equation);
712}
713
714} // namespace process
715
716} // namespace mcrl2
717
718#endif // MCRL2_PROCESS_TYPECHECK_H
Term containing a string.
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const term_list< Term > & tail() const
Returns the tail of the list.
Definition aterm_list.h:225
const Term & front() const
Returns the first element of the list.
Definition aterm_list.h:239
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
\brief Assignment of a data expression to a variable
Definition assignment.h:91
void translate_user_notation()
Translate user notation within the equations of the data specification.
data_expression typecheck_data_expression(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:75
const data_specification & typechecked_data_specification() const
Definition typecheck.h:120
void add_context_variables(const VariableContainer &variables)
const core::identifier_string & name() const
const data_expression_list & arguments() const
\brief Assignment of a data expression to a string
Definition assignment.h:182
\brief A data variable
Definition variable.h:28
const core::identifier_string & name() const
Definition variable.h:38
const sort_expression & sort() const
Definition variable.h:43
\brief An action label
const core::identifier_string & name() const
\brief A multiset of action names
const data::data_expression_list & arguments() const
const action_label & label() const
\brief The allow operator
const action_name_multiset_list & allow_set() const
\brief The at operator
const data::data_expression & time_stamp() const
const process_expression & operand() const
\brief The block operator
const core::identifier_string_list & block_set() const
\brief The communication operator
const communication_expression_list & comm_set() const
void add_context_action_labels(const ActionLabelContainer &actions, const data::sort_type_checker &sort_typechecker)
bool is_declared(const core::identifier_string &name) const
data::sorts_list matching_action_sorts(const core::identifier_string &name) const
bool is_declared(const core::identifier_string &name) const
data::sorts_list matching_process_sorts(const core::identifier_string &name, const data::data_expression_list &parameters) const
process_instance make_process_instance(const core::identifier_string &name, const data::sort_expression_list &formal_parameters, const data::data_expression_list &actual_parameters) const
process_identifier match_untyped_process_instance_assignment(const untyped_process_assignment &x) const
void add_process_identifiers(const ProcessIdentifierContainer &ids, const action_context &action_ctx, const data::sort_type_checker &sort_typechecker)
\brief The hide operator
const core::identifier_string_list & hide_set() const
\brief The if-then-else operator
const process_expression & else_case() const
const process_expression & then_case() const
const data::data_expression & condition() const
\brief The if-then operator
const process_expression & then_case() const
const data::data_expression & condition() const
\brief A process equation
\brief A process expression
\brief A process identifier
const data::variable_list & variables() const
Process specification consisting of a data specification, action labels, a sequence of process equati...
const std::vector< process_equation > & equations() const
Returns the equations of the process specification.
const process_expression & init() const
Returns the initialization of the process specification.
const data::data_specification & data() const
Returns the data specification.
const process::action_label_list & action_labels() const
Returns the action label specification.
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the process specification.
data::data_type_checker m_data_type_checker
Definition typecheck.h:591
process_expression typecheck_process_expression(const data::detail::variable_context &variables, const process_expression &x, const process_identifier *current_equation=nullptr)
Definition typecheck.h:672
detail::action_context m_action_context
Definition typecheck.h:592
data::detail::variable_context m_variable_context
Definition typecheck.h:594
process_type_checker(const data::data_specification &dataspec=data::data_specification())
Default constructor.
Definition typecheck.h:621
void operator()(process_specification &procspec)
Typecheck the process specification procspec.
Definition typecheck.h:636
static std::vector< process_identifier > equation_identifiers(const std::vector< process_equation > &equations)
Definition typecheck.h:596
detail::process_context m_process_context
Definition typecheck.h:593
process_type_checker(const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &action_labels, const ProcessIdentifierContainer &process_identifiers)
Definition typecheck.h:608
process_expression operator()(const process_expression &x, const process_identifier *current_equation=nullptr)
Type check a process expression. Throws a mcrl2::runtime_error exception if the expression is not wel...
Definition typecheck.h:630
\brief A rename expression
\brief The rename operator
const rename_expression_list & rename_set() 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
\brief An untyped process assginment
const data::untyped_identifier_assignment_list & assignments() const
const core::identifier_string & name() const
Standard exception class for reporting runtime errors.
Definition exception.h:27
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
add your file description here.
term_list< Term > reverse(const term_list< Term > &l)
Returns the list with the elements in reversed order.
std::string print_arguments(const Container &v)
Prints a comma separated list of the elements of v. If v is empty, the empty string is returned.
std::string pp(const identifier_string &x)
Definition core.cpp:26
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
std::string pp(const abstraction &x)
Definition data.cpp:39
@ warning
Definition logger.h:32
@ verbose
Definition logger.h:35
bool multi_actions_contains(const core::identifier_string_list &a, const action_name_multiset_list &A)
Definition typecheck.h:78
typecheck_builder make_typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const detail::process_context &process_identifiers, const detail::action_context &action_context, const process_identifier *current_equation=nullptr)
Definition typecheck.h:575
bool equal_multi_actions(core::identifier_string_list a1, core::identifier_string_list a2)
Definition typecheck.h:92
std::tuple< bool, data::data_expression_vector, std::string > match_action_parameters(const data::data_expression_list &parameters, const data::sort_expression_list &expected_sorts, const data::detail::variable_context &variable_context, data::data_type_checker &typechecker)
std::ostream & operator<<(std::ostream &out, const alphabet_node &x)
Definition alphabet.h:37
void make_allow(atermpp::aterm &t, const ARGUMENTS &... args)
void make_at(atermpp::aterm &t, const ARGUMENTS &... args)
process_expression typecheck_process_expression(const process_expression &x, const VariableContainer &variables=VariableContainer(), const data::data_specification &dataspec=data::data_specification(), const ActionLabelContainer &action_labels=ActionLabelContainer(), const ProcessIdentifierContainer &process_identifiers=ProcessIdentifierContainer(), const process_identifier *current_equation=nullptr)
Typecheck a process expression.
Definition typecheck.h:702
void make_if_then_else(atermpp::aterm &t, const ARGUMENTS &... args)
void make_hide(atermpp::aterm &t, const ARGUMENTS &... args)
action_label_list normalize_sorts(const action_label_list &x, const data::sort_specification &sortspec)
Definition process.cpp:67
void make_if_then(atermpp::aterm &t, const ARGUMENTS &... args)
void typecheck_process_specification(process_specification &proc_spec)
Type check a parsed mCRL2 process specification. Throws an exception if something went wrong.
Definition typecheck.h:687
void make_block(atermpp::aterm &t, const ARGUMENTS &... args)
action typecheck_action(const core::identifier_string &name, const data::data_expression_list &parameters, data::data_type_checker &typechecker, const data::detail::variable_context &variable_context, const detail::action_context &action_context)
Definition typecheck.h:28
void make_stochastic_operator(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const action_label &x)
Definition process.cpp:36
data::sorts_list sorts_list_intersection(const data::sorts_list &sorts1, const data::sorts_list &sorts2)
Definition typecheck.h:43
void make_process_instance_assignment(atermpp::aterm &t, const ARGUMENTS &... args)
void make_comm(atermpp::aterm &t, const ARGUMENTS &... args)
std::ostream & operator<<(std::ostream &out, const action_label &x)
void make_rename(atermpp::aterm &t, const ARGUMENTS &... args)
void make_sum(atermpp::aterm &t, const ARGUMENTS &... args)
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...
Definition indexed_set.h:72
add your file description here.
add your file description here.
void apply(T &result, const process::process_equation &x)
Definition builder.h:1129
void check_not_empty(const Container &c, const std::string &msg, const process_expression &x)
Definition typecheck.h:180
void check_action_declared(const core::identifier_string &a, const process_expression &x)
Definition typecheck.h:158
action typecheck_action(const core::identifier_string &name, const data::data_expression_list &parameters)
Definition typecheck.h:237
typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variable_context, const detail::process_context &process_context, const detail::action_context &action_context, const process_identifier *current_equation=nullptr)
Definition typecheck.h:140
void apply(T &result, const untyped_process_assignment &x)
Definition typecheck.h:285
const detail::process_context & m_process_context
Definition typecheck.h:136
void apply(T &result, const process::stochastic_operator &x)
Definition typecheck.h:555
void apply(T &result, const data::untyped_data_parameter &x)
Definition typecheck.h:345
data::data_type_checker & m_data_type_checker
Definition typecheck.h:134
void apply(T &result, const process::hide &x)
Definition typecheck.h:369
process_instance typecheck_process_instance(const core::identifier_string &name, const data::data_expression_list &parameters)
Definition typecheck.h:242
void apply(T &result, const process::if_then &x)
Definition typecheck.h:520
void check_rename_common_type(const core::identifier_string &a, const core::identifier_string &b, const process_expression &x)
Definition typecheck.h:204
bool is_action_name(const core::identifier_string &name)
Definition typecheck.h:227
void check_actions_declared(const core::identifier_string_list &act_list, const process_expression &x)
Definition typecheck.h:166
bool is_process_name(const core::identifier_string &name)
Definition typecheck.h:232
static std::map< core::identifier_string, data::data_expression > make_assignment_map(const data::untyped_identifier_assignment_list &assignments)
Definition typecheck.h:212
void check_not_equal(const T &first, const T &second, const std::string &msg, const process_expression &x)
Definition typecheck.h:189
void apply(T &result, const process::sum &x)
Definition typecheck.h:537
static bool has_empty_intersection(const data::sorts_list &s1, const data::sorts_list &s2)
Definition typecheck.h:197
void check_assignments(const process_identifier &P, const process_identifier &Q, const std::vector< data::assignment > &assignments, const untyped_process_assignment &x) const
Definition typecheck.h:264
void apply(T &result, const process::allow &x)
Definition typecheck.h:486
data::detail::variable_context m_variable_context
Definition typecheck.h:135
process_expression_builder< typecheck_builder > super
Definition typecheck.h:131
const process_identifier * m_current_equation
Definition typecheck.h:138
void apply(T &result, const process::block &x)
Definition typecheck.h:379
data::sorts_list action_sorts(const core::identifier_string &name)
Definition typecheck.h:153
void apply(T &result, const process::action &x)
Definition typecheck.h:363
void apply(T &result, const process::rename &x)
Definition typecheck.h:387
std::string print_untyped_process_assignment(const untyped_process_assignment &x) const
Definition typecheck.h:250
void apply(T &result, const process::if_then_else &x)
Definition typecheck.h:527
void apply(T &result, const process::at &x)
Definition typecheck.h:513
void apply(T &result, const process::comm &x)
Definition typecheck.h:408
const detail::action_context & m_action_context
Definition typecheck.h:137