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/pbes/fixpoint_symbol.h 10 : /// \brief The class fixpoint_symbol. 11 : 12 : #ifndef MCRL2_PBES_FIXPOINT_SYMBOL_H 13 : #define MCRL2_PBES_FIXPOINT_SYMBOL_H 14 : 15 : #include "mcrl2/data/data_specification.h" 16 : 17 : namespace mcrl2 18 : { 19 : 20 : namespace pbes_system 21 : { 22 : 23 : //--- start generated class fixpoint_symbol ---// 24 : /// \\brief A fixpoint symbol 25 : class fixpoint_symbol: public atermpp::aterm_appl 26 : { 27 : public: 28 : /// \\brief Default constructor. 29 62 : fixpoint_symbol() 30 62 : : atermpp::aterm_appl(core::detail::default_values::FixPoint) 31 62 : {} 32 : 33 : /// \\brief Constructor. 34 : /// \\param term A term 35 3759 : explicit fixpoint_symbol(const atermpp::aterm& term) 36 3759 : : atermpp::aterm_appl(term) 37 : { 38 3759 : assert(core::detail::check_rule_FixPoint(*this)); 39 3759 : } 40 : 41 : /// Move semantics 42 12391 : fixpoint_symbol(const fixpoint_symbol&) noexcept = default; 43 7801 : fixpoint_symbol(fixpoint_symbol&&) noexcept = default; 44 135 : fixpoint_symbol& operator=(const fixpoint_symbol&) noexcept = default; 45 98 : fixpoint_symbol& operator=(fixpoint_symbol&&) noexcept = default; 46 : //--- start user section fixpoint_symbol ---// 47 : /// \brief Returns the mu symbol. 48 : /// \return The mu symbol. 49 3129 : static fixpoint_symbol mu() 50 : { 51 6258 : return fixpoint_symbol(atermpp::aterm_appl(core::detail::function_symbol_Mu())); 52 : } 53 : 54 : /// \brief Returns the nu symbol. 55 : /// \return The nu symbol. 56 630 : static fixpoint_symbol nu() 57 : { 58 1260 : return fixpoint_symbol(atermpp::aterm_appl(core::detail::function_symbol_Nu())); 59 : } 60 : 61 : /// \brief Returns true if the symbol is mu. 62 : /// \return True if the symbol is mu. 63 747 : bool is_mu() const 64 : { 65 747 : return function() == core::detail::function_symbols::Mu; 66 : } 67 : 68 : /// \brief Returns true if the symbol is nu. 69 : /// \return True if the symbol is nu. 70 43 : bool is_nu() const 71 : { 72 43 : return function() == core::detail::function_symbols::Nu; 73 : } 74 : //--- end user section fixpoint_symbol ---// 75 : }; 76 : 77 : /// \\brief list of fixpoint_symbols 78 : typedef atermpp::term_list<fixpoint_symbol> fixpoint_symbol_list; 79 : 80 : /// \\brief vector of fixpoint_symbols 81 : typedef std::vector<fixpoint_symbol> fixpoint_symbol_vector; 82 : 83 : // prototype declaration 84 : std::string pp(const fixpoint_symbol& x); 85 : 86 : /// \\brief Outputs the object to a stream 87 : /// \\param out An output stream 88 : /// \\param x Object x 89 : /// \\return The output stream 90 : inline 91 88 : std::ostream& operator<<(std::ostream& out, const fixpoint_symbol& x) 92 : { 93 88 : return out << pbes_system::pp(x); 94 : } 95 : 96 : /// \\brief swap overload 97 : inline void swap(fixpoint_symbol& t1, fixpoint_symbol& t2) 98 : { 99 : t1.swap(t2); 100 : } 101 : //--- end generated class fixpoint_symbol ---// 102 : 103 : } // namespace pbes_system 104 : 105 : } // namespace mcrl2 106 : 107 : #endif // MCRL2_PBES_FIXPOINT_SYMBOL_H