Line data Source code
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 : // 9 : /// \file mcrl2/lps/deadlock.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_LPS_DEADLOCK_H 13 : #define MCRL2_LPS_DEADLOCK_H 14 : 15 : #include "mcrl2/data/print.h" 16 : 17 : namespace mcrl2 18 : { 19 : 20 : namespace lps 21 : { 22 : 23 : /// \brief Represents a deadlock 24 : /// \details A deadlock is 'delta' with an optional time tag. 25 : class deadlock 26 : { 27 : friend class deadlock_summand; 28 : 29 : protected: 30 : /// \brief The time of the deadlock. If <tt>m_time == data::undefined_real()</tt> 31 : /// the multi action has no time. 32 : data::data_expression m_time; 33 : 34 : public: 35 : /// \brief Constructor 36 31359 : deadlock(data::data_expression time = data::undefined_real()) 37 31359 : : m_time(time) 38 31359 : {} 39 : 40 : /// \brief Returns true if time is available. 41 : /// \return True if time is available. 42 20581 : bool has_time() const 43 : { 44 20581 : return m_time != data::undefined_real(); 45 : } 46 : 47 : /// \brief Returns the time. 48 : /// \return The time. 49 39431 : const data::data_expression& time() const 50 : { 51 39431 : return m_time; 52 : } 53 : 54 : /// \brief Returns the time. 55 : /// \return The time. 56 9011 : data::data_expression& time() 57 : { 58 9011 : return m_time; 59 : } 60 : 61 : /// \brief Returns a string representation of the deadlock 62 : std::string to_string() const 63 : { 64 : return std::string("delta") + (has_time() ? (" @ " + data::pp(m_time)) : ""); 65 : } 66 : 67 : /// \brief Comparison operator 68 : bool operator==(const deadlock& other) const 69 : { 70 : return m_time == other.m_time; 71 : } 72 : 73 : /// \brief Comparison operator 74 : bool operator!=(const deadlock& other) const 75 : { 76 : return !(*this == other); 77 : } 78 : 79 : /// \brief Swaps the contents 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 ---// 88 : /// \\brief list of deadlocks 89 : typedef atermpp::term_list<deadlock> deadlock_list; 90 : 91 : /// \\brief vector of deadlocks 92 : typedef std::vector<deadlock> deadlock_vector; 93 : 94 : // prototype declaration 95 : std::string pp(const deadlock& x); 96 : 97 : /// \\brief Outputs the object to a stream 98 : /// \\param out An output stream 99 : /// \\param x Object x 100 : /// \\return The output stream 101 : inline 102 4 : std::ostream& operator<<(std::ostream& out, const deadlock& x) 103 : { 104 4 : return out << lps::pp(x); 105 : } 106 : 107 : /// \\brief swap overload 108 : inline void swap(deadlock& t1, deadlock& t2) 109 : { 110 : t1.swap(t2); 111 : } 112 : //--- end generated class deadlock ---// 113 : 114 : // template function overloads 115 : std::set<data::variable> find_all_variables(const lps::deadlock& x); 116 : std::set<data::variable> find_free_variables(const lps::deadlock& x); 117 : std::string pp(const lps::deadlock& x); 118 : 119 : } // namespace lps 120 : 121 : } // namespace mcrl2 122 : 123 : #endif // MCRL2_LPS_DEADLOCK_H