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             : /// \file lts/detail/liblts_scc.h
      10             : 
      11             : #ifndef _LIBLTS_SCC_H
      12             : #define _LIBLTS_SCC_H
      13             : #include <unordered_set>
      14             : #include "mcrl2/lts/lts.h"
      15             : #include "mcrl2/utilities/logger.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace lts
      20             : {
      21             : 
      22             : namespace detail
      23             : {
      24             :   // An indexed sorted vector below contains the outgoing or incoming tau transitions per state,
      25             :   // grouped per state. The input consists of an automaton with transitions. The incoming/outcoming
      26             :   // tau transitions are grouped by state in the m_states_with_outgoing_or_incoming_tau_transition. 
      27             :   // It is as long as the lts aut has tau transitions. The vector m_indices is as long as the number
      28             :   // of states. For each state it contains the place in the other vector where its tau transitions
      29             :   // start. So, the tau transitions reside at position indices[s] to indices[s+1]. These indices
      30             :   // can be acquired using the functions lowerbound and upperbound. 
      31             :   // This data structure is chosen due to its minimal memory and time footprint. 
      32             :   template <class LTS_TYPE>
      33             :   class indexed_sorted_vector_for_tau_transitions
      34             :   {
      35             :     protected:
      36             :       typedef std::size_t state_type;
      37             :       typedef std::size_t label_type;
      38             : 
      39             :       std::vector <state_type> m_states_with_outgoing_or_incoming_tau_transition;
      40             :       std::vector <size_t> m_indices;
      41             : 
      42             :     public:
      43             : 
      44         576 :       indexed_sorted_vector_for_tau_transitions(const LTS_TYPE& aut, bool outgoing)
      45         576 :        : m_indices(aut.num_states()+1,0)
      46             :       {
      47             :         // First count the number of outgoing transitions per state and put it in indices.
      48        8162 :         for(const transition& t: aut.get_transitions())
      49             :         {
      50        7586 :           if (aut.is_tau(aut.apply_hidden_label_map(t.label())))
      51             :           {
      52        4154 :             m_indices[outgoing?t.from():t.to()]++;
      53             :           }
      54             :         }
      55             : 
      56             :         // Calculate the m_indices where the states with outgoing/incoming tau transition must be placed.
      57             :         // Put the starting index for state i at position i-1. When placing the transitions these indices
      58             :         // are decremented properly. 
      59             :         
      60         576 :         size_t sum=0;
      61        6524 :         for(state_type& i: m_indices)  // The vector is changed. This must be a reference. 
      62             :         {
      63        5948 :           sum=sum+i;
      64        5948 :           i=sum;
      65             :         }
      66             : 
      67             :         // Now declare enough space for all transitions and store them in reverse order, while
      68             :         // at the same time decrementing the indices in m_indices. 
      69         576 :         m_states_with_outgoing_or_incoming_tau_transition.resize(sum);
      70        8162 :         for(const transition& t: aut.get_transitions())
      71             :         {
      72        7586 :           if (aut.is_tau(aut.apply_hidden_label_map(t.label())))
      73             :           {
      74        4154 :             if (outgoing)
      75             :             {
      76        2077 :               assert(t.from()<m_indices.size());
      77        2077 :               assert(m_indices[t.from()]>0);
      78        2077 :               m_indices[t.from()]--;
      79        2077 :               assert(m_indices[t.from()] < m_states_with_outgoing_or_incoming_tau_transition.size());
      80        2077 :               m_states_with_outgoing_or_incoming_tau_transition[m_indices[t.from()]]=t.to();
      81             :             }
      82             :             else
      83             :             {
      84        2077 :               assert(t.to()<m_indices.size());
      85        2077 :               assert(m_indices[t.to()]>0);
      86        2077 :               m_indices[t.to()]--;
      87        2077 :               assert(m_indices[t.to()] < m_states_with_outgoing_or_incoming_tau_transition.size());
      88        2077 :               m_states_with_outgoing_or_incoming_tau_transition[m_indices[t.to()]]=t.from();
      89             :             }
      90             :           }
      91             :         }
      92         576 :         assert(m_indices.at(aut.num_states())==m_states_with_outgoing_or_incoming_tau_transition.size());
      93         576 :       }
      94             : 
      95             :       // Get the indexed transitions. 
      96        4154 :       const std::vector<state_type>& get_transitions() const
      97             :       {
      98        4154 :         return m_states_with_outgoing_or_incoming_tau_transition;
      99             :       }
     100             :     
     101             :       // Get the lowest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_tau_transition.
     102        5372 :       size_t lowerbound(const state_type s) const
     103             :       {
     104        5372 :         assert(s+1<m_indices.size());
     105        5372 :         return m_indices[s];
     106             :       }
     107             : 
     108             :       // Get 1 beyond the higest index of incoming/outging transitions stored in m_states_with_outgoing_or_incoming_tau_transition.
     109        5372 :       size_t upperbound(const state_type s) const
     110             :       {
     111        5372 :         assert(s+1<m_indices.size());
     112        5372 :         return m_indices[s+1];
     113             :       }
     114             : 
     115             :       // Drastically clear the vectors by resetting its memory usage to minimal. 
     116         288 :       void clear()   
     117             :       {
     118         288 :         std::vector <state_type>().swap(m_states_with_outgoing_or_incoming_tau_transition);
     119         288 :         std::vector <size_t>().swap(m_indices);
     120             :         
     121         288 :       }
     122             :   };
     123             : 
     124             : /// \brief This class contains an scc partitioner removing inert tau loops.
     125             : 
     126             : template < class LTS_TYPE>
     127             : class scc_partitioner
     128             : {
     129             : 
     130             :   public:
     131             :     /** \brief Creates an scc partitioner for an LTS.
     132             :      *  \details This scc partitioner calculates a partition
     133             :      *  of the state space of the transition system l using
     134             :      *  a straightforward algorithm found in A.V. Aho, J.E. Hopcroft
     135             :      *  and J.D. Ullman, Data structures and algorithms. Addison Wesley,
     136             :      *  1987 on page 224. All states that reside on a loop of internal
     137             :      *  actions are put in the same equivalence class. The function l.is_tau
     138             :      *  is used to determine whether an action is internal. Partitioning is
     139             :      *  done immediately when an instance of this class is created.
     140             :      *  When applying the function \ref replace_transition_system the
     141             :      *  automaton l is replaced by (aka shrinked to) the automaton modulo the
     142             :      *  calculated partition.
     143             :      *  \param[in] l reference to an LTS. */
     144             :     scc_partitioner(LTS_TYPE& l);
     145             : 
     146             :     /** \brief Destroys this partitioner. */
     147         288 :     ~scc_partitioner()=default;
     148             : 
     149             :     /** \brief The lts for which this partioner is created is replaced by the lts modulo
     150             :      *        the calculated partition.
     151             :      *  \details The number of states of the new lts becomes the number of
     152             :      *        equivalence classes. In each transition the start and end state
     153             :      *        are replaced by its equivalence class. If a transition has a tau
     154             :      *        label (which is checked using the function l.is_tau) then it
     155             :      *        is preserved if either from and to state are different, or
     156             :      *        \e preserve_divergence_loops is true. All non tau transitions are
     157             :      *        always preserved. The label numbers for preserved transitions are
     158             :      *        not changed. 
     159             :      *
     160             :      * \param[in] preserve_divergence_loops If true preserve a tau loop on states that
     161             :      *     were part of a larger tau loop in the input transition system. Otherwise idle
     162             :      *     tau loops are removed. */
     163             :     void replace_transition_system(const bool preserve_divergence_loops);
     164             : 
     165             :     /** \brief Gives the number of bisimulation equivalence classes of the LTS.
     166             :      *  \return The number of bisimulation equivalence classes of the LTS.
     167             :      */
     168             :     std::size_t num_eq_classes() const;
     169             : 
     170             :     /** \brief Gives the equivalence class number of a state.
     171             :      *  The equivalence class numbers range from 0 upto (and excluding)
     172             :      *  \ref num_eq_classes().
     173             :      *  \param[in] s A state number.
     174             :      *  \return The number of the equivalence class to which \e s
     175             :      *    belongs. */
     176             :     std::size_t get_eq_class(const std::size_t s) const;
     177             : 
     178             :     /** \brief Returns whether two states are in the same bisimulation
     179             :      *     equivalence class.
     180             :      * \param[in] s A state number.
     181             :      * \param[in] t A state number.
     182             :      * \retval true if \e s and \e t are in the same bisimulation
     183             :      *    equivalence class;
     184             :      * \retval false otherwise. */
     185             :     bool in_same_class(const std::size_t s, const std::size_t t) const;
     186             : 
     187             :   private:
     188             : 
     189             :     typedef std::size_t state_type;
     190             :     typedef std::size_t label_type;
     191             : 
     192             :     LTS_TYPE& aut;
     193             : 
     194             :     std::vector < state_type > block_index_of_a_state;
     195             :     std::vector < state_type > dfsn2state;
     196             :     state_type equivalence_class_index;
     197             : 
     198             :     void group_components(const state_type t,
     199             :                           const state_type equivalence_class_index,
     200             :                           const indexed_sorted_vector_for_tau_transitions<LTS_TYPE>& src_tgt_src,
     201             :                           std::vector < bool >& visited);
     202             :     void dfs_numbering(const state_type t,
     203             :                        const indexed_sorted_vector_for_tau_transitions<LTS_TYPE>& src_tgt,
     204             :                        std::vector < bool >& visited);
     205             : 
     206             : };
     207             : 
     208             : 
     209             : template < class LTS_TYPE>
     210         288 : scc_partitioner<LTS_TYPE>::scc_partitioner(LTS_TYPE& l)
     211         288 :   :aut(l),
     212         288 :     block_index_of_a_state(aut.num_states(),0),
     213         288 :     equivalence_class_index(0)
     214             : {
     215         288 :   mCRL2log(log::debug) << "Tau loop (SCC) partitioner created for " << l.num_states() << " states and " <<
     216           0 :               l.num_transitions() << " transitions" << std::endl;
     217             : 
     218         288 :   dfsn2state.reserve(aut.num_states());
     219             : 
     220             :   // Initialise the data structures used in the recursive DFS procedure.
     221         288 :   std::vector<bool> visited(aut.num_states(),false); 
     222         288 :   indexed_sorted_vector_for_tau_transitions<LTS_TYPE> src_tgt(aut,true); // Group the tau transitions ordered per outgoing states. 
     223             : 
     224             :   // Number the states via a depth first search
     225        2974 :   for (state_type i=0; i<aut.num_states(); ++i)
     226             :   {
     227        2686 :     dfs_numbering(i,src_tgt,visited);
     228             :   }
     229         288 :   src_tgt.clear();
     230             : 
     231         288 :   indexed_sorted_vector_for_tau_transitions<LTS_TYPE> tgt_src(aut,false);
     232         288 :   for (std::vector < state_type >::reverse_iterator i=dfsn2state.rbegin();
     233        2974 :        i!=dfsn2state.rend(); ++i)
     234             :   {
     235        2686 :     if (visited[*i])  // Visited is used inversely here.
     236             :     {
     237        2158 :       group_components(*i,equivalence_class_index,tgt_src,visited);
     238        2158 :       equivalence_class_index++;
     239             :     }
     240             :   }
     241         288 :   mCRL2log(log::debug) << "Tau loop (SCC) partitioner reduces lts to " << equivalence_class_index << " states." << std::endl;
     242             : 
     243         288 :   dfsn2state.clear();
     244         288 : }
     245             : 
     246             : 
     247             : template < class LTS_TYPE>
     248         240 : void scc_partitioner<LTS_TYPE>::replace_transition_system(const bool preserve_divergence_loops)
     249             : {
     250             :   // Put all the non inert transitions in a set. Add the transitions that form a self
     251             :   // loop. Such transitions only exist in case divergence preserving branching bisimulation is
     252             :   // used. A set is used to remove double occurrences of transitions.
     253         240 :   std::unordered_set < transition > resulting_transitions;
     254        3601 :   for (const transition& t: aut.get_transitions())
     255             :   {
     256        5386 :     if (!aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
     257        5386 :         preserve_divergence_loops ||
     258         962 :         block_index_of_a_state[t.from()]!=block_index_of_a_state[t.to()])
     259             :     {
     260        2890 :       resulting_transitions.insert(
     261        8670 :         transition(
     262             :           block_index_of_a_state[t.from()],
     263        2890 :           aut.apply_hidden_label_map(t.label()),
     264             :           block_index_of_a_state[t.to()]));
     265             :     }
     266             :   }
     267             : 
     268         240 :   aut.clear_transitions(resulting_transitions.size());
     269             :   // Copy the transitions from the set into the transition system.
     270             : 
     271        2766 :   for (const transition& t: resulting_transitions)
     272             :   {
     273        2526 :     aut.add_transition(transition(t.from(),t.label(),t.to()));
     274             :   }
     275             : 
     276             :   // Merge the states, by setting the state labels of each state to the concatenation of the state labels of its
     277             :   // equivalence class. 
     278         240 :   if (aut.has_state_info())   /* If there are no state labels this step can be ignored */
     279             :   {
     280             :     /* Create a vector for the new labels */
     281          33 :     std::vector<typename LTS_TYPE::state_label_t> new_labels(num_eq_classes());
     282             : 
     283         152 :     for(std::size_t i=aut.num_states(); i>0; )
     284             :     {
     285         119 :       --i;
     286         119 :       const std::size_t new_index=block_index_of_a_state[i];
     287         119 :       new_labels[new_index]=new_labels[new_index]+aut.state_label(i);
     288             :     }
     289             : 
     290         152 :     for(std::size_t i=0; i<num_eq_classes(); ++i)
     291             :     {
     292         119 :       aut.set_state_label(i,new_labels[i]);
     293             :     }
     294          33 :   }
     295             :   
     296         240 :   aut.set_num_states(num_eq_classes()); 
     297         240 :   aut.set_initial_state(get_eq_class(aut.initial_state()));
     298         240 : }
     299             : 
     300             : template < class LTS_TYPE>
     301         425 : std::size_t scc_partitioner<LTS_TYPE>::num_eq_classes() const
     302             : {
     303         425 :   return equivalence_class_index;
     304             : }
     305             : 
     306             : template < class LTS_TYPE>
     307         321 : std::size_t scc_partitioner<LTS_TYPE>::get_eq_class(const std::size_t s) const
     308             : {
     309         321 :   return block_index_of_a_state[s];
     310             : }
     311             : 
     312             : template < class LTS_TYPE>
     313          25 : bool scc_partitioner<LTS_TYPE>::in_same_class(const std::size_t s, const std::size_t t) const
     314             : {
     315          25 :   return get_eq_class(s)==get_eq_class(t);
     316             : }
     317             : 
     318             : // Private methods of scc_partitioner
     319             : 
     320             : template < class LTS_TYPE>
     321        4235 : void scc_partitioner<LTS_TYPE>::group_components(
     322             :   const state_type s,
     323             :   const state_type equivalence_class_index,
     324             :   const indexed_sorted_vector_for_tau_transitions<LTS_TYPE>& tgt_src,
     325             :   std::vector < bool >& visited)
     326             : {
     327        4235 :   if (!visited[s])
     328             :   {
     329        1549 :     return;
     330             :   }
     331        2686 :   visited[s] = false;
     332        2686 :   const size_t u=tgt_src.upperbound(s);  // only calculate the upperbound once. 
     333        4763 :   for(state_type i=tgt_src.lowerbound(s); i<u; ++i)
     334             :   {
     335        2077 :     group_components(tgt_src.get_transitions()[i],equivalence_class_index,tgt_src,visited);
     336             :   }
     337        2686 :   block_index_of_a_state[s]=equivalence_class_index;
     338             : }
     339             : 
     340             : template < class LTS_TYPE>
     341        4763 : void scc_partitioner<LTS_TYPE>::dfs_numbering(
     342             :   const state_type s,
     343             :   const indexed_sorted_vector_for_tau_transitions<LTS_TYPE>& src_tgt,
     344             :   std::vector < bool >& visited)
     345             : {
     346        4763 :   if (visited[s])
     347             :   {
     348        2077 :     return;
     349             :   }
     350        2686 :   visited[s] = true;
     351        2686 :   const size_t u=src_tgt.upperbound(s);  // only calculate the upperbound once. 
     352        4763 :   for(state_type i=src_tgt.lowerbound(s); i<u; ++i)
     353             :   {
     354        2077 :     dfs_numbering(src_tgt.get_transitions()[i],src_tgt,visited);
     355             :   }
     356        2686 :   dfsn2state.push_back(s);
     357             : }
     358             : 
     359             : } // namespace detail
     360             : 
     361             : template < class LTS_TYPE>
     362         209 : void scc_reduce(LTS_TYPE& l,const bool preserve_divergence_loops = false)
     363             : {
     364         209 :   detail::scc_partitioner<LTS_TYPE> scc_part(l);
     365         209 :   scc_part.replace_transition_system(preserve_divergence_loops);
     366         209 : }
     367             : 
     368             : }
     369             : }
     370             : #endif // _LIBLTS_SCC_H