mCRL2
Loading...
Searching...
No Matches
lps.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
15#include "mcrl2/lps/print.h"
16#include "mcrl2/lps/replace.h"
18
19namespace mcrl2
20{
21
22namespace lps
23{
24
25//--- start generated lps overloads ---//
26std::string pp(const lps::action_summand& x) { return lps::pp< lps::action_summand >(x); }
27std::string pp(const lps::deadlock& x) { return lps::pp< lps::deadlock >(x); }
28std::string pp(const lps::deadlock_summand& x) { return lps::pp< lps::deadlock_summand >(x); }
29std::string pp(const lps::linear_process& x) { return lps::pp< lps::linear_process >(x); }
30std::string pp(const lps::multi_action& x) { return lps::pp< lps::multi_action >(x); }
31std::string pp(const lps::process_initializer& x) { return lps::pp< lps::process_initializer >(x); }
32std::string pp(const lps::specification& x) { return lps::pp< lps::specification >(x); }
33std::string pp(const lps::stochastic_action_summand& x) { return lps::pp< lps::stochastic_action_summand >(x); }
34std::string pp(const lps::stochastic_distribution& x) { return lps::pp< lps::stochastic_distribution >(x); }
35std::string pp(const lps::stochastic_linear_process& x) { return lps::pp< lps::stochastic_linear_process >(x); }
36std::string pp(const lps::stochastic_process_initializer& x) { return lps::pp< lps::stochastic_process_initializer >(x); }
37std::string pp(const lps::stochastic_specification& x) { return lps::pp< lps::stochastic_specification >(x); }
38lps::multi_action normalize_sorts(const lps::multi_action& x, const data::sort_specification& sortspec) { return lps::normalize_sorts< lps::multi_action >(x, sortspec); }
39void normalize_sorts(lps::specification& x, const data::sort_specification& /* sortspec */) { lps::normalize_sorts< lps::specification >(x, x.data()); }
40void normalize_sorts(lps::stochastic_specification& x, const data::sort_specification& /* sortspec */) { lps::normalize_sorts< lps::stochastic_specification >(x, x.data()); }
41lps::multi_action translate_user_notation(const lps::multi_action& x) { return lps::translate_user_notation< lps::multi_action >(x); }
42std::set<data::sort_expression> find_sort_expressions(const lps::specification& x) { return lps::find_sort_expressions< lps::specification >(x); }
43std::set<data::sort_expression> find_sort_expressions(const lps::stochastic_specification& x) { return lps::find_sort_expressions< lps::stochastic_specification >(x); }
44std::set<data::variable> find_all_variables(const lps::linear_process& x) { return lps::find_all_variables< lps::linear_process >(x); }
45std::set<data::variable> find_all_variables(const lps::stochastic_linear_process& x) { return lps::find_all_variables< lps::stochastic_linear_process >(x); }
46std::set<data::variable> find_all_variables(const lps::specification& x) { return lps::find_all_variables< lps::specification >(x); }
47std::set<data::variable> find_all_variables(const lps::stochastic_specification& x) { return lps::find_all_variables< lps::stochastic_specification >(x); }
48std::set<data::variable> find_all_variables(const lps::deadlock& x) { return lps::find_all_variables< lps::deadlock >(x); }
49std::set<data::variable> find_all_variables(const lps::multi_action& x) { return lps::find_all_variables< lps::multi_action >(x); }
50std::set<data::variable> find_free_variables(const lps::linear_process& x) { return lps::find_free_variables< lps::linear_process >(x); }
51std::set<data::variable> find_free_variables(const lps::stochastic_linear_process& x) { return lps::find_free_variables< lps::stochastic_linear_process >(x); }
52std::set<data::variable> find_free_variables(const lps::specification& x) { return lps::find_free_variables< lps::specification >(x); }
53std::set<data::variable> find_free_variables(const lps::stochastic_specification& x) { return lps::find_free_variables< lps::stochastic_specification >(x); }
54std::set<data::variable> find_free_variables(const lps::deadlock& x) { return lps::find_free_variables< lps::deadlock >(x); }
55std::set<data::variable> find_free_variables(const lps::multi_action& x) { return lps::find_free_variables< lps::multi_action >(x); }
56std::set<data::variable> find_free_variables(const lps::process_initializer& x) { return lps::find_free_variables< lps::process_initializer >(x); }
57std::set<data::variable> find_free_variables(const lps::stochastic_process_initializer& x) { return lps::find_free_variables< lps::stochastic_process_initializer >(x); }
58std::set<data::function_symbol> find_function_symbols(const lps::specification& x) { return lps::find_function_symbols< lps::specification >(x); }
59std::set<data::function_symbol> find_function_symbols(const lps::stochastic_specification& x) { return lps::find_function_symbols< lps::stochastic_specification >(x); }
60std::set<core::identifier_string> find_identifiers(const lps::specification& x) { return lps::find_identifiers< lps::specification >(x); }
61std::set<core::identifier_string> find_identifiers(const lps::stochastic_specification& x) { return lps::find_identifiers< lps::stochastic_specification >(x); }
62std::set<process::action_label> find_action_labels(const lps::linear_process& x) { return lps::find_action_labels< lps::linear_process >(x); }
63std::set<process::action_label> find_action_labels(const lps::process_initializer& x) { return lps::find_action_labels< lps::process_initializer >(x); }
64std::set<process::action_label> find_action_labels(const lps::specification& x) { return lps::find_action_labels< lps::specification >(x); }
65std::set<process::action_label> find_action_labels(const lps::stochastic_specification& x) { return lps::find_action_labels< lps::stochastic_specification >(x); }
66//--- end generated lps overloads ---//
67
69{
70 return data::replace_variables(atermpp::container_cast<data::data_expression_list>(process_parameters),
72}
73
75{
76 std::ostringstream out;
77 core::detail::apply_printer<lps::detail::printer> printer(out);
78 printer.print_summand_numbers() = true;
79 printer.apply(x);
80 return out.str();
81}
82
84{
85 std::ostringstream out;
86 core::detail::apply_printer<lps::detail::printer> printer(out);
87 printer.print_summand_numbers() = true;
88 printer.apply(x);
89 return out.str();
90}
91
93{
95}
96
98{
100}
101
103{
105}
106
108{
110}
111
112namespace detail {
113
115{
117 unsigned int start_symbol_index = p.start_symbol_index("MultAct");
118 bool partial_parses = false;
119 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
121 return result;
122}
123
125{
126 multi_action result = lps::typecheck_multi_action(x, typechecker);
127 result = lps::translate_user_notation(result);
128 lps::normalize_sorts(result, data_spec);
129 return result;
130}
131
133{
134 multi_action result = lps::typecheck_multi_action(x, data_spec, action_decls);
135 result = lps::translate_user_notation(result);
136 lps::normalize_sorts(result, data_spec);
137 return result;
138}
139
141{
143 unsigned int start_symbol_index = p.start_symbol_index("ActionRenameSpec");
144 bool partial_parses = false;
145 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
147 return result;
148}
149
151{
152 using namespace mcrl2::data;
154 x = action_rename_specification(x.data() + spec.data(), x.action_labels(), x.rules());
156}
157
158} // namespace detail
159
160} // namespace lps
161
162} // namespace mcrl2
Read-only singly linked list of action rename rules.
const std::vector< action_rename_rule > & rules() const
Returns the action rename rules.
const data::data_specification & data() const
Returns the data action_rename_specification.
const process::action_label_list & action_labels() const
Returns the sequence of action labels.
LPS summand containing a multi-action.
data::data_expression_list next_state(const data::variable_list &process_parameters) const
Returns the next state corresponding to this summand.
Definition lps.cpp:68
const data::assignment_list & assignments() const
Returns the sequence of assignments.
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
\brief A timed multi-action
const data::data_specification & data() const
Returns the data specification.
Linear process specification.
LPS summand containing a multi-action.
\brief A stochastic distribution
\brief An untyped multi action or data application
D_ParserTables parser_tables_mcrl2
add your file description here.
add your file description here.
add your file description here.
add your file description here.
add your file description here.
add your file description here.
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
static data_specification const & default_specification()
Definition parse.h:31
Namespace for all data library functionality.
Definition abstraction.h:22
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:90
void replace_variables(T &x, const Substitution &sigma, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Definition replace.h:213
bool check_well_typedness(const T &x)
Checks well typedness of an LPS object, and will print error messages to stderr.
void complete_action_rename_specification(action_rename_specification &x, const lps::stochastic_specification &spec)
Definition lps.cpp:150
process::untyped_multi_action parse_multi_action_new(const std::string &text)
Definition lps.cpp:114
multi_action complete_multi_action(process::untyped_multi_action &x, multi_action_type_checker &typechecker, const data::data_specification &data_spec=data::detail::default_specification())
Definition lps.cpp:124
action_rename_specification parse_action_rename_specification_new(const std::string &text)
Definition lps.cpp:140
void find_function_symbols(const T &x, OutputIterator o)
Definition find.h:138
std::string pp_with_summand_numbers(const specification &x)
Definition lps.cpp:74
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
multi_action typecheck_multi_action(process::untyped_multi_action &mult_act, const data::data_specification &data_spec, const process::action_label_list &action_decls)
Type check a multi action Throws an exception if something went wrong.
Definition typecheck.h:128
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
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
action_rename_specification typecheck_action_rename_specification(const action_rename_specification &arspec, const lps::stochastic_specification &lpsspec)
Type checks an action rename specification.
Definition typecheck.h:157
lps::multi_action translate_user_notation(const lps::multi_action &x)
Definition lps.cpp:41
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
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
Substitution that maps data variables to data expressions. The substitution is stored as an assignmen...
lps::action_rename_specification parse_ActionRenameSpec(const core::parse_node &node) const
Definition parse_impl.h:123
process::untyped_multi_action parse_MultAct(const core::parse_node &node) const
Definition parse_impl.h:33