liblts_weak_bisim.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote (upon request by Matthew Hennessy)
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef _LIBLTS_WEAK_BISIM_H
#define _LIBLTS_WEAK_BISIM_H
#include "mcrl2/lts/detail/liblts_scc.h"
#include "mcrl2/lts/detail/liblts_tau_star_reduce.h"
#include "mcrl2/lts/detail/liblts_merge.h"
#include "mcrl2/lts/lts_aut.h"
#include "mcrl2/lts/lts_fsm.h"
#include "mcrl2/lts/lts_dot.h"
 
namespace mcrl2
{
namespace lts
{
namespace detail
{
 
template < class LTS_TYPE>
void weak_bisimulation_reduce(
  LTS_TYPE& l,
  const bool preserve_divergences = false)
{
  if (1 < l.num_states())
  {
    bisimulation_reduce_dnj(l, true, preserve_divergences);   //< Apply branching bisimulation to l.
  }
 
  std::size_t divergence_label;
  if (preserve_divergences)
  {
    divergence_label=mark_explicit_divergence_transitions(l);
  }
  if (1 < l.num_states())
  {
    reflexive_transitive_tau_closure(l);                      // Apply transitive tau closure to l.
    bisimulation_reduce_dnj(l, false, false);                 // Apply strong bisimulation to l.
  }
  scc_reduce(l);                                              // Remove tau loops.
  remove_redundant_transitions(l);                            // Remove transitions s -a-> s' if also s-a->-tau->s' or s-tau->-a->s' is present.
                                                              // Note that this is correct, because l is reduced modulo strong bisimulation and
                                                              // does not contain tau loops.
  if (preserve_divergences)
  {
    unmark_explicit_divergence_transitions(l,divergence_label);
  }
}
 
 
template < class LTS_TYPE>
bool destructive_weak_bisimulation_compare(
  LTS_TYPE& l1,
  LTS_TYPE& l2,
  const bool preserve_divergences=false)
{
  weak_bisimulation_reduce(l1,preserve_divergences);
  weak_bisimulation_reduce(l2,preserve_divergences);
  return destructive_bisimulation_compare_dnj(l1,l2);
}
 
 
template < class LTS_TYPE>
bool weak_bisimulation_compare(
  const LTS_TYPE& l1,
  const LTS_TYPE& l2,
  const bool preserve_divergences = false)
{
  LTS_TYPE l1_copy(l1);
  LTS_TYPE l2_copy(l2);
  return destructive_weak_bisimulation_compare(l1_copy, l2_copy,
                                                         preserve_divergences);
}
 
}
}
}
#endif  // #define _LIBLTS_WEAK_BISIM_H