LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_scc.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 100 108 92.6 %
Date: 2020-07-11 00:44:39 Functions: 15 15 100.0 %
Legend: Lines: hit not hit

          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         548 :   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         548 :       indexed_sorted_vector_for_tau_transitions(const LTS_TYPE& aut, bool outgoing)
      45         548 :        : m_indices(aut.num_states()+1,0)
      46             :       {
      47             :         // First count the number of outgoing transitions per state and put it in indices.
      48        8022 :         for(const transition& t: aut.get_transitions())
      49             :         {
      50        7474 :           if (aut.is_tau(aut.apply_hidden_label_map(t.label())))
      51             :           {
      52        4124 :             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         548 :         size_t sum=0;
      61        6400 :         for(state_type& i: m_indices)  // The vector is changed. This must be a reference. 
      62             :         {
      63        5852 :           sum=sum+i;
      64        5852 :           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         548 :         m_states_with_outgoing_or_incoming_tau_transition.resize(sum);
      70        8022 :         for(const transition& t: aut.get_transitions())
      71             :         {
      72        7474 :           if (aut.is_tau(aut.apply_hidden_label_map(t.label())))
      73             :           {
      74        4124 :             if (outgoing)
      75             :             {
      76        2062 :               assert(t.from()<m_indices.size());
      77        2062 :               assert(m_indices[t.from()]>0);
      78        2062 :               m_indices[t.from()]--;
      79        2062 :               assert(m_indices[t.from()] < m_states_with_outgoing_or_incoming_tau_transition.size());
      80        2062 :               m_states_with_outgoing_or_incoming_tau_transition[m_indices[t.from()]]=t.to();
      81             :             }
      82             :             else
      83             :             {
      84        2062 :               assert(t.to()<m_indices.size());
      85        2062 :               assert(m_indices[t.to()]>0);
      86        2062 :               m_indices[t.to()]--;
      87        2062 :               assert(m_indices[t.to()] < m_states_with_outgoing_or_incoming_tau_transition.size());
      88        2062 :               m_states_with_outgoing_or_incoming_tau_transition[m_indices[t.to()]]=t.from();
      89             :             }
      90             :           }
      91             :         }
      92         548 :         assert(m_indices.at(aut.num_states())==m_states_with_outgoing_or_incoming_tau_transition.size());
      93         548 :       }
      94             : 
      95             :       // Get the indexed transitions. 
      96        4124 :       const std::vector<state_type>& get_transitions() const
      97             :       {
      98        4124 :         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        5304 :       size_t lowerbound(const state_type s) const
     103             :       {
     104        5304 :         assert(s+1<m_indices.size());
     105        5304 :         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        5304 :       size_t upperbound(const state_type s) const
     110             :       {
     111        5304 :         assert(s+1<m_indices.size());
     112        5304 :         return m_indices[s+1];
     113             :       }
     114             : 
     115             :       // Drastically clear the vectors by resetting its memory usage to minimal. 
     116         274 :       void clear()   
     117             :       {
     118         274 :         std::vector <state_type>().swap(m_states_with_outgoing_or_incoming_tau_transition);
     119         274 :         std::vector <size_t>().swap(m_indices);
     120             :         
     121         274 :       }
     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         274 :     ~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. Note that this routine does not adapt the number of
     159             :      *        states or the initial state of the lts.
     160             :      *
     161             :      * \param[in] preserve_divergence_loops If true preserve a tau loop on states that
     162             :      *     were part of a larger tau loop in the input transition system. Otherwise idle
     163             :      *     tau loops are removed. */
     164             :     void replace_transition_system(const bool preserve_divergence_loops);
     165             : 
     166             :     /** \brief Gives the number of bisimulation equivalence classes of the LTS.
     167             :      *  \return The number of bisimulation equivalence classes of the LTS.
     168             :      */
     169             :     std::size_t num_eq_classes() const;
     170             : 
     171             :     /** \brief Gives the equivalence class number of a state.
     172             :      *  The equivalence class numbers range from 0 upto (and excluding)
     173             :      *  \ref num_eq_classes().
     174             :      *  \param[in] s A state number.
     175             :      *  \return The number of the equivalence class to which \e s
     176             :      *    belongs. */
     177             :     std::size_t get_eq_class(const std::size_t s) const;
     178             : 
     179             :     /** \brief Returns whether two states are in the same bisimulation
     180             :      *     equivalence class.
     181             :      * \param[in] s A state number.
     182             :      * \param[in] t A state number.
     183             :      * \retval true if \e s and \e t are in the same bisimulation
     184             :      *    equivalence class;
     185             :      * \retval false otherwise. */
     186             :     bool in_same_class(const std::size_t s, const std::size_t t) const;
     187             : 
     188             :   private:
     189             : 
     190             :     typedef std::size_t state_type;
     191             :     typedef std::size_t label_type;
     192             : 
     193             :     LTS_TYPE& aut;
     194             : 
     195             :     std::vector < state_type > block_index_of_a_state;
     196             :     std::vector < state_type > dfsn2state;
     197             :     state_type equivalence_class_index;
     198             : 
     199             :     void group_components(const state_type t,
     200             :                           const state_type equivalence_class_index,
     201             :                           const indexed_sorted_vector_for_tau_transitions<LTS_TYPE>& src_tgt_src,
     202             :                           std::vector < bool >& visited);
     203             :     void dfs_numbering(const state_type t,
     204             :                        const indexed_sorted_vector_for_tau_transitions<LTS_TYPE>& src_tgt,
     205             :                        std::vector < bool >& visited);
     206             : 
     207             : };
     208             : 
     209             : 
     210             : template < class LTS_TYPE>
     211         274 : scc_partitioner<LTS_TYPE>::scc_partitioner(LTS_TYPE& l)
     212             :   :aut(l),
     213         274 :     block_index_of_a_state(aut.num_states(),0),
     214         548 :     equivalence_class_index(0)
     215             : {
     216         274 :   mCRL2log(log::debug) << "Tau loop (SCC) partitioner created for " << l.num_states() << " states and " <<
     217           0 :               l.num_transitions() << " transitions" << std::endl;
     218             : 
     219         274 :   dfsn2state.reserve(aut.num_states());
     220             : 
     221             :   // Initialise the data structures used in the recursive DFS procedure.
     222         548 :   std::vector<bool> visited(aut.num_states(),false); 
     223         548 :   indexed_sorted_vector_for_tau_transitions<LTS_TYPE> src_tgt(aut,true); // Group the tau transitions ordered per outgoing states. 
     224             : 
     225             :   // Number the states via a depth first search
     226        2926 :   for (state_type i=0; i<aut.num_states(); ++i)
     227             :   {
     228        2652 :     dfs_numbering(i,src_tgt,visited);
     229             :   }
     230         274 :   src_tgt.clear();
     231             : 
     232         548 :   indexed_sorted_vector_for_tau_transitions<LTS_TYPE> tgt_src(aut,false);
     233        2926 :   for (std::vector < state_type >::reverse_iterator i=dfsn2state.rbegin();
     234        2926 :        i!=dfsn2state.rend(); ++i)
     235             :   {
     236        2652 :     if (visited[*i])  // Visited is used inversely here.
     237             :     {
     238        2124 :       group_components(*i,equivalence_class_index,tgt_src,visited);
     239        2124 :       equivalence_class_index++;
     240             :     }
     241             :   }
     242         274 :   mCRL2log(log::debug) << "Tau loop (SCC) partitioner reduces lts to " << equivalence_class_index << " states." << std::endl;
     243             : 
     244         274 :   dfsn2state.clear();
     245         274 : }
     246             : 
     247             : 
     248             : template < class LTS_TYPE>
     249         226 : void scc_partitioner<LTS_TYPE>::replace_transition_system(const bool preserve_divergence_loops)
     250             : {
     251             :   // Put all the non inert transitions in a set. Add the transitions that form a self
     252             :   // loop. Such transitions only exist in case divergence preserving branching bisimulation is
     253             :   // used. A set is used to remove double occurrences of transitions.
     254         452 :   std::unordered_set < transition > resulting_transitions;
     255        3531 :   for (const transition& t: aut.get_transitions())
     256             :   {
     257        8620 :     if (!aut.is_tau(aut.apply_hidden_label_map(t.label())) ||
     258        4260 :         preserve_divergence_loops ||
     259         955 :         block_index_of_a_state[t.from()]!=block_index_of_a_state[t.to()])
     260             :     {
     261        8502 :       resulting_transitions.insert(
     262        5668 :         transition(
     263             :           block_index_of_a_state[t.from()],
     264        2834 :           aut.apply_hidden_label_map(t.label()),
     265             :           block_index_of_a_state[t.to()]));
     266             :     }
     267             :   }
     268             : 
     269         226 :   aut.clear_transitions(resulting_transitions.size());
     270             :   // Copy the transitions from the set into the transition system.
     271             : 
     272        2704 :   for (const transition& t: resulting_transitions)
     273             :   {
     274        2478 :     aut.add_transition(transition(t.from(),t.label(),t.to()));
     275             :   }
     276             : 
     277             :   // Merge the states, by setting the state labels of each state to the concatenation of the state labels of its
     278             :   // equivalence class. 
     279         226 :   if (aut.has_state_info())   /* If there are no state labels this step can be ignored */
     280             :   {
     281             :     /* Create a vector for the new labels */
     282           0 :     std::vector<typename LTS_TYPE::state_label_t> new_labels(num_eq_classes());
     283             : 
     284           0 :     for(std::size_t i=aut.num_states(); i>0; )
     285             :     {
     286           0 :       --i;
     287           0 :       const std::size_t new_index=block_index_of_a_state[i];
     288           0 :       new_labels[new_index]=new_labels[new_index]+aut.state_label(i);
     289             :     }
     290             : 
     291           0 :     for(std::size_t i=0; i<num_eq_classes(); ++i)
     292             :     {
     293           0 :       aut.set_state_label(i,new_labels[i]);
     294             :     }
     295             :   }
     296             :   
     297         226 :   aut.set_num_states(num_eq_classes()); 
     298         226 :   aut.set_initial_state(get_eq_class(aut.initial_state()));
     299         226 : }
     300             : 
     301             : template < class LTS_TYPE>
     302         226 : std::size_t scc_partitioner<LTS_TYPE>::num_eq_classes() const
     303             : {
     304         226 :   return equivalence_class_index;
     305             : }
     306             : 
     307             : template < class LTS_TYPE>
     308         305 : std::size_t scc_partitioner<LTS_TYPE>::get_eq_class(const std::size_t s) const
     309             : {
     310         305 :   return block_index_of_a_state[s];
     311             : }
     312             : 
     313             : template < class LTS_TYPE>
     314          25 : bool scc_partitioner<LTS_TYPE>::in_same_class(const std::size_t s, const std::size_t t) const
     315             : {
     316          25 :   return get_eq_class(s)==get_eq_class(t);
     317             : }
     318             : 
     319             : // Private methods of scc_partitioner
     320             : 
     321             : template < class LTS_TYPE>
     322        4186 : void scc_partitioner<LTS_TYPE>::group_components(
     323             :   const state_type s,
     324             :   const state_type equivalence_class_index,
     325             :   const indexed_sorted_vector_for_tau_transitions<LTS_TYPE>& tgt_src,
     326             :   std::vector < bool >& visited)
     327             : {
     328        4186 :   if (!visited[s])
     329             :   {
     330        1534 :     return;
     331             :   }
     332        2652 :   visited[s] = false;
     333        2652 :   const size_t u=tgt_src.upperbound(s);  // only calculate the upperbound once. 
     334        4714 :   for(state_type i=tgt_src.lowerbound(s); i<u; ++i)
     335             :   {
     336        2062 :     group_components(tgt_src.get_transitions()[i],equivalence_class_index,tgt_src,visited);
     337             :   }
     338        2652 :   block_index_of_a_state[s]=equivalence_class_index;
     339             : }
     340             : 
     341             : template < class LTS_TYPE>
     342        4714 : void scc_partitioner<LTS_TYPE>::dfs_numbering(
     343             :   const state_type s,
     344             :   const indexed_sorted_vector_for_tau_transitions<LTS_TYPE>& src_tgt,
     345             :   std::vector < bool >& visited)
     346             : {
     347        4714 :   if (visited[s])
     348             :   {
     349        2062 :     return;
     350             :   }
     351        2652 :   visited[s] = true;
     352        2652 :   const size_t u=src_tgt.upperbound(s);  // only calculate the upperbound once. 
     353        4714 :   for(state_type i=src_tgt.lowerbound(s); i<u; ++i)
     354             :   {
     355        2062 :     dfs_numbering(src_tgt.get_transitions()[i],src_tgt,visited);
     356             :   }
     357        2652 :   dfsn2state.push_back(s);
     358             : }
     359             : 
     360             : } // namespace detail
     361             : 
     362             : template < class LTS_TYPE>
     363         197 : void scc_reduce(LTS_TYPE& l,const bool preserve_divergence_loops = false)
     364             : {
     365         394 :   detail::scc_partitioner<LTS_TYPE> scc_part(l);
     366         197 :   scc_part.replace_transition_system(preserve_divergence_loops);
     367         197 : }
     368             : 
     369             : }
     370             : }
     371             : #endif // _LIBLTS_SCC_H

Generated by: LCOV version 1.13