mCRL2
Loading...
Searching...
No Matches
process.cpp
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
16
17
18namespace mcrl2
19{
20
21namespace process
22{
23
24//--- start generated process overloads ---//
25std::string pp(const process::action_list& x) { return process::pp< process::action_list >(x); }
26std::string pp(const process::action_vector& x) { return process::pp< process::action_vector >(x); }
27std::string pp(const process::action_label_list& x) { return process::pp< process::action_label_list >(x); }
28std::string pp(const process::action_label_vector& x) { return process::pp< process::action_label_vector >(x); }
29std::string pp(const process::process_identifier_list& x) { return process::pp< process::process_identifier_list >(x); }
30std::string pp(const process::process_identifier_vector& x) { return process::pp< process::process_identifier_vector >(x); }
31std::string pp(const process::process_expression_list& x) { return process::pp< process::process_expression_list >(x); }
32std::string pp(const process::process_expression_vector& x) { return process::pp< process::process_expression_vector >(x); }
33std::string pp(const process::process_equation_list& x) { return process::pp< process::process_equation_list >(x); }
34std::string pp(const process::process_equation_vector& x) { return process::pp< process::process_equation_vector >(x); }
35std::string pp(const process::action& x) { return process::pp< process::action >(x); }
36std::string pp(const process::action_label& x) { return process::pp< process::action_label >(x); }
37std::string pp(const process::action_name_multiset& x) { return process::pp< process::action_name_multiset >(x); }
38std::string pp(const process::allow& x) { return process::pp< process::allow >(x); }
39std::string pp(const process::at& x) { return process::pp< process::at >(x); }
40std::string pp(const process::block& x) { return process::pp< process::block >(x); }
41std::string pp(const process::bounded_init& x) { return process::pp< process::bounded_init >(x); }
42std::string pp(const process::choice& x) { return process::pp< process::choice >(x); }
43std::string pp(const process::comm& x) { return process::pp< process::comm >(x); }
44std::string pp(const process::communication_expression& x) { return process::pp< process::communication_expression >(x); }
45std::string pp(const process::delta& x) { return process::pp< process::delta >(x); }
46std::string pp(const process::hide& x) { return process::pp< process::hide >(x); }
47std::string pp(const process::if_then& x) { return process::pp< process::if_then >(x); }
48std::string pp(const process::if_then_else& x) { return process::pp< process::if_then_else >(x); }
49std::string pp(const process::left_merge& x) { return process::pp< process::left_merge >(x); }
50std::string pp(const process::merge& x) { return process::pp< process::merge >(x); }
51std::string pp(const process::process_equation& x) { return process::pp< process::process_equation >(x); }
52std::string pp(const process::process_expression& x) { return process::pp< process::process_expression >(x); }
53std::string pp(const process::process_identifier& x) { return process::pp< process::process_identifier >(x); }
54std::string pp(const process::process_instance& x) { return process::pp< process::process_instance >(x); }
55std::string pp(const process::process_instance_assignment& x) { return process::pp< process::process_instance_assignment >(x); }
56std::string pp(const process::process_specification& x) { return process::pp< process::process_specification >(x); }
57std::string pp(const process::rename& x) { return process::pp< process::rename >(x); }
58std::string pp(const process::rename_expression& x) { return process::pp< process::rename_expression >(x); }
59std::string pp(const process::seq& x) { return process::pp< process::seq >(x); }
60std::string pp(const process::stochastic_operator& x) { return process::pp< process::stochastic_operator >(x); }
61std::string pp(const process::sum& x) { return process::pp< process::sum >(x); }
62std::string pp(const process::sync& x) { return process::pp< process::sync >(x); }
63std::string pp(const process::tau& x) { return process::pp< process::tau >(x); }
64std::string pp(const process::untyped_multi_action& x) { return process::pp< process::untyped_multi_action >(x); }
65std::string pp(const process::untyped_process_assignment& x) { return process::pp< process::untyped_process_assignment >(x); }
66process::action normalize_sorts(const process::action& x, const data::sort_specification& sortspec) { return process::normalize_sorts< process::action >(x, sortspec); }
67process::action_label_list normalize_sorts(const process::action_label_list& x, const data::sort_specification& sortspec) { return process::normalize_sorts< process::action_label_list >(x, sortspec); }
68void normalize_sorts(process::process_equation_vector& x, const data::sort_specification& sortspec) { process::normalize_sorts< process::process_equation_vector >(x, sortspec); }
69void normalize_sorts(process::process_specification& x, const data::sort_specification& /* sortspec */) { process::normalize_sorts< process::process_specification >(x, x.data()); }
70process::action translate_user_notation(const process::action& x) { return process::translate_user_notation< process::action >(x); }
71process::process_expression translate_user_notation(const process::process_expression& x) { return process::translate_user_notation< process::process_expression >(x); }
72void translate_user_notation(process::process_specification& x) { process::translate_user_notation< process::process_specification >(x); }
73std::set<data::sort_expression> find_sort_expressions(const process::action_label_list& x) { return process::find_sort_expressions< process::action_label_list >(x); }
74std::set<data::sort_expression> find_sort_expressions(const process::process_equation_vector& x) { return process::find_sort_expressions< process::process_equation_vector >(x); }
75std::set<data::sort_expression> find_sort_expressions(const process::process_expression& x) { return process::find_sort_expressions< process::process_expression >(x); }
76std::set<data::sort_expression> find_sort_expressions(const process::process_specification& x) { return process::find_sort_expressions< process::process_specification >(x); }
77std::set<data::variable> find_all_variables(const process::action& x) { return process::find_all_variables< process::action >(x); }
78std::set<data::variable> find_free_variables(const process::action& x) { return process::find_free_variables< process::action >(x); }
79std::set<data::variable> find_free_variables(const process::process_specification& x) { return process::find_free_variables< process::process_specification >(x); }
80std::set<core::identifier_string> find_identifiers(const process::process_specification& x) { return process::find_identifiers< process::process_specification >(x); }
81//--- end generated process overloads ---//
82
83void alphabet_reduce(process_specification& procspec, std::size_t duplicate_equation_limit)
84{
85 mCRL2log(log::verbose) << "applying alphabet reduction..." << std::endl;
86 process_expression init = procspec.init();
87
88 // cache the alphabet of pcrl equations and apply alphabet reduction to block({}, init)
89 std::vector<process_equation>& equations = procspec.equations();
90 std::map<process_identifier, multi_action_name_set> pcrl_equation_cache;
92 for (process_equation& equation: equations)
93 {
94 id_generator.add_identifier(equation.identifier().name());
95 }
96 pcrl_equation_cache = detail::compute_pcrl_equation_cache(equations, init);
97 core::identifier_string_list empty_blockset;
98 procspec.init() = push_block(empty_blockset, init, equations, id_generator, pcrl_equation_cache);
99
100 // remove duplicate equations
101 if (procspec.equations().size() < duplicate_equation_limit)
102 {
103 mCRL2log(log::debug) << "removing duplicate equations..." << std::endl;
105 mCRL2log(log::debug) << "removing duplicate equations finished" << std::endl;
106 }
107
108 mCRL2log(log::debug) << "alphabet reduction finished" << std::endl;
109}
110
112{
114 unsigned int start_symbol_index = p.start_symbol_index("ActDecl");
115 bool partial_parses = false;
116 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
117 action_label_vector result;
119 process::action_label_list v(result.begin(), result.end());
120 v = process::normalize_sorts(v, data_spec);
121 return v;
122}
123
124namespace detail {
125
127{
129 unsigned int start_symbol_index = p.start_symbol_index("ProcExpr");
130 bool partial_parses = false;
131 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
132 core::warn_and_or(node);
135 return result;
136}
137
139{
141 unsigned int start_symbol_index = p.start_symbol_index("mCRL2Spec");
142 bool partial_parses = false;
143 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
144 core::warn_and_or(node);
147 process_specification result = untyped_procspec.construct_process_specification();
148 return result;
149}
150
152{
155 if (alpha_reduce)
156 {
157 alphabet_reduce(x, 1000ul);
158 }
159}
160
161} // namespace detail
162
163} // namespace process
164
165} // namespace mcrl2
166
add your file description here.
A list of aterm objects.
Definition aterm_list.h:24
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
\brief An action label
\brief A multiset of action names
\brief The allow operator
\brief The at operator
\brief The block operator
\brief The bounded initialization
\brief The choice operator
\brief The communication operator
\brief The value delta
\brief The hide operator
\brief The if-then-else operator
\brief The if-then operator
\brief The left merge operator
\brief The merge operator
\brief A process equation
\brief A process expression
\brief A process identifier
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.
const process_expression & init() const
Returns the initialization of the process specification.
const data::data_specification & data() const
Returns the data specification.
\brief A rename expression
\brief The rename operator
\brief The sequential composition
\brief The distribution operator
\brief The sum operator
\brief The synchronization operator
\brief The value tau
\brief An untyped multi action or data application
\brief An untyped process assginment
D_ParserTables parser_tables_mcrl2
MCRL2_EXPORT bool init(rewriter_interface *i, RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
void syntax_error_fn(struct D_Parser *ap)
Custom syntax error function that prints both the line number and the column.
Definition dparser.cpp:463
struct D_ParseNode * ambiguity_fn(struct D_Parser *, int, struct D_ParseNode **)
Function for resolving ambiguities in the '_ -> _ <> _' operator for process expressions.
Definition dparser.cpp:332
void warn_left_merge_merge(const parse_node &)
Prints a warning for each occurrence of 'x ||_ y || z' in the parse tree.
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
@ verbose
Definition logger.h:35
process_specification parse_process_specification_new(const std::string &text)
Definition process.cpp:138
void complete_process_specification(process_specification &x, bool alpha_reduce=false)
Definition process.cpp:151
process_expression parse_process_expression_new(const std::string &text)
Definition process.cpp:126
std::map< process_identifier, multi_action_name_set > compute_pcrl_equation_cache(const std::vector< process_equation > &equations)
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:194
process_expression push_block(const core::identifier_string_list &B, const process_expression &x, std::vector< process_equation > &equations, data::set_identifier_generator &id_generator, std::map< process_identifier, multi_action_name_set > &pcrl_equation_cache)
std::vector< process_expression > process_expression_vector
\brief vector of process_expressions
process::action_label_list parse_action_declaration(const std::string &text, const data::data_specification &data_spec=data::detail::default_specification())
Parses an action declaration from a string.
Definition process.cpp:111
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
void typecheck_process_specification(process_specification &proc_spec)
Type check a parsed mCRL2 process specification. Throws an exception if something went wrong.
Definition typecheck.h:687
std::vector< process_equation > process_equation_vector
\brief vector of process_equations
void alphabet_reduce(process_specification &procspec, std::size_t duplicate_equation_limit=(std::numeric_limits< size_t >::max)())
Applies alphabet reduction to a process specification.
Definition process.cpp:83
std::vector< action > action_vector
\brief vector of actions
std::string pp(const action_label &x)
Definition process.cpp:36
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:150
void find_all_variables(const T &x, OutputIterator o)
Definition find.h:129
action translate_user_notation(const action &x)
Definition process.cpp:70
void remove_duplicate_equations(process_specification &procspec)
Removes duplicate equations from a process specification, using a bisimulation algorithm.
std::vector< action_label > action_label_vector
\brief vector of action_labels
std::vector< process_identifier > process_identifier_vector
\brief vector of process_identifiers
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.
add your file description here.
add your file description here.
Wrapper for D_ParseNode.
Definition dparser.h:86
Wrapper for D_Parser and its corresponding D_ParserTables.
Definition dparser.h:148
parse_node parse(const std::string &text, unsigned int start_symbol_index=0, bool partial_parses=false)
Parses a string. N.B. The user is responsible for destruction of the returned value by calling destro...
Definition dparser.cpp:209
unsigned int start_symbol_index(const std::string &name) const
Definition dparser.cpp:204
bool callback_ActDecl(const core::parse_node &node, action_label_vector &result) const
Definition parse_impl.h:61
untyped_process_specification parse_mCRL2Spec(const core::parse_node &node) const
Definition parse_impl.h:271
process::process_expression parse_ProcExpr(const core::parse_node &node) const
Definition parse_impl.h:181
process_specification construct_process_specification()
Definition parse_impl.h:30