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/action_summand.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_ACTION_SUMMAND_H
      13             : #define MCRL2_LPS_ACTION_SUMMAND_H
      14             : 
      15             : #include "mcrl2/lps/multi_action.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 multi-action.
      24             : class action_summand: public summand_base
      25             : {
      26             :   protected:
      27             :     /// \brief The super class
      28             :     typedef summand_base super;
      29             : 
      30             :     /// \brief The summation variables of the summand
      31             :     lps::multi_action m_multi_action;
      32             : 
      33             :     /// \brief The assignments of the next state
      34             :     data::assignment_list m_assignments;
      35             : 
      36             :   public:
      37             :     /// \brief Constructor.
      38          23 :     action_summand()
      39          23 :     {}
      40             : 
      41             :     /// \brief Constructor.
      42       34592 :     action_summand(const data::variable_list& summation_variables, const data::data_expression& condition, const lps::multi_action& action, const data::assignment_list& assignments)
      43       34592 :       : summand_base(summation_variables, condition),
      44       34592 :         m_multi_action(action),
      45       69184 :         m_assignments(assignments)
      46       34592 :     {}
      47             : 
      48             :     /// Move semantics
      49       36732 :     action_summand(const action_summand&) noexcept = default;
      50       71854 :     action_summand(action_summand&&) noexcept = default;
      51        2765 :     action_summand& operator=(const action_summand&) noexcept = default;
      52         331 :     action_summand& operator=(action_summand&&) noexcept = default;
      53             : 
      54             :     /// \brief Returns the multi-action of this summand.
      55      348006 :     const lps::multi_action& multi_action() const
      56             :     {
      57      348006 :       return m_multi_action;
      58             :     }
      59             : 
      60             :     /// \brief Returns the multi-action of this summand.
      61       10677 :     lps::multi_action& multi_action()
      62             :     {
      63       10677 :       return m_multi_action;
      64             :     }
      65             : 
      66             :     /// \brief Returns the sequence of assignments.
      67             :     /// \return The sequence of assignments.
      68       69316 :     const data::assignment_list& assignments() const
      69             :     {
      70       69316 :       return m_assignments;
      71             :     }
      72             : 
      73             :     /// \brief Returns the sequence of assignments.
      74             :     /// \return The sequence of assignments.
      75       12572 :     data::assignment_list& assignments()
      76             :     {
      77       12572 :       return m_assignments;
      78             :     }
      79             : 
      80             :     // TODO: check if this is correct (where is the documentation of the internal format?)
      81             :     /// \brief Returns true if the multi-action corresponding to this summand is equal to tau.
      82             :     /// \return True if the multi-action corresponding to this summand is equal to tau.
      83       16856 :     bool is_tau() const
      84             :     {
      85       16856 :       return multi_action().actions().empty();
      86             :     }
      87             : 
      88             :     /// \brief Returns true if time is available.
      89             :     /// \return True if time is available.
      90      100010 :     bool has_time() const
      91             :     {
      92      100010 :       return m_multi_action.has_time();
      93             :     }
      94             : 
      95             :     /// \brief Returns the next state corresponding to this summand.
      96             :     /// \details The next state is constructed out of the assignments in
      97             :     /// this summand, by substituting the assignments to the list of
      98             :     /// variables that are an argument of this function. In general this
      99             :     /// argument is the list with the process parameters of this process.
     100             :     /// \param process_parameters A sequence of data variables
     101             :     /// \return A symbolic representation of the next states
     102             :     data::data_expression_list next_state(const data::variable_list& process_parameters) const;
     103             : 
     104             :     /// \brief Swaps the contents
     105             :     void swap(action_summand& other)
     106             :     {
     107             :       summand_base::swap(other);
     108             :       using std::swap;
     109             :       swap(m_multi_action, other.m_multi_action);
     110             :       swap(m_assignments, other.m_assignments);
     111             :     }
     112             : };
     113             : 
     114             : //--- start generated class action_summand ---//
     115             : /// \\brief list of action_summands
     116             : typedef atermpp::term_list<action_summand> action_summand_list;
     117             : 
     118             : /// \\brief vector of action_summands
     119             : typedef std::vector<action_summand>    action_summand_vector;
     120             : 
     121             : // prototype declaration
     122             : std::string pp(const action_summand& x);
     123             : 
     124             : /// \\brief Outputs the object to a stream
     125             : /// \\param out An output stream
     126             : /// \\param x Object x
     127             : /// \\return The output stream
     128             : inline
     129           0 : std::ostream& operator<<(std::ostream& out, const action_summand& x)
     130             : {
     131           0 :   return out << lps::pp(x);
     132             : }
     133             : 
     134             : /// \\brief swap overload
     135             : inline void swap(action_summand& t1, action_summand& t2)
     136             : {
     137             :   t1.swap(t2);
     138             : }
     139             : //--- end generated class action_summand ---//
     140             : 
     141             : /// \brief Comparison operator for action summands.
     142             : inline
     143             : bool operator<(const action_summand& x, const action_summand& y)
     144             : {
     145             :   if (x.summation_variables() != y.summation_variables())
     146             :   {
     147             :     return x.summation_variables() < y.summation_variables();
     148             :   }
     149             :   if (x.condition() != y.condition())
     150             :   {
     151             :     return x.condition() < y.condition();
     152             :   }
     153             :   if (x.multi_action() != y.multi_action())
     154             :   {
     155             :     return x.multi_action() < y.multi_action();
     156             :   }
     157             :   return x.assignments() < y.assignments();
     158             : }
     159             : 
     160             : /// \brief Equality operator of action summands
     161             : inline
     162           1 : bool operator==(const action_summand& x, const action_summand& y)
     163             : {
     164           2 :   return x.summation_variables() == y.summation_variables() &&
     165           2 :          x.condition() == y.condition() &&
     166           3 :          x.multi_action() == y.multi_action() &&
     167           2 :          x.assignments() == y.assignments();
     168             : }
     169             : 
     170             : /// \brief Conversion to aterm_appl.
     171             : inline
     172          50 : atermpp::aterm_appl action_summand_to_aterm(const action_summand& s)
     173             : {
     174             :   atermpp::aterm_appl result = atermpp::aterm_appl(core::detail::function_symbol_LinearProcessSummand(),
     175          50 :                        s.summation_variables(),
     176             :                        s.condition(),
     177             :                        s.multi_action(),
     178          50 :                        s.multi_action().time(),
     179          50 :                        s.assignments(),
     180          50 :                        lps::stochastic_distribution()
     181         100 :                      );
     182          50 :   return result;
     183             : }
     184             : 
     185             : } // namespace lps
     186             : 
     187             : } // namespace mcrl2
     188             : 
     189             : #endif // MCRL2_LPS_ACTION_SUMMAND_H