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

          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          31 : void weak_bisimulation_reduce(
      37             :   LTS_TYPE& l,
      38             :   const bool preserve_divergences = false)
      39             : {
      40          31 :   bisimulation_reduce_dnj(l, true, preserve_divergences);
      41             :   //< Apply branching bisimulation to l.
      42             : 
      43             :   std::size_t divergence_label;
      44          31 :   if (preserve_divergences)
      45             :   {
      46          14 :     divergence_label=mark_explicit_divergence_transitions(l);
      47             :   } 
      48          31 :   reflexive_transitive_tau_closure(l);                        // Apply transitive tau closure to l.
      49          31 :   bisimulation_reduce_dnj(l, false, false);                  // Apply strong bisimulation to l.
      50          31 :   scc_reduce(l);                                              // Remove tau loops.
      51          31 :   remove_redundant_transitions(l);                            // Remove transitions s -a-> s' if also s-a->-tau->s' or s-tau->-a->s' is present.
      52             :                                                               // Note that this is correct, because l is reduced modulo strong bisimulation and
      53             :                                                               // does not contain tau loops. 
      54          31 :   if (preserve_divergences)
      55             :   {
      56          14 :     unmark_explicit_divergence_transitions(l,divergence_label);
      57             :   } 
      58          31 : }
      59             : 
      60             : 
      61             : /** \brief Checks whether the initial states of two LTSs are weakly bisimilar.
      62             :  * \details The LTSs l1 and l2 are not usable anymore after this call.
      63             :  *          The space consumption is O(n) and running time is dominated by the
      64             :  *          transitive closure (after branching bisimulation).
      65             :  * \param[in/out] l1 A first transition system.
      66             :  * \param[in/out] l2 A second transistion system.
      67             :  * \param[preserve_divergences] If true and branching is true, preserve tau loops on states.
      68             :  * \retval True iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar */
      69             : template < class LTS_TYPE>
      70           0 : bool destructive_weak_bisimulation_compare(
      71             :   LTS_TYPE& l1,
      72             :   LTS_TYPE& l2,
      73             :   const bool preserve_divergences=false)
      74             : {
      75           0 :   weak_bisimulation_reduce(l1,preserve_divergences);
      76           0 :   weak_bisimulation_reduce(l2,preserve_divergences);
      77           0 :   return destructive_bisimulation_compare_dnj(l1,l2);
      78             : }
      79             : 
      80             : 
      81             : /** \brief Checks whether the initial states of two LTSs are weakly bisimilar.
      82             :  *  \details The LTSs l1 and l2 are first duplicated and subsequently
      83             :  *           reduced modulo bisimulation. If memory space is a concern, one could consider to
      84             :  *           use destructive_weak_bisimulation_compare.  The running time
      85             :  *           of this routine is dominated by the transitive closure
      86             :  *           (after branching bisimulation).  It uses O(m+n) memory
      87             :  *           in addition to the copies of l1 and l2, where n is the
      88             :  *           number of states and m is the number of transitions.
      89             :  * \param[in/out] l1 A first transition system.
      90             :  * \param[in/out] l2 A second transistion system.
      91             :  * \param[preserve_divergences] If true and branching is true, preserve tau loops on states.
      92             :  * \retval True iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar */
      93             : template < class LTS_TYPE>
      94             : bool weak_bisimulation_compare(
      95             :   const LTS_TYPE& l1,
      96             :   const LTS_TYPE& l2,
      97             :   const bool preserve_divergences = false)
      98             : {
      99             :   LTS_TYPE l1_copy(l1);
     100             :   LTS_TYPE l2_copy(l2);
     101             :   return destructive_weak_bisimulation_compare(l1_copy, l2_copy,
     102             :                                                          preserve_divergences);
     103             : }
     104             : 
     105             : }
     106             : }
     107             : }
     108             : #endif  // #define _LIBLTS_WEAK_BISIM_H

Generated by: LCOV version 1.13