O(m log n)-time branching bisimulation algorithm with lazy evaluation of BLC sets.
More...
|
| #define | SPLIT_LEFT -1 |
| |
| #define | SPLIT_RIGHT 1 |
| |
| #define | SPLIT_SMALLER 0 |
| |
| #define | non_bottom_states_NewBotSt non_bottom_states[3] |
| |
| #define | bottom_and_non_bottom_size(coroutine) |
| |
| #define | DEBUG_coroutine_name(coroutine) |
| |
| #define | abort_if_bottom_size_too_large(coroutine) |
| |
| #define | abort_if_non_bottom_size_too_large_NewBotSt(i) |
| |
| #define | abort_if_size_too_large(coroutine, i) |
| |
| #define | new_start_bottom_states(idx) (assert(1<=(idx)), assert((idx)<=3), new_start_bottom_states_plus_one[(idx)-1]) |
| |
| #define | new_end_bottom_states(idx) (assert(1<=(idx)), assert((idx)<=2), new_end_bottom_states_plus_one[(idx)-1]) |
| |
| #define | new_end_bottom_states_NewBotSt (new_start_bottom_states_plus_one[2]) |
| |
| #define | new_start_bottom_states(idx) (assert(1<=(idx)), assert((idx)<=3), new_start_bottom_states_plus_one[(idx)-1]) |
| |
| #define | new_end_bottom_states(idx) (assert(1<=(idx)), assert((idx)<=2), new_end_bottom_states_plus_one[(idx)-1]) |
| |
| #define | new_end_bottom_states_NewBotSt (new_start_bottom_states_plus_one[2]) |
| |
| #define | PRINT_SG_PL(counter, sg_string, pl_string) (counter) << (1 == (counter) ? (sg_string) : (pl_string)) |
| |
| #define | PRINT_INT_PERCENTAGE(num, denom) (((num) * 200 + (denom)) / (denom) / 2) |
| |
|
| template<class LTS_TYPE > |
| void | mcrl2::lts::detail::bisimulation_reduce_gj_lazy_BLC (LTS_TYPE &l, const bool branching=false, const bool preserve_divergence=false) |
| | nonmember functions serving as interface with the rest of mCRL2
|
| |
| template<class LTS_TYPE > |
| bool | mcrl2::lts::detail::destructive_bisimulation_compare_gj_lazy_BLC (LTS_TYPE &l1, LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false, const bool 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_gj_lazy_BLC (const LTS_TYPE &l1, const LTS_TYPE &l2, const bool branching=false, const bool preserve_divergence=false) |
| | Checks whether the two initial states of two LTSs are strong or (divergence-preserving) branching bisimilar.
|
| |
O(m log n)-time branching bisimulation algorithm with lazy evaluation of BLC sets.
This algorithm is similar to liblts_bisim_dnj.h and liblts_bisim_gj.h. In the latter algorithm, it turned out that using BLC sets is rather slow; in particular, the initial partition is better constructed without maintaining BLC sets. This algorithm pushes the idea further and tries to refine BLC sets as little as possible. They are replaced by super-BLC sets, which contain transitions from a union of blocks, with one action label, to one constellation. Only if a single-block BLC set is required, the union of blocks is refined. This may happen only in the following two situations:
- when a block is refined under a large splitter, and the coroutines AvoidLrg and NewBotSt are the only ones to still run. In this situation, the coroutine for NewBotSt has to go through the large splitter to find states that should NOT go into AvoidLrg. NewBotSt should, however, only spend time on transitions that start in the current block, so a single-source BLC set is required.
- when
four_way_splitB() finds new bottom states and NewBotSt is large. Then, NewBotSt needs to be stabilized under all its outgoing transitions, but because it is large, we cannot just go through all these transitions; we are only allowed to go through the transitions starting in new bottom states. However, there may be BLC sets that only have transitions from non-bottom states, and to find these, we need the list of single-source BLC sets for this block. These situations do not occur for strong bisimulation, so no BLC sets need to be constructed in that case.
A disadvantage of this version may be that it is more difficult to estimate the number of transitions (for a progress message). The reason is that the earlier algorithm (in liblts_bisim_gj.h) used the number of BLC sets as a lower bound of the number of transitions, but with super-BLC sets this would not be very informative. This file provides an option (the preprocessor constant MORE_STATISTICS) to include an estimate of the number of transitions, based on a sample state. That means that in every block, one state is picked, and its outgoing transitions are used as an estimate how many transitions this block / equivalence class will have in the quotient. This method takes more effort – enabling the option may increase the running time by 5–10%. Therefore it is provided as an option, not always enabled.
Definition in file liblts_bisim_gj_lazy_BLC.h.
1.9.7