mCRL2
Loading...
Searching...
No Matches
action_summand.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_ACTION_SUMMAND_H
13#define MCRL2_LPS_ACTION_SUMMAND_H
14
17#include "mcrl2/lps/summand.h"
18
19namespace mcrl2 {
20
21namespace lps {
22
25{
26 protected:
29
32
35
36 public:
39 {}
40
44 m_multi_action(action),
46 {}
47
49 action_summand(const action_summand&) noexcept = default;
50 action_summand(action_summand&&) noexcept = default;
51 action_summand& operator=(const action_summand&) noexcept = default;
52 action_summand& operator=(action_summand&&) noexcept = default;
53
55 const lps::multi_action& multi_action() const
56 {
57 return m_multi_action;
58 }
59
62 {
63 return m_multi_action;
64 }
65
69 {
70 return m_assignments;
71 }
72
76 {
77 return m_assignments;
78 }
79
80 // TODO: check if this is correct (where is the documentation of the internal format?)
83 bool is_tau() const
84 {
85 return multi_action().actions().empty();
86 }
87
90 bool has_time() const
91 {
92 return m_multi_action.has_time();
93 }
94
102 data::data_expression_list next_state(const data::variable_list& process_parameters) const;
103
105 void swap(action_summand& other)
106 {
107 summand_base::swap(other);
108 using std::swap;
111 }
112};
113
114//--- start generated class action_summand ---//
117
119typedef std::vector<action_summand> action_summand_vector;
120
121// prototype declaration
122std::string pp(const action_summand& x);
123
128inline
129std::ostream& operator<<(std::ostream& out, const action_summand& x)
130{
131 return out << lps::pp(x);
132}
133
135inline void swap(action_summand& t1, action_summand& t2)
136{
137 t1.swap(t2);
138}
139//--- end generated class action_summand ---//
140
142inline
144{
146 {
148 }
149 if (x.condition() != y.condition())
150 {
151 return x.condition() < y.condition();
152 }
153 if (x.multi_action() != y.multi_action())
154 {
155 return x.multi_action() < y.multi_action();
156 }
157 return x.assignments() < y.assignments();
158}
159
161inline
163{
164 return x.summation_variables() == y.summation_variables() &&
165 x.condition() == y.condition() &&
166 x.multi_action() == y.multi_action() &&
167 x.assignments() == y.assignments();
168}
169
171inline
173{
176 s.condition(),
177 s.multi_action(),
178 s.multi_action().time(),
179 s.assignments(),
181 );
182 return result;
183}
184
185} // namespace lps
186
187} // namespace mcrl2
188
189#endif // MCRL2_LPS_ACTION_SUMMAND_H
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:267
LPS summand containing a multi-action.
lps::multi_action m_multi_action
The summation variables of the summand.
action_summand(const action_summand &) noexcept=default
Move semantics.
data::assignment_list & assignments()
Returns the sequence of assignments.
void swap(action_summand &other)
Swaps the contents.
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
action_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::multi_action &action, const data::assignment_list &assignments)
Constructor.
bool has_time() const
Returns true if time is available.
bool is_tau() const
Returns true if the multi-action corresponding to this summand is equal to tau.
summand_base super
The super class.
const lps::multi_action & multi_action() const
Returns the multi-action of this summand.
action_summand(action_summand &&) noexcept=default
const data::assignment_list & assignments() const
Returns the sequence of assignments.
data::assignment_list m_assignments
The assignments of the next state.
lps::multi_action & multi_action()
Returns the multi-action of this summand.
\brief A timed multi-action
bool has_time() const
Returns true if time is available.
const process::action_list & actions() const
const data::data_expression & time() const
\brief A stochastic distribution
Base class for LPS summands.
Definition summand.h:25
const data::data_expression & condition() const
Returns the condition expression.
Definition summand.h:60
void swap(summand_base &other)
Swaps the contents.
Definition summand.h:73
data::variable_list & summation_variables()
Returns the sequence of summation variables.
Definition summand.h:46
Multi-action class.
term_appl< aterm > aterm_appl
Definition aterm_appl.h:353
const atermpp::function_symbol & function_symbol_LinearProcessSummand()
atermpp::aterm_appl action_summand_to_aterm(const action_summand &s)
Conversion to aterm_appl.
atermpp::term_list< action_summand > action_summand_list
\brief list of action_summands
std::string pp(const action_summand &x)
Definition lps.cpp:26
std::ostream & operator<<(std::ostream &out, const action_summand &x)
void swap(action_summand &t1, action_summand &t2)
\brief swap overload
bool operator==(const action_summand &x, const action_summand &y)
Equality operator of action summands.
std::vector< action_summand > action_summand_vector
\brief vector of action_summands
bool operator<(const action_summand &x, const action_summand &y)
Comparison operator for action summands.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
void swap(atermpp::unprotected_aterm &t1, atermpp::unprotected_aterm &t2) noexcept
Swaps two aterms.
Definition aterm.h:384
add your file description here.
The class summand.