LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_bisim_gjkw.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 510 560 91.1 %
Date: 2020-07-11 00:44:39 Functions: 159 193 82.4 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
       2             : //
       3             : // Copyright: see the accompanying file COPYING or copy at
       4             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : /// \file lts/detail/liblts_bisim_gjkw.h
      11             : ///
      12             : /// \brief O(m log n)-time stuttering equivalence algorithm
      13             : ///
      14             : /// \details This file implements the efficient partition refinement algorithm
      15             : /// by Groote / Jansen / Keiren / Wijs to calculate the stuttering equivalence
      16             : /// quotient of a Kripke structure.  (Labelled transition systems are converted
      17             : /// to Kripke structures before the main algorithm).
      18             : /// The file accompanies the planned publication in the ACM Trans. Comput. Log.
      19             : /// Log. special issue for TACAS 2016, to appear in 2017.
      20             : ///
      21             : /// \author David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
      22             : 
      23             : #ifndef _LIBLTS_BISIM_GJKW_H
      24             : #define _LIBLTS_BISIM_GJKW_H
      25             : 
      26             : #include <unordered_map> // used during initialisation
      27             : #include <list>          // for the list of B_to_C_descriptors
      28             : 
      29             : #include "mcrl2/lts/detail/liblts_scc.h"
      30             : #include "mcrl2/lts/detail/liblts_merge.h"
      31             : #include "mcrl2/lts/detail/check_complexity.h"
      32             : #include "mcrl2/lts/detail/fixed_vector.h"
      33             : 
      34             : namespace mcrl2
      35             : {
      36             : namespace lts
      37             : {
      38             : namespace detail
      39             : {
      40             :                                                                                 #ifndef NDEBUG
      41             :                                                                                     /// \brief include something in Debug mode
      42             :                                                                                     /// \details In a few places, we have to include an additional parameter to
      43             :                                                                                     /// a function in Debug mode.  While it is in principle possible to use
      44             :                                                                                     /// #ifndef NDEBUG ... #endif, that would lead to distributing the code
      45             :                                                                                     /// over many code lines.  This macro expands to its arguments in Debug
      46             :                                                                                     /// mode and to nothing otherwise.
      47             :                                                                                     #define ONLY_IF_DEBUG(...) __VA_ARGS__
      48             :                                                                                 #else
      49             :                                                                                     #define ONLY_IF_DEBUG(...)
      50             :                                                                                 #endif
      51             : // state_type and trans_type are defined in check_complexity.h.
      52             : 
      53             : /// \brief type used to store label numbers and counts
      54             : typedef std::size_t label_type;
      55             : 
      56             : 
      57             : 
      58             : 
      59             : 
      60             : /* ************************************************************************* */
      61             : /*                                                                           */
      62             : /*                   R E F I N A B L E   P A R T I T I O N                   */
      63             : /*                                                                           */
      64             : /* ************************************************************************* */
      65             : 
      66             : 
      67             : 
      68             : 
      69             : 
      70             : /// \defgroup part_state
      71             : /// \brief data structures for a refinable partition
      72             : /// \details The following definitions provide a _refinable partition_ data
      73             : /// structure.  The basic idea is that we store a permutation of the states (in
      74             : /// a permutation_t array), so that states belonging to the same block are
      75             : /// adjacent, and also that blocks belonging to the same constellation are
      76             : /// adjacent.
      77             : ///
      78             : /// The basic structure therefore consists of the classes:
      79             : ///
      80             : /// state_info_ptr - an entry in the permutation array; it contains a
      81             : ///                     pointer to a state_info_entry.
      82             : /// permutation_t     - an array of permutation_entries.
      83             : /// constln_t         - contains information about a constellation, in
      84             : ///                     particular which slice of permutation_t contains its
      85             : ///                     states.
      86             : /// block_t           - contains information about a block, in particular which
      87             : ///                     slice of permutation_t contains its states, and its
      88             : ///                     constellation.
      89             : /// state_info_entry  - contains information about a state, in particular its
      90             : ///                     position in the permutation_t array and its block.
      91             : /// state_info_t      - an array of state_info_entries.
      92             : /// part_state_t      - the complete data structure combining state_info_t and
      93             : ///                     permutation_t.
      94             : ///
      95             : /// This basic structure is extended as follows:
      96             : /// - Because we combine this data structure with a partition of the
      97             : ///   transitions, a state_info_entry also contains information which slice of
      98             : ///   the incoming and outgoing, inert and non-inert transitions belong to the
      99             : ///   state.  In many cases the slice of this state ends exactly where the
     100             : ///   slice of the next state begins, so we can find the end of this state's
     101             : ///   slice by looking at the next state's state_info_entry.  Therefore,
     102             : ///   state_info_ptr actually contains a pointer to a state_info_entry with
     103             : ///   the additional guarantee that this is not the last entry in state_info_t.
     104             : ///   (To make this a small bit more type safe, we could change the type
     105             : ///   state_info_ptr to something like ``pointer to an array with two
     106             : ///   state_info_entries'', typedef state_info_entry (*state_info_ptr)[2];.
     107             : ///   Still, that would allow unsafe pointer juggling.)
     108             : /// - A block_t also contains information about its outgoing inert transitions.
     109             : /// - A state_info_entry also contains information used during `refine()` or
     110             : ///   `process_new_bottom()`.
     111             : ///@{
     112             : 
     113             : namespace bisim_gjkw
     114             : {
     115             : 
     116             : class state_info_entry;
     117             : 
     118             : typedef state_info_entry* state_info_ptr;
     119             : typedef const state_info_entry* state_info_const_ptr;
     120             : 
     121             : /// \class permutation_t
     122             : /// \brief stores a permutation of the states, ordered by block
     123             : /// \details This is the central concept of the _refinable partition_: the
     124             : /// permutation of the states, such that states belonging to the same block are
     125             : /// adjacent, and also that blocks belonging to the same constellation are
     126             : /// adjacent.
     127             : ///
     128             : /// Iterating over the states of a block or the blocks of a constellation will
     129             : /// therefore be done using the permutation_t array.
     130             : typedef fixed_vector<state_info_ptr> permutation_t;
     131             : typedef permutation_t::iterator permutation_iter_t;
     132             : typedef permutation_t::const_iterator permutation_const_iter_t;
     133             : 
     134             : class block_t;
     135             : class constln_t;
     136             : 
     137             : class B_to_C_entry;
     138             : class pred_entry;
     139             : class succ_entry;
     140             : typedef fixed_vector<B_to_C_entry>::iterator B_to_C_iter_t;
     141             : typedef fixed_vector<pred_entry>::iterator pred_iter_t;
     142             : typedef fixed_vector<succ_entry>::iterator succ_iter_t;
     143             : 
     144             : typedef fixed_vector<B_to_C_entry>::const_iterator B_to_C_const_iter_t;
     145             : typedef fixed_vector<pred_entry>::const_iterator pred_const_iter_t;
     146             : typedef fixed_vector<succ_entry>::const_iterator succ_const_iter_t;
     147             : class B_to_C_descriptor;
     148             : typedef std::list<B_to_C_descriptor> B_to_C_desc_list;
     149             : typedef B_to_C_desc_list::iterator B_to_C_desc_iter_t;
     150             : typedef B_to_C_desc_list::const_iterator B_to_C_desc_const_iter_t;
     151             : 
     152             : /// \class state_info_entry
     153             : /// \brief stores information about a single state
     154             : /// \details This class stores all other information about a state that the
     155             : /// partition needs.  In particular:  the block where the state belongs and the
     156             : /// position in the permutation array (i. e. the inverse of the permutation).
     157             : ///
     158             : /// A `state_info_entry` only works correctly if it is part of an array where
     159             : /// there is one more `state_info_entry`.  The reason is that iterators past
     160             : /// the last transition are not actually stored here, as they are equal to the
     161             : /// iterator to the first transition of the next state.  The array will contain
     162             : /// one additional ``state'' that is only used for these pointers.
     163         982 : class state_info_entry
     164             : {
     165             :   private:
     166             :     /// \brief iterator to first incoming transition
     167             :     /// \details also serves as iterator past the last incoming transition of
     168             :     /// the previous state.
     169             :     pred_iter_t state_in_begin;
     170             : 
     171             :     /// \brief iterator to first outgoing transition
     172             :     /// \details also serves as iterator past the last outgoing transition of
     173             :     /// the previous state.
     174             :     succ_iter_t state_out_begin;
     175             : 
     176             :     /// iterator to first _inert_ incoming transition
     177             :     pred_iter_t state_inert_in_begin;
     178             : 
     179             :     /// iterator to first _inert_ outgoing transition
     180             :     succ_iter_t state_inert_out_begin;
     181             : 
     182             :     /// iterator past the last _inert_ outgoing transition
     183             :     succ_iter_t state_inert_out_end;
     184             :   public:
     185             :     /// block where the state belongs
     186             :     block_t* block;
     187             : 
     188             :     /// position of the state in the permutation array
     189             :     permutation_iter_t pos;
     190             : 
     191             :     /// number of inert transitions to non-blue states
     192             :     state_type notblue;
     193             :   private:
     194             :     /// iterator to first outgoing transition to the constellation of interest
     195             :     succ_iter_t int_current_constln;
     196             :   public:
     197             :     /// get constellation where the state belongs
     198             :     const constln_t* constln() const;
     199             :     constln_t* constln();
     200             : 
     201       61362 :     succ_const_iter_t current_constln() const {  return int_current_constln;  }
     202        2222 :     succ_iter_t current_constln()  {  return int_current_constln;  }
     203        2101 :     void set_current_constln(succ_iter_t const new_current_constln)
     204             :     {
     205        2101 :         int_current_constln = new_current_constln;                              // current_constln points to a successor transition of this state:
     206        2101 :                                                                                 assert(succ_begin() <= int_current_constln);
     207        2101 :                                                                                 assert(int_current_constln <= succ_end());
     208             :                                                                                 // it points to a place where a constellation slice starts or ends:
     209             :                                                                                 // (This assertion cannot be tested because the types are not yet
     210             :                                                                                 // complete.)
     211             :                                                                                 // assert(succ_begin() == int_current_constln ||
     212             :                                                                                 //     succ_end() == int_current_constln ||
     213             :                                                                                 //     int_current_constln[-1].constln_slice !=
     214             :                                                                                 //                                 int_current_constln->constln_slice);
     215             :                                                                                 // it points to the relevant constellation:
     216             :                                                                                 // The following assertions cannot be executed immediately after each
     217             :                                                                                 // call.
     218             :                                                                                 // assert(succ_begin() == current_constln() ||
     219             :                                                                                 //                   *current_constln()[-1].target->constln() <= *SpC);
     220             :                                                                                 // assert(succ_end() == current_constln() ||
     221             :                                                                                 //                      *SpC <= *current_constln()->target->constln());
     222        2101 :     }
     223             : 
     224             :     /// iterator to first incoming transition
     225       26233 :     pred_const_iter_t pred_begin() const  {  return state_in_begin;  }
     226        7828 :     pred_iter_t pred_begin()  {  return state_in_begin;  }
     227         982 :     void set_pred_begin(pred_iter_t new_in_begin)
     228             :     {
     229         982 :         state_in_begin = new_in_begin;
     230         982 :     }
     231             : 
     232             :     /// iterator past the last incoming transition
     233      134649 :     pred_const_iter_t pred_end() const
     234      134649 :     {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
     235      134649 :         return this[1].state_in_begin;
     236             :     }
     237       13459 :     pred_iter_t pred_end()
     238       13459 :     {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
     239       13459 :         return this[1].state_in_begin;
     240             :     }
     241         927 :     void set_pred_end(pred_iter_t new_in_end)
     242         927 :     {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
     243         927 :         this[1].set_pred_begin(new_in_end);
     244         927 :     }
     245             : 
     246             :     /// iterator to first non-inert incoming transition
     247       26233 :     pred_const_iter_t noninert_pred_begin() const  {  return state_in_begin;  }
     248        3697 :     pred_iter_t noninert_pred_begin()  {  return state_in_begin;  }
     249             : 
     250             :     /// iterator past the last non-inert incoming transition
     251       55974 :     pred_const_iter_t noninert_pred_end() const  { return inert_pred_begin(); }
     252        5985 :     pred_iter_t noninert_pred_end()  {  return inert_pred_begin();  }
     253             : 
     254             :     /// iterator to first inert incoming transition
     255      160906 :     pred_const_iter_t inert_pred_begin() const { return state_inert_in_begin; }
     256        9691 :     pred_iter_t inert_pred_begin()  {  return state_inert_in_begin;  }
     257        1069 :     void set_inert_pred_begin(pred_iter_t new_inert_in_begin)
     258             :     {
     259        1069 :         state_inert_in_begin = new_inert_in_begin;                              assert(pred_begin() <= inert_pred_begin());
     260        1069 :                                                                                 assert(inert_pred_begin() <= pred_end());
     261        1069 :     }
     262             : 
     263             :     /// iterator one past the last inert incoming transition
     264      108416 :     pred_const_iter_t inert_pred_end() const { return pred_end(); }
     265        1595 :     pred_iter_t inert_pred_end()  {  return pred_end();  }
     266             : 
     267             :     /// iterator to first outgoing transition
     268      106238 :     succ_const_iter_t succ_begin() const  {  return state_out_begin;  }
     269       20421 :     succ_iter_t succ_begin()  {  return state_out_begin;  }
     270         982 :     void set_succ_begin(succ_iter_t new_out_begin)
     271             :     {
     272         982 :         state_out_begin = new_out_begin;
     273         982 :     }
     274             : 
     275             :     /// iterator past the last outgoing transition
     276      133217 :     succ_const_iter_t succ_end() const
     277      133217 :     {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
     278      133217 :         return this[1].state_out_begin;
     279             :     }
     280       23384 :     succ_iter_t succ_end()
     281       23384 :     {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
     282       23384 :         return this[1].state_out_begin;
     283             :     }
     284         927 :     void set_succ_end(succ_iter_t new_out_end)
     285         927 :     {                                                                           assert(s_i_begin <= this);  assert(this < s_i_end);
     286         927 :         this[1].set_succ_begin(new_out_end);                                    assert(succ_begin() <= succ_end());
     287         927 :     }
     288             : 
     289             :     /// iterator to first inert outgoing transition
     290      127289 :     succ_const_iter_t inert_succ_begin() const  {return state_inert_out_begin;}
     291        9829 :     succ_iter_t inert_succ_begin()  {  return state_inert_out_begin;  }
     292         142 :     void set_inert_succ_begin(succ_iter_t const new_inert_out_begin)
     293             :     {                                                                           // The following assertions cannot be tested because the respective
     294             :                                                                                 // types are not yet complete.
     295             :                                                                                 // if (new_inert_out_begin > inert_succ_begin())
     296             :                                                                                 // {
     297             :                                                                                 //     assert(*new_inert_out_begin[-1].target->constln()<=*constln());
     298             :                                                                                 //     assert(new_inert_out_begin[-1].target->block != block);
     299             :                                                                                 // }
     300             :                                                                                 // else if (new_inert_out_begin < inert_succ_begin())
     301             :                                                                                 // {
     302             :                                                                                 //     assert(new_inert_out_begin->target->block == block);
     303             :                                                                                 // }
     304         142 :         state_inert_out_begin = new_inert_out_begin;                            assert(succ_begin() <= inert_succ_begin());
     305         142 :                                                                                 assert(inert_succ_begin() <= inert_succ_end());
     306         142 :     }
     307             : 
     308             :     /// iterator past the last inert outgoing transition
     309      130476 :     succ_const_iter_t inert_succ_end() const  {  return state_inert_out_end;  }
     310       10450 :     succ_iter_t inert_succ_end()  {  return state_inert_out_end;  }
     311             : 
     312        1352 :     void set_inert_succ_begin_and_end(succ_iter_t new_inert_out_begin,
     313             :                                                  succ_iter_t new_inert_out_end)
     314             :     {
     315        1352 :         state_inert_out_begin = new_inert_out_begin;
     316        1352 :         state_inert_out_end = new_inert_out_end;                                assert(succ_begin() <= inert_succ_begin());
     317        1352 :                                                                                 assert(inert_succ_begin() <= inert_succ_end());
     318        1352 :                                                                                 assert(inert_succ_end() <= succ_end());
     319             :                                                                                 // The following assertions cannot be tested always, as the function
     320             :                                                                                 // may be called earlier than the assertions are reestablished.
     321             :                                                                                 // assert(succ_begin() == inert_succ_begin() ||
     322             :                                                                                 //            *inert_succ_begin()[-1].target->constln() <= *constln());
     323             :                                                                                 // assert(succ_begin() == inert_succ_begin() ||
     324             :                                                                                 //                      inert_succ_begin()[-1].target->block != block);
     325             :                                                                                 // assert(inert_succ_begin() == inert_succ_end() ||
     326             :                                                                                 //                      (inert_succ_begin()->target->block == block &&
     327             :                                                                                 //                       inert_succ_end()[-1].target->block == block));
     328             :                                                                                 // assert(succ_end() == inert_succ_end() ||
     329             :                                                                                 //                  *constln() < *inert_succ_end()->target->constln());
     330        1352 :     }
     331             : 
     332             :     bool surely_has_transition_to(const constln_t* SpC) const;
     333             :     bool surely_has_no_transition_to(const constln_t* SpC) const;
     334             :                                                                                 #ifndef NDEBUG
     335             :                                                                                     /// \brief print a short state identification for debugging
     336             :                                                                                     /// \details This function is only available if compiled in Debug mode.
     337           0 :                                                                                     std::string debug_id_short() const
     338             :                                                                                     {
     339           0 :                                                                                         assert(s_i_begin <= this);
     340           0 :                                                                                         assert(this < s_i_end);
     341           0 :                                                                                         return std::to_string(this - s_i_begin);
     342             :                                                                                     }
     343             : 
     344             :                                                                                     /// \brief print a state identification for debugging
     345             :                                                                                     /// \details This function is only available if compiled in Debug mode.
     346           0 :                                                                                     std::string debug_id() const
     347             :                                                                                     {
     348           0 :                                                                                         return "state " + debug_id_short();
     349             :                                                                                     }
     350             :                                                                                   private:
     351             :                                                                                     /// \brief pointer at the first entry in the `state_info` array
     352             :                                                                                     static state_info_const_ptr s_i_begin;
     353             : 
     354             :                                                                                     /// \brief pointer past the last actual entry in the `state_info` array
     355             :                                                                                     /// \details `state_info` actually contains an additional entry that is
     356             :                                                                                     /// only used partially, namely to store pointers to the end of the
     357             :                                                                                     /// transition slices of the last state.  In other words, `s_i_end` points
     358             :                                                                                     /// at this additional, partially used entry.
     359             :                                                                                     static state_info_const_ptr s_i_end;
     360             : 
     361             :                                                                                     friend class part_state_t;
     362             :                                                                                   public:
     363             :                                                                                     mutable check_complexity::state_counter_t work_counter;
     364             :                                                                                 #endif
     365             : };
     366             : 
     367             : 
     368             : /// swap two permutations
     369        2082 : static inline void swap_permutation(permutation_iter_t s1,
     370             :                                                         permutation_iter_t s2)
     371             : {
     372             :     // swap contents of permutation array
     373        2082 :     std::swap(*s1, *s2);
     374             :     // swap pointers to permutation array
     375        2082 :     (*s1)->pos = s1;
     376        2082 :     (*s2)->pos = s2;
     377        2082 : }
     378             : 
     379             : /// \class block_t
     380             : /// \brief stores information about a block
     381             : /// \details A block corresponds to a slice of the permutation array.  As the
     382             : /// number of blocks is initially unknown, we will allocate instances of this
     383             : /// class dynamically.
     384             : ///
     385             : /// The slice in the permutation array containing the states of the block is
     386             : /// subdivided into the following subslices (in this order):
     387             : /// 1. unmarked non-bottom states
     388             : /// 2. marked non-bottom states (initially empty)
     389             : /// 3. unmarked bottom states
     390             : /// 4. marked bottom states (initially empty)
     391             : ///
     392             : /// A state should be marked iff it is a predecessor of the current splitter
     393             : /// (through a strong transition).  The marking is later extended to the red
     394             : /// states;  that are the states with a weak transition to the splitter.
     395             : ///
     396             : /// (During the execution of some functions, more slices are subdivided
     397             : /// further;  however, as these subdivisions are local to a single function,
     398             : /// they are not stored here.)
     399             : ///
     400             : /// The blocks keep track of the total number of blocks allocated and number
     401             : /// themselves sequentially using the static member `nr_of_blocks`.  It is
     402             : /// therefore impossible to have multiple refinements running at the same time.
     403             : class block_t
     404             : {
     405             :   private:
     406             :     /// iterator past the last state of the block
     407             :     permutation_iter_t int_end;
     408             : 
     409             :     /// iterator to the first state of the block
     410             :     permutation_iter_t int_begin;
     411             : 
     412             :     /// iterator to the first marked non-bottom state of the block
     413             :     permutation_iter_t int_marked_nonbottom_begin;
     414             : 
     415             :     /// iterator to the first bottom state of the block
     416             :     permutation_iter_t int_bottom_begin;
     417             : 
     418             :     /// iterator to the first marked bottom state of the block
     419             :     permutation_iter_t int_marked_bottom_begin;
     420             : 
     421             :     /// \brief iterator to the first inert transition of the block
     422             :     /// \details If there are no inert transitions, then `inert_begin` and
     423             :     /// `inert_end` point to the end of the B_to_C-slice containing transitions
     424             :     /// from the block to its own constellation.  If there is no such slice,
     425             :     /// both are equal to `B_to_C`.
     426             :     B_to_C_iter_t int_inert_begin;
     427             : 
     428             :     /// iterator past the last inert transition of the block
     429             :     B_to_C_iter_t int_inert_end;
     430             :   public:
     431             :     /// \brief list of B_to_C with transitions from this block
     432             :     /// \details This list serves two purposes: it contains all
     433             :     /// B_to_C_descriptors, so that the constellations reachable from this
     434             :     /// block can be found; and if this block has transitions to the current
     435             :     /// splitter SpC\SpB, then the first element of the list points to these
     436             :     /// transitions.
     437             :     B_to_C_desc_list to_constln;
     438             :   private:
     439             :     /// constellation to which the block belongs
     440             :     constln_t* int_constln;
     441             : 
     442             :     /// \brief next block in the list of refinable blocks
     443             :     /// \details If this is the last block in the list, `refinable_next` points
     444             :     /// to this very block.  Consequently, it is possible to check whether some
     445             :     /// block is refinable without an additional variable.
     446             :     block_t* refinable_next;
     447             : 
     448             :     /// first block in the list of refinable blocks
     449             :     static block_t* refinable_first;
     450             : 
     451             :     /// \brief unique sequence number of this block
     452             :     /// \details After the stuttering equivalence algorithm has terminated,
     453             :     /// this number is used as a state number in the quotient Kripke structure.
     454             :     /// (For blocks that contain extra Kripke states, the number is set to
     455             :     /// BLOCK_NO_SEQNR).
     456             :     state_type int_seqnr;
     457             : 
     458             : #define BLOCK_NO_SEQNR ((state_type) -1)
     459             : 
     460             :   public:
     461             :     /// \brief total number of blocks with unique sequence number allocated
     462             :     /// \details Upon starting the stuttering equivalence algorithm, the number
     463             :     /// of blocks must be zero.
     464             :     static state_type nr_of_blocks;
     465             : 
     466             :     /// \brief constructor
     467             :     /// \details The constructor initialises the block to: all states are
     468             :     /// bottom states, no state is marked, the block is not refinable.
     469             :     /// \param constln_ constellation to which the block belongs
     470             :     /// \param begin_   initial iterator to the first state of the block
     471             :     /// \param end_     initial iterator past the last state of the block
     472         556 :     block_t(constln_t* const constln_, permutation_iter_t const begin_,
     473             :                                                  permutation_iter_t const end_)
     474         556 :       : int_end(end_),
     475             :         int_begin(begin_),
     476             :         int_marked_nonbottom_begin(begin_), // no non-bottom state is marked
     477             :         int_bottom_begin(begin_), // all states are bottom states
     478             :         int_marked_bottom_begin(end_), // no bottom state is marked
     479             :         // int_inert_begin -- is initialised by part_trans_t::create_new_block
     480             :         // int_inert_end -- is initialised by part_trans_t::create_new_block
     481             :         to_constln(), // empty list
     482             :         int_constln(constln_),
     483             :         refinable_next(nullptr),
     484         556 :         int_seqnr(BLOCK_NO_SEQNR)
     485             :     {                                                                           // The following assertions hold trivially.
     486             :                                                                                 // assert(int_begin <= int_marked_nonbottom_begin);
     487             :                                                                                 // assert(int_marked_nonbottom_begin <= int_bottom_begin);
     488             :                                                                                 // assert(int_bottom_begin <= int_marked_bottom_begin);
     489             :                                                                                 // assert(int_marked_bottom_begin <= int_end);
     490         556 :                                                                                 assert(int_bottom_begin < int_end);
     491             :                                                                                 // The following assertions cannot be tested because constln_t is not
     492             :                                                                                 // yet complete.
     493             :                                                                                 // assert(int_constln->begin() <= int_begin);
     494             :                                                                                 // assert(int_end <= int_constln->end());
     495         556 :     }
     496             : 
     497         556 :     ~block_t()  {  }
     498             : 
     499             :     /// assigns a unique sequence number
     500         279 :     void assign_seqnr()
     501         279 :     {                                                                           assert(BLOCK_NO_SEQNR == int_seqnr);
     502         279 :         int_seqnr = nr_of_blocks++;
     503         279 :     }
     504             : 
     505        2028 :     state_type seqnr() const  {  return int_seqnr;  }
     506             : 
     507             :     /// provides an arbitrary refinable block
     508        2250 :     static block_t* get_some_refinable()  {  return refinable_first;  }
     509             : 
     510             :     /// \brief checks whether the block is refinable
     511             :     /// \returns true if the block is refinable
     512       11452 :     bool is_refinable() const  {  return nullptr != refinable_next;  }
     513             : 
     514             :     /// \brief makes a block refinable (i. e. inserts it into the respective
     515             :     /// list)
     516             :     /// \returns true if the block was not refinable before
     517        1046 :     bool make_refinable()
     518             :     {
     519        1046 :         if (is_refinable())
     520             :         {
     521         422 :             return false;
     522             :         }
     523         624 :         refinable_next = nullptr == refinable_first ? this : refinable_first;
     524         624 :         refinable_first = this;
     525         624 :         return true;
     526             :     }
     527             : 
     528             :     /// \brief makes a block non-refinable (i. e. removes it from the
     529             :     /// respective list)
     530             :     /// \details This member function only works if the block is the first one
     531             :     /// in the list (which will normally be the case).
     532         624 :     void make_nonrefinable()
     533         624 :     {                                                                           assert(refinable_first == this);
     534         624 :         refinable_first = refinable_next == this ? nullptr : refinable_next;
     535         624 :         refinable_next = nullptr;
     536         624 :     }
     537             : 
     538             :     /// provides the number of states in the block
     539       47003 :     state_type size() const  {  return int_end - int_begin;  }
     540             : 
     541             :     /// \brief provides the number of marked bottom states in the block
     542             :     /// \details This size includes the old bottom states.
     543        3164 :     state_type marked_bottom_size() const
     544             :     {
     545        3164 :         return marked_bottom_end() - marked_bottom_begin();
     546             :     }
     547             : 
     548             :     /// \brief provides the number of marked states in the block
     549             :     /// \details This size includes the old bottom states;  in other words, the
     550             :     /// old bottom states are always regarded as marked.
     551        3076 :     state_type marked_size() const
     552             :     {
     553        6152 :         return marked_nonbottom_end() - marked_nonbottom_begin() +
     554        6152 :                                                         marked_bottom_size();
     555             :     }
     556             : 
     557             :     /// provides the number of unmarked bottom states in the block
     558        2393 :     state_type unmarked_bottom_size() const
     559             :     {
     560        2393 :         return unmarked_bottom_end() - unmarked_bottom_begin();
     561             :     }
     562             : 
     563             :     /// \brief compares two blocks for ordering them
     564             :     /// \details The blocks are ordered according to their positions in the
     565             :     /// permutation array.  This is a suitable order, as blocks may be refined,
     566             :     /// but never swap positions as a whole.  Refining will make the new
     567             :     /// subblocks compare in the same way to other blocks as the original,
     568             :     /// larger block.
     569             :     bool operator<(const block_t& other) const
     570             :     {
     571             :         return begin() < other.begin();
     572             :     }
     573             : 
     574             :     /// constellation where the block belongs to
     575       10406 :     const constln_t* constln() const  {  return int_constln;  }
     576      252873 :     constln_t* constln()  {  return int_constln;  }
     577         501 :     void set_constln(constln_t* new_constln)
     578             :     {                                                                           // The following assertion cannot be tested because the type constln_t
     579         501 :         int_constln = new_constln;                                              // is not yet complete.
     580             :                                                                                 // assert(nullptr == int_constln ||
     581             :                                                                                 //                             (int_constln->begin() <= int_begin &&
     582             :                                                                                 //                                     int_end <= int_constln->end()));
     583         501 :     }
     584             : 
     585             :     /// read FromRed
     586             :     B_to_C_descriptor* FromRed(const constln_t* SpC);
     587             : 
     588             :     /// set FromRed to an existing element in to_constln
     589             :     void SetFromRed(B_to_C_desc_iter_t new_fromred);
     590             : 
     591             :     /// iterator to the first state in the block
     592       18625 :     permutation_const_iter_t begin()  const  {  return int_begin;  }
     593       11016 :     permutation_iter_t begin()  {  return int_begin;  }
     594          57 :     void set_begin(permutation_iter_t new_begin)
     595             :     {
     596          57 :         int_begin = new_begin;                                                  assert(int_begin <= int_marked_nonbottom_begin);
     597          57 :     }
     598             : 
     599             :     /// iterator past the last state in the block
     600       53606 :     permutation_const_iter_t end()  const  {  return int_end;  }
     601       18455 :     permutation_iter_t end()  {  return int_end;  }
     602         308 :     void set_end(permutation_iter_t new_end)
     603             :     {
     604         308 :         int_end = new_end;                                                      assert(int_marked_bottom_begin <= int_end); assert(int_bottom_begin < int_end);
     605         308 :     }
     606             : 
     607             :     /// iterator to the first non-bottom state in the block
     608       39977 :     permutation_const_iter_t nonbottom_begin()  const  {  return int_begin;  }
     609        1951 :     permutation_iter_t nonbottom_begin()  {  return int_begin;  }
     610             : 
     611             :     /// iterator past the last non-bottom state in the block
     612       43037 :     permutation_const_iter_t nonbottom_end() const { return int_bottom_begin; }
     613         753 :     permutation_iter_t nonbottom_end()  {  return int_bottom_begin;  }
     614             :     void set_nonbottom_end(permutation_iter_t new_nonbottom_end)
     615             :     {
     616             :         int_bottom_begin = new_nonbottom_end;                                   assert(int_marked_nonbottom_begin <= int_bottom_begin);
     617             :                                                                                 assert(int_bottom_begin <= int_marked_bottom_begin);
     618             :                                                                                 assert(int_bottom_begin < int_end);
     619             :     }
     620             : 
     621             :     /// iterator to the first bottom state in the block
     622      103019 :     permutation_const_iter_t bottom_begin() const  { return int_bottom_begin; }
     623        2985 :     permutation_iter_t bottom_begin()  {  return int_bottom_begin;  }
     624         860 :     void set_bottom_begin(permutation_iter_t new_bottom_begin)
     625             :     {
     626         860 :         int_bottom_begin = new_bottom_begin;                                    assert(int_marked_nonbottom_begin <= int_bottom_begin);
     627         860 :                                                                                 assert(int_bottom_begin <= int_marked_bottom_begin);
     628             :                                                                                 // assert(int_bottom_begin < int_end);
     629         860 :     }
     630             : 
     631             :     /// iterator past the last bottom state in the block
     632       33579 :     permutation_const_iter_t bottom_end() const  {  return int_end;  }
     633        1201 :     permutation_iter_t bottom_end()  {  return int_end;  }
     634             : 
     635             :     /// iterator to the first unmarked non-bottom state in the block
     636             :     permutation_const_iter_t unmarked_nonbottom_begin()const{return int_begin;}
     637         865 :     permutation_iter_t unmarked_nonbottom_begin()  {  return int_begin;  }
     638             : 
     639             :     /// iterator past the last unmarked non-bottom state in the block
     640             :     permutation_const_iter_t unmarked_nonbottom_end() const
     641             :     {
     642             :         return int_marked_nonbottom_begin;
     643             :     }
     644         408 :     permutation_iter_t unmarked_nonbottom_end()
     645             :     {
     646         408 :         return int_marked_nonbottom_begin;
     647             :     }
     648             :     void set_unmarked_nonbottom_end(permutation_iter_t
     649             :                                                     new_unmarked_nonbottom_end)
     650             :     {
     651             :         int_marked_nonbottom_begin = new_unmarked_nonbottom_end;                assert(int_begin <= int_marked_nonbottom_begin);
     652             :                                                                                 assert(int_marked_nonbottom_begin <= int_bottom_begin);
     653             :     }
     654             : 
     655             :     /// iterator to the first marked non-bottom state in the block
     656       13482 :     permutation_const_iter_t marked_nonbottom_begin() const
     657             :     {
     658       13482 :         return int_marked_nonbottom_begin;
     659             :     }
     660        2878 :     permutation_iter_t marked_nonbottom_begin()
     661             :     {
     662        2878 :         return int_marked_nonbottom_begin;
     663             :     }
     664        1482 :     void set_marked_nonbottom_begin(permutation_iter_t
     665             :                                                     new_marked_nonbottom_begin)
     666             :     {
     667        1482 :         int_marked_nonbottom_begin = new_marked_nonbottom_begin;                assert(int_begin <= int_marked_nonbottom_begin);
     668        1482 :                                                                                 assert(int_marked_nonbottom_begin <= int_bottom_begin);
     669        1482 :     }
     670             : 
     671             :     /// iterator one past the last marked non-bottom state in the block
     672       13482 :     permutation_const_iter_t marked_nonbottom_end() const
     673             :     {
     674       13482 :         return int_bottom_begin;
     675             :     }
     676        1563 :     permutation_iter_t marked_nonbottom_end()  {  return int_bottom_begin;  }
     677             : 
     678             :     /// iterator to the first unmarked bottom state in the block
     679        2393 :     permutation_const_iter_t unmarked_bottom_begin() const
     680             :     {
     681        2393 :         return int_bottom_begin;
     682             :     }
     683        1085 :     permutation_iter_t unmarked_bottom_begin()  {  return int_bottom_begin;  }
     684             : 
     685             :     /// iterator past the last unmarked bottom state in the block
     686        2393 :     permutation_const_iter_t unmarked_bottom_end() const
     687             :     {
     688        2393 :         return int_marked_bottom_begin;
     689             :     }
     690        1368 :     permutation_iter_t unmarked_bottom_end()  {return int_marked_bottom_begin;}
     691             :     void set_unmarked_bottom_end(permutation_iter_t new_unmarked_bottom_end)
     692             :     {
     693             :         int_marked_bottom_begin = new_unmarked_bottom_end;                      assert(int_bottom_begin <= int_marked_bottom_begin);
     694             :                                                                                 assert(int_marked_bottom_begin <= int_end);
     695             :     }
     696             : 
     697             :     /// iterator to the first marked bottom state in the block
     698       13570 :     permutation_const_iter_t marked_bottom_begin() const
     699             :     {
     700       13570 :         return int_marked_bottom_begin;
     701             :     }
     702        7508 :     permutation_iter_t marked_bottom_begin()  {return int_marked_bottom_begin;}
     703        2959 :     void set_marked_bottom_begin(permutation_iter_t new_marked_bottom_begin)
     704             :     {
     705        2959 :         int_marked_bottom_begin = new_marked_bottom_begin;                      assert(int_bottom_begin <= int_marked_bottom_begin);
     706        2959 :                                                                                 assert(int_marked_bottom_begin <= int_end);
     707        2959 :     }
     708             : 
     709             :     /// \brief iterator past the last marked bottom state in the block
     710             :     /// \details This includes the old bottom states.
     711       13570 :     permutation_const_iter_t marked_bottom_end() const  {  return int_end;  }
     712        1127 :     permutation_iter_t marked_bottom_end()  {  return int_end;  }
     713             : 
     714             :     /// iterator to the first inert transition of the block
     715       64443 :     B_to_C_const_iter_t inert_begin() const  {  return int_inert_begin;  }
     716        4116 :     B_to_C_iter_t inert_begin()  {  return int_inert_begin;  }
     717         933 :     void set_inert_begin(B_to_C_iter_t new_inert_begin)
     718             :     {
     719         933 :         int_inert_begin = new_inert_begin;                                      assert(int_inert_begin <= int_inert_end);
     720         933 :     }
     721             : 
     722             :     /// iterator past the last inert transition of the block
     723       56562 :     B_to_C_const_iter_t inert_end() const  {  return int_inert_end;  }
     724        6722 :     B_to_C_iter_t inert_end()  {  return int_inert_end;  }
     725         791 :     void set_inert_end(B_to_C_iter_t new_inert_end)
     726             :     {
     727         791 :         int_inert_end = new_inert_end;                                          assert(int_inert_begin <= int_inert_end);
     728         791 :     }
     729         556 :     void set_inert_begin_and_end(B_to_C_iter_t new_inert_begin,
     730             :                                                    B_to_C_iter_t new_inert_end)
     731             :     {
     732         556 :         int_inert_begin = new_inert_begin;
     733         556 :         int_inert_end = new_inert_end;                                          assert(int_inert_begin <= int_inert_end);
     734         556 :     }
     735             : 
     736             :     /// \brief mark a non-bottom state
     737             :     /// \details Marking is done by moving the state to the slice of the marked
     738             :     /// non-bottom states of the block.
     739             :     /// \param s the non-bottom state that has to be marked
     740             :     /// \returns true if the state was not marked before
     741         362 :     bool mark_nonbottom(state_info_ptr s)
     742         362 :     {                                                                           assert(s->pos < nonbottom_end());  assert(nonbottom_begin() <= s->pos);
     743         362 :         if (marked_nonbottom_begin() <= s->pos)  return false;
     744         327 :         set_marked_nonbottom_begin(marked_nonbottom_begin() - 1);
     745         327 :         swap_permutation(s->pos, marked_nonbottom_begin());
     746         327 :         return true;
     747             :     }
     748             : 
     749             :     /// \brief mark a state
     750             :     /// \details Marking is done by moving the state to the slice of the marked
     751             :     /// bottom or non-bottom states of the block.  If `s` is an old bottom
     752             :     /// state, it is treated as if it already were marked.
     753             :     /// \param s the state that has to be marked
     754             :     /// \returns true if the state was not marked before
     755        1558 :     bool mark(state_info_ptr s)
     756        1558 :     {                                                                           assert(s->pos < end());
     757        1558 :         if (bottom_begin() <= s->pos)
     758             :         {
     759        1400 :             if (marked_bottom_begin() <= s->pos)  return false;
     760        1327 :             set_marked_bottom_begin(marked_bottom_begin() - 1);
     761        1327 :             swap_permutation(s->pos, marked_bottom_begin());
     762        1327 :             return true;
     763             :         }
     764         158 :         return mark_nonbottom(s);
     765             :     }
     766             : 
     767             :     /// \brief refine the block (the blue subblock is smaller)
     768             :     /// \details This function is called after a refinement function has found
     769             :     /// that the blue subblock is the smaller one.  It creates a new block for
     770             :     /// the blue states.
     771             :     /// \param blue_nonbottom_end iterator past the last blue non-bottom state
     772             :     /// \returns pointer to the new (blue) block
     773             :     block_t* split_off_blue(permutation_iter_t blue_nonbottom_end);
     774             : 
     775             :     /// \brief refine the block (the red subblock is smaller)
     776             :     /// \details This function is called after a refinement function has found
     777             :     /// that the red subblock is the smaller one.  It creates a new block for
     778             :     /// the red states.
     779             :     /// \param red_nonbottom_begin iterator to the first red non-bottom state
     780             :     /// \returns pointer to the new (red) block
     781             :     block_t* split_off_red(permutation_iter_t red_nonbottom_begin);
     782             :                                                                                 #ifndef NDEBUG
     783             :                                                                                     /// \brief print a block identification for debugging
     784             :                                                                                     /// \details This function is only available if compiled in Debug mode.
     785           0 :                                                                                     std::string debug_id() const
     786             :                                                                                     {
     787           0 :                                                                                         return "block [" + std::to_string(begin() - perm_begin) + "," +
     788           0 :                                                                                             std::to_string(end() - perm_begin) + ")" +
     789           0 :                                                                                             (BLOCK_NO_SEQNR != seqnr() ?" (#"+std::to_string(seqnr())+")" :"");
     790             :                                                                                     }
     791             : 
     792             :                                                                                     /// \brief provide an iterator to the beginning of the permutation array
     793             :                                                                                     /// \details This iterator is required to be able to print identifications
     794             :                                                                                     /// for debugging.  It is only available if compiled in Debug mode.
     795           0 :                                                                                     static permutation_const_iter_t permutation_begin()  { return perm_begin; }
     796             : 
     797             :                                                                                     mutable check_complexity::block_counter_t work_counter;
     798             :                                                                                   private:
     799             :                                                                                     static permutation_const_iter_t perm_begin;
     800             : 
     801             :                                                                                     friend class part_state_t;
     802             :                                                                                 #endif
     803             : };
     804             : 
     805             : 
     806             : /// \class constln_t
     807             : /// \brief stores information about a constellation
     808             : /// \details A constellation corresponds to a slice in the permutation array;
     809             : /// its boundaries are also block boundaries.  As the number of constellations
     810             : /// is initially unknown, we will allocate it dynamically.
     811             : class constln_t
     812             : {
     813             :   private:
     814             :     /// iterator past the last state in the constellation
     815             :     permutation_iter_t int_end;
     816             : 
     817             :     /// iterator to the first state in the constellation
     818             :     permutation_iter_t int_begin;
     819             : 
     820             :     /// \brief next constellation in the list of non-trivial constellations
     821             :     /// \details If this is the last constellation in the list,
     822             :     /// `nontrivial_next` points to this very constellation.  Consequently, it
     823             :     /// is possible to check whether some constellation is trivial without an
     824             :     /// additional variable.
     825             :     constln_t* nontrivial_next;
     826             : 
     827             :     /// first constellation in the list of non-trivial constellations
     828             :     static constln_t* nontrivial_first;
     829             :   public:
     830             :     /// \brief iterator to the first transition into this constellation that
     831             :     /// needs postprocessing
     832             :     /// \details In `postprocess_new_bottom()`, all transitions from a refined
     833             :     /// block to the present constellation have to be gone through.  Because
     834             :     /// during this process the refined block may be refined even further, we
     835             :     /// need `postprocess_begin` and `postprocess_end` to store which
     836             :     /// transitions have to be gone through overall.
     837             :     ///
     838             :     /// If no transitions to this constellation need to be postprocessed, the
     839             :     /// variable is set to the same value as postprocess_end, preferably to
     840             :     /// part_trans_t::B_to_C->end().
     841             :     B_to_C_iter_t postprocess_begin;
     842             : 
     843             :     /// \brief iterator past the last transition into this constellation that
     844             :     /// needs postprocessing
     845             :     B_to_C_iter_t postprocess_end;
     846             : 
     847             :     /// \brief sort key to order constellation-related information
     848             :     /// \details When a constellation is created anew, it it assigned a sort
     849             :     /// key that is lower than the constellation it came from, but never lower
     850             :     /// than the sort key of any other constellation that was lower than the
     851             :     /// original constellation.  This ensures that the order of other
     852             :     /// constellations does not change.
     853             :     const state_type sort_key;
     854             : 
     855             :     /// \brief constructor
     856             :     /// \param begin_ iterator to the first state in the constellation
     857             :     /// \param end_   iterator past the last state in the constellation
     858         556 :     constln_t(state_type sort_key_, permutation_iter_t begin_,
     859             :                        permutation_iter_t end_, B_to_C_iter_t postprocess_none)
     860         556 :       : int_end(end_),
     861             :         int_begin(begin_),
     862             :         nontrivial_next(nullptr),
     863             :         postprocess_begin(postprocess_none),
     864             :         postprocess_end(postprocess_none),
     865         556 :         sort_key(sort_key_)
     866         556 :     {                                                                           assert(int_begin<int_end);  assert((state_type)(int_end-int_begin)<=sort_key);
     867         556 :     }
     868             : 
     869             :     /// \brief destructor
     870         556 :     ~constln_t()  {  }
     871             : 
     872             :     /// \brief provides an arbitrary non-trivial constellation
     873             :     /// \details The static function is implemented in a way to provide the
     874             :     /// first constellation in the list of non-trivial constellations.
     875        1613 :     static constln_t* get_some_nontrivial()  {  return nontrivial_first;  }
     876             : 
     877             :     /// \brief provides the next non-trivial constellation
     878             :     /// \details This (non-static!) function just returns the next non-trivial
     879             :     /// constellation in the list.  Note: If this constellation is the last in
     880             :     /// the list of non-trivial constellations, the convention is that the next
     881             :     /// pointer points to this constellation self (to distinguish it from
     882             :     /// nullptr).
     883         775 :     const constln_t* get_nontrivial_next() const  {  return nontrivial_next;  }
     884             : 
     885             :     /// \brief makes a constellation trivial (i. e. removes it from the
     886             :     /// respective list)
     887             :     /// \details This member function only works if the constellation is the
     888             :     /// first one in the list (which will normally be the case).
     889         214 :     void make_trivial()
     890         214 :     {                                                                           assert(nontrivial_first == this);
     891         214 :         nontrivial_first = nontrivial_next == this ? nullptr : nontrivial_next;
     892         214 :         nontrivial_next = nullptr;
     893         214 :     }
     894             : 
     895             :     /// \brief makes a constellation non-trivial (i. e. inserts it into the
     896             :     /// respective list)
     897         419 :     void make_nontrivial()
     898             :     {
     899         419 :         if (nullptr == nontrivial_next)
     900             :         {
     901         214 :             nontrivial_next = nullptr == nontrivial_first ? this
     902             :                                                           : nontrivial_first;
     903         214 :             nontrivial_first = this;
     904             :         }
     905         419 :     }
     906             : 
     907             :     /// \brief returns true iff the constellation is trivial
     908             :     /// \details If this constellation is the last in the list of non-trivial
     909             :     /// constellations, the convention is that the next pointer points to this
     910             :     /// constellation itself (to distinguish it from nullptr).
     911        8219 :     bool is_trivial() const
     912             :     {
     913        8219 :         return nullptr == nontrivial_next;
     914             :     }
     915             : 
     916             :     /// \brief constant iterator to the first state in the constellation
     917       25213 :     permutation_const_iter_t begin() const  {  return int_begin;  }
     918             :     /// \brief iterator to the first state in the constellation
     919       11592 :     permutation_iter_t begin()  {  return int_begin;  }
     920             :     /// \brief set the iterator to the first state in the constellation
     921         192 :     void set_begin(permutation_iter_t new_begin)
     922             :     {
     923         192 :         int_begin = new_begin;                                                  assert(int_begin < int_end);
     924         192 :     }
     925             : 
     926             :     /// \brief constant iterator past the last state in the constellation
     927       67902 :     permutation_const_iter_t end() const  {  return int_end;  }
     928             :     /// \brief iterator past the last state in the constellation
     929        3692 :     permutation_iter_t end()  {  return int_end;  }
     930             :     /// \brief set the iterator past the last state in the constellation
     931         309 :     void set_end(permutation_iter_t new_end)
     932             :     {
     933         309 :         int_end = new_end;                                                      assert(int_begin < int_end);
     934         309 :     }
     935             : 
     936             :     /// \brief returns number of states in the constellation
     937       53072 :     state_type size() const  {  return int_end - int_begin;  }
     938             : 
     939             :     /// \brief compares two constellations for ordering them
     940             :     /// \details Constellations are ordered according to their sort keys.  The
     941             :     /// keys have to be assigned in a way that when a constellation is split,
     942             :     /// the parts are placed where the split constellation was in the order.
     943             :     /// This can be achieved by assigning sort keys that are related to the
     944             :     /// size of the constellation.
     945       36432 :     bool operator<(const constln_t& other) const
     946             :     {
     947       36432 :         return sort_key < other.sort_key;
     948             :     }
     949       11552 :     bool operator> (const constln_t& other) const  {  return other < *this;  }
     950       13687 :     bool operator<=(const constln_t& other) const  { return !(other < *this); }
     951             :     bool operator>=(const constln_t& other) const  { return !(*this < other); }
     952             : 
     953             :     /// \brief split off a single block from the constellation
     954             :     /// \details The function splits the current constellation after its first
     955             :     /// block or before its last block, whichever is smaller.  It creates a new
     956             :     /// constellation for the split-off block and returns a pointer to the
     957             :     /// block.
     958         501 :     block_t* split_off_small_block()
     959         501 :     {                                                                           assert(begin() < end());
     960         501 :         block_t* const FirstB = (*begin())->block;
     961         501 :         block_t* const LastB = end()[-1]->block;                                assert(FirstB != LastB);
     962         501 :         if (FirstB->end() == LastB->begin())  make_trivial();                   assert(FirstB->constln() == this);  assert(LastB->constln() == this);
     963         501 :                                                                                 assert(postprocess_begin == postprocess_end);
     964             :         // 2.5: Choose a small splitter block SpB subset of SpC from P,
     965             :         //      i.e. |SpB| <= 1/2*|SpC|
     966             :         /// It doesn't matter very much how ties are resolved here:
     967             :         /// `part_tr.change_to_C()` is faster if the first block is selected to
     968             :         /// be split off.  `part_tr.split_s_inert_out()` is faster if the last
     969             :         /// block is selected.
     970         501 :         if (FirstB->size() > LastB->size())
     971             :         {
     972             :             // 2.6: Create a new constellation NewC
     973             :             // 2.6: ... and move SpB from SpC to NewC
     974             :             constln_t* NewC =
     975         618 :                     new constln_t(sort_key - (LastB->begin() - begin()),
     976         309 :                                        LastB->begin(), end(), postprocess_end);
     977         309 :             set_end(LastB->begin());
     978         309 :             LastB->set_constln(NewC);
     979         309 :             return LastB;
     980             :         }
     981             :         else
     982             :         {
     983             :             // 2.6: Create a new constellation NewC
     984             :             // 2.6: ... and move SpB from SpC to NewC
     985             :             constln_t* NewC =
     986         384 :                     new constln_t(sort_key - (end() - FirstB->end()), begin(),
     987         192 :                                                FirstB->end(), postprocess_end);
     988         192 :             set_begin(FirstB->end());
     989         192 :             FirstB->set_constln(NewC);
     990         192 :             return FirstB;
     991             :         }
     992             :     }
     993             :                                                                                 #ifndef NDEBUG
     994             :                                                                                     /// \brief print a constellation identification for debugging
     995           0 :                                                                                     std::string debug_id() const
     996             :                                                                                     {
     997           0 :                                                                                         return "constellation [" +
     998           0 :                                                                                                    std::to_string(begin() - block_t::permutation_begin()) +
     999           0 :                                                                                                    "," + std::to_string(end() - block_t::permutation_begin()) +
    1000           0 :                                                                                                    ") (#" + std::to_string(sort_key) + ")";
    1001             :                                                                                     }
    1002             :                                                                                 #endif
    1003             : };
    1004             : 
    1005             : 
    1006             : template <class LTS_TYPE>
    1007             : class bisim_partitioner_gjkw_initialise_helper;
    1008             : 
    1009             : class part_trans_t;
    1010             : 
    1011             : /// \class part_state_t
    1012             : /// \brief refinable partition data structure
    1013             : /// \details This class collects all information about a partition of the
    1014             : /// states.
    1015             : class part_state_t
    1016             : {
    1017             :   public:
    1018             :     /// \brief permutation array
    1019             :     /// \details This is the central element of the data structure:  In this
    1020             :     /// array, states that belong to the same block are stored in adjacent
    1021             :     /// elements, and blocks that belong to the same constellation are stored
    1022             :     /// in adjacent slices.
    1023             :     permutation_t permutation;
    1024             : 
    1025             :   private:
    1026             :     /// \brief array with all other information about states
    1027             :     /// \details We allocate 1 additional ``state'' to allow for the iterators
    1028             :     /// past the last transition, as described in the documentation of
    1029             :     /// `state_info_entry`.
    1030             :     fixed_vector<state_info_entry> state_info;
    1031             : 
    1032             :     template <class LTS_TYPE>
    1033             :     friend class bisim_partitioner_gjkw_initialise_helper;
    1034             :   public:
    1035             :     /// \brief constructor
    1036             :     /// \details The constructor allocates memory, but does not actually
    1037             :     /// initialise the partition.  Immediately afterwards, the initialisation
    1038             :     /// helper `bisim_partitioner_gjkw_initialise_helper::init_transitions()`
    1039             :     /// should be called.
    1040             :     /// \param n number of states in the Kripke structure
    1041          55 :     part_state_t(state_type n)
    1042          55 :       : permutation(n),
    1043          55 :         state_info(n+1) //< an additional ``state'' is needed to store pointers
    1044             :             // to the end of the slices of transitions of the last state
    1045          55 :     {                                                                           assert(0 == block_t::nr_of_blocks);
    1046             :                                                                                 #ifndef NDEBUG
    1047          55 :                                                                                     block_t::perm_begin = permutation.begin();
    1048          55 :                                                                                     state_info_entry::s_i_begin = state_info.data();
    1049          55 :                                                                                     state_info_entry::s_i_end = state_info_entry::s_i_begin + n;
    1050             :                                                                                 #endif
    1051          55 :     }
    1052             : 
    1053             :     /// \brief destructor
    1054             :     /// \details The destructor assumes that the caller has already executed
    1055             :     /// `clear()` to deallocate the memory for the partition.
    1056          55 :     ~part_state_t()
    1057          55 :     {                                                                           assert(state_info.empty());  assert(permutation.empty());
    1058          55 :     }
    1059             : 
    1060             :     /// \brief deallocates constellations and blocks
    1061             :     /// \details This function can be called shortly before destructing the
    1062             :     /// partition.  Afterwards, the data structure is in a unusable state,
    1063             :     /// as all information on states, blocks and constellations is deleted and
    1064             :     /// deallocated.
    1065          55 :     void clear()
    1066             :     {
    1067             :         // We have to deallocate constellations first because deallocating
    1068             :         // blocks makes the constellations inaccessible.
    1069         611 :         for (permutation_iter_t permutation_iter = permutation.end();
    1070         611 :                                      permutation.begin() != permutation_iter; )
    1071             :         {
    1072         556 :             constln_t* const C = permutation_iter[-1]->constln();               assert(C->end() == permutation_iter);
    1073             :             // permutation_iter[-1]->block->set_constln(nullptr);               // assert that constellation is trivial:
    1074         556 :                                                                                 assert(permutation_iter[-1]->block->begin() == C->begin());
    1075         556 :             permutation_iter = C->begin();
    1076         556 :             delete C;
    1077             :         }
    1078             :                                                                                 #ifndef NDEBUG
    1079          55 :                                                                                     state_type deleted_blocks = 0;
    1080             :                                                                                 #endif
    1081         611 :         for (permutation_iter_t permutation_iter = permutation.end();
    1082         611 :                                      permutation.begin() != permutation_iter; )
    1083             :         {
    1084         556 :             block_t* const B = permutation_iter[-1]->block;                     assert(B->end() == permutation_iter);
    1085         556 :             permutation_iter = B->begin();
    1086             :                                                                                 #ifndef NDEBUG
    1087         556 :                                                                                     if (BLOCK_NO_SEQNR != B->seqnr())  ++deleted_blocks;
    1088         277 :                                                                                     else                               assert(0 == deleted_blocks);
    1089             :                                                                                 #endif
    1090         556 :             delete B;
    1091          55 :         }                                                                       assert(deleted_blocks == block_t::nr_of_blocks);
    1092          55 :         block_t::nr_of_blocks = 0;
    1093          55 :         state_info.clear();
    1094          55 :         permutation.clear();
    1095          55 :     }
    1096             : 
    1097             :     /// \brief provide size of state space
    1098             :     /// \returns the stored size of the state space
    1099          55 :     state_type state_size() const  {  return permutation.size();  }
    1100             : 
    1101             :     /// \brief find block of a state
    1102             :     /// \param s number of the state
    1103             :     /// \returns a pointer to the block where state s resides in
    1104          57 :     const block_t* block(state_type s) const
    1105             :     {
    1106          57 :         return state_info[s].block;
    1107             :     }
    1108             :                                                                                 #ifndef NDEBUG
    1109             :                                                                                   private:
    1110             :                                                                                     /// \brief print a slice of the partition (typically a block)
    1111             :                                                                                     /// \details If the slice indicated by the parameters is not empty, the
    1112             :                                                                                     /// states in this slice will be printed.
    1113             :                                                                                     /// \param message text printed as a title if the slice is not empty
    1114             :                                                                                     /// \param B       block that is being printed (it is checked whether
    1115             :                                                                                     ///                states belong to this block)
    1116             :                                                                                     /// \param begin   iterator to the beginning of the slice
    1117             :                                                                                     /// \param end     iterator past the end of the slice
    1118             :                                                                                     void print_block(const char* message, const block_t* B,
    1119             :                                                                                         permutation_const_iter_t begin, permutation_const_iter_t end) const;
    1120             :                                                                                   public:
    1121             :                                                                                     /// \brief print the partition as a tree (per constellation and block)
    1122             :                                                                                     /// \details The function prints all constellations (in order); for each
    1123             :                                                                                     /// constellation it prints the blocks it consists of; and for each block,
    1124             :                                                                                     /// it lists its states, separated into nonbottom and bottom states.
    1125             :                                                                                     /// \param part_tr partition for the transitions
    1126             :                                                                                     void print_part(const part_trans_t& part_tr) const;
    1127             : 
    1128             :                                                                                     /// \brief print all transitions
    1129             :                                                                                     /// \details For each state (in order), its outgoing transitions are
    1130             :                                                                                     /// listed, sorted by goal constellation.  The function also indicates
    1131             :                                                                                     /// where the current constellation pointer of the state points at.
    1132             :                                                                                     void print_trans() const;
    1133             :                                                                                 #endif
    1134             : };
    1135             : 
    1136             : ///@} (end of group part_state)
    1137             : 
    1138             : 
    1139             : 
    1140             : 
    1141             : 
    1142             : /* ************************************************************************* */
    1143             : /*                                                                           */
    1144             : /*                           T R A N S I T I O N S                           */
    1145             : /*                                                                           */
    1146             : /* ************************************************************************* */
    1147             : 
    1148             : 
    1149             : 
    1150             : 
    1151             : 
    1152             : /// \defgroup part_trans
    1153             : /// \brief data structures for transitions used during partition refinement
    1154             : /// \details These definitions provide a partition for transition data
    1155             : /// structure that can be used for the partition refinement algorithm.
    1156             : ///
    1157             : /// Basically, transitions are stored in three arrays:
    1158             : /// - `pred`: transitions ordered by goal state, to allow finding all
    1159             : ///   predecessors of a goal state.
    1160             : /// - `succ`: transitions ordered by source state and goal constellation, to
    1161             : ///   allow finding all successors of a source state.  Given a transition in
    1162             : ///   this array, it is easy to find all transitions from the same source state
    1163             : ///   to the same goal constellation.  It is possible to find out, in time
    1164             : ///   logarithmic in the out-degree, whether a state has a transition to a
    1165             : ///   given constellation.
    1166             : /// - `B_to_C`: a permutation of the transitions such that transitions from the
    1167             : ///    same source block to the same goal constellation are adjacent.  Further,
    1168             : ///    this array does not need a specific sort order.
    1169             : ///
    1170             : /// Within this sort order, inert transitions are always placed after non-inert
    1171             : /// transitions.
    1172             : ///
    1173             : /// state_info_entry and block_t (defined above) contain pointers to the slices
    1174             : /// of these arrays.  For the incoming transitions, they contain enough
    1175             : /// information; for the outgoing and the B_to_C-transitions, we additionally
    1176             : /// use so-called _descriptors_ that show which slice belongs together.
    1177             : /// The above was the original design described in our publication
    1178             : /// [Groote/Jansen/Keiren/Wijs 2017].  This code reduces the descriptor for the
    1179             : /// outgoing transitions to a single pointer, which is stored in the `succ`
    1180             : /// array directly.
    1181             : 
    1182             : ///@{
    1183             : 
    1184             : /* pred_entry, succ_entry, and B_to_C_entry contain the data that is stored
    1185             : about a transition.  Every transition has one of each data structure; the three
    1186             : structures are linked through the iterators (used here as pointers). */
    1187        1116 : class succ_entry
    1188             : {
    1189             :   public:
    1190             :     B_to_C_iter_t B_to_C;
    1191             :     state_info_ptr target;
    1192             : 
    1193             :   private:
    1194             :     /// \brief points to the last or the first transition to the same
    1195             :     /// constellation
    1196             :     /// \details We need to know, given a transition, which other transitions
    1197             :     /// with the same source state and the same goal constellation there are.
    1198             :     /// This pointer, in most cases, points to the last transition with the
    1199             :     /// same source state and goal constellation, with the exception:  If this
    1200             :     /// `succ_entry` is actually the last transition, then the pointer points
    1201             :     /// to the first such transition.  In that way, one can find the first and
    1202             :     /// the last relevant transition with one or two levels of dereferencing.
    1203             :     ///
    1204             :     /// The advantage of this pointer is that one does not need to allocate a
    1205             :     /// separate data structure containing this information.
    1206             :     succ_iter_t int_slice_begin_or_before_end;
    1207             :   public:
    1208             : 
    1209        2686 :     succ_iter_t slice_begin_or_before_end()
    1210             :     {
    1211        2686 :         return int_slice_begin_or_before_end;
    1212             :     }
    1213             : 
    1214       63274 :     succ_const_iter_t slice_begin_or_before_end() const
    1215             :     {
    1216       63274 :         return int_slice_begin_or_before_end;
    1217             :     }
    1218             : 
    1219        2485 :     void set_slice_begin_or_before_end(succ_iter_t new_value)
    1220             :     {
    1221        2485 :         int_slice_begin_or_before_end = new_value;
    1222        2485 :     }
    1223             : 
    1224             : 
    1225        5798 :     succ_iter_t slice_begin()
    1226             :     {
    1227        5798 :         if (this < &*int_slice_begin_or_before_end)
    1228        1200 :         {                                                                       assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end <= this);
    1229        1200 :             return int_slice_begin_or_before_end->
    1230        1200 :                                                  int_slice_begin_or_before_end;
    1231        4598 :         }                                                                       assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end == this);
    1232        4598 :         return int_slice_begin_or_before_end;
    1233             :     }
    1234             : 
    1235         138 :     succ_const_iter_t slice_begin() const
    1236             :     {
    1237         138 :         if (this < &*int_slice_begin_or_before_end)
    1238           6 :         {                                                                       assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end <= this);
    1239           6 :             return int_slice_begin_or_before_end->
    1240           6 :                                                  int_slice_begin_or_before_end;
    1241         132 :         }                                                                       assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end == this);
    1242         132 :         return int_slice_begin_or_before_end;
    1243             :     }
    1244             : 
    1245        5883 :     static succ_iter_t slice_end(succ_iter_t this_)
    1246             :     {
    1247        5883 :         if (this_ < this_->int_slice_begin_or_before_end)
    1248        1204 :         {                                                                       assert(this_->int_slice_begin_or_before_end->
    1249             :                                                                                                                        int_slice_begin_or_before_end <= this_);
    1250        1204 :             return this_->int_slice_begin_or_before_end + 1;
    1251        4679 :         }                                                                       assert(this_->int_slice_begin_or_before_end->
    1252             :                                                                                                                        int_slice_begin_or_before_end == this_);
    1253             :         // The following line requires an iterator but a normal method would
    1254             :         // only have a pointer, not an iterator.  That's why we need to jump
    1255             :         // through the `static` hoop.
    1256        4679 :         return this_ + 1;
    1257             :     }
    1258             : 
    1259         548 :     static succ_const_iter_t slice_end(succ_const_iter_t this_)
    1260             :     {
    1261         548 :         if (this_ < this_->int_slice_begin_or_before_end)
    1262          20 :         {                                                                       assert(this_->int_slice_begin_or_before_end->
    1263             :                                                                                                                        int_slice_begin_or_before_end <= this_);
    1264          20 :             return this_->int_slice_begin_or_before_end + 1;
    1265         528 :         }                                                                       assert(this_->int_slice_begin_or_before_end->
    1266             :                                                                                                                        int_slice_begin_or_before_end == this_);
    1267             :         // The following line requires an iterator but a normal method would
    1268             :         // only have a pointer, not an iterator.  That's why we need to jump
    1269             :         // through the `static` hoop.
    1270         528 :         return this_ + 1;
    1271             :     }
    1272             :                                                                                 #ifndef NDEBUG
    1273             :                                                                                     /// adds work (for time complexity measurement) to every transition in the
    1274             :                                                                                     /// slice to which `this_` belongs.
    1275             :                                                                                     static void slice_add_work_to_transns(succ_const_iter_t this_,
    1276             :                                                                                                   enum check_complexity::counter_type ctr, unsigned max_value);
    1277             :                                                                                 #endif
    1278             : };
    1279             : 
    1280             : 
    1281        1116 : class pred_entry
    1282             : {
    1283             :   public:
    1284             :     succ_iter_t succ;
    1285             :     state_info_ptr source;
    1286             :                                                                                 #ifndef NDEBUG
    1287             :                                                                                     /// \brief print a short transition identification for debugging
    1288             :                                                                                     /// \details This function is only available if compiled in Debug mode.
    1289           0 :                                                                                     std::string debug_id_short() const
    1290             :                                                                                     {
    1291           0 :                                                                                         return "from " + source->debug_id_short() + " to " +
    1292           0 :                                                                                                                                 succ->target->debug_id_short();
    1293             :                                                                                     }
    1294             : 
    1295             :                                                                                     /// \brief print a transition identification for debugging
    1296             :                                                                                     /// \details This function is only available if compiled in Debug mode.
    1297           0 :                                                                                     std::string debug_id() const
    1298             :                                                                                     {
    1299           0 :                                                                                         return "transition " + debug_id_short();
    1300             :                                                                                     }
    1301             : 
    1302             :                                                                                     mutable check_complexity::trans_counter_t work_counter;
    1303             :                                                                                 #endif
    1304             : };
    1305             : 
    1306             : 
    1307        1116 : class B_to_C_entry
    1308             : {
    1309             :   public:
    1310             :     pred_iter_t pred;
    1311             :     B_to_C_desc_iter_t B_to_C_slice;
    1312             : };
    1313             :                                                                                 #ifndef NDEBUG
    1314             :                                                                                     /// adds work (for time complexity measurement) to every transition in the
    1315             :                                                                                     /// slice.
    1316         137 :                                                                                     inline void succ_entry::slice_add_work_to_transns(succ_const_iter_t this_,
    1317             :                                                                                                    enum check_complexity::counter_type ctr, unsigned max_value)
    1318             :                                                                                     {
    1319         137 :                                                                                         succ_const_iter_t iter = this_->slice_begin();
    1320         137 :                                                                                         succ_const_iter_t end = slice_end(this_);
    1321         137 :                                                                                         assert(iter < end);
    1322         137 :                                                                                         mCRL2complexity(iter->B_to_C->pred, add_work(ctr, max_value), );
    1323         199 :                                                                                         while (++iter != end)
    1324             :                                                                                         {
    1325             :                                                                                             // treat temporary counters specially
    1326          31 :                                                                                             mCRL2complexity(iter->B_to_C->pred,
    1327             :                                                                                                                        add_work_notemporary(ctr, max_value), );
    1328             :                                                                                         }
    1329         137 :                                                                                     }
    1330             :                                                                                 #endif
    1331             : /* B_to_C_descriptor is a data type that indicates which slice of states
    1332             : belongs together. */
    1333             : class B_to_C_descriptor
    1334             : {
    1335             :   public:
    1336             :     B_to_C_iter_t end, begin;
    1337             : 
    1338        1334 :     B_to_C_descriptor(B_to_C_iter_t begin_, B_to_C_iter_t end_)
    1339        1334 :       : end(end_),
    1340        1334 :         begin(begin_)
    1341        1334 :     {  }
    1342             : 
    1343             :     /// compute the source block of the transitions in this slice
    1344       14477 :     const block_t* from_block() const
    1345       14477 :     {                                                                           assert(begin < end);  assert(begin->pred->succ->B_to_C == begin);
    1346       14477 :         return begin->pred->source->block;
    1347             :     }
    1348       67305 :     block_t* from_block()
    1349       67305 :     {                                                                           assert(begin < end);  assert(begin->pred->succ->B_to_C == begin);
    1350       67305 :         return begin->pred->source->block;
    1351             :     }
    1352             : 
    1353             :     /// compute the goal constellation of the transitions in this slice
    1354       29382 :     const constln_t* to_constln() const
    1355       29382 :     {                                                                           assert(begin < end);  assert(begin->pred->succ->B_to_C == begin);
    1356       29382 :         return begin->pred->succ->target->constln();
    1357             :     }
    1358       66804 :     constln_t* to_constln()
    1359       66804 :     {                                                                           assert(begin < end);  assert(begin->pred->succ->B_to_C == begin);
    1360       66804 :         return begin->pred->succ->target->constln();
    1361             :     }
    1362             : 
    1363             :     /// \brief returns true iff the slice is marked for postprocessing
    1364             :     /// \details The function uses the data registered with the goal
    1365             :     /// constellation.
    1366         172 :     bool needs_postprocessing() const
    1367         172 :     {                                                                           assert(to_constln()->postprocess_end <= begin ||
    1368             :                                                                                                                          end <= to_constln()->postprocess_end);
    1369         172 :                                                                                 assert(to_constln()->postprocess_begin <= begin ||
    1370             :                                                                                                                        end <= to_constln()->postprocess_begin);
    1371         219 :         return to_constln()->postprocess_begin <= begin &&
    1372         219 :                                           end <= to_constln()->postprocess_end;
    1373             :     }
    1374             :                                                                                 #ifndef NDEBUG
    1375             :                                                                                     /// \brief print a B_to_C slice identification for debugging
    1376             :                                                                                     /// \details This function is only available if compiled in Debug mode.
    1377           0 :                                                                                     std::string debug_id() const
    1378             :                                                                                     {
    1379           0 :                                                                                         assert(begin < end);
    1380           0 :                                                                                         std::string result("slice containing transition");
    1381           0 :                                                                                         if (end - begin > 1)
    1382           0 :                                                                                             result += "s ";
    1383             :                                                                                         else
    1384           0 :                                                                                             result += " ";
    1385           0 :                                                                                         B_to_C_const_iter_t iter = begin;
    1386           0 :                                                                                         assert(iter->pred->succ->B_to_C == iter);
    1387           0 :                                                                                         result += iter->pred->debug_id_short();
    1388           0 :                                                                                         if (end - iter > 4)
    1389             :                                                                                         {
    1390           0 :                                                                                             assert(iter[1].pred->succ->B_to_C == iter+1);
    1391           0 :                                                                                             result += ", ";
    1392           0 :                                                                                             result += iter[1].pred->debug_id_short();
    1393           0 :                                                                                             result += ", ...";
    1394           0 :                                                                                             iter = end - 3;
    1395             :                                                                                         }
    1396           0 :                                                                                         while (++iter != end)
    1397             :                                                                                         {
    1398           0 :                                                                                             assert(iter->pred->succ->B_to_C == iter);
    1399           0 :                                                                                             result += ", ";
    1400           0 :                                                                                             result += iter->pred->debug_id_short();
    1401             :                                                                                         }
    1402           0 :                                                                                         return result;
    1403             :                                                                                     }
    1404             : 
    1405             :                                                                                     /// The function is meant to transfer work temporarily assigned to the
    1406             :                                                                                     /// B_to_C slice to the transitions in the slice.  It is used during
    1407             :                                                                                     /// handling of new bottom states, so the work is only assigned to
    1408             :                                                                                     /// transitions that start in a (new) bottom state.
    1409             :                                                                                     /// If at this moment no such (new) bottom state has been found, the work
    1410             :                                                                                     /// is kept with the slice and the function returns false.  The work should
    1411             :                                                                                     /// be transferred later (but if there is no later transfer, it should be
    1412             :                                                                                     /// tested that the function returns true).
    1413         132 :                                                                                     bool add_work_to_bottom_transns(enum check_complexity::counter_type ctr,
    1414             :                                                                                                                                             unsigned max_value)
    1415             :                                                                                     {
    1416         132 :                                                                                         bool added = false;
    1417             : 
    1418         602 :                                                                                         for (B_to_C_const_iter_t iter = begin; iter != end; ++iter)
    1419             :                                                                                         {
    1420         940 :                                                                                             if (iter->pred->source->pos >=
    1421         940 :                                                                                                                      iter->pred->source->block->bottom_begin())
    1422             :                                                                                             {
    1423             :                                                                                                 // source state of the transition is a bottom state
    1424         240 :                                                                                                 mCRL2complexity(iter->pred, add_work(ctr, max_value), );
    1425         240 :                                                                                                 added = true;
    1426             :                                                                                             }
    1427             :                                                                                         }
    1428         132 :                                                                                         return added;
    1429             :                                                                                     }
    1430             : 
    1431             :                                                                                     mutable check_complexity::B_to_C_counter_t work_counter;
    1432             :                                                                                 #endif
    1433             : };
    1434             : 
    1435             : 
    1436             : /* part_trans_t collects and organises all data for the transitions. */
    1437             : class part_trans_t
    1438             : {
    1439             :   private:
    1440             :     fixed_vector<pred_entry> pred;
    1441             :     fixed_vector<succ_entry> succ;
    1442             :     fixed_vector<B_to_C_entry> B_to_C;
    1443             : 
    1444             :     template <class LTS_TYPE>
    1445             :     friend class bisim_partitioner_gjkw_initialise_helper;
    1446             : 
    1447         142 :     void swap_in(B_to_C_iter_t const pos1, B_to_C_iter_t const pos2)
    1448         142 :     {                                                                           assert(B_to_C.end() > pos1);  assert(pos1->pred->succ->B_to_C == pos1);
    1449         142 :                                                                                 assert(B_to_C.end() > pos2);  assert(pos2->pred->succ->B_to_C == pos2);
    1450             :         // swap contents
    1451         142 :         pred_entry const temp_entry(*pos1->pred);
    1452         142 :         *pos1->pred = *pos2->pred;
    1453         142 :         *pos2->pred = temp_entry;
    1454             :         // swap pointers to contents
    1455         142 :         pred_iter_t const temp_iter(pos1->pred);
    1456         142 :         pos1->pred = pos2->pred;
    1457         142 :         pos2->pred = temp_iter;                                                 assert(B_to_C.end() > pos1);  assert(pos1->pred->succ->B_to_C == pos1);
    1458         142 :                                                                                 assert(B_to_C.end() > pos2);  assert(pos2->pred->succ->B_to_C == pos2);
    1459         142 :     }
    1460             : 
    1461        1188 :     void swap_out(pred_iter_t const pos1, pred_iter_t const pos2)
    1462        1188 :     {                                                                           assert(pred.end() > pos1);  assert(pos1->succ->B_to_C->pred == pos1);
    1463        1188 :                                                                                 assert(pred.end() > pos2);  assert(pos2->succ->B_to_C->pred == pos2);
    1464        1188 :                                                                                 assert(pos1->succ->slice_begin() == pos2->succ->slice_begin());
    1465        1188 :                                                                                 assert(succ_entry::slice_end(pos1->succ) == succ_entry::slice_end(pos2->succ));
    1466             :         // swap contents, but do not swap slice_begin_or_before_end
    1467        1188 :         B_to_C_iter_t const temp_B_to_C(pos1->succ->B_to_C);
    1468        1188 :         state_info_ptr const temp_target(pos1->succ->target);
    1469        1188 :         pos1->succ->B_to_C = pos2->succ->B_to_C;
    1470        1188 :         pos1->succ->target = pos2->succ->target;
    1471        1188 :         pos2->succ->B_to_C = temp_B_to_C;
    1472        1188 :         pos2->succ->target = temp_target;
    1473             :         // swap pointers to contents
    1474        1188 :         succ_iter_t const temp_iter(pos1->succ);
    1475        1188 :         pos1->succ = pos2->succ;
    1476        1188 :         pos2->succ = temp_iter;                                                 assert(pred.end() > pos1);  assert(pos1->succ->B_to_C->pred == pos1);
    1477        1188 :                                                                                 assert(pred.end() > pos2);  assert(pos2->succ->B_to_C->pred == pos2);
    1478        1188 :                                                                                 assert(pos1->succ->slice_begin() == pos2->succ->slice_begin());
    1479        1188 :                                                                                 assert(succ_entry::slice_end(pos1->succ) == succ_entry::slice_end(pos2->succ));
    1480        1188 :     }
    1481             : 
    1482        1807 :     void swap_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2)
    1483        1807 :     {                                                                           assert(succ.end() > pos1);  assert(pos1->B_to_C->pred->succ == pos1);
    1484        1807 :                                                                                 assert(succ.end() > pos2);  assert(pos2->B_to_C->pred->succ == pos2);
    1485             :         // swap contents
    1486        1807 :         B_to_C_entry const temp_entry(*pos1->B_to_C);
    1487        1807 :         *pos1->B_to_C = *pos2->B_to_C;
    1488        1807 :         *pos2->B_to_C = temp_entry;
    1489             :         // swap pointers to contents
    1490        1807 :         B_to_C_iter_t const temp_iter(pos1->B_to_C);
    1491        1807 :         pos1->B_to_C = pos2->B_to_C;
    1492        1807 :         pos2->B_to_C = temp_iter;                                               assert(succ.end() > pos1);  assert(pos1->B_to_C->pred->succ == pos1);
    1493        1807 :                                                                                 assert(succ.end() > pos2);  assert(pos2->B_to_C->pred->succ == pos2);
    1494        1807 :     }
    1495             : 
    1496             :     // *pos1 -> *pos2 -> *pos3 -> *pos1
    1497         419 :     void swap3_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2,
    1498             :                                                         succ_iter_t const pos3)
    1499         419 :     {                                                                           assert(succ.end() > pos1);  assert(pos1->B_to_C->pred->succ == pos1);
    1500         419 :                                                                                 assert(succ.end() > pos2);  assert(pos2->B_to_C->pred->succ == pos2);
    1501         419 :                                                                                 assert(succ.end() > pos3);  assert(pos3->B_to_C->pred->succ == pos3);
    1502         419 :                                                                                 assert(pos1 != pos2 || pos1 == pos3);
    1503             :         // swap contents
    1504         419 :         B_to_C_entry const temp_entry(*pos1->B_to_C);
    1505         419 :         *pos1->B_to_C = *pos3->B_to_C;
    1506         419 :         *pos3->B_to_C = *pos2->B_to_C;
    1507         419 :         *pos2->B_to_C = temp_entry;
    1508             :         // swap pointers to contents
    1509         419 :         B_to_C_iter_t const temp_iter(pos2->B_to_C);
    1510         419 :         pos2->B_to_C = pos3->B_to_C;
    1511         419 :         pos3->B_to_C = pos1->B_to_C;
    1512         419 :         pos1->B_to_C = temp_iter;                                               assert(succ.end() > pos1);  assert(pos1->B_to_C->pred->succ == pos1);
    1513         419 :                                                                                 assert(succ.end() > pos2);  assert(pos2->B_to_C->pred->succ == pos2);
    1514         419 :                                                                                 assert(succ.end() > pos3);  assert(pos3->B_to_C->pred->succ == pos3);
    1515         419 :     }
    1516             :   public:
    1517          55 :     part_trans_t(trans_type m)
    1518          55 :       : pred(m),
    1519             :         succ(m),
    1520          55 :         B_to_C(m)
    1521          55 :     {  }
    1522          55 :     ~part_trans_t()
    1523          55 :     {                                                                           assert(B_to_C.empty());  assert(succ.empty());  assert(pred.empty());
    1524          55 :     }
    1525             : 
    1526             :     /// clear allocated memory
    1527          55 :     void clear()
    1528             :     {
    1529             :         // B_to_C_descriptors are deallocated when their respective lists are
    1530             :         // deallocated by destructing the blocks.
    1531          55 :         B_to_C.clear();
    1532          55 :         succ.clear();
    1533          55 :         pred.clear();
    1534          55 :     }
    1535             : 
    1536          55 :     trans_type trans_size() const  {  return pred.size();  }
    1537             : 
    1538             :     /* split_inert_to_C splits the B_to_C slice of block b to its own
    1539             :     constellation into two slices: one for the inert and one for the non-inert
    1540             :     transitions.  It is called with SpB just after a constellation is split, as
    1541             :     the transitions from SpB to itself (= the inert transitions) now go to a
    1542             :     different constellation than the other transitions from SpB to its old
    1543             :     constellation.  It does, however, not adapt the other transition arrays to
    1544             :     reflect that noninert and inert transitions from block b would go to
    1545             :     different constellations.
    1546             :     Its time complexity is O(1+min {|out_noninert(b-->C)|, |out_inert(b)|}). */
    1547             :     void split_inert_to_C(block_t* B);
    1548             : 
    1549             :     /* part_trans_t::change_to_C has to be called after a transition target has
    1550             :     changed its constellation.  The member function will adapt the transition
    1551             :     data structure.  It assumes that the transition is non-inert and that the
    1552             :     new constellation does not (yet) have inert incoming transitions.  It
    1553             :     returns the boundary between transitions to OldC and transitions to NewC in
    1554             :     the state's outgoing transition array. */
    1555             :     succ_iter_t change_to_C(pred_iter_t pred_iter,                              ONLY_IF_DEBUG( constln_t* SpC, constln_t* NewC, )
    1556             :                bool first_transition_of_state, bool first_transition_of_block);
    1557             : 
    1558             :     /* split_s_inert_out splits the outgoing transitions from s to its own
    1559             :     constellation into two:  the inert transitions become transitions to the
    1560             :     new constellation of which s is now part;  the non-inert transitions remain
    1561             :     transitions to OldC.  It returns the boundary between transitions to
    1562             :     OldC and transitions to NewC in the outgoing transition array of s.
    1563             :     Its time complexity is O(1 + min { |out_\nottau(s)|, |out_\tau(s)| }). */
    1564             :     bool split_s_inert_out(state_info_ptr s                                     ONLY_IF_DEBUG(, constln_t* OldC)
    1565             :                                            );
    1566             : 
    1567             :     /* part_trans_t::make_noninert makes the transition identified by succ_iter
    1568             :     noninert. */
    1569         142 :     void make_noninert(succ_iter_t const succ_iter)
    1570             :     {
    1571             :         // change B_to_C
    1572             :         B_to_C_iter_t const other_B_to_C =
    1573         142 :                     succ_iter->B_to_C->pred->source->block->inert_begin();      assert(succ_iter->B_to_C->B_to_C_slice->begin <= other_B_to_C);
    1574         142 :                                                                                 assert(other_B_to_C <= succ_iter->B_to_C);
    1575         142 :                                                                                 assert(succ_iter->B_to_C < succ_iter->B_to_C->B_to_C_slice->end);
    1576         142 :         swap_B_to_C(succ_iter, other_B_to_C->pred->succ);
    1577         142 :         succ_iter->B_to_C->pred->source->block->set_inert_begin(other_B_to_C +
    1578             :                                                                             1);
    1579             :         // change pred
    1580         142 :         pred_iter_t const other_pred = succ_iter->target->inert_pred_begin();   assert(succ_iter->target->pred_begin() <= other_pred);
    1581         142 :                                                                                 assert(other_pred <= succ_iter->B_to_C->pred);
    1582         142 :                                                                                 assert(succ_iter->B_to_C->pred < succ_iter->target->pred_end());
    1583         142 :         swap_in(succ_iter->B_to_C, other_pred->succ->B_to_C);
    1584         142 :         succ_iter->target->set_inert_pred_begin(other_pred + 1);
    1585             :         // change succ
    1586             :         succ_iter_t const other_succ =
    1587         142 :                            succ_iter->B_to_C->pred->source->inert_succ_begin(); assert(succ_iter->B_to_C->pred->source->succ_begin() <= other_succ);
    1588         142 :                                                                                 assert(other_succ <= succ_iter);
    1589         142 :                                                                                 assert(succ_iter < succ_iter->B_to_C->pred->source->succ_end());
    1590         142 :         swap_out(succ_iter->B_to_C->pred, other_succ->B_to_C->pred);
    1591         142 :         succ_iter->B_to_C->pred->source->set_inert_succ_begin(other_succ + 1);
    1592         142 :     }
    1593             : 
    1594             :     /* part_trans_t::new_block_created splits the B_to_C-slices to reflect that
    1595             :     some transitions now start in the new block NewB.  They can no longer be in
    1596             :     the same slice as the transitions that start in the old block.
    1597             :     
    1598             :     We need separate functions for blue and red blocks because the B_to_C-slice
    1599             :     of the red block should come after the B_to_C-slice of the blue block,
    1600             :     at least while postprocessing.
    1601             : 
    1602             :     Its time complexity is O(1 + |out(NewB)|). */
    1603             :     void new_blue_block_created(block_t* OldB, block_t* NewB);
    1604             :     void new_red_block_created(block_t*OldB,block_t*NewB, bool postprocessing);
    1605             : 
    1606       17518 :     B_to_C_const_iter_t B_to_C_begin() const  {  return B_to_C.begin();  }
    1607         121 :     B_to_C_iter_t       B_to_C_end  ()        {  return B_to_C.end  ();  }
    1608        1133 :     pred_const_iter_t pred_end() const  {  return pred.end();  }
    1609         198 :     succ_const_iter_t succ_end() const  {  return succ.end();  }
    1610             :                                                                                 #ifndef NDEBUG
    1611             :                                                                                     /// \brief assert that the data structure is consistent and stable
    1612             :                                                                                     void assert_stability(const part_state_t& part_st) const;
    1613             :                                                                                 #endif
    1614             : };
    1615             : 
    1616             : ///@} (end of group part_trans)
    1617             : 
    1618             : 
    1619             : 
    1620             : 
    1621             : 
    1622             : 
    1623             : /* ************************************************************************* */
    1624             : /*                                                                           */
    1625             : /*                            A L G O R I T H M S                            */
    1626             : /*                                                                           */
    1627             : /* ************************************************************************* */
    1628             : 
    1629             : 
    1630             : 
    1631             : 
    1632             : 
    1633             : /// \defgroup part_refine
    1634             : /// \brief classes to calculate the stutter equivalence quotient of a LTS
    1635             : ///@{
    1636             : 
    1637             : 
    1638             : 
    1639             : /*=============================================================================
    1640             : =                create initial partition and data structures                 =
    1641             : =============================================================================*/
    1642             : 
    1643             : 
    1644             : 
    1645             : /// \class bisim_partitioner_gjkw_initialise_helper
    1646             : /// \brief helps with initialising the refinable partition data structure
    1647             : /// \details Before allocating memory for the refinable partition data
    1648             : /// structure, the number of states and transitions (including extra states
    1649             : /// generated by the translation from labelled transition system to Kripke
    1650             : /// structure) has to be known.  This class serves to calculate these numbers.
    1651             : ///
    1652             : /// The helper class also initialises the variables used by check_complexity to
    1653             : /// find the number of states and transitions in time complexity checks.
    1654             : template<class LTS_TYPE>
    1655          55 : class bisim_partitioner_gjkw_initialise_helper
    1656             : {
    1657             :   private:
    1658             :     LTS_TYPE& aut;
    1659             :     state_type nr_of_states;
    1660             :     const state_type orig_nr_of_states;
    1661             :     trans_type nr_of_transitions;
    1662             : 
    1663             :     // key and hash function for (action, target state) pair. Required since
    1664             :     // unordered_map does not directly allow to use pair keys
    1665             :     class Key 
    1666             :     {
    1667             :       public:
    1668             :         label_type first;
    1669             :         state_type second;
    1670             : 
    1671         920 :         Key(const label_type& f, const state_type& s)
    1672             :           : first(f),
    1673         920 :             second(s)
    1674         920 :         {} 
    1675             : 
    1676         616 :         bool operator==(const Key &other) const 
    1677             :         {
    1678         616 :             return first == other.first && second == other.second;
    1679             :         }
    1680             :     };
    1681             : 
    1682             :     class KeyHasher 
    1683             :     {
    1684             :       public:
    1685         920 :         std::size_t operator()(const Key& k) const
    1686             :         {
    1687        1840 :             return std::hash<label_type>()(k.first) ^
    1688        1840 :                                       (std::hash<state_type>()(k.second) << 1);
    1689             :         }
    1690             :     };
    1691             :     // Map used to convert LTS to Kripke structure
    1692             :     // (also used when converting Kripke structure back to LTS)
    1693             :     std::unordered_map<Key, state_type, KeyHasher> extra_kripke_states;
    1694             : 
    1695             :     // temporary map to keep track of blocks. maps transition labels (different
    1696             :     // from tau) to blocks
    1697             :     std::unordered_map<label_type, state_type> action_block_map;
    1698             : 
    1699             :     std::vector<state_type> noninert_out_per_state, inert_out_per_state;
    1700             :     std::vector<state_type> noninert_in_per_state, inert_in_per_state;
    1701             :     std::vector<state_type> noninert_out_per_block, inert_out_per_block;
    1702             :     std::vector<state_type> states_per_block;
    1703             :     state_type nr_of_nonbottom_states;
    1704             :   public:
    1705             :     bisim_partitioner_gjkw_initialise_helper(LTS_TYPE& l, bool branching,
    1706             :                                                      bool preserve_divergence);
    1707             : 
    1708             :     /// initialise the state in part_st and the transitions in part_tr
    1709             :     void init_transitions(part_state_t& part_st, part_trans_t& part_tr,
    1710             :                                      bool branching, bool preserve_divergence);
    1711             : 
    1712             :     // replace_transition_system() replaces the transitions of the LTS stored here by
    1713             :     // those of its bisimulation quotient.  However, it does not change
    1714             :     // anything else; in particular, it does not change the number of states of
    1715             :     // the LTS.
    1716             :     void replace_transition_system(const part_state_t& part_st,                 ONLY_IF_DEBUG( bool branching, )
    1717             :                                    bool preserve_divergence);
    1718             : 
    1719             :     /// provides the number of states in the Kripke structure
    1720        1147 :     state_type get_nr_of_states() const  {  return nr_of_states;  }
    1721             : 
    1722             :     /// provides the number of transitions in the Kripke structure
    1723         110 :     trans_type get_nr_of_transitions() const  {  return nr_of_transitions;  }
    1724             : };
    1725             : 
    1726             : 
    1727             : 
    1728             : /*=============================================================================
    1729             : =                                 main class                                  =
    1730             : =============================================================================*/
    1731             : 
    1732             : 
    1733             : 
    1734             : struct refine_shared_t;
    1735             : 
    1736             : } // end namespace bisim_gjkw
    1737             : 
    1738             : /// \class bisim_partitioner_gjkw
    1739             : /// \brief implements the main algorithm for the stutter equivalence quotient
    1740             : template <class LTS_TYPE>
    1741             : class bisim_partitioner_gjkw
    1742             : {
    1743             :   private:
    1744             :     bisim_gjkw::bisim_partitioner_gjkw_initialise_helper<LTS_TYPE> init_helper;
    1745             :     bisim_gjkw::part_state_t part_st;
    1746             :     bisim_gjkw::part_trans_t part_tr;
    1747             :   public:
    1748             :     // The constructor constructs the data structures and immediately
    1749             :     // calculates the bisimulation quotient.  However, it does not change the
    1750             :     // LTS.
    1751          55 :     bisim_partitioner_gjkw(LTS_TYPE& l, bool branching = false,
    1752             :                                         bool preserve_divergence = false)
    1753             :       : init_helper(l, branching, preserve_divergence),
    1754             :         part_st(init_helper.get_nr_of_states()),
    1755          55 :         part_tr(init_helper.get_nr_of_transitions())
    1756          55 :     {                                                                           assert(branching || !preserve_divergence);
    1757          55 :         create_initial_partition_gjkw(branching, preserve_divergence);
    1758          55 :         refine_partition_until_it_becomes_stable_gjkw();
    1759          55 :     }
    1760          55 :     ~bisim_partitioner_gjkw()
    1761             :     {
    1762          55 :         part_tr.clear();
    1763          55 :         part_st.clear();
    1764          55 :     }
    1765             : 
    1766             :     // replace_transition_system() replaces the transitions of the LTS stored here by
    1767             :     // those of its bisimulation quotient.  However, it does not change
    1768             :     // anything else; in particular, it does not change the number of states of
    1769             :     // the LTS.
    1770          53 :     void replace_transition_system(bool branching, bool preserve_divergence)
    1771             :     {
    1772             :         (void) branching; // avoid warning about unused parameter.
    1773          53 :         init_helper.replace_transition_system(part_st,                          ONLY_IF_DEBUG( branching, )
    1774             :                                                        preserve_divergence);
    1775          53 :     }
    1776             : 
    1777           0 :     static state_type num_eq_classes()
    1778             :     {
    1779           0 :         return bisim_gjkw::block_t::nr_of_blocks;
    1780             :     }
    1781             : 
    1782           0 :     state_type get_eq_class(state_type s) const
    1783             :     {
    1784           0 :         return part_st.block(s)->seqnr();
    1785             :     }
    1786             : 
    1787           2 :     bool in_same_class(state_type s, state_type t) const
    1788             :     {
    1789           2 :         return part_st.block(s) == part_st.block(t);
    1790             :     }
    1791             : 
    1792             :   private:
    1793             : 
    1794             :     /*-------- dbStutteringEquivalence -- Algorithm 2 of [GJKW 2017] --------*/
    1795             : 
    1796             :     void create_initial_partition_gjkw(bool branching,
    1797             :                                                      bool preserve_divergence);
    1798             :     void refine_partition_until_it_becomes_stable_gjkw();
    1799             : 
    1800             :     /*----------------- Refine -- Algorithm 3 of [GJKW 2017] ----------------*/
    1801             : 
    1802             :     bisim_gjkw::block_t* refine(bisim_gjkw::block_t* RfnB,
    1803             :               const bisim_gjkw::constln_t* SpC,
    1804             :               const bisim_gjkw::B_to_C_descriptor* FromRed,
    1805             :               bool postprocessing                                               ONLY_IF_DEBUG( , const bisim_gjkw::constln_t* NewC = nullptr )
    1806             :                                  );
    1807             : 
    1808             :     /*--------- PostprocessNewBottom -- Algorithm 4 of [GJKW 2017] ----------*/
    1809             : 
    1810             :     bisim_gjkw::block_t* postprocess_new_bottom(bisim_gjkw::block_t* RedB);
    1811             : };
    1812             : 
    1813             : ///@} (end of group part_refine)
    1814             : 
    1815             : 
    1816             : 
    1817             : 
    1818             : 
    1819             : /* ************************************************************************* */
    1820             : /*                                                                           */
    1821             : /*                             I N T E R F A C E                             */
    1822             : /*                                                                           */
    1823             : /* ************************************************************************* */
    1824             : 
    1825             : 
    1826             : 
    1827             : 
    1828             : 
    1829             : /// \defgroup part_interface
    1830             : /// \brief nonmember functions serving as interface with the rest of mCRL2
    1831             : /// \details These functions are copied, almost without changes, from
    1832             : /// liblts_bisim_gw.h, which was written by Anton Wijs.
    1833             : ///@{
    1834             : 
    1835             : /** \brief Reduce transition system l with respect to strong or (divergence
    1836             :  *  preserving) branching bisimulation.
    1837             :  * \param[in,out] l                   The transition system that is reduced.
    1838             :  * \param         branching           If true branching bisimulation is
    1839             :  *                                    applied, otherwise strong bisimulation.
    1840             :  * \param         preserve_divergence Indicates whether loops of internal
    1841             :  *                                    actions on states must be preserved. If
    1842             :  *                                    false these are removed. If true these
    1843             :  *                                    are preserved. */
    1844             : template <class LTS_TYPE>
    1845             : void bisimulation_reduce_gjkw(LTS_TYPE& l, bool branching = false,
    1846             :                                             bool preserve_divergence = false);
    1847             : 
    1848             : /** \brief Checks whether the two initial states of two LTSs are strong or
    1849             :  * branching bisimilar.
    1850             :  * \details The LTSs l1 and l2 are not usable anymore after this call.
    1851             :  * The space consumption is O(n) and time is O(m log n). It uses the branching
    1852             :  * bisimulation algorithm by Groote/Jansen/Keiren/Wijs.
    1853             :  * \param[in,out] l1                  A first transition system.
    1854             :  * \param[in,out] l2                  A second transistion system.
    1855             :  * \param         branching           If true branching bisimulation is used,
    1856             :  *                                    otherwise strong bisimulation is applied.
    1857             :  * \param         preserve_divergence If true and branching is true, preserve
    1858             :  *                                    tau loops on states.
    1859             :  * \retval True iff the initial states of the current transition system and l2
    1860             :  * are (divergence preserving) (branching) bisimilar. */
    1861             : template <class LTS_TYPE>
    1862             : bool destructive_bisimulation_compare_gjkw(LTS_TYPE& l1, LTS_TYPE& l2,
    1863             :                     bool branching = false, bool preserve_divergence = false,
    1864             :                                     bool generate_counter_examples = false);
    1865             : 
    1866             : /** \brief Checks whether the two initial states of two LTSs are strong or
    1867             :  * branching bisimilar.
    1868             :  * \details The LTSs l1 and l2 are first duplicated and subsequently reduced
    1869             :  * modulo bisimulation. If memory space is a concern, one could consider to use
    1870             :  * destructive_bisimulation_compare. This routine uses the O(m log n) branching
    1871             :  * bisimulation routine. It runs in O(m log n) time and uses O(n) memory, where
    1872             :  * n is the number of states and m is the number of transitions.
    1873             :  * \param[in,out] l1                  A first transition system.
    1874             :  * \param[in,out] l2                  A second transistion system.
    1875             :  * \param         branching           If true branching bisimulation is used,
    1876             :  *                                    otherwise strong bisimulation is applied.
    1877             :  * \param         preserve_divergence If true and branching is true, preserve
    1878             :  *                                    tau loops on states.
    1879             :  * \retval True iff the initial states of the current transition system and l2
    1880             :  * are (divergence preserving) (branching) bisimilar. */
    1881             : template <class LTS_TYPE>
    1882             : bool bisimulation_compare_gjkw(const LTS_TYPE& l1, const LTS_TYPE& l2,
    1883             :                     bool branching = false, bool preserve_divergence = false);
    1884             : 
    1885             : /// calculates the bisimulation quotient of a LTS.
    1886             : template <class LTS_TYPE>
    1887          53 : void bisimulation_reduce_gjkw(LTS_TYPE& l, bool const branching /* = false */,
    1888             :                                   bool const preserve_divergence /* = false */)
    1889             : {
    1890             :   // First, remove tau loops in case of branching bisimulation.
    1891          53 :   if (branching)
    1892             :   {
    1893          34 :     scc_reduce(l, preserve_divergence);
    1894             :   }
    1895             : 
    1896             :   // Second, apply the branching bisimulation reduction algorithm. If there are
    1897             :   // no taus, this will automatically yield strong bisimulation.
    1898         106 :   detail::bisim_partitioner_gjkw<LTS_TYPE> bisim_part(l, branching,
    1899             :                                                           preserve_divergence);
    1900             : 
    1901             :   // Assign the reduced LTS
    1902          53 :   bisim_part.replace_transition_system(branching, preserve_divergence);
    1903          53 : }
    1904             : 
    1905             : template <class LTS_TYPE>
    1906             : inline bool bisimulation_compare_gjkw(const LTS_TYPE& l1, const LTS_TYPE& l2,
    1907             :           bool branching /* = false */, bool preserve_divergence /* = false */)
    1908             : {
    1909             :   LTS_TYPE l1_copy(l1);
    1910             :   LTS_TYPE l2_copy(l2);
    1911             :   return destructive_bisimulation_compare_gjkw(l1_copy, l2_copy, branching,
    1912             :                                                           preserve_divergence);
    1913             : }
    1914             : 
    1915             : template <class LTS_TYPE>
    1916           2 : bool destructive_bisimulation_compare_gjkw(LTS_TYPE& l1, LTS_TYPE& l2,
    1917             :           bool branching /* = false */, bool preserve_divergence /* = false */,
    1918             :                                            bool generate_counter_examples /* = false */,
    1919             :                                            bool /*structured_output = false */)
    1920             : {
    1921           2 :   if (generate_counter_examples)
    1922             :   {
    1923           0 :     mCRL2log(log::warning) << "The GJKW branching bisimulation algorithm does "
    1924             :                                             "not generate counterexamples.\n";
    1925             :   }
    1926           2 :   state_type init_l2 = l2.initial_state() + l1.num_states();
    1927           2 :   mcrl2::lts::detail::merge(l1, l2);
    1928           2 :   l2.clear(); // No use for l2 anymore.
    1929             : 
    1930             :   // First remove tau loops in case of branching bisimulation.
    1931           2 :   if (branching)
    1932             :   {
    1933           0 :     detail::scc_partitioner<LTS_TYPE> scc_part(l1);
    1934           0 :     scc_part.replace_transition_system(preserve_divergence);
    1935           0 :     init_l2 = scc_part.get_eq_class(init_l2);
    1936             :   }
    1937             : 
    1938           4 :   detail::bisim_partitioner_gjkw<LTS_TYPE> bisim_part(l1, branching,
    1939             :                                                           preserve_divergence);
    1940           4 :   return bisim_part.in_same_class(l1.initial_state(), init_l2);
    1941             : }
    1942             : 
    1943             : ///@} (end of group part_interface)
    1944             : 
    1945             : 
    1946             : 
    1947             : 
    1948             : 
    1949             : /* ************************************************************************* */
    1950             : /*                                                                           */
    1951             : /*                       I M P L E M E N T A T I O N S                       */
    1952             : /*                                                                           */
    1953             : /* ************************************************************************* */
    1954             : 
    1955             : 
    1956             : 
    1957             : 
    1958             : 
    1959             : // This section contains implementations of functions that refer to details of
    1960             : // classes defined later, so they could not be defined at the point of
    1961             : // declaration.
    1962             : 
    1963             : namespace bisim_gjkw
    1964             : {
    1965             : 
    1966             : /// get the constellation of the state
    1967        1172 : inline const constln_t* state_info_entry::constln() const
    1968             : {
    1969        1172 :     return block->constln();
    1970             : }
    1971             : 
    1972      246968 : inline constln_t* state_info_entry::constln()
    1973             : {
    1974      246968 :     return block->constln();
    1975             : }
    1976             : 
    1977             : /// read FromRed
    1978         294 : inline B_to_C_descriptor* block_t::FromRed(const constln_t* const SpC)
    1979             : {
    1980         294 :     if (!to_constln.empty() && to_constln.front().to_constln() == SpC)
    1981             :     {
    1982         166 :         return &*to_constln.begin();
    1983             :     }
    1984             :     else
    1985             :     {
    1986             :                                                                                 #ifndef NDEBUG
    1987         290 :                                                                                     for (B_to_C_desc_const_iter_t iter = to_constln.begin();
    1988         290 :                                                                                                                               to_constln.end() != iter; ++iter)
    1989             :                                                                                     {
    1990         162 :                                                                                         assert(iter->from_block() == this);
    1991         162 :                                                                                         assert(iter->to_constln() != SpC);
    1992             :                                                                                     }
    1993             :                                                                                 #endif
    1994         128 :         return nullptr;
    1995             :     }
    1996             : }
    1997             : 
    1998             : 
    1999             : /// set FromRed to an existing element in to_constln
    2000         790 : inline void block_t::SetFromRed(B_to_C_desc_iter_t const new_fromred)
    2001         790 : {                                                                               assert(!to_constln.empty());
    2002         790 :     if (to_constln.begin() != new_fromred)
    2003             :     {
    2004          76 :         to_constln.splice(to_constln.begin(), to_constln, new_fromred);
    2005         790 :     }                                                                           assert(new_fromred->from_block() == this);
    2006         790 : }
    2007             : 
    2008             : 
    2009             : /// \brief quick check to find out whether the state has a transition to `SpC`
    2010             : /// \details If the current constellation pointer happens to be set to `SpC`,
    2011             : /// the function can quickly find out whether the state has a transition to
    2012             : /// `SpC`.
    2013             : /// The function should not be called for the constellation in which the state
    2014             : /// resides.
    2015             : /// \param SpC constellation of interest
    2016             : /// \returns true if the state is known to have a transition to `SpC`
    2017             : /// \memberof state_info_entry
    2018          67 : inline bool state_info_entry::surely_has_transition_to(const constln_t* const
    2019             :                                                                      SpC) const
    2020          67 : {                                                                               assert(succ_begin()<=current_constln()); assert(current_constln()<=succ_end());
    2021          67 :                                                                                 assert(succ_begin() == current_constln() || succ_end() == current_constln() ||
    2022             :                                                                                         *current_constln()[-1].target->constln() <
    2023             :                                                                                                                         *current_constln()->target->constln());
    2024          67 :                                                                                 assert(constln() != SpC);
    2025             :     // either current_constln()->target or current_constln()[-1].target is in
    2026             :     // SpC
    2027         191 :     if (current_constln() != succ_end() &&
    2028         124 :                                    current_constln()->target->constln() == SpC)
    2029             :     {
    2030          51 :         return true;
    2031             :     }
    2032          16 :     return false;
    2033             : }
    2034             : 
    2035             : 
    2036             : /// \brief quick check to find out whether the state has _no_ transition to
    2037             : /// `SpC`
    2038             : /// \details If the current constellation pointer happens to be set to `SpC` or
    2039             : /// its successor, the function can quickly find out whether the state has a
    2040             : /// transition to `SpC`.
    2041             : /// The function should not be called for the constellation in which the state
    2042             : /// resides.
    2043             : /// \param SpC constellation of interest
    2044             : /// \returns true if the state is known to have _no_ transition to `SpC`
    2045             : /// \memberof state_info_entry
    2046          16 : inline bool state_info_entry::surely_has_no_transition_to(
    2047             :                                               const constln_t* const SpC) const
    2048          16 : {                                                                               assert(succ_begin()<=current_constln()); assert(current_constln()<=succ_end());
    2049          16 :                                                                                 assert(succ_begin() == current_constln() || succ_end() == current_constln() ||
    2050             :                                                                                         *current_constln()[-1].target->constln() <
    2051             :                                                                                                                         *current_constln()->target->constln());
    2052          16 :                                                                                 assert(constln() != SpC);
    2053             :     // condition:
    2054             :     // current_constln()->target is in a constellation > SpC and
    2055             :     // current_constln()[-1].target is in a constellation < SpC.
    2056          38 :     if (current_constln() != succ_end() &&
    2057          22 :                                  *current_constln()->target->constln() <= *SpC)
    2058             :     {
    2059           0 :         return false;
    2060             :     }
    2061          45 :     if (current_constln() != succ_begin() &&
    2062          29 :                               *SpC <= *current_constln()[-1].target->constln())
    2063             :     {
    2064           1 :         return false;
    2065             :     }
    2066          15 :     return true;
    2067             : }
    2068             : 
    2069             : 
    2070             : } // end namespace bisim_gjkw
    2071             : } // end namespace detail
    2072             : } // end namespace lts
    2073             : } // end namespace mcrl2
    2074             : 
    2075             : #endif // ifndef _LIBLTS_BISIM_GJKW_H

Generated by: LCOV version 1.13