mCRL2
Loading...
Searching...
No Matches
process_context.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_PROCESS_DETAIL_PROCESS_CONTEXT_H
13#define MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H
14
18
19namespace mcrl2 {
20
21namespace process {
22
23namespace detail {
24
26{
27 private:
28 std::multimap<core::identifier_string, process_identifier> m_process_identifiers;
29
30 // returns true if all left hand sides of assignments appear as the name of a variable in parameters
32 {
33 for (const data::untyped_identifier_assignment& a: assignments)
34 {
35 if (std::find_if(parameters.begin(), parameters.end(), [&](const data::variable& v) { return a.lhs() == v.name(); }) == parameters.end())
36 {
37 return false;
38 }
39 }
40 return true;
41 }
42
43 // returns an assignment that does not match with the list of parameters
45 {
47 std::set<core::identifier_string> parameter_names;
48 for (const data::variable& param: parameters)
49 {
50 parameter_names.insert(param.name());
51 }
52 auto i = std::find_if(assignments.begin(), assignments.end(), [&](const data::untyped_identifier_assignment& a) { return !contains(parameter_names, a.lhs()); });
53 assert(i != assignments.end());
54 return *i;
55 }
56
57 public:
58 bool is_declared(const core::identifier_string& name) const
59 {
60 return m_process_identifiers.find(name) != m_process_identifiers.end();
61 }
62
63 template <typename ProcessIdentifierContainer>
64 void add_process_identifiers(const ProcessIdentifierContainer& ids, const action_context& action_ctx, const data::sort_type_checker& sort_typechecker)
65 {
66 for (const process_identifier& id: ids)
67 {
68 const core::identifier_string& name = id.name();
69
70 if (action_ctx.is_declared(name))
71 {
72 throw mcrl2::runtime_error("declaration of both process and action " + core::pp(name));
73 }
74
75 // Insert id in m_process_identifiers; N.B. Before that check if it already exists
76 auto range = m_process_identifiers.equal_range(id.name());
77 if (range.first != m_process_identifiers.end())
78 {
79 for (auto i = range.first; i != range.second; ++i)
80 {
81 if (i->second == id)
82 {
83 throw mcrl2::runtime_error("double declaration of process " + process::pp(id));
84 }
85 }
86 }
87 m_process_identifiers.insert(range.first, std::make_pair(id.name(), id));
88
89 for (const data::variable& v: id.variables())
90 {
91 sort_typechecker(v.sort());
92 }
93
94 //check that all formal parameters of the process are unique.
95 if (!data::detail::unique_names(id.variables()))
96 {
97 throw mcrl2::runtime_error("the formal variables in process " + process::pp(id) + " are not unique");
98 }
99 }
100 }
101
102 // returns the process identifier that corresponds to the untyped process assignment x
104 {
105 auto range = m_process_identifiers.equal_range(x.name());
106 if (range.first == m_process_identifiers.end())
107 {
108 throw mcrl2::runtime_error("process " + core::pp(x.name()) + " not declared");
109 }
110 std::vector<process_identifier> result;
111 for (auto k = range.first; k != range.second; ++k)
112 {
113 const process_identifier& id = k->second;
114 if (is_matching_assignment(x.assignments(), id.variables()))
115 {
116 result.push_back(id);
117 }
118 }
119 if (result.empty())
120 {
121 std::string detailed_message;
122
123 // If there is only one matching process, give a more detailed error message.
124 if (std::distance(range.first, range.second) == 1)
125 {
126 const process_identifier& id = range.first->second;
128 detailed_message = "Missing parameter: " + core::pp(a.lhs()) + '\n';
129 }
130 throw mcrl2::runtime_error("There is no process " + core::pp(x.name()) + " containing all assignments in " + process::pp(x) + ".\n" + detailed_message);
131 }
132 if (result.size() > 1)
133 {
134 throw mcrl2::runtime_error("There are multiple processes named " + core::pp(x.name()) + " containing all assignments in " + process::pp(x) + ".");
135 }
136 return result.front();
137 }
138
140 {
141 auto range = m_process_identifiers.equal_range(name);
142 assert(range.first != m_process_identifiers.end());
143 for (auto k = range.first; k != range.second; ++k)
144 {
145 const process_identifier& id = k->second;
146 if (data::detail::parameter_sorts(id.variables()) == formal_parameters)
147 {
148 return process_instance(id, actual_parameters);
149 }
150 }
151 throw mcrl2::runtime_error("no matching process found for " + core::pp(name) + "(" + data::pp(formal_parameters) + ")");
152 }
153
155 {
156 data::sorts_list result;
157 auto range = m_process_identifiers.equal_range(name);
158 for (auto k = range.first; k != range.second; ++k)
159 {
160 const process_identifier& id = k->second;
161 if (id.variables().size() == parameters.size())
162 {
163 result.push_front(data::detail::parameter_sorts(id.variables()));
164 }
165 }
166 return atermpp::reverse(result);
167 }
168
169 void clear()
170 {
171 m_process_identifiers.clear();
172 }
173};
174
175} // namespace detail
176
177} // namespace process
178
179} // namespace mcrl2
180
181#endif // MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H
add your file description here.
Term containing a string.
A list of aterm objects.
Definition aterm_list.h:24
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_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
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 string
Definition assignment.h:182
const core::identifier_string & lhs() const
Definition assignment.h:213
\brief A data variable
Definition variable.h:28
bool is_declared(const core::identifier_string &name) const
bool is_matching_assignment(const data::untyped_identifier_assignment_list &assignments, const data::variable_list &parameters) 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
std::multimap< core::identifier_string, process_identifier > m_process_identifiers
process_identifier match_untyped_process_instance_assignment(const untyped_process_assignment &x) const
data::untyped_identifier_assignment find_violating_assignment(const data::untyped_identifier_assignment_list &assignments, const data::variable_list &parameters) const
void add_process_identifiers(const ProcessIdentifierContainer &ids, const action_context &action_ctx, const data::sort_type_checker &sort_typechecker)
\brief A process identifier
\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
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 pp(const identifier_string &x)
Definition core.cpp:26
data::sort_expression_list parameter_sorts(const Container &parameters)
Returns the sorts of a sequence of parameters.
bool unique_names(const VariableContainer &variables)
Returns true if the names of the given variables are unique.
std::string pp(const abstraction &x)
Definition data.cpp:39
std::string pp(const action_label &x)
Definition process.cpp:36
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
Definition indexed_set.h:86
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.