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_summand.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_DEADLOCK_SUMMAND_H
      13             : #define MCRL2_LPS_DEADLOCK_SUMMAND_H
      14             : 
      15             : #include "mcrl2/lps/deadlock.h"
      16             : #include "mcrl2/lps/stochastic_distribution.h"
      17             : #include "mcrl2/lps/summand.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace lps {
      22             : 
      23             : /// \brief LPS summand containing a deadlock.
      24             : class deadlock_summand: public summand_base
      25             : {
      26             :   protected:
      27             :     /// \brief The super class
      28             :     typedef summand_base super;
      29             : 
      30             :     /// \brief The deadlock of the summand
      31             :     lps::deadlock m_deadlock;
      32             : 
      33             :   public:
      34             :     /// \brief Constructor.
      35             :     // TODO: check if the default constructor results in a deadlock summand
      36           2 :     deadlock_summand()
      37           2 :     {}
      38             : 
      39             :     /// \brief Constructor.
      40       32026 :     deadlock_summand(const data::variable_list& summation_variables, const data::data_expression& condition, const lps::deadlock& delta)
      41       32026 :       : summand_base(summation_variables, condition),
      42       32026 :         m_deadlock(delta)
      43       32026 :     {}
      44             : 
      45             :     /// Move semantics
      46       14297 :     deadlock_summand(const deadlock_summand&) noexcept = default;
      47       69611 :     deadlock_summand(deadlock_summand&&) noexcept = default;
      48         730 :     deadlock_summand& operator=(const deadlock_summand&) noexcept = default;
      49           2 :     deadlock_summand& operator=(deadlock_summand&&) noexcept = default;
      50             : 
      51             :     /// \brief Returns the deadlock of this summand.
      52       51204 :     const lps::deadlock& deadlock() const
      53             :     {
      54       51204 :       return m_deadlock;
      55             :     }
      56             : 
      57             :     /// \brief Returns the deadlock of this summand.
      58        8685 :     lps::deadlock& deadlock()
      59             :     {
      60        8685 :       return m_deadlock;
      61             :     }
      62             : 
      63             :     /// \brief Returns true if time is available.
      64             :     /// \return True if time is available.
      65        9232 :     bool has_time() const
      66             :     {
      67        9232 :       return m_deadlock.has_time();
      68             :     }
      69             : 
      70             :     /// \brief Swaps the contents
      71             :     void swap(deadlock_summand& other)
      72             :     {
      73             :       summand_base::swap(other);
      74             :       using std::swap;
      75             :       swap(m_deadlock, other.m_deadlock);
      76             :     }
      77             : };
      78             : 
      79             : //--- start generated class deadlock_summand ---//
      80             : /// \\brief list of deadlock_summands
      81             : typedef atermpp::term_list<deadlock_summand> deadlock_summand_list;
      82             : 
      83             : /// \\brief vector of deadlock_summands
      84             : typedef std::vector<deadlock_summand>    deadlock_summand_vector;
      85             : 
      86             : // prototype declaration
      87             : std::string pp(const deadlock_summand& x);
      88             : 
      89             : /// \\brief Outputs the object to a stream
      90             : /// \\param out An output stream
      91             : /// \\param x Object x
      92             : /// \\return The output stream
      93             : inline
      94           4 : std::ostream& operator<<(std::ostream& out, const deadlock_summand& x)
      95             : {
      96           4 :   return out << lps::pp(x);
      97             : }
      98             : 
      99             : /// \\brief swap overload
     100             : inline void swap(deadlock_summand& t1, deadlock_summand& t2)
     101             : {
     102             :   t1.swap(t2);
     103             : }
     104             : //--- end generated class deadlock_summand ---//
     105             : 
     106             : /// \brief Conversion to atermappl.
     107             : /// \return The deadlock summand converted to aterm format.
     108             : inline
     109          32 : atermpp::aterm_appl deadlock_summand_to_aterm(const deadlock_summand& s)
     110             : {
     111             :   atermpp::aterm_appl result = atermpp::aterm_appl(core::detail::function_symbol_LinearProcessSummand(),
     112          32 :                        s.summation_variables(),
     113             :                        s.condition(),
     114          64 :                        atermpp::aterm_appl(core::detail::function_symbol_Delta()),
     115          32 :                        s.deadlock().time(),
     116          64 :                        data::assignment_list(),
     117          32 :                        stochastic_distribution()
     118          96 :                      );
     119          32 :   return result;
     120             : }
     121             : 
     122             : } // namespace lps
     123             : 
     124             : } // namespace mcrl2
     125             : 
     126             : #endif // MCRL2_LPS_DEADLOCK_SUMMAND_H