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             : 
      11             : #ifndef MCRL2_LTS_DETAIL_TRANSITION_H
      12             : #define MCRL2_LTS_DETAIL_TRANSITION_H
      13             : 
      14             : #include <set>
      15             : #include "mcrl2/lts/transition.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace lts
      20             : {
      21             : 
      22             : namespace detail
      23             : {
      24             : 
      25       22899 : inline std::size_t apply_hidden_labels(const std::size_t n, const std::set<std::size_t>& hidden_action_set)
      26             : {
      27       22899 :   if (hidden_action_set.count(n)==0)
      28             :   {
      29       22899 :     return n;
      30             :   }
      31           0 :   return lts::const_tau_label_index;  // 0 is the index of the internal action. 
      32             : }
      33             : 
      34             : class compare_transitions_slt
      35             : {
      36             :   protected:
      37             :     const std::set<std::size_t>& m_hide_action_set;
      38             : 
      39             :   public:
      40         161 :     compare_transitions_slt(const std::set<std::size_t>& hide_action_set)
      41         161 :      : m_hide_action_set(hide_action_set)
      42         161 :     {}
      43             : 
      44        6938 :     bool operator()(const transition& t1, const transition& t2)
      45             :     {
      46        6938 :       if (t1.from() != t2.from())
      47             :       {
      48        6130 :         return t1.from() < t2.from();
      49             :       }
      50             :       else 
      51             :       {
      52         808 :         const std::size_t n1=apply_hidden_labels(t1.label(), m_hide_action_set);
      53         808 :         const std::size_t n2=apply_hidden_labels(t2.label(), m_hide_action_set);
      54         808 :         if (n1 != n2)
      55             :         {
      56         496 :           return n1 < n2;
      57             :         }
      58             :         else
      59             :         {
      60         312 :           return t1.to() < t2.to();
      61             :         }
      62             :       }
      63             :     }
      64             : };
      65             : 
      66             : class compare_transitions_lts
      67             : {
      68             :   protected:
      69             :     const std::set<std::size_t>& m_hide_action_set;
      70             : 
      71             :   public:
      72         504 :     compare_transitions_lts(const std::set<std::size_t>& hide_action_set)
      73         504 :      : m_hide_action_set(hide_action_set)
      74         504 :     {}
      75             : 
      76       10359 :     bool operator()(const transition& t1, const transition& t2)
      77             :     {
      78       10359 :       const std::size_t n1=apply_hidden_labels(t1.label(), m_hide_action_set);
      79       10359 :       const std::size_t n2=apply_hidden_labels(t2.label(), m_hide_action_set);
      80       10359 :       if (n1 != n2)
      81             :       {
      82        2934 :         return n1 < n2;
      83             :       }
      84        7425 :       else if (t1.to() != t2.to())
      85             :       {
      86        6759 :         return t1.to() < t2.to();
      87             :       }
      88             :       else
      89             :       {
      90         666 :         return t1.from() < t2.from();
      91             :       }
      92             :     }
      93             : };
      94             : 
      95             : } // detail
      96             : } // lts
      97             : } // mcrl2
      98             : 
      99             : #endif