mCRL2
Loading...
Searching...
No Matches
is_well_typed.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_IS_WELL_TYPED_H
13#define MCRL2_LPS_IS_WELL_TYPED_H
14
18#include <boost/iterator/transform_iterator.hpp>
19
20namespace mcrl2 {
21
22namespace lps {
23
24namespace detail
25{
26
29{
30 // The result of the last well typedness check.
31 bool result;
32
33 // Error message are written to the output stream error.
34 mutable std::ostringstream error;
35
37 : result(false)
38 {}
39
41 bool check_time(const data::data_expression& t, const std::string& type) const
42 {
44 {
45 error << "is_well_typed(" << type << ") failed: time " << t << " doesn't have sort real." << std::endl;
46 return false;
47 }
48 return true;
49 }
50
52 bool check_condition(const data::data_expression& t, const std::string& type) const
53 {
55 {
56 error << "is_well_typed(" << type << ") failed: condition " << t << " doesn't have sort bool." << std::endl;
57 return false;
58 }
59 return true;
60 }
61
63 bool check_assignments(const data::assignment_list& l, const std::string& type) const
64 {
66 {
67 error << "is_well_typed(" << type << ") failed: the assignments " << l << " are not well typed." << std::endl;
68 return false;
69 }
70 auto lhs = [](const data::assignment& a) { return a.lhs(); };
72 boost::make_transform_iterator(l.begin(), lhs),
73 boost::make_transform_iterator(l.end() , lhs)
74 )
75 )
76 {
77 error << "is_well_typed(" << type << ") failed: data assignments " << l << " don't have unique left hand sides." << std::endl;
78 return false;
79 }
80 return true;
81 }
82
84 template <typename Container>
85 bool is_well_typed_container(const Container& c) const
86 {
87 for (auto i = c.begin(); i != c.end(); ++i)
88 {
89 if (!is_well_typed(*i))
90 {
91 return false;
92 }
93 }
94 return true;
95 }
96
100 {
101 (void)d; // Suppress an unused variable warning.
102 return true;
103 }
104
107 bool is_well_typed(const data::variable& d) const
108 {
109 (void)d; // Suppress an unused variable warning.
110 return true;
111 }
112
116 {
117 (void)d; // Suppress an unused variable warning.
118 return true;
119 }
120
123 bool is_well_typed(const data::assignment& a) const
124 {
125 if (a.lhs().sort() != a.rhs().sort())
126 {
127 std::clog << "is_well_typed(data_assignment) failed: the left and right hand sides "
128 << a.lhs() << " and " << a.rhs() << " have different sorts." << std::endl;
129 return false;
130 }
131 return true;
132 }
133
137 {
138 (void)d; // Suppress an unused variable warning.
139 return true;
140 }
141
144 bool is_well_typed(const process::action& a) const
145 {
146 (void)a; // Suppress an unused variable warning.
147 return true;
148 }
149
156 bool is_well_typed(const deadlock& d) const
157 {
158 if (d.has_time())
159 {
160 check_time(d.time(), "deadlock");
161 }
162 return true;
163 }
164
171 bool is_well_typed(const multi_action& a) const
172 {
173 if (a.has_time())
174 {
175 check_time(a.time(), "multi_action");
176 }
177 return true;
178 }
179
182 bool is_well_typed(const action_summand& s) const
183 {
185 {
186 error << "is_well_typed(action_summand) failed: summation variables " << core::detail::print_list(s.summation_variables()) << " don't have unique names." << std::endl;
187 return false;
188 }
189 if (!check_condition(s.condition(), "action_summand"))
190 {
191 return false;
192 }
193 if (!is_well_typed(s.multi_action()))
194 {
195 return false;
196 }
197 if (!check_assignments(s.assignments(), "action_summand"))
198 {
199 return false;
200 }
201 return true;
202 }
203
206 bool is_well_typed(const deadlock_summand& s) const
207 {
208 if (!check_condition(s.condition(), "deadlock_summand"))
209 {
210 return false;
211 }
212 if (!is_well_typed(s.deadlock()))
213 {
214 return false;
215 }
216 return true;
217 }
218
228 template <typename ActionSummand>
230 {
231 // check 2)
233 {
234 error << "is_well_typed(linear_process) failed: process parameters " << core::detail::print_list(p.process_parameters()) << " don't have unique names." << std::endl;
235 return false;
236 }
237
238 // check 4)
239 std::set<core::identifier_string> names;
240 for (auto i = p.process_parameters().begin(); i != p.process_parameters().end(); ++i)
241 {
242 names.insert(i->name());
243 }
244 for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i)
245 {
246 if (!data::detail::check_variable_names(i->summation_variables(), names))
247 {
248 error << "is_well_typed(linear_process) failed: some of the names of the summation variables " << core::detail::print_list(i->summation_variables()) << " also appear as process parameters." << std::endl;
249 return false;
250 }
251 }
252
253 // check 5)
254 for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i)
255 {
257 {
258 error << "is_well_typed(linear_process) failed: some left hand sides of the assignments " << core::detail::print_list(i->assignments()) << " do not appear as process parameters." << std::endl;
259 return false;
260 }
261 }
262
263 // check 6)
265 {
266 return false;
267 }
269 {
270 return false;
271 }
272 return true;
273 }
274
292 template <typename LinearProcess, typename InitialProcessExpression>
294 const std::set<data::variable>& free_variables) const
295 {
296 std::set<data::sort_expression> declared_sorts = data::detail::make_set(spec.data().sorts());
297 std::set<process::action_label> declared_labels = data::detail::make_set(spec.action_labels());
298 auto const& action_summands = spec.process().action_summands();
299
300 // check 1)
301 for (auto i = action_summands.begin(); i != action_summands.end(); ++i)
302 {
303 if (!(data::detail::check_variable_sorts(i->summation_variables(), declared_sorts)))
304 {
305 error << "is_well_typed(specification) failed: some of the sorts of the summation variables " << core::detail::print_list(i->summation_variables()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl;
306 return false;
307 }
308 }
309
310 // check 2)
311 if (!(data::detail::check_variable_sorts(spec.process().process_parameters(), declared_sorts)))
312 {
313 error << "is_well_typed(specification) failed: some of the sorts of the process parameters " << core::detail::print_list(spec.process().process_parameters()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl;
314 return false;
315 }
316
317 // check 3)
318 if (!(data::detail::check_variable_sorts(spec.global_variables(), declared_sorts)))
319 {
320 error << "is_well_typed(specification) failed: some of the sorts of the free variables " << core::detail::print_list(spec.global_variables()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl;
321 return false;
322 }
323
324 // check 4)
325 if (!(detail::check_action_label_sorts(spec.action_labels(), declared_sorts)))
326 {
327 error << "is_well_typed(specification) failed: some of the sorts occurring in the action labels " << core::detail::print_list(spec.action_labels()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl;
328 return false;
329 }
330
331 // check 5)
332 for (const action_summand& s: action_summands)
333 {
334 if (!(detail::check_action_labels(s.multi_action().actions(), declared_labels)))
335 {
336 error << "is_well_typed(specification) failed: some of the labels occurring in the actions " << core::detail::print_list(s.multi_action().actions()) << " are not declared in the action specification " << core::detail::print_list(spec.action_labels()) << std::endl;
337 return false;
338 }
339 }
340 if (!is_well_typed(spec.process()))
341 {
342 return false;
343 }
344 if (!spec.data().is_well_typed())
345 {
346 return false;
347 }
348 if (!free_variables.empty())
349 {
350 error << "is_well_typed(specification) failed: some of the free variables were not declared\n";
351 error << "declared global variables: " << core::detail::print_list(spec.global_variables()) << std::endl;
352 error << "occurring free variables: " << core::detail::print_list(free_variables) << std::endl;
353 return false;
354 }
355
356 // check 3)
358 {
359 error << "is_well_typed(specification) failed: global variables " << core::detail::print_list(spec.global_variables()) << " don't have unique names." << std::endl;
360 return false;
361 }
362
363 return true;
364 }
365
366 bool is_well_typed(const specification& spec) const
367 {
368 std::set<data::variable> free_variables = lps::find_free_variables(spec);
369 return is_well_typed(spec, free_variables);
370 }
371
373 {
374 std::set<data::variable> free_variables = lps::find_free_variables(spec);
375 return is_well_typed(spec, free_variables);
376 }
377
378 template <typename Term>
379 bool operator()(const Term& t) const
380 {
381 return is_well_typed(t);
382 }
383};
384
386template <typename T>
387bool is_well_typed(const T& x)
388{
390 return checker(x);
391}
392
394template <typename T>
395bool check_well_typedness(const T& x)
396{
398 bool result = checker(x);
399 if (!result)
400 {
401 mCRL2log(log::error) << checker.error.str();
402 }
403 return result;
404}
405
406} // namespace detail
407
408} // namespace lps
409
410} // namespace mcrl2
411
412#endif // MCRL2_LPS_IS_WELL_TYPED_H
Add your file description here.
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
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
\brief Assignment of a data expression to a variable
Definition assignment.h:91
const data_expression & rhs() const
Definition assignment.h:122
const variable & lhs() const
Definition assignment.h:117
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
bool is_well_typed() const
Returns true if.
\brief A sort expression
const std::set< sort_expression > & sorts() const
Gets the normalised sort declarations including those that are system defined. This is the set with a...
\brief A data variable
Definition variable.h:28
const sort_expression & sort() const
Definition variable.h:43
LPS summand containing a multi-action.
const lps::multi_action & multi_action() const
Returns the multi-action of this summand.
const data::assignment_list & assignments() const
Returns the sequence of assignments.
LPS summand containing a deadlock.
const lps::deadlock & deadlock() const
Returns the deadlock of this summand.
Represents a deadlock.
Definition deadlock.h:26
bool has_time() const
Returns true if time is available.
Definition deadlock.h:42
const data::data_expression & time() const
Returns the time.
Definition deadlock.h:49
const std::vector< ActionSummand > & action_summands() const
Returns the sequence of action summands.
const deadlock_summand_vector & deadlock_summands() const
Returns the sequence of deadlock summands.
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
\brief A timed multi-action
bool has_time() const
Returns true if time is available.
const data::data_expression & time() const
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the LPS.
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 LinearProcess & process() const
Returns the linear process of the specification.
const data::data_specification & data() const
Returns the data specification.
Linear process specification.
const data::data_expression & condition() const
Returns the condition expression.
Definition summand.h:60
data::variable_list & summation_variables()
Returns the sequence of summation variables.
Definition summand.h:46
\brief An action label
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
std::string print_list(const Container &v, const std::string &message="", bool print_index=false, bool boundary_spaces=true)
Creates a string representation of a container.
bool check_variable_sorts(const VariableContainer &variables, const SortContainer &sorts)
Returns true if the domain sorts and the range sort of the given variables are contained in sorts.
bool check_variable_names(variable_list const &variables, const std::set< core::identifier_string > &names)
Returns true if names of the given variables are not contained in names.
bool sequence_contains_duplicates(Iterator first, Iterator last)
Returns true if the sequence [first, last) contains duplicates.
bool check_assignment_variables(assignment_list const &assignments, variable_list const &variables)
Returns true if the left hand sides of assignments are contained in variables.
bool unique_names(const VariableContainer &variables)
Returns true if the names of the given variables are unique.
std::set< typename Container::value_type > make_set(const Container &c)
Makes a set of the given container.
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
variable_list free_variables(const data_expression &x)
Definition data.cpp:195
bool is_well_typed(const T &x)
Checks well typedness of an LPS object.
bool check_action_labels(const process::action_list &actions, const std::set< process::action_label > &labels)
Returns true if the labels of the given actions are contained in labels.
bool check_action_label_sorts(const process::action_label_list &action_labels, const std::set< data::sort_expression > &sorts)
Returns true if the sorts of the given action labels are contained in sorts.
bool check_well_typedness(const T &x)
Checks well typedness of an LPS object, and will print error messages to stderr.
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
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.
Function object for applying a substitution to LPS data types.
bool is_well_typed(const linear_process_base< ActionSummand > &p) const
Checks well typedness of a linear process.
bool is_well_typed(const process::action &a) const
Traverses an action.
bool is_well_typed(const action_summand &s) const
Checks well typedness of a summand.
bool check_time(const data::data_expression &t, const std::string &type) const
Checks if the sort of t has type real.
bool is_well_typed(const data::assignment &a) const
Traverses an assignment.
bool check_condition(const data::data_expression &t, const std::string &type) const
Checks if the sort of t has type bool.
bool is_well_typed(const stochastic_specification &spec) const
bool is_well_typed(const data::variable &d) const
Checks well typedness of a variable.
bool check_assignments(const data::assignment_list &l, const std::string &type) const
Checks if the assignments are well typed and have unique left hand sides.
bool is_well_typed(const specification &spec) const
bool is_well_typed(const data::sort_expression &d) const
Checks well typedness of a sort expression.
bool is_well_typed_container(const Container &c) const
Checks well typedness of the elements of a container.
bool is_well_typed(const process::action_label &d) const
Traverses an action label.
bool is_well_typed(const specification_base< LinearProcess, InitialProcessExpression > &spec, const std::set< data::variable > &free_variables) const
Checks well typedness of a linear process specification.
bool is_well_typed(const deadlock &d) const
Checks well typedness of a deadlock.
bool is_well_typed(const data::data_expression &d) const
Checks well typedness of a data expression.
bool is_well_typed(const deadlock_summand &s) const
Checks well typedness of a summand.
bool is_well_typed(const multi_action &a) const
Checks well typedness of a multi-action.