mCRL2
Loading...
Searching...
No Matches
merge_data_specifications.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_DATA_MERGE_DATA_SPECIFICATIONS_H
13#define MCRL2_DATA_MERGE_DATA_SPECIFICATIONS_H
14
16
17namespace mcrl2 {
18
19namespace data {
20
26inline
28{
29 data_specification result = dataspec1;
30
31 // Merge the sorts.
32 for(const basic_sort& s: dataspec2.user_defined_sorts())
33 {
34 if (std::find(dataspec1.user_defined_sorts().begin(),dataspec1.user_defined_sorts().end(),s)==dataspec1.user_defined_sorts().end())
35 {
36 result.add_sort(s);
37 }
38 }
39
40 // Merge the aliases.
41 for(const alias& a: dataspec2.user_defined_aliases())
42 {
43 if (std::find(dataspec1.user_defined_aliases().begin(),dataspec1.user_defined_aliases().end(),a)==dataspec1.user_defined_aliases().end())
44 {
45 result.add_alias(a);
46 }
47 }
48
49 // Merge the constructors.
50 for(const function_symbol& f: dataspec2.user_defined_constructors())
51 {
52 if (std::find(dataspec1.user_defined_constructors().begin(),dataspec1.user_defined_constructors().end(),f)==
53 dataspec1.user_defined_constructors().end())
54 {
55 result.add_constructor(f);
56 }
57 }
58
59 // Merge the mappings.
60 for(const function_symbol& f: dataspec2.user_defined_mappings())
61 {
62 if (std::find(dataspec1.user_defined_mappings().begin(),dataspec1.user_defined_mappings().end(),f)==dataspec1.user_defined_mappings().end())
63 {
64 result.add_mapping(f);
65 }
66 }
67
68 // Merge the data equations.
69 for(const data_equation& e: dataspec2.user_defined_equations())
70 {
71 if (std::find(dataspec1.user_defined_equations().begin(),dataspec1.user_defined_equations().end(),e)==dataspec1.user_defined_equations().end())
72 {
73 result.add_equation(e);
74 }
75 }
76
78 try
79 {
80 // Type check the resulting specification.
81 // Throw an exception when there is an issue.
83 }
84 catch (mcrl2::runtime_error& e)
85 {
86 throw mcrl2::runtime_error(std::string("Merging of two data specifications fails.\n") + e.what());
87 }
88
89 return result;
90}
91
92} // namespace data
93
94} // namespace mcrl2
95
96#endif // MCRL2_DATA_MERGE_DATA_SPECIFICATIONS_H
\brief A sort alias
Definition alias.h:26
\brief A basic sort
Definition basic_sort.h:26
\brief A data equation
const function_symbol_vector & user_defined_constructors() const
Gets the constructors defined by the user, excluding those that are system defined.
void add_mapping(const function_symbol &f)
Adds a mapping to this specification.
void add_equation(const data_equation &e)
Adds an equation to this specification.
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
const data_equation_vector & user_defined_equations() const
Gets all user defined equations.
void add_constructor(const function_symbol &f)
Adds a constructor to this specification.
\brief A function symbol
const basic_sort_vector & user_defined_sorts() const
Gets all sorts defined by a user (excluding the system defined sorts).
void add_alias(const alias &a)
Adds an alias (new name for a sort) to this specification.
void add_sort(const basic_sort &s)
Adds a sort to this specification.
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
data_specification merge_data_specifications(const data_specification &dataspec1, const data_specification &dataspec2)
Merges two data specifications. Throws an exception if conflicts are detected.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72