mCRL2
Loading...
Searching...
No Matches
deadlock_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_DEADLOCK_SUMMAND_H
13#define MCRL2_LPS_DEADLOCK_SUMMAND_H
14
15#include "mcrl2/lps/deadlock.h"
17#include "mcrl2/lps/summand.h"
18
19namespace mcrl2 {
20
21namespace lps {
22
25{
26 protected:
29
32
33 public:
35 // TODO: check if the default constructor results in a deadlock summand
37 {}
38
42 m_deadlock(delta)
43 {}
44
46 deadlock_summand(const deadlock_summand&) noexcept = default;
47 deadlock_summand(deadlock_summand&&) noexcept = default;
48 deadlock_summand& operator=(const deadlock_summand&) noexcept = default;
49 deadlock_summand& operator=(deadlock_summand&&) noexcept = default;
50
52 const lps::deadlock& deadlock() const
53 {
54 return m_deadlock;
55 }
56
59 {
60 return m_deadlock;
61 }
62
65 bool has_time() const
66 {
67 return m_deadlock.has_time();
68 }
69
72 {
73 summand_base::swap(other);
74 using std::swap;
76 }
77};
78
79//--- start generated class deadlock_summand ---//
82
84typedef std::vector<deadlock_summand> deadlock_summand_vector;
85
86// prototype declaration
87std::string pp(const deadlock_summand& x);
88
93inline
94std::ostream& operator<<(std::ostream& out, const deadlock_summand& x)
95{
96 return out << lps::pp(x);
97}
98
101{
102 t1.swap(t2);
103}
104//--- end generated class deadlock_summand ---//
105
108inline
110{
113 s.condition(),
115 s.deadlock().time(),
118 );
119 return result;
120}
121
122} // namespace lps
123
124} // namespace mcrl2
125
126#endif // MCRL2_LPS_DEADLOCK_SUMMAND_H
LPS summand containing a deadlock.
summand_base super
The super class.
lps::deadlock m_deadlock
The deadlock of the summand.
deadlock_summand(deadlock_summand &&) noexcept=default
void swap(deadlock_summand &other)
Swaps the contents.
deadlock_summand(const deadlock_summand &) noexcept=default
Move semantics.
deadlock_summand(const data::variable_list &summation_variables, const data::data_expression &condition, const lps::deadlock &delta)
Constructor.
const lps::deadlock & deadlock() const
Returns the deadlock of this summand.
bool has_time() const
Returns true if time is available.
lps::deadlock & deadlock()
Returns the deadlock of this summand.
Represents a deadlock.
Definition deadlock.h:26
bool has_time() const
Returns true if time is available.
Definition deadlock.h:42
const data::data_expression & time() const
Returns the time.
Definition deadlock.h:49
\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
add your file description here.
term_appl< aterm > aterm_appl
Definition aterm_appl.h:353
const atermpp::function_symbol & function_symbol_Delta()
const atermpp::function_symbol & function_symbol_LinearProcessSummand()
atermpp::aterm_appl deadlock_summand_to_aterm(const deadlock_summand &s)
Conversion to atermappl.
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)
void swap(action_summand &t1, action_summand &t2)
\brief swap overload
atermpp::term_list< deadlock_summand > deadlock_summand_list
\brief list of deadlock_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.