mCRL2
Loading...
Searching...
No Matches
deadlock.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_H
13#define MCRL2_LPS_DEADLOCK_H
14
15#include "mcrl2/data/print.h"
16
17namespace mcrl2
18{
19
20namespace lps
21{
22
26{
27 friend class deadlock_summand;
28
29 protected:
33
34 public:
37 : m_time(time)
38 {}
39
42 bool has_time() const
43 {
44 return m_time != data::undefined_real();
45 }
46
50 {
51 return m_time;
52 }
53
57 {
58 return m_time;
59 }
60
62 std::string to_string() const
63 {
64 return std::string("delta") + (has_time() ? (" @ " + data::pp(m_time)) : "");
65 }
66
68 bool operator==(const deadlock& other) const
69 {
70 return m_time == other.m_time;
71 }
72
74 bool operator!=(const deadlock& other) const
75 {
76 return !(*this == other);
77 }
78
80 void swap(deadlock& other)
81 {
82 using std::swap;
83 swap(m_time, other.m_time);
84 }
85};
86
87//--- start generated class deadlock ---//
90
92typedef std::vector<deadlock> deadlock_vector;
93
94// prototype declaration
95std::string pp(const deadlock& x);
96
101inline
102std::ostream& operator<<(std::ostream& out, const deadlock& x)
103{
104 return out << lps::pp(x);
105}
106
108inline void swap(deadlock& t1, deadlock& t2)
109{
110 t1.swap(t2);
111}
112//--- end generated class deadlock ---//
113
114// template function overloads
115std::set<data::variable> find_all_variables(const lps::deadlock& x);
116std::set<data::variable> find_free_variables(const lps::deadlock& x);
117std::string pp(const lps::deadlock& x);
118
119} // namespace lps
120
121} // namespace mcrl2
122
123#endif // MCRL2_LPS_DEADLOCK_H
A list of aterm objects.
Definition aterm_list.h:24
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
bool operator!=(const deadlock &other) const
Comparison operator.
Definition deadlock.h:74
data::data_expression m_time
The time of the deadlock. If m_time == data::undefined_real() the multi action has no time.
Definition deadlock.h:32
deadlock(data::data_expression time=data::undefined_real())
Constructor.
Definition deadlock.h:36
bool has_time() const
Returns true if time is available.
Definition deadlock.h:42
std::string to_string() const
Returns a string representation of the deadlock.
Definition deadlock.h:62
const data::data_expression & time() const
Returns the time.
Definition deadlock.h:49
void swap(deadlock &other)
Swaps the contents.
Definition deadlock.h:80
data::data_expression & time()
Returns the time.
Definition deadlock.h:56
bool operator==(const deadlock &other) const
Comparison operator.
Definition deadlock.h:68
Provides utilities for pretty printing.
const data::data_expression & undefined_real()
Returns a data expression of type Real that corresponds to 'undefined'.
Definition undefined.h:66
std::string pp(const abstraction &x)
Definition data.cpp:39
std::string pp(const action_summand &x)
Definition lps.cpp:26
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
void swap(action_summand &t1, action_summand &t2)
\brief swap overload
atermpp::term_list< deadlock > deadlock_list
\brief list of deadlocks
Definition deadlock.h:89
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:48
std::vector< deadlock > deadlock_vector
\brief vector of deadlocks
Definition deadlock.h:92
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_core &t1, atermpp::unprotected_aterm_core &t2) noexcept
Swaps two aterms.
Definition aterm.h:462