mCRL2
Loading...
Searching...
No Matches
process_specification.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_PROCESS_SPECIFICATION_H
13#define MCRL2_PROCESS_PROCESS_SPECIFICATION_H
14
16#include "mcrl2/core/print.h"
17#include "mcrl2/data/data_io.h"
20
21namespace mcrl2
22{
23
25namespace process
26{
27
28class process_specification;
29atermpp::aterm_appl process_specification_to_aterm(const process_specification& spec);
30void complete_data_specification(process_specification&);
31
32// template function overloads
33std::string pp(const process_specification& x);
34void normalize_sorts(process_specification& x, const data::sort_specification& sortspec);
35void translate_user_notation(process::process_specification& x);
36std::set<data::sort_expression> find_sort_expressions(const process::process_specification& x);
37std::set<core::identifier_string> find_identifiers(const process::process_specification& x);
38std::set<data::variable> find_free_variables(const process::process_specification& x);
39
43inline
45{
47}
48
50//<ProcSpec> ::= ProcSpec(<DataSpec>, <ActSpec>, <GlobVarSpec>, <ProcEqnSpec>, <ProcInit>)
52{
53 protected:
56
59
61 std::set<data::variable> m_global_variables;
62
64 std::vector<process_equation> m_equations;
65
68
72 {
74 m_data = data::data_specification(atermpp::down_cast<atermpp::aterm_appl>(*i++));
75 m_action_labels = atermpp::down_cast<process::action_label_list>(atermpp::down_cast<atermpp::aterm_appl>(*i++)[0]);
76 data::variable_list global_variables = atermpp::down_cast<data::variable_list>(atermpp::down_cast<atermpp::aterm_appl>(*i++)[0]);
77 m_global_variables = std::set<data::variable>(global_variables.begin(),global_variables.end());
78 process_equation_list l = atermpp::down_cast<process_equation_list>(atermpp::down_cast<atermpp::aterm_appl>(*i++)[0]);
79 atermpp::aterm_appl init = atermpp::down_cast<atermpp::aterm_appl>(*i);
80 m_initial_process = process_expression(atermpp::down_cast<atermpp::aterm_appl>(init[0]));
81 m_equations = std::vector<process_equation>(l.begin(), l.end());
82 }
83
84 public:
87 {}
88
92 {
96 }
97
100 : m_data(data),
102 m_equations(equations.begin(), equations.end()),
104 {}
105
113 : m_data(data),
116 m_equations(equations.begin(), equations.end()),
118 {}
119
123 {
124 return m_data;
125 }
126
130 {
131 return m_data;
132 }
133
137 {
138 return m_action_labels;
139 }
140
144 {
145 return m_action_labels;
146 }
147
150 const std::set<data::variable>& global_variables() const
151 {
152 return m_global_variables;
153 }
154
157 std::set<data::variable>& global_variables()
158 {
159 return m_global_variables;
160 }
161
164 const std::vector<process_equation>& equations() const
165 {
166 return m_equations;
167 }
168
171 std::vector<process_equation>& equations()
172 {
173 return m_equations;
174 }
175
179 {
180 return m_initial_process;
181 }
182
186 {
187 return m_initial_process;
188 }
189};
190
191//--- start generated class process_specification ---//
192// prototype declaration
193std::string pp(const process_specification& x);
194
199inline
200std::ostream& operator<<(std::ostream& out, const process_specification& x)
201{
202 return out << process::pp(x);
203}
204//--- end generated class process_specification ---//
205
209inline
211{
212 std::set<data::sort_expression> s = process::find_sort_expressions(spec);
213 spec.data().add_context_sorts(s);
214}
215
219inline
221{
228 );
229}
230
232inline
234{
236}
237
239inline
241{
242 return !(spec1 == spec2);
243}
244
245} // namespace process
246
247} // namespace mcrl2
248
249#endif // MCRL2_PROCESS_PROCESS_SPECIFICATION_H
250
251
Iterator for term_appl.
const function_symbol & function() const
Returns the function symbol belonging to an aterm_appl.
Definition aterm_appl.h:174
const_iterator begin() const
Returns an iterator pointing to the first argument.
Definition aterm_appl.h:195
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:281
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:274
void add_context_sorts(const Container &c, typename atermpp::enable_if_container< Container >::type *=nullptr)
Adds the sorts in c to the context sorts.
\brief A process expression
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.
void construct_from_aterm(const atermpp::aterm_appl &t)
Initializes the specification with an aterm.
process_specification(data::data_specification data, process::action_label_list action_labels, process_equation_list equations, process_expression init)
Constructor that sets the global variables to empty;.
process::action_label_list m_action_labels
The action specification of the specification.
process_expression & init()
Returns the initialization of the process specification.
const process_expression & init() const
Returns the initialization of the process specification.
process_specification(atermpp::aterm_appl t)
Constructor.
process_specification(data::data_specification data, process::action_label_list action_labels, data::variable_list global_variables, process_equation_list equations, process_expression init)
Constructor of a process specification.
std::vector< process_equation > & equations()
Returns the equations of the process specification.
std::set< data::variable > m_global_variables
The set of global variables.
const data::data_specification & data() const
Returns the data specification.
std::vector< process_equation > m_equations
The equations of the specification.
const process::action_label_list & action_labels() const
Returns the action label specification.
data::data_specification m_data
The data specification of the specification.
process_expression m_initial_process
The initial state of the specification.
process::action_label_list & action_labels()
Returns the action label specification.
data::data_specification & data()
Returns the data specification.
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the process specification.
std::set< data::variable > & global_variables()
Returns the declared free variables of the process specification.
Functions for pretty printing ATerms.
add your file description here.
add your file description here.
term_appl< aterm > aterm_appl
Definition aterm_appl.h:353
const atermpp::function_symbol & function_symbol_ProcSpec()
const atermpp::function_symbol & function_symbol_GlobVarSpec()
bool check_term_ProcSpec(const Term &t)
const atermpp::function_symbol & function_symbol_ProcessInit()
const atermpp::function_symbol & function_symbol_ActSpec()
const atermpp::function_symbol & function_symbol_ProcEqnSpec()
atermpp::aterm_appl data_specification_to_aterm(const data_specification &s)
Definition data_io.cpp:44
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:194
void complete_data_specification(process_specification &)
Adds all sorts that appear in the process specification spec to the data specification of spec.
std::set< data::sort_expression > find_sort_expressions(const process::action_label_list &x)
Definition process.cpp:73
action_label_list normalize_sorts(const action_label_list &x, const data::sort_specification &sortspec)
Definition process.cpp:67
std::string pp(const action_label &x)
Definition process.cpp:36
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:150
atermpp::aterm_appl process_specification_to_aterm(const process_specification &spec)
Conversion to aterm_appl.
action translate_user_notation(const action &x)
Definition process.cpp:70
bool operator==(const process_specification &spec1, const process_specification &spec2)
Equality operator.
std::ostream & operator<<(std::ostream &out, const action_label &x)
bool operator!=(const process_specification &spec1, const process_specification &spec2)
Inequality operator.
bool is_process_specification(const atermpp::aterm_appl &x)
Test for a process specification expression.
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.
static const atermpp::function_symbol ProcSpec