mCRL2
Loading...
Searching...
No Matches
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
l1A first transition system.
l2A second transistion system.
branchingIf true branching bisimulation is used, otherwise strong bisimulation is applied.
preserve_divergenceIf true and branching is true, preserve tau loops on states.
Return values
Trueiff the initial states of the transition systems l1 and l2 are ((divergence-preserving) branching) bisimilar.

Definition at line 5582 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]l1A first transition system.
[in,out]l2A second transistion system.
branchingIf true branching bisimulation is used, otherwise strong bisimulation is applied.
preserve_divergenceIf true and branching is true, preserve tau loops on states.
Return values
Trueiff 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]lThe transition system that is reduced.
branchingIf true branching bisimulation is applied, otherwise strong bisimulation.
preserve_divergenceIndicates whether loops of internal actions on states must be preserved. If false these are removed. If true these are preserved.

Definition at line 5491 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]lThe transition system that is reduced.
branchingIf true branching bisimulation is applied, otherwise strong bisimulation.
preserve_divergenceIndicates 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]l1A first transition system.
[in,out]l2A second transistion system.
branchingIf true branching bisimulation is used, otherwise strong bisimulation is applied.
preserve_divergenceIf 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 5536 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]l1A first transition system.
[in,out]l2A second transistion system.
branchingIf true branching bisimulation is used, otherwise strong bisimulation is applied.
preserve_divergenceIf true and branching is true, preserve tau loops on states.
Return values
Trueiff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar.