mCRL2
|
O(m log n)-time stuttering equivalence algorithm. More...
Go to the source code of this file.
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) |
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) |
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.
Definition in file liblts_bisim_gjkw.h.
#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.