mCRL2
Loading...
Searching...
No Matches
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_LPS_SPECIFICATION_H
13#define MCRL2_LPS_SPECIFICATION_H
14
15#include "mcrl2/data/data_io.h"
19
20#include <cerrno>
21
22namespace mcrl2
23{
24
26namespace lps
27{
28
29// prototype definitions
30template <typename Object> bool check_well_typedness(const Object& o);
31template <typename LinearProcess, typename InitialProcessExpression> class specification_base;
32template <typename LinearProcess, typename InitialProcessExpression> atermpp::aterm_appl specification_to_aterm(const specification_base<LinearProcess, InitialProcessExpression>& spec);
33class specification;
35
36// template function overloads
39
43inline
45{
47}
48
49template <typename LinearProcess, typename InitialProcessExpression>
51{
52 protected:
55
58
60 std::set<data::variable> m_global_variables;
61
63 LinearProcess m_process;
64
66 InitialProcessExpression m_initial_process;
67
68 public:
70 typedef LinearProcess process_type;
71
73 typedef InitialProcessExpression initial_process_type;
74
77 { }
78
87 const std::set<data::variable>& global_variables,
88 const LinearProcess& lps,
89 const InitialProcessExpression& initial_process)
90 :
91 m_data(data),
94 m_process(lps),
96 {
97 assert(lps.process_parameters().size()==initial_process.expressions().size());
98 }
99
102 const LinearProcess& process() const
103 {
104 return m_process;
105 }
106
109 LinearProcess& process()
110 {
111 return m_process;
112 }
113
117 {
118 return m_data;
119 }
120
124 {
125 return m_data;
126 }
127
132 {
133 return m_action_labels;
134 }
135
140 {
141 return m_action_labels;
142 }
143
146 const std::set<data::variable>& global_variables() const
147 {
148 return m_global_variables;
149 }
150
153 std::set<data::variable>& global_variables()
154 {
155 return m_global_variables;
156 }
157
160 const InitialProcessExpression& initial_process() const
161 {
162 return m_initial_process;
163 }
164
167 InitialProcessExpression& initial_process()
168 {
169 return m_initial_process;
170 }
171};
172
174class specification: public specification_base<linear_process, process_initializer>
175{
176 protected:
178
179 public:
181 specification() = default;
182
191 const std::set<data::variable>& global_variables,
192 const linear_process& lps,
195 {
197 }
198};
199
200//--- start generated class specification ---//
201// prototype declaration
202std::string pp(const specification& x);
203
208inline
209std::ostream& operator<<(std::ostream& out, const specification& x)
210{
211 return out << lps::pp(x);
212}
213//--- end generated class specification ---//
214
215std::string pp_with_summand_numbers(const specification& x);
216
217// template function overloads
218std::set<data::sort_expression> find_sort_expressions(const lps::specification& x);
219std::set<data::variable> find_all_variables(const lps::specification& x);
220std::set<data::variable> find_free_variables(const lps::specification& x);
221std::set<data::function_symbol> find_function_symbols(const lps::specification& x);
222std::set<core::identifier_string> find_identifiers(const lps::specification& x);
223std::set<process::action_label> find_action_labels(const lps::specification& x);
224
227template <typename LinearProcess, typename InitialProcessExpression>
229{
235 spec.initial_process()
236 );
237}
238
240inline
241bool operator==(const specification& spec1, const specification& spec2)
242{
243 return specification_to_aterm(spec1) == specification_to_aterm(spec2);
244}
245
247inline
248bool operator!=(const specification& spec1, const specification& spec2)
249{
250 return !(spec1 == spec2);
251}
252
255inline
257{
258 std::set<data::sort_expression> s = lps::find_sort_expressions(spec);
259 spec.data().add_context_sorts(s);
260}
261
262} // namespace lps
263
264} // namespace mcrl2
265
266#endif // MCRL2_LPS_SPECIFICATION_H
const function_symbol & function() const
Returns the function symbol belonging to an aterm_appl.
Definition aterm_appl.h:174
void add_context_sorts(const Container &c, typename atermpp::enable_if_container< Container >::type *=nullptr)
Adds the sorts in c to the context sorts.
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the LPS.
LinearProcess & process()
Returns a reference to the linear process of the specification.
process::action_label_list m_action_labels
The action specification of the specification.
specification_base(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const LinearProcess &lps, const InitialProcessExpression &initial_process)
Constructor.
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 InitialProcessExpression & initial_process() const
Returns the initial process.
const LinearProcess & process() const
Returns the linear process of the specification.
process::action_label_list & action_labels()
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
data::data_specification & data()
Returns a reference to the data specification.
const data::data_specification & data() const
Returns the data specification.
std::set< data::variable > m_global_variables
The set of global variables.
LinearProcess process_type
The process type.
InitialProcessExpression & initial_process()
Returns a reference to the initial process.
InitialProcessExpression initial_process_type
The initial process type.
LinearProcess m_process
The linear process of the specification.
std::set< data::variable > & global_variables()
Returns the declared free variables of the LPS.
data::data_specification m_data
The data specification of the specification.
InitialProcessExpression m_initial_process
The initial state of the specification.
Linear process specification.
specification()=default
Constructor.
specification_base< linear_process, process_initializer > super
specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::set< data::variable > &global_variables, const linear_process &lps, const process_initializer &initial_process)
Constructor.
add your file description here.
The class linear_process.
term_appl< aterm > aterm_appl
Definition aterm_appl.h:353
const atermpp::function_symbol & function_symbol_GlobVarSpec()
const atermpp::function_symbol & function_symbol_LinProcSpec()
const atermpp::function_symbol & function_symbol_ActSpec()
atermpp::aterm_appl data_specification_to_aterm(const data_specification &s)
Definition data_io.cpp:44
void find_function_symbols(const T &x, OutputIterator o)
Definition find.h:138
atermpp::aterm_appl specification_to_aterm(const specification_base< LinearProcess, InitialProcessExpression > &spec)
Conversion to aterm_appl.
atermpp::aterm_appl linear_process_to_aterm(const linear_process_base< ActionSummand > &p)
Conversion to aterm_appl.
std::string pp_with_summand_numbers(const specification &x)
Definition lps.cpp:74
void complete_data_specification(specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
bool is_specification(const atermpp::aterm_appl &x)
Test for a specification expression.
bool check_well_typedness(const linear_process &x)
Definition lps.cpp:92
std::string pp(const action_summand &x)
Definition lps.cpp:26
void find_sort_expressions(const T &x, OutputIterator o)
Definition find.h:117
std::ostream & operator<<(std::ostream &out, const action_summand &x)
lps::multi_action normalize_sorts(const multi_action &x, const data::sort_specification &sortspec)
Definition lps.cpp:38
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
bool operator!=(const specification &spec1, const specification &spec2)
Inequality operator.
bool operator==(const action_summand &x, const action_summand &y)
Equality operator of action summands.
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:96
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:48
void find_action_labels(const T &x, OutputIterator o)
Returns all action labels that occur in an object.
Definition find.h:172
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
The class process_initializer.
static const atermpp::function_symbol LinProcSpec