LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts - sigref.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 142 150 94.7 %
Date: 2019-09-14 00:54:39 Functions: 32 35 91.4 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen Keiren
       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 sigref.h
      10             : /// \brief Implementation of LTS reductions using the signature refinement
      11             : ///        approach of S. Blom and S. Orzan.
      12             : /// \author Jeroen Keiren
      13             : 
      14             : #ifndef MCRL2_LTS_SIGREF_H
      15             : #define MCRL2_LTS_SIGREF_H
      16             : 
      17             : #include <set>
      18             : #include <map>
      19             : #include <iostream>
      20             : #include "mcrl2/lts/lts.h"
      21             : #include "mcrl2/lts/lts_utilities.h"
      22             : #include "mcrl2/utilities/logger.h"
      23             : 
      24             : namespace mcrl2
      25             : {
      26             : namespace lts
      27             : {
      28             : 
      29             : /** \brief A signature is a pair of an action label and a block */
      30             : typedef std::set<std::pair<std::size_t, std::size_t> > signature_t;
      31             : 
      32             : /** \brief Base class for signature computation */
      33             : template < class LTS_T >
      34          53 : class signature
      35             : {
      36             : protected:
      37             :   /** \brief The labelled transition system for which the signature is computed */
      38             :   const LTS_T& m_lts;
      39             : 
      40             :   /** \brief Signature stored per state */
      41             :   std::vector<signature_t> m_sig;
      42             : 
      43             : public:
      44             :   /** \brief Constructor
      45             :     */
      46          53 :   signature(const LTS_T& lts_)
      47          53 :     : m_lts(lts_), m_sig(m_lts.num_states(), signature_t())
      48          53 :   {}
      49             : 
      50             :   /** \brief Compute a new signature based on \a partition.
      51             :     * \param[in] partition The current partition
      52             :     */
      53             :   virtual void compute_signature(const std::vector<std::size_t>& partition) = 0;
      54             : 
      55             :   /** \brief Compute the transitions for the quotient according to \a partition.
      56             :     * \param[in] partition The partition that is used to compute the quotient
      57             :     * \param[out] transitions A set to which the transitions of the quotient are written
      58             :     */
      59          19 :   virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
      60             :   {
      61         247 :     for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
      62             :     {
      63         228 :       transitions.insert(transition(partition[i->from()], i->label(), partition[i->to()]));
      64             :     }
      65          19 :   }
      66             : 
      67             :   /** \brief Return the signature for state \a i.
      68             :     * \param[in] i The state for which to return the signature.
      69             :     * \pre i < m_lts.num_states().
      70             :     */
      71        5814 :   virtual const signature_t& get_signature(std::size_t i) const
      72             :   {
      73        5814 :     return m_sig[i];
      74             :   }
      75             : };
      76             : 
      77             : /** \brief Class for computing the signature for strong bisimulation */
      78             : template < class LTS_T >
      79          19 : class signature_bisim: public signature<LTS_T>
      80             : {
      81             : protected:
      82             :   using signature<LTS_T>::m_lts;
      83             :   using signature<LTS_T>::m_sig;
      84             : 
      85             : public:
      86             :   /** \brief Constructor */
      87          19 :   signature_bisim(const LTS_T& lts_)
      88          19 :     : signature<LTS_T>(lts_)
      89             :   {
      90          19 :     mCRL2log(log::verbose, "sigref") << "initialising signature computation for strong bisimulation" << std::endl;
      91          19 :   }
      92             : 
      93             :   /** \overload */
      94             :   virtual void
      95          58 :   compute_signature(const std::vector<std::size_t>& partition)
      96             :   {
      97             :     // compute signatures
      98          58 :     m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
      99        1350 :     for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
     100             :     {
     101        1292 :       m_sig[i->from()].insert(std::make_pair(m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
     102             :     }
     103          58 :   }
     104             : 
     105             : };
     106             : 
     107             : /** \brief Class for computing the signature for branching bisimulation */
     108             : template < class LTS_T >
     109          34 : class signature_branching_bisim: public signature<LTS_T>
     110             : {
     111             : protected:
     112             :   using signature<LTS_T>::m_lts;
     113             :   using signature<LTS_T>::m_sig;
     114             : 
     115             :   /** \brief Store the incoming transitions per state */
     116             :   outgoing_transitions_per_state_t m_prev_transitions;
     117             : 
     118             :   /** \brief Insert function
     119             :     * \param[in] partition The current partition
     120             :     * \param[in] t source state
     121             :     * \param[in] label_ transition label
     122             :     * \param[in] block target block
     123             :     *
     124             :     * Insert function as described in S. Blom, S. Orzan,
     125             :     * "Distributed Branching Bisimulation Reduction of State Spaces",
     126             :     * Proc. PDMC 2003.
     127             :     *
     128             :     * Inserts the pair (label_, block) in the signature of t, as well as
     129             :     * the signatures of all tau-predecessors of t within the same block.
     130             :     */
     131        3487 :   void insert(const std::vector<std::size_t>& partition, const std::size_t t, const std::size_t label_, const std::size_t block)
     132             :   {
     133        3487 :     if(m_sig[t].insert(std::make_pair(label_, block)).second)
     134             :     {
     135             :       // std::pair<outgoing_transitions_per_state_t::const_iterator, outgoing_transitions_per_state_t::const_iterator> pred_range
     136             :       //    = m_prev_transitions.equal_range(t);
     137             : 
     138             :       // for(outgoing_transitions_per_state_t::const_iterator i = pred_range.first; i != pred_range.second; ++i)
     139             :       // for(const outgoing_pair_t& p: m_prev_transitions[t])
     140        6859 :       for (std::size_t i=m_prev_transitions.lowerbound(t); i<m_prev_transitions.upperbound(t); ++i)
     141             :       {
     142        4164 :         const outgoing_pair_t& p = m_prev_transitions.get_transitions()[i];
     143        4164 :         if(m_lts.is_tau(m_lts.apply_hidden_label_map(label(p))) && partition[t] == partition[to(p)])
     144             :         {
     145        2297 :           insert(partition, to(p), label_, block);
     146             :         }
     147             :       }
     148             :     }
     149        3487 :   }
     150             : 
     151             : public:
     152             :   /** \brief Constructor  */
     153          34 :   signature_branching_bisim(const LTS_T& lts_)
     154             :     : signature<LTS_T>(lts_),
     155          34 :       m_prev_transitions(lts_.get_transitions(),lts_.num_states(),false)  // transitions stored backward. 
     156             :   {
     157          34 :     mCRL2log(log::verbose, "sigref") << "initialising signature computation for branching bisimulation" << std::endl;
     158          34 :   }
     159             : 
     160             :   /** \overload */
     161          46 :   virtual void compute_signature(const std::vector<std::size_t>& partition)
     162             :   {
     163             :     // compute signatures
     164          46 :     m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
     165         933 :     for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
     166             :     {
     167         887 :       if (!(m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())) && (partition[i->from()] == partition[i->to()])))
     168             :       {
     169         533 :         insert(partition, i->from(), m_lts.apply_hidden_label_map(i->label()), partition[i->to()]);
     170             :       }
     171             :     }
     172          46 :   }
     173             : 
     174             :   /** \overload */
     175          19 :   virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
     176             :   {
     177         305 :     for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
     178             :     {
     179         286 :       if(partition[i->from()] != partition[i->to()] || !m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
     180             :       {
     181         166 :         transitions.insert(transition(partition[i->from()], m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
     182             :       }
     183             :     }
     184          19 :   }
     185             : };
     186             : 
     187             : /** \brief Class for computing the signature for divergence preserving branching bisimulation */
     188             : template < class LTS_T >
     189          15 : class signature_divergence_preserving_branching_bisim: public signature_branching_bisim<LTS_T>
     190             : {
     191             : protected:
     192             :   using signature_branching_bisim<LTS_T>::m_lts;
     193             :   using signature_branching_bisim<LTS_T>::m_sig;
     194             :   using signature_branching_bisim<LTS_T>::insert;
     195             : 
     196             :   /** \brief Record for each vertex whether it is in a tau-scc */
     197             :   std::vector<bool> m_divergent;
     198             : 
     199             :   /** \brief Iterative implementation of Tarjan's SCC algorithm.
     200             :    *
     201             :    * based on an earlier implementation by Sjoerd Cranen
     202             :    *
     203             :    * For the non-trivial tau-sccs (i.e. SCCs with more than one state, or
     204             :    * single-state SCCs with a tau-loop, we set \a m_divergent to true.
     205             :    */
     206          15 :   void compute_tau_sccs()
     207             :   {
     208          15 :     std::size_t unused = 1, lastscc = 1;
     209          30 :     std::vector<std::size_t> scc(m_lts.num_states(), 0);
     210          30 :     std::vector<std::size_t> low(m_lts.num_states(), 0);
     211          30 :     std::stack<std::size_t> stack;
     212          30 :     std::stack<std::size_t> sccstack;
     213             : 
     214             :     // Record forward transition relation sorted by state.
     215          30 :     outgoing_transitions_per_state_t m_lts_succ_transitions(m_lts.get_transitions(),m_lts.num_states(),true);
     216             : 
     217         273 :     for (std::size_t i = 0; i < m_lts.num_states(); ++i)
     218             :     {
     219         258 :       if (scc[i] == 0)
     220          81 :         stack.push(i);
     221        1298 :       while (!stack.empty())
     222             :       {
     223         520 :         const std::size_t vi = stack.top();
     224             : 
     225             :         // Outgoing transitions of vi.
     226             :         // std::pair<outgoing_transitions_per_state_t::const_iterator, outgoing_transitions_per_state_t::const_iterator> succ_range
     227             :         //  = m_lts_succ_transitions.equal_range(vi);
     228             : 
     229         520 :         if (low[vi] == 0 && scc[vi] == 0)
     230             :         {
     231         258 :           scc[vi] = unused;
     232         258 :           low[vi] = unused++;
     233         258 :           sccstack.push(vi);
     234             : 
     235             :           // for (outgoing_transitions_per_state_t::const_iterator t = succ_range.first; t != succ_range.second; ++t)
     236             :           // for (const outgoing_pair_t& t: m_lts_succ_transitions[vi]) 
     237             :           // for (const outgoing_pair_t& t: m_lts_succ_transitions[vi]) 
     238         624 :           for (std::size_t i=m_lts_succ_transitions.lowerbound(vi); i<m_lts_succ_transitions.upperbound(vi); ++i)
     239             :           {
     240         366 :             const outgoing_pair_t& t=m_lts_succ_transitions.get_transitions()[i];
     241         366 :             if ((low[to(t)] == 0) && (scc[to(t)] == 0) && (m_lts.is_tau(m_lts.apply_hidden_label_map(label(t)))))
     242             :             {
     243         181 :               stack.push(to(t));
     244             :             }
     245             :           }
     246             :         }
     247             :         else
     248             :         {
     249             :           // for (outgoing_transitions_per_state_t::const_iterator t = succ_range.first; t != succ_range.second; ++t)
     250         629 :           for (std::size_t i=m_lts_succ_transitions.lowerbound(vi); i<m_lts_succ_transitions.upperbound(vi); ++i)
     251             :           {
     252         367 :             const outgoing_pair_t& t=m_lts_succ_transitions.get_transitions()[i];
     253         367 :             if ((low[to(t)] != 0) && (m_lts.is_tau(m_lts.apply_hidden_label_map(label(t)))))
     254         105 :               low[vi] = low[vi] < low[to(t)] ? low[vi] : low[to(t)];
     255             :           }
     256         262 :           if (low[vi] == scc[vi])
     257             :           {
     258         183 :             std::size_t tos, scc_id = lastscc++;
     259         366 :             std::vector<std::size_t> this_scc;
     260         258 :             do
     261             :             {
     262         258 :               tos = sccstack.top();
     263         258 :               low[tos] = 0;
     264         258 :               scc[tos] = scc_id;
     265         258 :               sccstack.pop();
     266         258 :               this_scc.push_back(tos);
     267             :             }
     268             :             while (tos != vi);
     269             : 
     270             :             // We only consider non-trivial sccs, hence
     271             :             // if the scc consists of a single schate, check whether it has a tau-loop
     272         183 :             if(this_scc.size() == 1)
     273             :             {
     274             :               // for(outgoing_transitions_per_state_t::const_iterator i = succ_range.first; i != succ_range.second; ++i)
     275             :               // for (const outgoing_pair_t& i: m_lts_succ_transitions[vi]) 
     276         390 :               for (std::size_t i_=m_lts_succ_transitions.lowerbound(vi); i_<m_lts_succ_transitions.upperbound(vi); ++i_)
     277             :               {
     278         223 :                 const outgoing_pair_t& i=m_lts_succ_transitions.get_transitions()[i_];
     279         223 :                 if(vi == to(i) && m_lts.is_tau(m_lts.apply_hidden_label_map(label(i))))
     280             :                 {
     281           4 :                   m_divergent[tos] = true;
     282           4 :                   break;
     283             :                 }
     284             :               }
     285             :             }
     286             :             else
     287             :             {
     288          12 :               m_divergent[tos] = true;
     289             :             }
     290             :           }
     291         262 :           stack.pop();
     292             :         }
     293             :       }
     294             :     }
     295          15 :   }
     296             : 
     297             : public:
     298             :   /** \brief Constructor
     299             :     *
     300             :     * This initialises \a m_divergent to record for each vertex whether it is
     301             :     * in a tau-scc.
     302             :     */
     303          15 :   signature_divergence_preserving_branching_bisim(const LTS_T& lts_)
     304             :     : signature_branching_bisim<LTS_T>(lts_),
     305          15 :       m_divergent(lts_.num_states(), false)
     306             :   {
     307          15 :     mCRL2log(log::verbose, "sigref") << "initialising signature computation for divergence preserving branching bisimulation" << std::endl;
     308          15 :     compute_tau_sccs();
     309          15 :   }
     310             : 
     311             :   /** \overload
     312             :     *
     313             :     * Compute the signature as in branching bisimulation. In addition, add the
     314             :     * (tau, B) for edges s -tau-> t for which s,t in B and m_divergent[t]
     315             :     */
     316          38 :   virtual void compute_signature(const std::vector<std::size_t>& partition)
     317             :   {
     318             :     // compute signatures
     319          38 :     m_sig = std::vector<signature_t>(m_lts.num_states(), signature_t());
     320        1345 :     for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
     321             :     {
     322        4638 :       if(!(partition[i->from()] == partition[i->to()] && m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
     323        3458 :          || m_divergent[i->to()])
     324             :       {
     325         657 :         insert(partition, i->from(), m_lts.apply_hidden_label_map(i->label()), partition[i->to()]);
     326             :       }
     327             :     }
     328          38 :   }
     329             : 
     330             :   /** \overload */
     331          15 :   virtual void quotient_transitions(std::set<transition>& transitions, const std::vector<std::size_t>& partition)
     332             :   {
     333         381 :     for(std::vector<transition>::const_iterator i = m_lts.get_transitions().begin(); i != m_lts.get_transitions().end(); ++i)
     334             :     {
     335        1466 :       if(!(partition[i->from()] == partition[i->to()] && m_lts.is_tau(m_lts.apply_hidden_label_map(i->label())))
     336        1102 :          || m_sig[i->from()].find(std::make_pair(m_lts.apply_hidden_label_map(i->label()), partition[i->to()])) != m_sig[i->from()].end())
     337             :       {
     338         309 :         transitions.insert(transition(partition[i->from()], m_lts.apply_hidden_label_map(i->label()), partition[i->to()]));
     339             :       }
     340             :     }
     341          15 :   }
     342             : };
     343             : 
     344             : 
     345             : /** \brief Signature based reductions for labelled transition systems.
     346             :   *
     347             :   * The implementation is based on the description in
     348             :   * S. Blom, S. Orzan. "Distributed Branching Bisimulation Reduction of State
     349             :   * Spaces", in Proc. PDMC 2003.
     350             :   *
     351             :   * The specific signature is a parameter of the algorithm.
     352             :   */
     353             : template < class LTS_T, typename Signature >
     354          53 : class sigref
     355             : {
     356             : 
     357             : protected:
     358             :   /** \brief Current partition; for each state (std::size_t) the block in which
     359             :              it resides is recorded. */
     360             :   std::vector<std::size_t> m_partition;
     361             : 
     362             :   /** \brief The number of blocks in the current partition */
     363             :   std::size_t m_count;
     364             : 
     365             :   /** \brief The LTS that we are reducing */
     366             :   LTS_T& m_lts;
     367             : 
     368             :   /** \brief Instance of a class performing the signature computation for the
     369             :              current equivalence */
     370             :   Signature m_signature;
     371             : 
     372             :   /** \brief Print a signature (for debugging purposes) */
     373           0 :   std::string print_sig(const signature_t& sig)
     374             :   {
     375           0 :     std::stringstream os;
     376           0 :     os << "{ ";
     377           0 :     for(signature_t::const_iterator i = sig.begin(); i != sig.end() ; ++i)
     378             :     {
     379           0 :       os << " (" << pp(m_lts.action_label(i->first)) << ", " << i->second << ") ";
     380             :     }
     381           0 :     os << " }";
     382           0 :     return os.str();
     383             :   }
     384             : 
     385             :   /** \brief Compute the partition. Repeatedly updates the signatures, and
     386             :              the partition, until the partition stabilises */
     387          53 :   void compute_partition()
     388             :   {
     389          53 :     std::size_t count_prev = m_count;
     390          53 :     std::size_t iterations = 0;
     391             : 
     392          53 :     m_lts.sort_transitions(mcrl2::lts::lbl_tgt_src);
     393             : 
     394         142 :     do
     395             :     {
     396         142 :       mCRL2log(log::verbose, "sigref") << "Iteration " << iterations
     397           0 :                                        << " currently have " << m_count << " blocks" << std::endl;
     398             : 
     399         142 :       m_signature.compute_signature(m_partition);
     400             : 
     401         142 :       count_prev = m_count;
     402             : 
     403             :       // Map signatures to block numbers
     404         284 :       std::map<signature_t, std::size_t> hashtable;
     405         142 :       m_count = 0;
     406        2613 :       for(std::size_t i = 0; i < m_lts.num_states(); ++i)
     407             :       {
     408        2471 :         if(hashtable.find(m_signature.get_signature(i)) == hashtable.end())
     409             :         {
     410         872 :           mCRL2log(log::debug, "sigref") << "Adding block for signature " << print_sig(m_signature.get_signature(i)) << std::endl;
     411         872 :           hashtable[m_signature.get_signature(i)] = m_count++;
     412             :         }
     413             :       }
     414             : 
     415             :       // Map states to block numbers
     416        2613 :       for(std::size_t i = 0; i < m_lts.num_states(); ++i)
     417             :       {
     418        2471 :         m_partition[i] = hashtable[m_signature.get_signature(i)];
     419             :       }
     420             : 
     421         142 :       ++iterations;
     422             : 
     423         142 :     } while (count_prev != m_count);
     424             : 
     425          53 :     mCRL2log(log::verbose, "sigref") << "Done after " << iterations << " iterations with " << m_count << " blocks" << std::endl;
     426          53 :   }
     427             : 
     428             :   /** \brief Perform the quotient with respect to the partition that has
     429             :              been computed */
     430          53 :   void quotient()
     431             :   {
     432             :     // Assign the reduced LTS
     433          53 :     m_lts.set_num_states(m_count);
     434          53 :     m_lts.set_initial_state(m_partition[m_lts.initial_state()]);
     435             : 
     436             :     // Compute quotient transitions
     437             :     // implemented in the signature class because it differs per equivalence.
     438         106 :     std::set<transition> transitions;
     439          53 :     m_signature.quotient_transitions(transitions, m_partition);
     440             : 
     441             :     // Set quotient transitions
     442          53 :     m_lts.clear_transitions();
     443         463 :     for(std::set<transition>::const_iterator i = transitions.begin(); i != transitions.end(); ++i)
     444             :     {
     445         410 :       m_lts.add_transition(*i);
     446             :     }
     447          53 :   }
     448             : 
     449             : public:
     450             :   /** \brief Constructor
     451             :     * \param[in] lts_ The LTS that is being reduced
     452             :     */
     453          53 :   sigref(LTS_T& lts_)
     454             :     : m_partition(std::vector<std::size_t>(lts_.num_states(), 0)),
     455             :       m_count(0),
     456             :       m_lts(lts_),
     457          53 :       m_signature(lts_)
     458          53 :   {}
     459             : 
     460             :   /** \brief Perform the reduction, modulo the equivalence for which the
     461             :     *        signature has been passed in as template parameter
     462             :     */
     463          53 :   void run()
     464             :   {
     465             :     // No need for state labels in the reduced LTS.
     466          53 :     m_lts.clear_state_labels();
     467          53 :     compute_partition();
     468          53 :     quotient();
     469          53 :   }
     470             : };
     471             : 
     472             : } // namespace lts
     473             : } // namespace mcrl2
     474             : 
     475             : #endif // MCRL2_LTS_SIGREF_H

Generated by: LCOV version 1.12