Part_interface

nonmember functions serving as interface with the rest of mCRL2 More...

Functions
template<class LTS_TYPE >
void	mcrl2::lts::detail::bisimulation_reduce_dnj (LTS_TYPE &l, bool const branching=false, bool const 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_dnj (LTS_TYPE &l1, LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false, bool const generate_counter_examples=false, const std::string &="", bool=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
template<class LTS_TYPE >
bool	mcrl2::lts::detail::bisimulation_compare_dnj (const LTS_TYPE &l1, const LTS_TYPE &l2, bool const branching=false, bool const preserve_divergence=false)
	Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
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

nonmember functions serving as interface with the rest of mCRL2

These functions are copied, almost without changes, from liblts_bisim_gw.h, which was written by Anton Wijs.

Function Documentation

bisimulation_compare_dnj()

template<class LTS_TYPE >

bool mcrl2::lts::detail::bisimulation_compare_dnj ( const LTS_TYPE &  l1, const LTS_TYPE &  l2, bool const  branching = false, bool const  preserve_divergence = false  )

inline

Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.

The LTSs l1 and l2 are first duplicated and subsequently reduced modulo bisimulation. If memory is a concern, one could consider to use destructive_bisimulation_compare(). This routine uses the O(m log n) branching bisimulation algorithm developed in 2018 by David N. Jansen. It runs in O(m log n) time and uses O(m) memory, where n is the number of states and m is the number of transitions.

Parameters

l1	A first transition system.
l2	A second transistion system.
branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
preserve_divergence	If true and branching is true, preserve tau loops on states.

Return values

True	iff the initial states of the transition systems l1 and l2 are ((divergence-preserving) branching) bisimilar.

Definition at line 5589 of file liblts_bisim_dnj.h.

bisimulation_compare_gjkw()

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  )

inline

Checks whether the two initial states of two LTSs are strong or branching bisimilar.

The LTSs l1 and l2 are first duplicated and subsequently reduced modulo bisimulation. If memory space is a concern, one could consider to use destructive_bisimulation_compare. This routine uses the O(m log n) branching bisimulation routine. It runs in O(m log n) time and uses O(n) memory, where n is the number of states and m is the number of transitions.

Parameters

[in,out]	l1	A first transition system.
[in,out]	l2	A second transistion system.
	branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
	preserve_divergence	If true and branching is true, preserve tau loops on states.

Return values

True	iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar.

Definition at line 1906 of file liblts_bisim_gjkw.h.

bisimulation_reduce_dnj()

template<class LTS_TYPE >

void mcrl2::lts::detail::bisimulation_reduce_dnj	(	LTS_TYPE &	l,
		bool const	branching = false,
		bool const	preserve_divergence = false
	)

Reduce transition system l with respect to strong or (divergence-preserving) branching bisimulation.

Parameters

[in,out]	l	The transition system that is reduced.
	branching	If true branching bisimulation is applied, otherwise strong bisimulation.
	preserve_divergence	Indicates whether loops of internal actions on states must be preserved. If false these are removed. If true these are preserved.

Definition at line 5489 of file liblts_bisim_dnj.h.

bisimulation_reduce_gjkw()

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.

calculates the bisimulation quotient of a LTS.

Parameters

[in,out]	l	The transition system that is reduced.
	branching	If true branching bisimulation is applied, otherwise strong bisimulation.
	preserve_divergence	Indicates whether loops of internal actions on states must be preserved. If false these are removed. If true these are preserved.

Definition at line 1887 of file liblts_bisim_gjkw.h.

destructive_bisimulation_compare_dnj()

template<class LTS_TYPE >

bool mcrl2::lts::detail::destructive_bisimulation_compare_dnj	(	LTS_TYPE &	l1,
		LTS_TYPE &	l2,
		bool const	branching = false,
		bool const	preserve_divergence = false,
		bool const	generate_counter_examples = false,
		const std::string &	= "",
		bool	= false
	)

Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.

This routine uses the O(m log n) branching bisimulation algorithm developed in 2018 by David N. Jansen. It runs in O(m log n) time and uses O(m) memory, where n is the number of states and m is the number of transitions.

The LTSs l1 and l2 are not usable anymore after this call.

Parameters

[in,out]	l1	A first transition system.
[in,out]	l2	A second transistion system.
	branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
	preserve_divergence	If true and branching is true, preserve tau loops on states.
	generate_counter_examples	(non-functional, only in the interface for historical reasons)

Returns

True iff the initial states of the transition systems l1 and l2 are ((divergence-preserving) branching) bisimilar.

Definition at line 5542 of file liblts_bisim_dnj.h.

destructive_bisimulation_compare_gjkw() [1/2]

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
	)

Definition at line 1916 of file liblts_bisim_gjkw.h.

destructive_bisimulation_compare_gjkw() [2/2]

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.

The LTSs l1 and l2 are not usable anymore after this call. The space consumption is O(n) and time is O(m log n). It uses the branching bisimulation algorithm by Groote/Jansen/Keiren/Wijs.

Parameters

[in,out]	l1	A first transition system.
[in,out]	l2	A second transistion system.
	branching	If true branching bisimulation is used, otherwise strong bisimulation is applied.
	preserve_divergence	If true and branching is true, preserve tau loops on states.

Return values

True	iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar.