Line data    Source code

       1             : // Author(s): Muck van Weerdenburg, Jan Friso Groote
       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             : 
      10             : /** \file
      11             :  *
      12             :  * \brief A header file defining a transition as a triple from,label,to.
      13             :  * \author Muck van Weerdenburg, Jan Friso Groote
      14             :  */
      15             : 
      16             : 
      17             : #ifndef MCRL2_LTS_TRANSITION_H
      18             : #define MCRL2_LTS_TRANSITION_H
      19             : 
      20             : #include <functional>
      21             : 
      22             : namespace mcrl2
      23             : {
      24             : namespace lts
      25             : {
      26             : 
      27             : static const std::size_t const_tau_label_index=0;
      28             : 
      29             : /** \brief Transition sort styles.
      30             :  * \details This enumerated type defines sort styles for transitions.
      31             :  * They can be used to sort the transitions of an LTS based on various
      32             :  * criteria. */
      33             : enum transition_sort_style
      34             : {
      35             :   src_lbl_tgt, /**< Sort first on source state, then on label, then on target state */
      36             :   lbl_tgt_src /**< Sort first on label, then on target state, then on source state*/
      37             : };
      38             : 
      39             : /// \brief A class containing triples, source label and target representing transitions.
      40             : /// \details A transition consists of three indices, indicated by transition::size_type
      41             : ///          that refer to a source, label and target.
      42             : class transition
      43             : {
      44             :   public:
      45             :     /// \brief The type of the elements in a transition.
      46             :     typedef std::size_t size_type;
      47             : 
      48             :   private:
      49             :     size_type m_from;
      50             :     size_type m_label;
      51             :     size_type m_to;
      52             : 
      53             :   public:
      54             :     // There is no default constructor
      55             :     transition() = delete;
      56             : 
      57             :     /// \brief Constructor (there is no default constructor).
      58       21115 :     transition(const std::size_t f,
      59             :                const std::size_t l,
      60       21115 :                const std::size_t t):m_from(f),m_label(l),m_to(t)
      61       21115 :     {}
      62             : 
      63             :     /// \brief Copy constructor.
      64             :     transition(const transition& t) = default;
      65             : 
      66             :     /// \brief Move constructor.
      67             :     transition(transition&& t) = default;
      68             : 
      69             :     /// \brief Assignment.
      70             :     transition& operator=(const transition& t) = default;
      71             : 
      72             :     /// \brief Move assignment.
      73             :     transition& operator=(transition&& t) = default;
      74             : 
      75             :     /// \brief The source of the transition.
      76             :     size_type
      77      106404 :     from() const
      78             :     {
      79      106404 :       return m_from;
      80             :     }
      81             : 
      82             :     /// \brief The label of the transition.
      83       96758 :     size_type label() const
      84             :     {
      85       96758 :       return m_label;
      86             :     }
      87             : 
      88             :     ///\brief The target of the transition.
      89             :     size_type
      90       98550 :     to() const
      91             :     {
      92       98550 :       return m_to;
      93             :     }
      94             : 
      95             :     /// \brief Set the source of the transition.
      96             :     void
      97             :     set_from(const size_type from)
      98             :     {
      99             :       m_from = from;
     100             :     }
     101             : 
     102             :     /// \brief Set the label of the transition.
     103             :     void
     104         653 :     set_label(const size_type label)
     105             :     {
     106         653 :       m_label = label;
     107         653 :     }
     108             : 
     109             :     ///\brief Set the target of the transition.
     110             :     void
     111             :     set_to(const size_type to)
     112             :     {
     113             :       m_to = to;
     114             :     }
     115             : 
     116             :     ///\brief Standard equality on transitions.
     117             :     bool
     118         989 :     operator ==(const transition& t) const
     119             :     {
     120         989 :       return m_from == t.m_from && m_label == t.m_label && m_to == t.m_to;
     121             :     }
     122             : 
     123             :     ///\brief Standard inequality on transitions.
     124             :     bool
     125             :     operator !=(const transition& t) const
     126             :     {
     127             :       return !(*this==t);
     128             :     }
     129             : 
     130             :     ///\brief Standard lexicographic ordering on transitions.
     131             :     ///\details The ordering is lexicographic from left to right.
     132             :     ///         First t.from are compared, then the label, and
     133             :     ///         if these do not determine the ordering, to is investigated.
     134             :     bool
     135       12661 :     operator <(const transition& t) const
     136             :     {
     137       17281 :       return m_from < t.m_from || (m_from == t.m_from && (m_label
     138       17281 :                                    < t.m_label || (m_label == t.m_label && m_to < t.m_to)));
     139             :     }
     140             : };
     141             : 
     142             : } // namespace lts
     143             : } // namespace mcrl2
     144             : 
     145             : namespace std
     146             : {
     147             : 
     148             : /// \brief specialization of the standard std::hash function.
     149             : template<>
     150             : struct hash<mcrl2::lts::transition>
     151             : {
     152        2890 :   std::size_t operator()(const mcrl2::lts::transition& t) const
     153             :   {
     154        2890 :     return t.from() << 2 ^ t.label() << 1 ^ t.to();
     155             :   }
     156             : };
     157             : 
     158             : } // namespace std
     159             : 
     160             : 
     161             : #include "mcrl2/lts/detail/transition.h"
     162             : 
     163             : #endif // MCRL2_LTS_TRANSITION_H