mCRL2
Loading...
Searching...
No Matches
liblts_bisim_gjkw.h File Reference

O(m log n)-time stuttering equivalence algorithm. More...

Go to the source code of this file.

Classes

class  mcrl2::lts::detail::bisim_gjkw::state_info_entry
 stores information about a single state More...
 
class  mcrl2::lts::detail::bisim_gjkw::block_t
 stores information about a block More...
 
class  mcrl2::lts::detail::bisim_gjkw::constln_t
 stores information about a constellation More...
 
class  mcrl2::lts::detail::bisim_gjkw::part_state_t
 refinable partition data structure More...
 
class  mcrl2::lts::detail::bisim_gjkw::succ_entry
 
class  mcrl2::lts::detail::bisim_gjkw::pred_entry
 
class  mcrl2::lts::detail::bisim_gjkw::B_to_C_entry
 
class  mcrl2::lts::detail::bisim_gjkw::B_to_C_descriptor
 
class  mcrl2::lts::detail::bisim_gjkw::part_trans_t
 
class  mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >
 helps with initialising the refinable partition data structure More...
 
class  mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::Key
 
class  mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE >::KeyHasher
 
class  mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >
 implements the main algorithm for the stutter equivalence quotient More...
 

Namespaces

namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
 
namespace  mcrl2::lts
 The main LTS namespace.
 
namespace  mcrl2::lts::detail
 A base class for the lts_dot labelled transition system.
 
namespace  mcrl2::lts::detail::bisim_gjkw
 

Macros

#define ONLY_IF_DEBUG(...)   __VA_ARGS__
 include something in Debug mode
 
#define BLOCK_NO_SEQNR   ((state_type) -1)
 

Typedefs

typedef state_info_entrymcrl2::lts::detail::bisim_gjkw::state_info_ptr
 
typedef const state_info_entrymcrl2::lts::detail::bisim_gjkw::state_info_const_ptr
 
typedef fixed_vector< state_info_ptrmcrl2::lts::detail::bisim_gjkw::permutation_t
 
typedef permutation_t::iterator mcrl2::lts::detail::bisim_gjkw::permutation_iter_t
 
typedef permutation_t::const_iterator mcrl2::lts::detail::bisim_gjkw::permutation_const_iter_t
 
typedef fixed_vector< B_to_C_entry >::iterator mcrl2::lts::detail::bisim_gjkw::B_to_C_iter_t
 
typedef fixed_vector< pred_entry >::iterator mcrl2::lts::detail::bisim_gjkw::pred_iter_t
 
typedef fixed_vector< succ_entry >::iterator mcrl2::lts::detail::bisim_gjkw::succ_iter_t
 
typedef fixed_vector< B_to_C_entry >::const_iterator mcrl2::lts::detail::bisim_gjkw::B_to_C_const_iter_t
 
typedef fixed_vector< pred_entry >::const_iterator mcrl2::lts::detail::bisim_gjkw::pred_const_iter_t
 
typedef fixed_vector< succ_entry >::const_iterator mcrl2::lts::detail::bisim_gjkw::succ_const_iter_t
 
typedef std::list< B_to_C_descriptormcrl2::lts::detail::bisim_gjkw::B_to_C_desc_list
 
typedef B_to_C_desc_list::iterator mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_iter_t
 
typedef B_to_C_desc_list::const_iterator mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_const_iter_t
 

Functions

static void mcrl2::lts::detail::bisim_gjkw::swap_permutation (permutation_iter_t s1, permutation_iter_t s2)
 swap two permutations
 
template<class LTS_TYPE >
void mcrl2::lts::detail::bisimulation_reduce_gjkw (LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)
 Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
 
template<class LTS_TYPE >
bool mcrl2::lts::detail::destructive_bisimulation_compare_gjkw (LTS_TYPE &l1, LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false, bool generate_counter_examples=false)
 Checks whether the two initial states of two LTSs are strong or branching bisimilar.
 
template<class LTS_TYPE >
bool mcrl2::lts::detail::bisimulation_compare_gjkw (const LTS_TYPE &l1, const LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false)
 Checks whether the two initial states of two LTSs are strong or branching bisimilar.
 
template<class LTS_TYPE >
bool mcrl2::lts::detail::destructive_bisimulation_compare_gjkw (LTS_TYPE &l1, LTS_TYPE &l2, bool branching, bool preserve_divergence, bool generate_counter_examples, const std::string &, bool)
 

Detailed Description

O(m log n)-time stuttering equivalence algorithm.

This file implements the efficient partition refinement algorithm by Groote / Jansen / Keiren / Wijs to calculate the stuttering equivalence quotient of a Kripke structure. (Labelled transition systems are converted to Kripke structures before the main algorithm). The file accompanies the planned publication in the ACM Trans. Comput. Log. Log. special issue for TACAS 2016, to appear in 2017.

Author
David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands

Definition in file liblts_bisim_gjkw.h.

Macro Definition Documentation

◆ ONLY_IF_DEBUG

#define ONLY_IF_DEBUG (   ...)    __VA_ARGS__

include something in Debug mode

In a few places, we have to include an additional parameter to a function in Debug mode. While it is in principle possible to use #ifndef NDEBUG ... #endif, that would lead to distributing the code over many code lines. This macro expands to its arguments in Debug mode and to nothing otherwise.

Definition at line 47 of file liblts_bisim_gjkw.h.