mCRL2
Loading...
Searching...
No Matches
typecheck.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_TYPECHECK_H
13#define MCRL2_LPS_TYPECHECK_H
14
17
18namespace mcrl2
19{
20
21namespace lps
22{
23
25{
26 protected:
30
31 public:
32 template <typename VariableContainer, typename ActionLabelContainer>
34 const VariableContainer& variables,
35 const ActionLabelContainer& action_labels
36 )
37 : m_data_type_checker(dataspec)
38 {
41 }
42
45 : m_data_type_checker(dataspec)
46 {}
47
54 {
55 std::vector<process::action> actions;
56 try
57 {
58 for (const data::untyped_data_parameter& a: x.actions())
59 {
60 actions.push_back(process::typecheck_action(a.name(), a.arguments(), m_data_type_checker, m_variable_context, m_action_context));
61 }
62 }
63 catch (mcrl2::runtime_error& e)
64 {
65 throw mcrl2::runtime_error(std::string(e.what()) + "\ntype checking of multiaction failed (" + process::pp(x) + ")");
66 }
67 return multi_action(process::action_list(actions.begin(), actions.end()));
68 }
69};
70
72{
73 protected:
76
78 {
80 data::detail::variable_context variable_context;
85 return action_rename_rule(x.variables(), condition, lhs, rhs);
86 }
87
88 public:
92 : m_data_type_checker(data::data_specification())
93 {}
94
101 {
102 mCRL2log(log::verbose) << "type checking action rename specification..." << std::endl;
104 action_rename_specification result = arspec;
106 result.data().translate_user_notation();
109 process::action_label_list action_labels = lpsspec.action_labels() + arspec.action_labels();
111 for (action_rename_rule& rule: result.rules())
112 {
113 rule = typecheck_action_rename_rule(rule, action_labels);
114 }
115 mCRL2log(log::debug) << "type checking action rename specification finished" << std::endl;
116 return result;
117 }
118};
119
127inline
129 const data::data_specification& data_spec,
130 const process::action_label_list& action_decls
131 )
132{
133 multi_action_type_checker typechecker(data_spec, data::variable_list(), action_decls);
134 return typechecker(mult_act);
135}
136
143inline
145 multi_action_type_checker& typechecker
146 )
147{
148 return typechecker(mult_act);
149}
150
155
156inline
158 const action_rename_specification& arspec,
159 const lps::stochastic_specification& lpsspec)
160{
162 return typechecker(arspec, lpsspec);
163}
164
165
166} // namespace lps
167
168} // namespace mcrl2
169
170#endif // MCRL2_LPS_TYPECHECK_H
Action rename specifications.
A list of aterm objects.
Definition aterm_list.h:24
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 data::data_expression & condition() const
Returns the condition of the rule.
const process::process_expression & rhs() const
Returns the right hand side of the rule.
const data::variable_list & variables() const
Returns the variables of the rule.
const process::action & lhs() const
Returns the left hand side of the rule.
Read-only singly linked list of action rename rules.
const std::vector< action_rename_rule > & rules() const
Returns the action rename rules.
const data::data_specification & data() const
Returns the data action_rename_specification.
const process::action_label_list & action_labels() const
Returns the sequence of action labels.
action_rename_specification operator()(const action_rename_specification &arspec, const stochastic_specification &lpsspec)
Type check an action_rename_specification.
Definition typecheck.h:100
process::detail::action_context m_action_context
Definition typecheck.h:75
action_rename_rule typecheck_action_rename_rule(const action_rename_rule &x, const process::action_label_list &action_labels)
Definition typecheck.h:77
data::data_type_checker m_data_type_checker
Definition typecheck.h:74
action_rename_type_checker()
Default constructor for an action rename type checker.
Definition typecheck.h:91
multi_action_type_checker(const data::data_specification &dataspec=data::data_specification())
Default constructor.
Definition typecheck.h:44
multi_action operator()(const process::untyped_multi_action &x)
Type check a multi action. Throws a mcrl2::runtime_error exception if the expression is not well type...
Definition typecheck.h:53
data::detail::variable_context m_variable_context
Definition typecheck.h:29
process::detail::action_context m_action_context
Definition typecheck.h:28
data::data_type_checker m_data_type_checker
Definition typecheck.h:27
multi_action_type_checker(const data::data_specification &dataspec, const VariableContainer &variables, const ActionLabelContainer &action_labels)
Definition typecheck.h:33
\brief A timed multi-action
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
const data::data_specification & data() const
Returns the data specification.
const core::identifier_string & name() const
const data::data_expression_list & arguments() const
const action_label & label() const
void add_context_action_labels(const ActionLabelContainer &actions, const data::sort_type_checker &sort_typechecker)
\brief A process expression
\brief An untyped multi action or data application
const data::untyped_data_parameter_list & actions() 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:391
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
@ verbose
Definition logger.h:37
multi_action typecheck_multi_action(process::untyped_multi_action &mult_act, const data::data_specification &data_spec, const process::action_label_list &action_decls)
Type check a multi action Throws an exception if something went wrong.
Definition typecheck.h:128
action_rename_specification typecheck_action_rename_specification(const action_rename_specification &arspec, const lps::stochastic_specification &lpsspec)
Type checks an action rename specification.
Definition typecheck.h:157
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
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
std::string pp(const action_label &x)
Definition process.cpp:36
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.