Line data    Source code

       1             : // Author(s): Jan Friso Groote (upon request by Matthew Hennessy)
       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_weak_bisim.h
      10             : /// \brief This file defines an algorithm for weak bisimulation, by
      11             : ///        calculating the transitive tau closure and apply strong
      12             : ///        bisimulation afterwards. In order to apply this algorithm
      13             : ///        it is advisable to first apply a branching bisimulation reduction.
      14             : 
      15             : #ifndef _LIBLTS_WEAK_BISIM_H
      16             : #define _LIBLTS_WEAK_BISIM_H
      17             : #include "mcrl2/lts/detail/liblts_scc.h"
      18             : #include "mcrl2/lts/detail/liblts_tau_star_reduce.h"
      19             : #include "mcrl2/lts/detail/liblts_merge.h"
      20             : #include "mcrl2/lts/lts_aut.h"
      21             : #include "mcrl2/lts/lts_fsm.h"
      22             : #include "mcrl2/lts/lts_dot.h"
      23             : 
      24             : namespace mcrl2
      25             : {
      26             : namespace lts
      27             : {
      28             : namespace detail
      29             : {
      30             : 
      31             : /** \brief Reduce LTS l with respect to (divergence-preserving) weak bisimulation.
      32             :  * \param[in/out] l The transition system that is reduced.
      33             :  * \param[in] preserve_divergences Indicates whether loops of internal actions on states must be preserved. If false
      34             :  *            these are removed. If true these are preserved.  */
      35             : template < class LTS_TYPE>
      36          35 : void weak_bisimulation_reduce(
      37             :   LTS_TYPE& l,
      38             :   const bool preserve_divergences = false)
      39             : {
      40          35 :   if (1 < l.num_states())
      41             :   {
      42          33 :     bisimulation_reduce_dnj(l, true, preserve_divergences);   //< Apply branching bisimulation to l.
      43             :   }
      44             : 
      45             :   std::size_t divergence_label;
      46          35 :   if (preserve_divergences)
      47             :   {
      48          16 :     divergence_label=mark_explicit_divergence_transitions(l);
      49             :   }
      50          35 :   if (1 < l.num_states())
      51             :   {
      52          24 :     reflexive_transitive_tau_closure(l);                      // Apply transitive tau closure to l.
      53          24 :     bisimulation_reduce_dnj(l, false, false);                 // Apply strong bisimulation to l.
      54             :   }
      55          35 :   scc_reduce(l);                                              // Remove tau loops.
      56          35 :   remove_redundant_transitions(l);                            // Remove transitions s -a-> s' if also s-a->-tau->s' or s-tau->-a->s' is present.
      57             :                                                               // Note that this is correct, because l is reduced modulo strong bisimulation and
      58             :                                                               // does not contain tau loops.
      59          35 :   if (preserve_divergences)
      60             :   {
      61          16 :     unmark_explicit_divergence_transitions(l,divergence_label);
      62             :   }
      63          35 : }
      64             : 
      65             : 
      66             : /** \brief Checks whether the initial states of two LTSs are weakly bisimilar.
      67             :  * \details The LTSs l1 and l2 are not usable anymore after this call.
      68             :  *          The space consumption is O(n) and running time is dominated by the
      69             :  *          transitive closure (after branching bisimulation).
      70             :  * \param[in/out] l1 A first transition system.
      71             :  * \param[in/out] l2 A second transistion system.
      72             :  * \param[preserve_divergences] If true and branching is true, preserve tau loops on states.
      73             :  * \retval True iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar */
      74             : template < class LTS_TYPE>
      75           0 : bool destructive_weak_bisimulation_compare(
      76             :   LTS_TYPE& l1,
      77             :   LTS_TYPE& l2,
      78             :   const bool preserve_divergences=false)
      79             : {
      80           0 :   weak_bisimulation_reduce(l1,preserve_divergences);
      81           0 :   weak_bisimulation_reduce(l2,preserve_divergences);
      82           0 :   return destructive_bisimulation_compare_dnj(l1,l2);
      83             : }
      84             : 
      85             : 
      86             : /** \brief Checks whether the initial states of two LTSs are weakly bisimilar.
      87             :  *  \details The LTSs l1 and l2 are first duplicated and subsequently
      88             :  *           reduced modulo bisimulation. If memory space is a concern, one could consider to
      89             :  *           use destructive_weak_bisimulation_compare.  The running time
      90             :  *           of this routine is dominated by the transitive closure
      91             :  *           (after branching bisimulation).  It uses O(m+n) memory
      92             :  *           in addition to the copies of l1 and l2, where n is the
      93             :  *           number of states and m is the number of transitions.
      94             :  * \param[in/out] l1 A first transition system.
      95             :  * \param[in/out] l2 A second transistion system.
      96             :  * \param[preserve_divergences] If true and branching is true, preserve tau loops on states.
      97             :  * \retval True iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar */
      98             : template < class LTS_TYPE>
      99             : bool weak_bisimulation_compare(
     100             :   const LTS_TYPE& l1,
     101             :   const LTS_TYPE& l2,
     102             :   const bool preserve_divergences = false)
     103             : {
     104             :   LTS_TYPE l1_copy(l1);
     105             :   LTS_TYPE l2_copy(l2);
     106             :   return destructive_weak_bisimulation_compare(l1_copy, l2_copy,
     107             :                                                          preserve_divergences);
     108             : }
     109             : 
     110             : }
     111             : }
     112             : }
     113             : #endif  // #define _LIBLTS_WEAK_BISIM_H