mCRL2
Loading...
Searching...
No Matches
linear_process.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_LINEAR_PROCESS_H
13#define MCRL2_LPS_LINEAR_PROCESS_H
14
17// #include "mcrl2/lps/process_initializer.h" Is not used in this file.
18
19namespace mcrl2
20{
21
22namespace lps
23{
24
25namespace detail
26{
27
28// helper function for linear_process_base::linear_process_base(const atermpp::aterm_appl& lps)
29template <typename Summand>
32 const multi_action&,
35 )
36{
37 throw mcrl2::runtime_error("make_action_summand is not defined!");
38}
39
40template <>
41inline
43 const data::data_expression& condition,
44 const multi_action& a,
45 const data::assignment_list& assignments,
46 const stochastic_distribution& distribution
47 )
48{
49 (void)distribution; // Suppress an unused variable warning.
50 assert(!distribution.is_defined());
51 return action_summand(summation_variables, condition, a, assignments);
52}
53
54} // namespace detail
55
56class linear_process; // prototype declaration
57bool check_well_typedness(const linear_process& x);
58
59class stochastic_linear_process; // prototype declaration
60bool check_well_typedness(const stochastic_linear_process& x);
61
62template <typename ActionSummand>
64{
65 protected:
68
71
73 std::vector<ActionSummand> m_action_summands;
74
75 public:
77 typedef ActionSummand action_summand_type;
78
81
85 const std::vector<ActionSummand>& action_summands
86 )
87 :
91 { }
92
96 explicit linear_process_base(const atermpp::aterm_appl& lps, bool stochastic_distributions_allowed = true)
97 {
100 m_process_parameters = down_cast<data::variable_list>(lps[0]);
101 const auto& summands = atermpp::down_cast<atermpp::aterm_list>(lps[1]);
102 for (const atermpp::aterm& summand: summands)
103 {
105 const auto& t = down_cast<atermpp::aterm_appl>(summand);
106
107 const auto& summation_variables = down_cast<data::variable_list>(t[0]);
108 const auto& condition = down_cast<data::data_expression>(t[1]);
109 const auto& time = down_cast<data::data_expression>(t[3]);
110 const auto& assignments = down_cast<data::assignment_list>(t[4]);
111 const auto& distribution = down_cast<stochastic_distribution>(t[5]);
112 if (!stochastic_distributions_allowed && distribution.is_defined())
113 {
114 throw mcrl2::runtime_error("Summand with stochastic distribution encountered, while this tool is not yet able to deal with stochastic distributions.");
115 }
116 if (down_cast<atermpp::aterm_appl>(t[2]).function() == core::detail::function_symbols::Delta)
117 {
118 m_deadlock_summands.push_back(deadlock_summand(summation_variables, condition, deadlock(time)));
119 }
120 else
121 {
122 assert(lps::is_multi_action(down_cast<atermpp::aterm_appl>(t[2])));
123 const auto& actions = down_cast<process::action_list>(down_cast<atermpp::aterm_appl>(t[2])[0]);
124 m_action_summands.push_back(detail::make_action_summand<ActionSummand>(summation_variables, condition, multi_action(actions, time), assignments, distribution));
125 }
126 }
127 }
128
131 std::size_t summand_count() const
132 {
133 return m_deadlock_summands.size() + m_action_summands.size();
134 }
135
138 const std::vector<ActionSummand>& action_summands() const
139 {
140 return m_action_summands;
141 }
142
145 std::vector<ActionSummand>& action_summands()
146 {
147 return m_action_summands;
148 }
149
153 {
154 return m_deadlock_summands;
155 }
156
160 {
161 return m_deadlock_summands;
162 }
163
167 {
169 }
170
174 {
176 }
177
180 bool has_time() const
181 {
182 for (auto i = m_action_summands.begin(); i != m_action_summands.end(); ++i)
183 {
184 if (i->has_time())
185 {
186 return true;
187 }
188 }
189 for (auto i = m_deadlock_summands.begin(); i != m_deadlock_summands.end(); ++i)
190 {
191 if (i->deadlock().has_time())
192 {
193 return true;
194 }
195 }
196 return false;
197 }
198};
199
201class linear_process: public linear_process_base<action_summand>
202{
204
205 public:
207 linear_process() = default;
208
213 )
215 { }
216
219 explicit linear_process(const atermpp::aterm_appl& lps, bool = false)
220 : super(lps, false)
221 { }
222};
223
226template <typename ActionSummand>
228{
230 for (auto i = p.deadlock_summands().rbegin(); i != p.deadlock_summands().rend(); ++i)
231 {
233 summands.push_front(s);
234 }
235 for (auto i = p.action_summands().rbegin(); i != p.action_summands().rend(); ++i)
236 {
238 summands.push_front(s);
239 }
240
243 summands
244 );
245}
246
247//--- start generated class linear_process ---//
248// prototype declaration
249std::string pp(const linear_process& x);
250
255inline
256std::ostream& operator<<(std::ostream& out, const linear_process& x)
257{
258 return out << lps::pp(x);
259}
260//--- end generated class linear_process ---//
261
265inline
267{
269}
270
271// template function overloads
272std::set<data::variable> find_all_variables(const lps::linear_process& x);
273std::set<data::variable> find_free_variables(const lps::linear_process& x);
274std::set<process::action_label> find_action_labels(const lps::linear_process& x);
275
276} // namespace lps
277
278} // namespace mcrl2
279
280#endif // MCRL2_LPS_LINEAR_PROCESS_H
add your file description here.
The aterm base class that provides protection of the underlying shared terms.
Definition aterm.h:186
const function_symbol & function() const
Returns the function symbol belonging to an aterm_appl.
Definition aterm_appl.h:174
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
LPS summand containing a multi-action.
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
deadlock_summand_vector & deadlock_summands()
Returns the sequence of deadlock summands.
const std::vector< ActionSummand > & action_summands() const
Returns the sequence of action summands.
deadlock_summand_vector m_deadlock_summands
The deadlock summands of the process.
linear_process_base()=default
Constructor.
data::variable_list m_process_parameters
The process parameters of the process.
linear_process_base(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const std::vector< ActionSummand > &action_summands)
Constructor.
linear_process_base(const atermpp::aterm_appl &lps, bool stochastic_distributions_allowed=true)
Constructor.
bool has_time() const
Returns true if time is available in at least one of the summands.
data::variable_list & process_parameters()
Returns the sequence of process parameters.
std::vector< ActionSummand > m_action_summands
The action summands of the process.
ActionSummand action_summand_type
The action summand type.
const deadlock_summand_vector & deadlock_summands() const
Returns the sequence of deadlock summands.
std::vector< ActionSummand > & action_summands()
Returns the sequence of action summands.
std::size_t summand_count() const
Returns the number of LPS summands.
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
linear_process(const data::variable_list &process_parameters, const deadlock_summand_vector &deadlock_summands, const action_summand_vector &action_summands)
Constructor.
linear_process(const atermpp::aterm_appl &lps, bool=false)
Constructor.
linear_process()=default
Constructor.
linear_process_base< action_summand > super
\brief A timed multi-action
\brief A stochastic distribution
bool is_defined() const
Returns true if the distribution is defined, i.e. it contains a valid distribution....
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
term_appl< aterm > aterm_appl
Definition aterm_appl.h:353
const Derived & down_cast(const Base &t, typename std::enable_if< is_convertible< Base, Derived >::value &&!std::is_base_of< Derived, Base >::value >::type *=nullptr)
A cheap cast from one aterm based type to another When casting one aterm based type into another,...
Definition aterm.h:259
bool check_term_LinearProcess(const Term &t)
bool check_rule_LinearProcessSummand(const Term &t)
const atermpp::function_symbol & function_symbol_LinearProcess()
action_summand make_action_summand< action_summand >(const data::variable_list &summation_variables, const data::data_expression &condition, const multi_action &a, const data::assignment_list &assignments, const stochastic_distribution &distribution)
Summand make_action_summand(const data::variable_list &, const data::data_expression &, const multi_action &, const data::assignment_list &, const stochastic_distribution &)
atermpp::aterm_appl action_summand_to_aterm(const action_summand &s)
Conversion to aterm_appl.
atermpp::aterm_appl linear_process_to_aterm(const linear_process_base< ActionSummand > &p)
Conversion to aterm_appl.
atermpp::aterm_appl deadlock_summand_to_aterm(const deadlock_summand &s)
Conversion to atermappl.
bool check_well_typedness(const linear_process &x)
Definition lps.cpp:92
std::string pp(const action_summand &x)
Definition lps.cpp:26
std::vector< deadlock_summand > deadlock_summand_vector
\brief vector of deadlock_summands
std::ostream & operator<<(std::ostream &out, const action_summand &x)
std::set< data::variable > find_free_variables(const lps::deadlock &x)
Definition lps.cpp:54
std::vector< action_summand > action_summand_vector
\brief vector of action_summands
bool is_linear_process(const atermpp::aterm_appl &x)
Test for a linear_process expression.
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
bool is_multi_action(const atermpp::aterm_appl &x)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
static const atermpp::function_symbol Delta
static const atermpp::function_symbol LinearProcess