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
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

Typedefs
using	mcrl2::lts::detail::label_type = std::size_t
	type used to store label numbers and counts
using	mcrl2::lts::detail::bisim_gjkw::state_info_ptr = state_info_entry *
using	mcrl2::lts::detail::bisim_gjkw::state_info_const_ptr = const state_info_entry *
using	mcrl2::lts::detail::bisim_gjkw::permutation_t = fixed_vector< state_info_ptr >
using	mcrl2::lts::detail::bisim_gjkw::permutation_iter_t = permutation_t::iterator
using	mcrl2::lts::detail::bisim_gjkw::permutation_const_iter_t = permutation_t::const_iterator
using	mcrl2::lts::detail::bisim_gjkw::B_to_C_iter_t = fixed_vector< B_to_C_entry >::iterator
using	mcrl2::lts::detail::bisim_gjkw::pred_iter_t = fixed_vector< pred_entry >::iterator
using	mcrl2::lts::detail::bisim_gjkw::succ_iter_t = fixed_vector< succ_entry >::iterator
using	mcrl2::lts::detail::bisim_gjkw::B_to_C_const_iter_t = fixed_vector< B_to_C_entry >::const_iterator
using	mcrl2::lts::detail::bisim_gjkw::pred_const_iter_t = fixed_vector< pred_entry >::const_iterator
using	mcrl2::lts::detail::bisim_gjkw::succ_const_iter_t = fixed_vector< succ_entry >::const_iterator
using	mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_list = std::list< B_to_C_descriptor >
using	mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_iter_t = B_to_C_desc_list::iterator
using	mcrl2::lts::detail::bisim_gjkw::B_to_C_desc_const_iter_t = B_to_C_desc_list::const_iterator

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.