LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_bisim.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 438 496 88.3 %
Date: 2020-07-11 00:44:39 Functions: 26 26 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg, Jan Friso Groote
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file lts/detail/liblts_bisim.h
      10             : 
      11             : #ifndef _LIBLTS_BISIM_H
      12             : #define _LIBLTS_BISIM_H
      13             : #include "mcrl2/trace/trace.h"
      14             : #include "mcrl2/lts/lts_utilities.h"
      15             : #include "mcrl2/lts/detail/liblts_scc.h"
      16             : #include "mcrl2/lts/detail/liblts_merge.h"
      17             : #include "mcrl2/lts/lts_aut.h"
      18             : #include "mcrl2/lts/lts_fsm.h"
      19             : #include "mcrl2/lts/lts_dot.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : namespace lts
      24             : {
      25             : namespace detail
      26             : {
      27             : 
      28             : template < class LTS_TYPE>
      29             : class bisim_partitioner
      30             : {
      31             : 
      32             :   public:
      33             :     /** \brief Creates a bisimulation partitioner for an LTS.
      34             :      *  \details This bisimulation partitioner applies the algorithm
      35             :      *  defined in J.F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering
      36             :      *  equivalence. In M.S. Paterson, editor, Proceedings 17th ICALP, Warwick, volume 443 of Lecture Notes in Computer
      37             :      *  Science, pages 626-638. Springer-Verlag, 1990. The only difference is that this algorithm uses actions labels
      38             :      *  on transitions. Therefore, each list of non_inert_transitions is grouped such that all transitions with the
      39             :      *  same label are grouped together. Tau transitions (which have as label index the number of labels) occur at the
      40             :      *  beginning of this list.
      41             :      *
      42             :      *  If branching is true, then branching bisimulation is used, otherwise strong bisimulation is applied.
      43             :      *  If preserve_divergence is true, then branching must be true. In this case states with an internal tau loop
      44             :      *  are considered to be different from states without a tau loop. In this way the divergences are preserved.
      45             :      *
      46             :      *  The input transition system is not allowed to contain tau loops, except that if preserve_divergence is true
      47             :      *  tau loops on a single state are allowed as they indicate divergences. Using the scc partitioner the tau
      48             :      *  loops must first be removed before applying this algorithm.
      49             :      *  \warning Note that when compiled with optimisations, bisimulation partitioning
      50             :      *  is much faster than compiled without any optimisation. The difference can go up to a factor 10.
      51             :      *  \param[in] l Reference to the LTS. The LTS l is only changed if \ref replace_transition_system is called. */
      52         215 :     bisim_partitioner(
      53             :       LTS_TYPE& l,
      54             :       const bool branching=false,
      55             :       const bool preserve_divergence=false)
      56             :        : max_state_index(0), 
      57         215 :          aut(l) 
      58             :     {
      59         215 :       assert(branching || !preserve_divergence);
      60         215 :       mCRL2log(log::verbose) << (preserve_divergence?"Divergence preserving b":"B") <<
      61           0 :                   (branching?"ranching b":"") << "isimulation partitioner created for "
      62           0 :                   << l.num_states() << " states and " <<
      63             :                   l.num_transitions() << " transitions\n";
      64         215 :       create_initial_partition(branching,preserve_divergence);
      65         215 :       refine_partition_until_it_becomes_stable(branching, preserve_divergence);
      66         215 :     }
      67             : 
      68             : 
      69             :     /** \brief Destroys this partitioner. */
      70         215 :     ~bisim_partitioner()=default;
      71             : 
      72             :     /** \brief Replaces the transition relation of the current lts by the transitions
      73             :      *         of the bisimulation reduced transition system.
      74             :      * \details Each transition (s,l,s') is replaced by a transition (t,l,t') where
      75             :      * t and t' are the equivalence classes to which classes of the LTS. If the label l is
      76             :      * internal, which is detected using the function is_tau, then it is only returned
      77             :      * if t!=t' or preserve_divergence=true. This effectively removes all inert transitions.
      78             :      * Duplicates are removed from the transitions in the new lts.
      79             :      * Also the number of states and the initial state are adapted by this method.
      80             :      *
      81             :      * \pre The bisimulation equivalence classes have been computed.
      82             :      * \param[in] branching Causes non internal transitions to be removed.
      83             :      * \param[in] preserve_divergences Preserves tau loops on states. */
      84         197 :     void replace_transition_system(const bool branching, const bool preserve_divergences)
      85             :     {
      86             :       // Put all the non inert transitions in a set. Add the transitions that form a self
      87             :       // loop. Such transitions only exist in case divergence preserving branching bisimulation is
      88             :       // used. A set is used to remove double occurrences of transitions.
      89         394 :       std::set < transition > resulting_transitions;
      90             : 
      91        1849 :       for (const transition& i: aut.get_transitions()) 
      92             :       {
      93        1652 :         const bool is_transition_i_hidden=aut.is_tau(aut.apply_hidden_label_map(i.label()));
      94        4005 :         if (!branching ||
      95        1066 :             !is_transition_i_hidden ||
      96        3685 :             get_eq_class(i.from())!=get_eq_class(i.to()) ||
      97          93 :             (preserve_divergences && i.from()==i.to()))
      98             :         {
      99        1990 :           resulting_transitions.insert(
     100             :             transition(
     101             :               get_eq_class(i.from()),
     102             : // In the line below all hidden transitions are replaced by an explicit tau. It is possible to 
     103             : // always use i.label() where the resulting transition is only implicitly hidden. This has as effect that
     104             : // the labels of non inert hidden transitions are preserved (e.g. for use in counter examples) but that
     105             : // there are possibly multiple hidden transitions between states, leading to a larger number of 
     106             : // transitions than strictly necessary. 
     107         510 :               (is_transition_i_hidden?aut.tau_label_index():i.label()),
     108             :               get_eq_class(i.to())));
     109             :         }
     110             :       }
     111             :       // Remove the old transitions
     112         197 :       aut.clear_transitions();
     113             : 
     114             :       // Copy the transitions from the set into the transition system.
     115        1397 :       for (const transition& t: resulting_transitions)
     116             :       {
     117        1200 :         aut.add_transition(t);
     118             :       }
     119             :      
     120             :       // Merge the states, by setting the state labels of each state to the concatenation of the state labels of its
     121             :       // equivalence class. 
     122         197 :       if (aut.has_state_info())   /* If there are no state labels this step can be ignored */
     123             :       {
     124             :         /* Create a vector for the new labels */
     125           0 :         std::vector<typename LTS_TYPE::state_label_t> new_labels(num_eq_classes());
     126             : 
     127           0 :         for(std::size_t i=aut.num_states(); i>0; )
     128             :         {
     129           0 :           --i;
     130           0 :           const std::size_t new_index=get_eq_class(i);
     131           0 :           new_labels[new_index] = new_labels[new_index] + aut.state_label(i);
     132             :         }
     133             : 
     134           0 :         aut.set_num_states(num_eq_classes());
     135           0 :         for(std::size_t i=0; i<num_eq_classes(); ++i)
     136             :         {
     137           0 :           aut.set_state_label(i,new_labels[i]);
     138             :         }
     139             :       }
     140             :       else
     141             :       {
     142         197 :         aut.set_num_states(num_eq_classes());
     143             :       }
     144             :       
     145         197 :       aut.set_initial_state(get_eq_class(aut.initial_state()));
     146         197 :     }
     147             : 
     148             :     /** \brief Gives the number of bisimulation equivalence classes of the LTS.
     149             :      *  \return The number of bisimulation equivalence classes of the LTS.
     150             :      */
     151         197 :     std::size_t num_eq_classes() const
     152             :     {
     153         197 :       return max_state_index;
     154             :     }
     155             : 
     156             : 
     157             :     /** \brief Gives the bisimulation equivalence class number of a state.
     158             :      *  \param[in] s A state number.
     159             :      *  \return The number of the bisimulation equivalence class to which \e s belongs. */
     160        3927 :     std::size_t get_eq_class(const std::size_t s) const
     161             :     {
     162        3927 :       assert(s<block_index_of_a_state.size());
     163        3927 :       return blocks[block_index_of_a_state[s]].state_index;
     164             :     }
     165             : 
     166             : 
     167             :     /** \brief Returns whether two states are in the same bisimulation equivalence class.
     168             :      *  \param[in] s A state number.
     169             :      *  \param[in] t A state number.
     170             :      *  \retval true if \e s and \e t are in the same bisimulation equivalence class;
     171             :      *  \retval false otherwise. */
     172          19 :     bool in_same_class(const std::size_t s, const std::size_t t) const
     173             :     {
     174          19 :       return get_eq_class(s)==get_eq_class(t);
     175             :     }
     176             : 
     177             : 
     178             :     /** \brief Returns a vector of counter traces.
     179             :      *  \details The states s and t are non bisimilar states. If they are
     180             :      *           bisimilar an exception is raised. A counter trace of the form sigma a is
     181             :      *           returned, which has the property that s-sigma->s'-a-> and t-sigma->t'-/a->,
     182             :      *           or vice versa, s-sigma->s'-/a-> and t-sigma->t'-a->. A vector of such
     183             :      *           counter traces is returned.
     184             :      *  \param[in] s A state number.
     185             :      *  \param[in] t A state number.
     186             :      *  \param[in] branching_bisimulation A boolean indicating whether the branching bisimulation partitioner has been used.
     187             :      *  \return A vector containing counter traces. */
     188             :     std::set < mcrl2::trace::Trace > counter_traces(const std::size_t s, const std::size_t t, const bool branching_bisimulation);
     189             : 
     190             :   private:
     191             : 
     192             :     typedef std::size_t block_index_type;
     193             :     typedef std::size_t state_type;
     194             :     typedef std::size_t label_type;
     195             : 
     196             :     state_type max_state_index;
     197             :     LTS_TYPE& aut;
     198             : 
     199        6189 :     struct non_bottom_state
     200             :     {
     201             :       state_type state;
     202             :       std::vector < state_type > inert_transitions; // Only the target state is interesting.
     203             : 
     204         969 :       non_bottom_state(const state_type s)
     205         969 :         : state(s)
     206         969 :       {}
     207         244 :       non_bottom_state(const state_type s, const std::vector < state_type > &it)
     208         244 :         : state(s), inert_transitions(it)
     209         244 :       {}
     210             :     };
     211             : 
     212       11778 :     struct block
     213             :     {
     214             :       state_type state_index;                   // The state number that represent the states in this block
     215             :       block_index_type block_index;             // The sequence number of this block.
     216             :       block_index_type parent_block_index;      // Index of the parent block.
     217             :       // If there is no parent block, this refers to the block
     218             :       // itself.
     219             :       std::pair < label_type, block_index_type > splitter;
     220             :       // The action and block that caused this block to split.
     221             :       // This information is only defined if the block has been split.
     222             :       std::vector < state_type > bottom_states; // The non bottom states must be ordered
     223             :       // on tau reachability. The deepest
     224             :       // states occur first in the vector.
     225             :       std::vector < non_bottom_state > non_bottom_states;
     226             :       // The non_inert transitions are grouped per label. The (non-inert) transitions
     227             :       // with tau labels are at the end of this vector.
     228             :       std::vector < transition > non_inert_transitions;
     229             : 
     230         215 :       void swap(block& b)
     231             :       {
     232         215 :         state_type state_index1=b.state_index;
     233         215 :         b.state_index=state_index;
     234         215 :         state_index=state_index1;
     235             : 
     236         215 :         block_index_type block_index1=b.block_index;
     237         215 :         b.block_index=block_index;
     238         215 :         block_index=block_index1;
     239             : 
     240         215 :         block_index_type parent_block_index1=b.parent_block_index;
     241         215 :         b.parent_block_index=parent_block_index;
     242         215 :         parent_block_index=parent_block_index1;
     243             : 
     244         215 :         std::pair < label_type, block_index_type > splitter1=b.splitter;
     245         215 :         b.splitter=splitter;
     246         215 :         splitter=splitter1;
     247         215 :         bottom_states.swap(b.bottom_states);
     248         215 :         non_bottom_states.swap(b.non_bottom_states);
     249         215 :         non_inert_transitions.swap(b.non_inert_transitions);
     250         215 :       }
     251             :     };
     252             : 
     253             :     std::vector < block > blocks;
     254             : 
     255             :     // std::vector < bool > block_is_active;       // Indicates whether this is still a block in the partition.
     256             :     // Blocks that are split become inactive.
     257             :     std::vector < state_type > block_index_of_a_state;
     258             :     std::vector < bool > block_flags;
     259             :     std::vector < bool > block_is_in_to_be_processed;
     260             :     std::vector < bool > state_flags;
     261             : 
     262             :     std::vector< block_index_type > to_be_processed;
     263             :     std::vector< block_index_type > BL;
     264             : 
     265         215 :     void create_initial_partition(const bool branching,
     266             :                                   const bool preserve_divergences)
     267             : 
     268             :     {
     269         215 :       to_be_processed.clear();
     270             : 
     271         430 :       block initial_partition;
     272             : 
     273             :       // First store the bottom and non bottom states.
     274         215 :       sort_transitions(aut.get_transitions(), aut.hidden_label_map(), mcrl2::lts::src_lbl_tgt);
     275             : 
     276         215 :       state_type last_non_stored_state_number=0;
     277         215 :       bool bottom_state=true;
     278         430 :       std::vector < state_type > current_inert_transitions;
     279             : 
     280             :       {
     281             :         // Reserve enough space, such that no reallocations of the vector are required when adding transitions.
     282             :         // For this purpose, first the number of inert transitions must be counted, to avoid reserving too much
     283             :         // space. This for instance leads to a waste of memory (terabytes for reducing 30M states), especially,
     284             :         // when calculating ia strong bisimulation reduction.
     285         215 :         std::size_t initial_partition_non_inert_counter=0;
     286         215 :         std::size_t current_inert_transition_counter=0;
     287         215 :         const std::vector<transition> & trans=aut.get_transitions();
     288        1975 :         for (std::vector<transition>::const_iterator r=trans.begin(); r!=trans.end(); ++r)
     289             :         {
     290        1760 :           const transition t= *r;
     291        1760 :           if (branching && aut.is_tau(aut.apply_hidden_label_map(t.label())))
     292             :           {
     293         365 :             if (preserve_divergences && t.from()==t.to())
     294             :             {
     295          16 :               initial_partition_non_inert_counter++;
     296             :             }
     297             :             else
     298             :             {
     299         349 :               current_inert_transition_counter++;
     300             :             }
     301             :           }
     302             :         }
     303         215 :         current_inert_transitions.reserve(initial_partition_non_inert_counter);
     304         215 :         initial_partition.non_inert_transitions.reserve(current_inert_transition_counter);
     305             :       }
     306             : 
     307         215 :       const std::vector<transition>& trans=aut.get_transitions();
     308        1975 :       for (std::vector<transition>::const_iterator r=trans.begin(); r!=trans.end(); ++r)
     309             :       {
     310        1760 :         const transition t=* r;
     311             : 
     312        1760 :         if (branching && aut.is_tau(aut.apply_hidden_label_map(t.label())))
     313             :         {
     314         365 :           if (preserve_divergences && t.from()==t.to())
     315             :           {
     316          16 :             initial_partition.non_inert_transitions.push_back(transition(t.from(),aut.tau_label_index(),t.to()));
     317             :           }
     318             :           else
     319             :           {
     320         349 :             current_inert_transitions.push_back(t.to());
     321         349 :             bottom_state=false;
     322             :           }
     323             :         }
     324        1760 :         std::vector<transition>::const_iterator next_i=r;
     325        1760 :         ++next_i;
     326        1760 :         if (next_i==trans.end() || t.from()!=next_i->from())
     327             :         {
     328             :           // store the current from state
     329        1425 :           for (; last_non_stored_state_number<t.from(); ++last_non_stored_state_number)
     330             :           {
     331         139 :             initial_partition.bottom_states.push_back(last_non_stored_state_number);
     332             :           }
     333             : 
     334        1147 :           if (bottom_state)
     335             :           {
     336         889 :             initial_partition.bottom_states.push_back(t.from());
     337             :           }
     338             :           else
     339             :           {
     340         258 :             initial_partition.non_bottom_states.push_back(non_bottom_state(t.from()));
     341         258 :             current_inert_transitions.swap(initial_partition.non_bottom_states.back().inert_transitions);
     342         258 :             bottom_state=true;
     343             :           }
     344        1147 :           assert(last_non_stored_state_number==t.from());
     345        1147 :           last_non_stored_state_number++;
     346             :         }
     347             :       }
     348             : 
     349         495 :       for (; last_non_stored_state_number<aut.num_states(); ++last_non_stored_state_number)
     350             :       {
     351         140 :         initial_partition.bottom_states.push_back(last_non_stored_state_number);
     352             :       }
     353             : 
     354             :       // Sort the non-bottom states such that the deepest states occur first.
     355             :       // Raise an exception if there is a non trivial tau loop.
     356             : 
     357         215 :       order_on_tau_reachability(initial_partition.non_bottom_states);
     358             : 
     359             :       // Store the non-inert transitions (i.e. the non tau transitions)
     360         215 :       sort_transitions(aut.get_transitions(), aut.hidden_label_map(), mcrl2::lts::lbl_tgt_src);
     361         215 :       const std::vector<transition> & trans1=aut.get_transitions();
     362        1975 :       for (std::vector<transition>::const_iterator r=trans1.begin(); r!=trans1.end(); ++r)
     363             :       {
     364        1760 :         const transition t= *r;
     365        1760 :         if (!branching || !aut.is_tau(aut.apply_hidden_label_map(t.label())))
     366             :         {
     367             :           // Note that by sorting the transitions first, the non_inert_transitions are grouped per label.
     368        1395 :           initial_partition.non_inert_transitions.push_back(t);
     369             :         }
     370             :       }
     371             : 
     372             :       // block_is_active.push_back(true);
     373         215 :       initial_partition.block_index=0;
     374         215 :       initial_partition.state_index=0;
     375         215 :       max_state_index=1;
     376         215 :       initial_partition.parent_block_index=0;
     377         215 :       initial_partition.splitter=std::pair< label_type, block_index_type > (0,0);
     378         215 :       blocks.push_back(block());
     379         215 :       blocks.back().swap(initial_partition);
     380         215 :       block_index_of_a_state=std::vector < block_index_type >(aut.num_states(),0);
     381         215 :       block_flags.push_back(false);
     382         215 :       state_flags=std::vector < bool >(aut.num_states(),false);
     383         215 :       block_is_in_to_be_processed.push_back(false);
     384         215 :       to_be_processed.clear();
     385         215 :       BL.clear();
     386         215 :     } // end create_initial_partition
     387             : 
     388             : // Refine the partition until the partition has become stable
     389             : #ifndef NDEBUG
     390         215 :     void refine_partition_until_it_becomes_stable(const bool branching, const bool preserve_divergence)
     391             : #else
     392             :     void refine_partition_until_it_becomes_stable(const bool, const bool)
     393             : #endif
     394             :     {
     395             : #ifndef NDEBUG
     396         215 :       std::size_t consistency_check_counter=1;
     397         215 :       std::size_t consistency_check_barrier=1;
     398             : #endif
     399         215 :       bool partition_is_unstable=true; // This boolean indicates that the partition becomes unstable
     400             :       // because an inert transition becomes non inert.
     401        4265 :       while (!to_be_processed.empty() || partition_is_unstable)
     402             :       {
     403             : #ifndef NDEBUG
     404             :         // Avoid checking too often. This is too time consuming, even in debug mode.
     405        2025 :         consistency_check_counter++;
     406        2025 :         if (consistency_check_counter>=consistency_check_barrier)
     407             :         {
     408         532 :           consistency_check_counter=0;
     409         532 :           consistency_check_barrier=consistency_check_barrier*2;
     410         532 :           check_internal_consistency_of_the_partitioning_data_structure(branching, preserve_divergence);
     411             :         }
     412             : #endif
     413        2025 :         if (to_be_processed.empty() && partition_is_unstable)
     414             :         {
     415             :           // Put all blocks in to_be_processed;
     416         798 :           for (block_index_type i=0; i< blocks.size(); ++i)
     417             :           {
     418         555 :             to_be_processed.push_back(i);
     419             :           }
     420         243 :           block_is_in_to_be_processed=std::vector < bool >(blocks.size(),true);
     421         243 :           partition_is_unstable=false;
     422             :         }
     423             : 
     424        2025 :         const block_index_type splitter_index=to_be_processed.back();
     425             :         // assert(block_is_in_to_be_processed[splitter_index]||!block_is_active[splitter_index]);
     426        2025 :         to_be_processed.pop_back();
     427        2025 :         block_is_in_to_be_processed[splitter_index]=false;
     428             : 
     429             :         // Split with the splitter block, unless it is to_be_processed as we have to reconsider it
     430             :         // completely anyhow at some later point.
     431             : 
     432             :         // Walk through the non_inert_transitions via a natural number, because
     433             :         // the blocks and the non_inert_transitions can move around in memory. This makes it
     434             :         // unsafe to use interators.
     435             : 
     436        6444 :         for (std::size_t i=0; i<blocks[splitter_index].non_inert_transitions.size(); ++i)
     437             :         {
     438             :           // The flag of the starting state of *i is raised and its block is added to BL;
     439             : 
     440        4419 :           assert(blocks[splitter_index].non_inert_transitions[i].from()<aut.num_states());
     441        4419 :           state_flags[blocks[splitter_index].non_inert_transitions[i].from()]=true;
     442        4419 :           const block_index_type marked_block_index=block_index_of_a_state[blocks[splitter_index].non_inert_transitions[i].from()];
     443        4419 :           if (block_flags[marked_block_index]==false)
     444             :           {
     445        2540 :             block_flags[marked_block_index]=true;
     446        2540 :             BL.push_back(marked_block_index);
     447             :           }
     448             : 
     449             :           // If the label of the next action is different, we must carry out the splitting.
     450        7706 :           if ((i+1)==blocks[splitter_index].non_inert_transitions.size() ||
     451        9861 :               aut.apply_hidden_label_map(blocks[splitter_index].non_inert_transitions[i].label())!=
     452        6574 :               aut.apply_hidden_label_map(blocks[splitter_index].non_inert_transitions[i+1].label()))
     453             :           {
     454             :             // We consider BL which contains references to all blocks from which a state from splitter
     455             :             // can be reached. If not all flags of the non bottom states in a block in BL are set, the
     456             :             // non flagged non bottom states are moved to a new block.
     457             : 
     458        2232 :             split_the_blocks_in_BL(partition_is_unstable,aut.apply_hidden_label_map(blocks[splitter_index].non_inert_transitions[i].label()),splitter_index);
     459             : 
     460             :           }
     461             : 
     462             :         }
     463             :       }
     464             : #ifndef NDEBUG
     465         215 :       check_internal_consistency_of_the_partitioning_data_structure(branching, preserve_divergence);
     466             : #endif
     467         215 :       block_flags.clear();
     468         215 :       block_is_in_to_be_processed.clear();
     469         215 :       state_flags.clear();
     470         215 :       to_be_processed.clear();
     471         215 :       BL.clear();
     472         215 :     }
     473             : 
     474             : 
     475             : 
     476             :     void refine_partion_with_respect_to_divergences(void);
     477             : 
     478        2232 :     void split_the_blocks_in_BL(
     479             :       bool& partition_is_unstable,
     480             :       const label_type splitter_label,
     481             :       const block_index_type splitter_block)
     482             :     {
     483        4772 :       for (std::vector < block_index_type > :: const_iterator i1=BL.begin();
     484        4772 :            i1!=BL.end(); ++i1)
     485             :       {
     486             :         // assert(block_is_active[*i1]);
     487        2540 :         block_flags[*i1]=false;
     488        5080 :         std::vector < state_type > flagged_states;
     489        5080 :         std::vector < state_type > non_flagged_states;
     490        5080 :         std::vector < state_type > i1_bottom_states;
     491        2540 :         i1_bottom_states.swap(blocks[*i1].bottom_states);
     492             : 
     493        9372 :         for (std::vector < state_type >::const_iterator j=i1_bottom_states.begin();
     494        9372 :              j!=i1_bottom_states.end(); ++j)
     495             :         {
     496        6832 :           if (state_flags[*j])
     497             :           {
     498             :             // state is flagged.
     499        3766 :             flagged_states.push_back(*j);
     500             :           }
     501             :           else
     502             :           {
     503             :             // state is not flagged. It will be moved to a new block.
     504        3066 :             non_flagged_states.push_back(*j);
     505        3066 :             block_index_of_a_state[*j]=blocks.size();
     506             :           }
     507             :         }
     508        2540 :         assert(!flagged_states.empty()||!blocks[*i1].non_bottom_states.empty()||i1_bottom_states.empty());
     509        2540 :         block_index_type reset_state_flags_block=*i1;
     510             : 
     511        2540 :         if (!non_flagged_states.empty())
     512             :         {
     513             :           // There are flagged and non flagged states. So, the block must be split.
     514             :           // Move the unflagged states to the new block.
     515             : 
     516         735 :           if (mCRL2logEnabled(log::debug))
     517             :           {
     518           0 :             const std::size_t m = static_cast<std::size_t>(std::pow(10.0, std::floor(std::log10(static_cast<double>((blocks.size()+1)/2)))));
     519           0 :             if ((blocks.size()+1)/2 % m==0)
     520             :             {
     521           0 :               mCRL2log(log::debug) << "Bisimulation partitioner: create block " << (blocks.size()+1)/2 << std::endl;
     522             :             }
     523             :           }
     524             :           // Record how block *i1 is split, to use this to generate counter examples.
     525         735 :           blocks[*i1].splitter=std::pair< label_type, block_index_type > (splitter_label,splitter_block);
     526             : 
     527             :           // Create a first new block.
     528         735 :           blocks.push_back(block());
     529         735 :           block_index_type new_block1=blocks.size()-1;
     530             :           // block_is_active.push_back(true);
     531         735 :           blocks.back().state_index=max_state_index;
     532         735 :           max_state_index++;
     533         735 :           blocks.back().block_index=new_block1;
     534         735 :           blocks.back().parent_block_index=*i1;
     535             : 
     536         735 :           non_flagged_states.swap(blocks.back().bottom_states);
     537             :           // Put the indices of first split block to to_be_processed.
     538         735 :           to_be_processed.push_back(blocks.back().block_index);
     539         735 :           block_is_in_to_be_processed.push_back(true);
     540             : 
     541             :           // Create a second new block.
     542         735 :           blocks.push_back(block());
     543         735 :           block_index_type new_block2=blocks.size()-1;
     544             :           // block_is_active.push_back(true);
     545         735 :           blocks.back().state_index=blocks[*i1].state_index;
     546         735 :           blocks.back().block_index=new_block2;
     547         735 :           reset_state_flags_block=new_block2;
     548         735 :           blocks.back().parent_block_index=*i1;
     549             : 
     550             :           // Move the flagged states to the second block, and let the block index of these states refer to this block.
     551         735 :           flagged_states.swap(blocks.back().bottom_states);
     552         735 :           std::vector < state_type > &reference_to_flagged_states_of_block2=blocks.back().bottom_states;
     553        2081 :           for (std::vector < state_type >::const_iterator j=reference_to_flagged_states_of_block2.begin();
     554        2081 :                j!=reference_to_flagged_states_of_block2.end(); ++j)
     555             :           {
     556        1346 :             block_index_of_a_state[*j]=new_block2;
     557             :           }
     558             : 
     559             :           // Put the indices of second split block to to_be_processed.
     560         735 :           to_be_processed.push_back(blocks.back().block_index);
     561         735 :           block_is_in_to_be_processed.push_back(true);
     562             : 
     563             :           // reset the flag of block *i1, which is being split.
     564         735 :           block_is_in_to_be_processed[*i1]=false;
     565             :           // block_is_active[*i1]=false;
     566             : 
     567             :           // The flag fields of the new blocks is set to false;
     568         735 :           block_flags.push_back(false);
     569         735 :           block_flags.push_back(false);
     570             : 
     571             :           // Declare already some space for transitions, such that we can
     572             :           // put inert transitions that become non inert in there when investigating
     573             :           // the non bottom states. After investigating the non bottom states,
     574             :           // the transitions are split over the vectors below.
     575             : 
     576        1470 :           std::vector < transition > flagged_non_inert_transitions;
     577        1470 :           std::vector < transition > non_flagged_non_inert_transitions;
     578             :           // Reserve enough space for transitions to be copied. Otherwise, resizing may lead to
     579             :           // lot of unneccesary copying...
     580         735 :           flagged_non_inert_transitions.reserve(blocks[*i1].non_inert_transitions.size());
     581         735 :           non_flagged_non_inert_transitions.reserve(blocks[*i1].non_inert_transitions.size());
     582             : 
     583             :           // Next we scan the non-bottom states of *i1. If for some non-bottom state the flag is not raised
     584             :           // and if none of the outgoing P-inert transitions leads to a state in the old block then this
     585             :           // state becomes a non bottom state of B2.
     586             : 
     587        1470 :           std::vector < non_bottom_state > flagged_non_bottom_states;
     588        1470 :           std::vector < non_bottom_state > non_flagged_non_bottom_states;
     589        1470 :           std::vector < non_bottom_state > i1_non_bottom_states;
     590         735 :           i1_non_bottom_states.swap(blocks[*i1].non_bottom_states);
     591        1530 :           for (typename std::vector < non_bottom_state >::iterator k=i1_non_bottom_states.begin();
     592        1530 :                k!=i1_non_bottom_states.end(); ++k)
     593             :           {
     594         795 :             const std::vector < state_type > &inert_transitions=k->inert_transitions;
     595         795 :             if (!state_flags[k->state])
     596             :             {
     597         636 :               bool all_transitions_end_in_unflagged_block=true;
     598        1369 :               for (std::vector < state_type > :: const_iterator l=inert_transitions.begin();
     599        1369 :                    all_transitions_end_in_unflagged_block && l!=inert_transitions.end(); ++l)
     600             :               {
     601         733 :                 if (block_index_of_a_state[*l]!= new_block1)
     602             :                 {
     603         183 :                   block_index_of_a_state[*l]=new_block2;
     604         183 :                   all_transitions_end_in_unflagged_block=false;
     605             :                 }
     606             :               }
     607         636 :               if (all_transitions_end_in_unflagged_block)
     608             :               {
     609             :                 // Move *k to the non flagged block. Swap the inert transitions to avoid copying.
     610         906 :                 non_bottom_state s(k->state);
     611         453 :                 s.inert_transitions.swap(k->inert_transitions);
     612         453 :                 non_flagged_non_bottom_states.push_back(s);
     613         453 :                 block_index_of_a_state[k->state]=new_block1;
     614         453 :                 continue;
     615             :               }
     616             :             }
     617             :             // Move *k to the flagged block; note that the transitions can have become
     618             :             // non-inert. So, investigate them separately.
     619         684 :             std::vector < state_type > remaining_inert_transitions;
     620         781 :             for (std::vector < state_type > :: const_iterator l=inert_transitions.begin();
     621         781 :                  l!=inert_transitions.end(); ++l)
     622             :             {
     623         439 :               if (block_index_of_a_state[*l]==new_block1)
     624             :               {
     625             :                 // The transition *l (*k,tau_label,*l) becomes a non inert transition in the new
     626             :                 // block.
     627         177 :                 non_flagged_non_inert_transitions.push_back(transition(k->state,aut.tau_label_index(),*l));
     628             :               }
     629             :               else
     630             :               {
     631             :                 // The transition represented by *l remains an inert transition.
     632         262 :                 block_index_of_a_state[*l]=new_block2;
     633         262 :                 remaining_inert_transitions.push_back(*l);
     634             :               }
     635             :             }
     636         342 :             if (remaining_inert_transitions.empty()) // The last outgoing inert tau transition just became non inert.
     637             :               // k->state has become a bottom state. Otherwise it remains
     638             :               // a non bottom state.
     639             :             {
     640          98 :               blocks[new_block2].bottom_states.push_back(k->state);
     641          98 :               block_index_of_a_state[k->state]=new_block2;
     642          98 :               partition_is_unstable=true;
     643             :             }
     644             :             else
     645             :             {
     646         244 :               flagged_non_bottom_states.push_back(non_bottom_state(k->state,remaining_inert_transitions));
     647         244 :               block_index_of_a_state[k->state]=new_block2;
     648             :             }
     649             :           }
     650         735 :           non_flagged_non_bottom_states.swap(blocks[new_block1].non_bottom_states);
     651         735 :           flagged_non_bottom_states.swap(blocks[new_block2].non_bottom_states);
     652             : 
     653             :           // Finally the non-inert transitions are distributed over both blocks in the obvious way.
     654             :           // Note that this must be done after all states are properly put into a new block.
     655             : 
     656         735 :           assert(*i1 < blocks.size());
     657        1470 :           std::vector < transition > i1_non_inert_transitions;
     658         735 :           i1_non_inert_transitions.swap(blocks[*i1].non_inert_transitions);
     659        6954 :           for (std::vector < transition >::iterator k=i1_non_inert_transitions.begin();
     660        6954 :                k!=i1_non_inert_transitions.end(); ++k)
     661             :           {
     662        6219 :             if (block_index_of_a_state[k->to()]==new_block1)
     663             :             {
     664        4282 :               non_flagged_non_inert_transitions.push_back(*k);
     665             :             }
     666             :             else
     667             :             {
     668        1937 :               block_index_of_a_state[k->to()]=new_block2;
     669        1937 :               flagged_non_inert_transitions.push_back(*k);
     670             :             }
     671             :           }
     672             : 
     673             :           // Only put the parts that we need to store. Avoid that reserved space for
     674             :           // current_inert_transition_counter and flagged_non_inert_transitions is stored
     675             :           // in the non_inert_transitions in both blocks. Therefore, we do not use a copy
     676             :           // constructor, but put elements in there one by one.
     677             :           // The two lines below were old code, wasting memory bandwidth.
     678             :           // non_flagged_non_inert_transitions.swap(blocks[new_block1].non_inert_transitions);
     679             :           // flagged_non_inert_transitions.swap(blocks[new_block2].non_inert_transitions);
     680             : 
     681         735 :           blocks[new_block1].non_inert_transitions.reserve(non_flagged_non_inert_transitions.size());
     682        5194 :           for(std::vector < transition > ::const_iterator i=non_flagged_non_inert_transitions.begin();
     683        5194 :                     i!=non_flagged_non_inert_transitions.end(); i++)
     684             :           {
     685        4459 :             blocks[new_block1].non_inert_transitions.push_back(*i);
     686             :           }
     687             : 
     688         735 :           blocks[new_block2].non_inert_transitions.reserve(flagged_non_inert_transitions.size());
     689        2672 :           for(std::vector < transition > ::const_iterator i=flagged_non_inert_transitions.begin();
     690        2672 :                     i!=flagged_non_inert_transitions.end(); i++)
     691             :           {
     692        1937 :             blocks[new_block2].non_inert_transitions.push_back(*i);
     693             :           }
     694             :         }
     695             :         else
     696             :         {
     697             :           // Nothing changed, so put the bottom states back again.
     698        1805 :           i1_bottom_states.swap(blocks[*i1].bottom_states);
     699             :         }
     700             :         // reset the state flags
     701        2540 :         std::vector < state_type > &flagged_states_to_be_unflagged=blocks[reset_state_flags_block].bottom_states;
     702        6404 :         for (std::vector < state_type >::const_iterator j=flagged_states_to_be_unflagged.begin();
     703        6404 :              j!=flagged_states_to_be_unflagged.end(); ++j)
     704             :         {
     705        3864 :           state_flags[*j]=false;
     706             :         }
     707             : 
     708        2540 :         std::vector < non_bottom_state > &flagged_states_to_be_unflagged1=blocks[reset_state_flags_block].non_bottom_states;
     709        3556 :         for (typename std::vector < non_bottom_state >::const_iterator j=flagged_states_to_be_unflagged1.begin();
     710        3556 :              j!=flagged_states_to_be_unflagged1.end(); ++j)
     711             :         {
     712        1016 :           state_flags[j->state]=false;
     713             :         }
     714             :       }
     715        2232 :       BL.clear();
     716        2232 :     }
     717         607 :     void order_recursively_on_tau_reachability(
     718             :       const state_type s,
     719             :       std::map < state_type, std::vector < state_type > >& inert_transition_map,
     720             :       std::vector < non_bottom_state >& new_non_bottom_states,
     721             :       std::set < state_type >& visited)
     722             :     {
     723         607 :       if (inert_transition_map.count(s)>0) // The state s is a bottom state. We need not to investigate these.
     724             :       {
     725         443 :         if (visited.count(s)==0)
     726             :         {
     727         258 :           visited.insert(s);
     728         258 :           std::vector < state_type> &inert_transitions=inert_transition_map[s];
     729         607 :           for (std::vector < state_type>::const_iterator j=inert_transitions.begin();
     730         607 :                j!=inert_transitions.end(); j++)
     731             :           {
     732         349 :             order_recursively_on_tau_reachability(*j,inert_transition_map,new_non_bottom_states,visited);
     733             :           }
     734         258 :           new_non_bottom_states.push_back(non_bottom_state(s));
     735         258 :           inert_transitions.swap(new_non_bottom_states.back().inert_transitions);
     736             :         }
     737             :       }
     738         607 :     }
     739             : 
     740         215 :     void order_on_tau_reachability(std::vector < non_bottom_state > &non_bottom_states)
     741             :     {
     742         430 :       std::set < state_type > visited;
     743         430 :       std::map < state_type, std::vector < state_type > > inert_transition_map;
     744         473 :       for (typename std::vector < non_bottom_state >::iterator i=non_bottom_states.begin();
     745         473 :            i!=non_bottom_states.end(); ++i)
     746             :       {
     747         258 :         i->inert_transitions.swap(inert_transition_map[i->state]);
     748             :       }
     749         430 :       std::vector < non_bottom_state > new_non_bottom_states;
     750             : 
     751         473 :       for (typename std::vector < non_bottom_state >::const_iterator i=non_bottom_states.begin();
     752         473 :            i!=non_bottom_states.end(); ++i)
     753             :       {
     754         258 :         order_recursively_on_tau_reachability(i->state, inert_transition_map, new_non_bottom_states, visited);
     755             :       }
     756         215 :       new_non_bottom_states.swap(non_bottom_states);
     757         215 :     }
     758             : 
     759           1 :     std::set < mcrl2::trace::Trace > counter_traces_aux(
     760             :       const state_type s,
     761             :       const state_type t,
     762             :       const mcrl2::lts::outgoing_transitions_per_state_action_t& outgoing_transitions,
     763             :       const bool branching_bisimulation) const
     764             :     {
     765             :       // First find the smallest block containing both states s and t.
     766             :       // Find all blocks containing s.
     767           2 :       std::set < block_index_type > blocks_containing_s;
     768           1 :       block_index_type b_s=block_index_of_a_state[s];
     769           1 :       blocks_containing_s.insert(b_s);
     770           3 :       while (blocks[b_s].parent_block_index!=b_s)
     771             :       {
     772           1 :         b_s=blocks[b_s].parent_block_index;
     773           1 :         blocks_containing_s.insert(b_s);
     774             :       }
     775             : 
     776             :       // Find the first smallest block containing t and s
     777           1 :       block_index_type b_C=block_index_of_a_state[t];
     778           5 :       while (blocks_containing_s.count(b_C)==0)
     779             :       {
     780           2 :         assert(blocks[b_C].parent_block_index!=b_C);
     781           2 :         b_C=blocks[b_C].parent_block_index;
     782             :       }
     783             : 
     784             :       // Now b_C is the smallest block containing both s and t.
     785             : 
     786           1 :       const label_type l=blocks[b_C].splitter.first;
     787           1 :       const block_index_type B__=blocks[b_C].splitter.second;
     788           2 :       std::set < state_type > l_reachable_states_for_s;
     789           2 :       std::set < state_type > visited1;
     790           1 :       reachable_states_in_block_s_via_label_l(s,b_C,l,outgoing_transitions, l_reachable_states_for_s,visited1,branching_bisimulation);
     791             : 
     792           2 :       std::set < state_type> B_s_reacha;
     793           2 :       std::set < state_type> B_s_nonreacha;
     794           2 :       for (const state_type i: l_reachable_states_for_s)
     795             :       {
     796           1 :         block_index_type b=block_index_of_a_state[i];
     797           1 :         bool reached=b==B__;
     798           1 :         do
     799             :         {
     800           2 :           b=blocks[b].parent_block_index;
     801           2 :           if (b==B__)
     802             :           {
     803           1 :             reached=true;
     804             :           }
     805             :         }
     806           2 :         while (!reached && b!=blocks[b].parent_block_index);
     807             : 
     808           1 :         if (reached)
     809             :         {
     810           1 :           B_s_reacha.insert(i);
     811             :         }
     812             :         else
     813             :         {
     814           0 :           B_s_nonreacha.insert(i);
     815             :         }
     816             :       }
     817             : 
     818           2 :       std::set < state_type > l_reachable_states_for_t;
     819           2 :       std::set < state_type > visited2;
     820           1 :       reachable_states_in_block_s_via_label_l(t,b_C,l,outgoing_transitions, l_reachable_states_for_t,visited2,branching_bisimulation);
     821             : 
     822           2 :       std::set < state_type> B_t_reacha;
     823           2 :       std::set < state_type> B_t_nonreacha;
     824           1 :       for (std::set < state_type >::const_iterator i=l_reachable_states_for_t.begin();
     825           1 :            i!=l_reachable_states_for_t.end(); ++i)
     826             :       {
     827           0 :         block_index_type b=block_index_of_a_state[*i];
     828           0 :         bool reached=b==B__;
     829           0 :         do
     830             :         {
     831           0 :           b=blocks[b].parent_block_index;
     832           0 :           if (b==B__)
     833             :           {
     834           0 :             reached=true;
     835             :           }
     836             :         }
     837           0 :         while (!reached && b!=blocks[b].parent_block_index);
     838             : 
     839           0 :         if (reached)
     840             :         {
     841           0 :           B_t_reacha.insert(*i);
     842             :         }
     843             :         else
     844             :         {
     845           0 :           B_t_nonreacha.insert(*i);
     846             :         }
     847             :       }
     848           1 :       assert((B_s_reacha.empty() && !B_t_reacha.empty()) ||
     849             :              (!B_s_reacha.empty() && B_t_reacha.empty()));
     850             : 
     851           1 :       std::set < mcrl2::trace::Trace > resulting_counter_traces;
     852             : 
     853           1 :       if (B_s_reacha.empty())
     854             :       {
     855           0 :         B_s_reacha.swap(B_t_reacha);
     856           0 :         B_s_nonreacha.swap(B_t_nonreacha);
     857             :       }
     858             : 
     859           1 :       assert(!B_s_reacha.empty());
     860             : 
     861             : 
     862           1 :       if (B_t_nonreacha.empty())
     863             :       {
     864             :         // The counter trace is simply the label l.
     865           2 :         mcrl2::trace::Trace counter_trace;
     866           2 :         counter_trace.addAction(mcrl2::lps::multi_action(mcrl2::process::action(
     867           1 :                                 mcrl2::process::action_label(core::identifier_string(mcrl2::lts::pp(aut.action_label(l))),mcrl2::data::sort_expression_list()),
     868             :                                 mcrl2::data::data_expression_list())));
     869           1 :         resulting_counter_traces.insert(counter_trace);
     870             :       }
     871             :       else
     872             :       {
     873           0 :         for (std::set < state_type>::const_iterator i_s=B_s_reacha.begin();
     874           0 :              i_s!=B_s_reacha.end(); ++i_s)
     875             :         {
     876           0 :           for (std::set < state_type>::const_iterator i_t=B_t_nonreacha.begin();
     877           0 :                i_t!=B_t_nonreacha.end(); ++i_t)
     878             :           {
     879           0 :             const std::set < mcrl2::trace::Trace > counter_traces=
     880           0 :                             counter_traces_aux(*i_s,*i_t,outgoing_transitions,branching_bisimulation);
     881             :             // Add l to these traces and add them to resulting_counter_traces
     882           0 :             for (std::set< mcrl2::trace::Trace >::const_iterator j=counter_traces.begin();
     883           0 :                  j!=counter_traces.end(); ++j)
     884             :             {
     885           0 :               mcrl2::trace::Trace new_counter_trace;
     886           0 :               new_counter_trace.addAction(mcrl2::lps::multi_action(mcrl2::process::action(
     887           0 :                                 mcrl2::process::action_label(core::identifier_string(mcrl2::lts::pp(aut.action_label(l))),mcrl2::data::sort_expression_list()),
     888             :                                 mcrl2::data::data_expression_list())));
     889           0 :               mcrl2::trace::Trace old_counter_trace=*j;
     890           0 :               old_counter_trace.resetPosition();
     891           0 :               for (std::size_t k=0 ; k< old_counter_trace.number_of_actions(); k++)
     892             :               {
     893           0 :                 new_counter_trace.addAction(old_counter_trace.currentAction());
     894           0 :                 old_counter_trace.increasePosition();
     895             :               }
     896           0 :               resulting_counter_traces.insert(new_counter_trace);
     897             :             }
     898             :           }
     899             :         }
     900             : 
     901             :       }
     902           2 :       return resulting_counter_traces;
     903             :     }
     904             : 
     905             : 
     906             : 
     907           2 :     void reachable_states_in_block_s_via_label_l(
     908             :       const state_type s,
     909             :       const block_index_type block_index_for_bottom_state,
     910             :       const label_type l,
     911             :       const mcrl2::lts::outgoing_transitions_per_state_action_t& outgoing_transitions,
     912             :       std::set < state_type > &result_set,
     913             :       std::set < state_type > &visited,
     914             :       const bool branching_bisimulation) const
     915             :     {
     916             :       // This function yields a set of states that are reachable via a sequence of tau steps
     917             :       // in block block_index_for_bottom_state, followed by an l step.
     918             :       // The technique used is to search through tau transitions from s, until a bottom state
     919             :       // in the current class is found. From this state all reachable states are put in the result set.
     920           2 :       if (visited.count(s)>0)
     921             :       {
     922           0 :         return;
     923             :       }
     924             : 
     925           2 :       visited.insert(s);
     926             :       // Put all l reachable states in the result set.
     927           3 :       for (outgoing_transitions_per_state_action_t::const_iterator i1=outgoing_transitions.lower_bound(std::pair<state_type,label_type>(s,l));
     928           3 :            i1!=outgoing_transitions.upper_bound(std::pair<state_type, label_type>(s,l)); ++i1)
     929             :       {
     930           1 :         result_set.insert(to(i1));
     931             :       }
     932             : 
     933             :       // Search for tau reachable states that are still in the block with block_index_for_bottom_state.
     934           2 :       if (branching_bisimulation)
     935             :       {
     936           0 :         for (label_type lab=0; lab<aut.num_action_labels(); ++lab)
     937             :         {
     938           0 :           if (aut.is_tau(aut.apply_hidden_label_map(lab)))
     939             :           {
     940           0 :             for (outgoing_transitions_per_state_action_t::const_iterator i=outgoing_transitions.lower_bound(std::pair<state_type,label_type>(s,lab));
     941           0 :                  i!=outgoing_transitions.upper_bound(std::pair<state_type, label_type>(s,lab)); ++i)
     942             :             {
     943             :               // Now find out whether the block index of to(i) is part of the block with index block_index_for_bottom_state.
     944           0 :               block_index_type b=block_index_of_a_state[to(i)];
     945           0 :               while (b!=block_index_for_bottom_state && blocks[b].parent_block_index!=b)
     946             :               {
     947           0 :                 assert(blocks[b].parent_block_index!=b);
     948           0 :                 b=blocks[b].parent_block_index;
     949             :               }
     950           0 :               if (b==block_index_for_bottom_state)
     951             :               {
     952           0 :                 reachable_states_in_block_s_via_label_l(
     953             :                   to(i),
     954             :                   block_index_for_bottom_state,
     955             :                   l,
     956             :                   outgoing_transitions,
     957             :                   result_set,
     958             :                   visited,
     959             :                   branching_bisimulation);
     960             :               }
     961             :             }
     962             :           }
     963             :         }
     964             :       }
     965             :     }
     966             : 
     967             : 
     968             : #ifndef NDEBUG
     969             :     // The method below is intended to check the consistency of the internal data
     970             :     // structure. Its sole purpose is to detect programming errors. It has no
     971             :     // side effects on the data structure. If a problem occurs, execution halts with
     972             :     // an assert.
     973             : 
     974         747 :     void check_internal_consistency_of_the_partitioning_data_structure(
     975             :       const bool branching,
     976             :       const bool preserve_divergence) const
     977             :     {
     978         747 :       state_type total_number_of_states=0;
     979         747 :       std::size_t total_number_of_transitions=0;
     980             : 
     981         747 :       assert(!blocks.empty());
     982        1494 :       std::set < block_index_type > block_indices;
     983             : 
     984         747 :       assert(block_index_of_a_state.size()==aut.num_states());
     985        5398 :       for (typename std::vector < block >::const_iterator i=blocks.begin();
     986        5398 :            i!=blocks.end(); ++i)
     987             :       {
     988             :         // Check the block_index.
     989        4651 :         assert(i->block_index<blocks.size());
     990        4651 :         assert(block_indices.count(i->block_index)==0);
     991        4651 :         block_indices.insert(i->block_index);
     992             : 
     993             :         // Check the bottom states.
     994        4651 :         const std::vector < state_type > &i_bottom_states=i->bottom_states;
     995             : 
     996       10153 :         for (std::vector < state_type >::const_iterator j=i_bottom_states.begin();
     997       10153 :              j!=i_bottom_states.end(); ++j)
     998             :         {
     999        5502 :           total_number_of_states++;
    1000        5502 :           assert(*j<aut.num_states());
    1001             :           // Check that the block number of the state is maintained properly.
    1002        5502 :           assert(block_index_of_a_state[*j]==i->block_index);
    1003             :         }
    1004             : 
    1005             :         // Check the non bottom states. In particular check that there is no tau loop
    1006             :         // in these non bottom states.
    1007        4651 :         const std::vector < non_bottom_state > &i_non_bottom_states=i->non_bottom_states;
    1008        9302 :         std::set < state_type > visited;
    1009        9302 :         std::set < state_type > local_bottom_states;
    1010        5642 :         for (typename std::vector < non_bottom_state >::const_iterator j=i_non_bottom_states.begin();
    1011        5642 :              j!=i_non_bottom_states.end(); ++j)
    1012             :         {
    1013         991 :           local_bottom_states.insert(j->state);
    1014             :         }
    1015             : 
    1016        5642 :         for (typename std::vector < non_bottom_state >::const_iterator j=i_non_bottom_states.begin();
    1017        5642 :              j!=i_non_bottom_states.end(); ++j)
    1018             :         {
    1019         991 :           total_number_of_states++;
    1020         991 :           assert(j->state<aut.num_states());
    1021             :           // Check that the block number of the state is maintained properly.
    1022         991 :           assert(block_index_of_a_state[j->state]==i->block_index);
    1023         991 :           const std::vector < state_type > &j_inert_transitions=j->inert_transitions;
    1024        2161 :           for (std::vector < state_type >::const_iterator k=j_inert_transitions.begin();
    1025        2161 :                k!=j_inert_transitions.end(); k++)
    1026             :           {
    1027        1170 :             total_number_of_transitions++;
    1028        1170 :             assert(*k<aut.num_states());
    1029             :             // Check that the inert transitions are well ordered.
    1030        1170 :             assert(visited.count(*k)>0 || local_bottom_states.count(*k)==0);
    1031             :           }
    1032         991 :           visited.insert(j->state);
    1033             :         }
    1034             : 
    1035             :         // Check the non_inert_transitions. It is required that the transitions
    1036             :         // are grouped per label, and that tau transitions must be inert.
    1037             : 
    1038        4651 :         const std::vector < transition > &i_non_inert_transitions=i->non_inert_transitions;
    1039        9302 :         std::set < label_type > observed_action_labels;
    1040       12048 :         for (std::vector < transition >::const_iterator j=i_non_inert_transitions.begin();
    1041       12048 :              j!=i_non_inert_transitions.end(); ++j)
    1042             :         {
    1043        7397 :           total_number_of_transitions++;
    1044        7397 :           assert(j->to()<aut.num_states());
    1045        7397 :           assert(j->from()<aut.num_states());
    1046             : 
    1047             :           // Check proper grouping of action labels.
    1048        7397 :           std::vector < transition >::const_iterator j_next=j;
    1049        7397 :           j_next++;
    1050        7397 :           if (j_next==i_non_inert_transitions.end() || (aut.apply_hidden_label_map(j->label())!=aut.apply_hidden_label_map(j_next->label())))
    1051             :           {
    1052        3995 :             assert(observed_action_labels.count(aut.apply_hidden_label_map(j->label()))==0);
    1053        3995 :             observed_action_labels.insert(aut.apply_hidden_label_map(j->label()));
    1054             :           }
    1055             : 
    1056             :           // Check whether tau transition in non inert transition vector is inert.
    1057        7397 :           if (!preserve_divergence && branching && aut.is_tau(aut.apply_hidden_label_map(j->label())))
    1058             :           {
    1059         260 :             assert(j->to()!=j->from());
    1060             :           }
    1061             : 
    1062             :           // Check whether the target state of the transition is in the current block.
    1063        7397 :           assert(block_index_of_a_state[j->to()]==i->block_index);
    1064             :         }
    1065             :       }
    1066             : 
    1067             :       // Check total number of states and transitions.
    1068         747 :       assert(total_number_of_states==aut.num_states());
    1069         747 :       assert(total_number_of_transitions==aut.num_transitions());
    1070             : 
    1071             :       // Check block_index_of_a_state
    1072         747 :       assert(block_index_of_a_state.size()==aut.num_states());
    1073        7240 :       for (std::vector < state_type >::const_iterator i=block_index_of_a_state.begin();
    1074        7240 :            i!=block_index_of_a_state.end(); ++i)
    1075             :       {
    1076        6493 :         assert(blocks[*i].block_index== *i);
    1077             :       }
    1078             : 
    1079             :       // Check block_flags that the block flags are all set to false
    1080        5398 :       for (std::vector < bool >::const_iterator i=block_flags.begin();
    1081        5398 :            i!=block_flags.end(); ++i)
    1082             :       {
    1083        4651 :         assert(!*i);
    1084             :       }
    1085             : 
    1086             :       // Check that state_flags are all false.
    1087        7240 :       for (std::vector < bool >::const_iterator i=state_flags.begin();
    1088        7240 :            i!=state_flags.end(); ++i)
    1089             :       {
    1090        6493 :         assert(!*i);
    1091             :       }
    1092             : 
    1093             :       // Check to_be_processed
    1094             :       // Check block_is_in_to_be_processed
    1095        1494 :       std::vector < bool > temporary_block_is_in_to_be_processed(blocks.size(),false);
    1096             : 
    1097        1873 :       for (std::vector< block_index_type > ::const_iterator i=to_be_processed.begin();
    1098        1873 :            i!=to_be_processed.end(); ++i)
    1099             :       {
    1100        1126 :         temporary_block_is_in_to_be_processed[*i]=true;
    1101             :       }
    1102        5398 :       for (state_type i=0; i<blocks.size(); ++i)
    1103             :       {
    1104        4651 :         assert(!block_is_in_to_be_processed[i] || temporary_block_is_in_to_be_processed[i]);
    1105             :       }
    1106             : 
    1107             :       // Check that BL is empty.
    1108         747 :       assert(BL.empty());
    1109             : 
    1110         747 :     }
    1111             : 
    1112             : #endif // not NDEBUG
    1113             : 
    1114             : };
    1115             : 
    1116             : 
    1117             : /** \brief Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
    1118             :  * \param[in/out] l The transition system that is reduced.
    1119             :  * \param[in] branching If true branching bisimulation is applied, otherwise strong bisimulation.
    1120             :  * \param[in] preserve_divergences Indicates whether loops of internal actions on states must be preserved. If false
    1121             :  *            these are removed. If true these are preserved.  */
    1122             : template < class LTS_TYPE>
    1123             : void bisimulation_reduce(
    1124             :   LTS_TYPE& l,
    1125             :   const bool branching = false,
    1126             :   const bool preserve_divergences = false);
    1127             : 
    1128             : 
    1129             : /** \brief Checks whether the two initial states of two lts's are strong or branching bisimilar.
    1130             :  * \details This lts and the lts l2 are not usable anymore after this call.
    1131             :  *          The space consumption is O(n) and time is O(nm). It uses the branching bisimulation
    1132             :  *          algorithm by Groote and Vaandrager from 1990.
    1133             :  * \param[in/out] l1 A first transition system.
    1134             :  * \param[in/out] l2 A second transition system.
    1135             :  * \param[branching] If true branching bisimulation is used, otherwise strong bisimulation is applied.
    1136             :  * \param[preserve_divergences] If true and branching is true, preserve tau loops on states.
    1137             :  * \retval True iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar */
    1138             : template < class LTS_TYPE>
    1139             : bool destructive_bisimulation_compare(
    1140             :   LTS_TYPE& l1,
    1141             :   LTS_TYPE& l2,
    1142             :   const bool branching=false,
    1143             :   const bool preserve_divergences=false,
    1144             :   const bool generate_counter_examples = false);
    1145             : 
    1146             : 
    1147             : /** \brief Checks whether the two initial states of two lts's are strong or branching bisimilar.
    1148             :  *  \details The current transitions system and the lts l2 are first duplicated and subsequently
    1149             :  *           reduced modulo bisimulation. If memory space is a concern, one could consider to
    1150             :  *           use destructive_bisimulation_compare. This routine uses the Groote-Vaandrager
    1151             :  *           branching bisimulation routine. It runs in O(mn) and uses O(n) memory where n is the
    1152             :  *           number of states and m is the number of transitions.
    1153             :  * \param[in/out] l1 A first transition system.
    1154             :  * \param[in/out] l2 A second transistion system.
    1155             :  * \param[branching] If true branching bisimulation is used, otherwise strong bisimulation is applied.
    1156             :  * \param[preserve_divergences] If true and branching is true, preserve tau loops on states.
    1157             :  * \retval True iff the initial states of the current transition system and l2 are (divergence preserving) (branching) bisimilar */
    1158             : template < class LTS_TYPE>
    1159             : bool bisimulation_compare(
    1160             :   const LTS_TYPE& l1,
    1161             :   const LTS_TYPE& l2,
    1162             :   const bool branching=false,
    1163             :   const bool preserve_divergences=false,
    1164             :   const bool generate_counter_examples = false);
    1165             : 
    1166             : 
    1167             : 
    1168             : 
    1169             : 
    1170             : template < class LTS_TYPE>
    1171           1 : std::set < mcrl2::trace::Trace > bisim_partitioner<LTS_TYPE>::counter_traces(
    1172             :   const std::size_t s,
    1173             :   const std::size_t t,
    1174             :   const bool branching_bisimulation)
    1175             : {
    1176           1 :   if (get_eq_class(s)==get_eq_class(t))
    1177             :   {
    1178           0 :     throw mcrl2::runtime_error("Requesting a counter trace for two bisimilar states. Such a trace is not useful.");
    1179             :   }
    1180             : 
    1181           2 :   const outgoing_transitions_per_state_action_t outgoing_transitions=transitions_per_outgoing_state_action_pair(aut.get_transitions(),aut.hidden_label_map());
    1182           2 :   return counter_traces_aux(s,t,outgoing_transitions,branching_bisimulation);
    1183             : }
    1184             : 
    1185             : 
    1186             : template < class LTS_TYPE>
    1187         197 : void bisimulation_reduce(LTS_TYPE& l,
    1188             :                          const bool branching /*=false */,
    1189             :                          const bool preserve_divergences /*=false */)
    1190             : {
    1191             :   // First, remove tau loops in case of branching bisimulation.
    1192         197 :   if (branching)
    1193             :   {
    1194          66 :     scc_reduce(l,preserve_divergences);
    1195             :   }
    1196             : 
    1197             :   // Secondly, apply the branching bisimulation reduction algorithm. If there are no tau's,
    1198             :   // this will automatically yield strong bisimulation.
    1199         394 :   detail::bisim_partitioner<LTS_TYPE> bisim_part(l, branching, preserve_divergences);
    1200             : 
    1201             :   // Assign the reduced LTS
    1202         197 :   bisim_part.replace_transition_system(branching,preserve_divergences);
    1203         197 : }
    1204             : 
    1205             : template < class LTS_TYPE>
    1206             : bool bisimulation_compare(
    1207             :   const LTS_TYPE& l1,
    1208             :   const LTS_TYPE& l2,
    1209             :   const bool branching /* =false*/,
    1210             :   const bool preserve_divergences /*=false*/,
    1211             :   const bool generate_counter_examples /*= false*/,
    1212             :   const bool structured_output /* = false */)
    1213             : {
    1214             :   LTS_TYPE l1_copy(l1);
    1215             :   LTS_TYPE l2_copy(l2);
    1216             :   return destructive_bisimulation_compare(l1_copy,l2_copy,branching,preserve_divergences,
    1217             :                                           generate_counter_examples, structured_output);
    1218             : }
    1219             : 
    1220             : template < class LTS_TYPE>
    1221          18 : bool destructive_bisimulation_compare(
    1222             :   LTS_TYPE& l1,
    1223             :   LTS_TYPE& l2,
    1224             :   const bool branching /* =false*/,
    1225             :   const bool preserve_divergences /*=false*/,
    1226             :   const bool generate_counter_examples /* = false */,
    1227             :   const bool /*structured_output = false */)
    1228             : {
    1229          18 :   std::size_t init_l2 = l2.initial_state() + l1.num_states();
    1230          18 :   mcrl2::lts::detail::merge(l1,l2);
    1231          18 :   l2.clear(); // No use for l2 anymore.
    1232             : 
    1233             : 
    1234             :   // First remove tau loops in case of branching bisimulation.
    1235          18 :   if (branching)
    1236             :   {
    1237           0 :     detail::scc_partitioner<LTS_TYPE> scc_part(l1);
    1238           0 :     scc_part.replace_transition_system(preserve_divergences);
    1239           0 :     init_l2 = scc_part.get_eq_class(init_l2);
    1240             :   }
    1241             : 
    1242          36 :   detail::bisim_partitioner<LTS_TYPE> bisim_part(l1, branching, preserve_divergences);
    1243          18 :   if (generate_counter_examples && !bisim_part.in_same_class(l1.initial_state(),init_l2))
    1244             :   {
    1245           2 :     std::set < mcrl2::trace::Trace > counter_example_traces=bisim_part.counter_traces(l1.initial_state(),init_l2,branching);
    1246           1 :     std::size_t count=0;
    1247           2 :     for (std::set < mcrl2::trace::Trace >::const_iterator i=counter_example_traces.begin();
    1248           2 :          i!=counter_example_traces.end(); ++i,++count)
    1249             :     {
    1250           2 :       std::stringstream filename_s;
    1251           1 :       filename_s << "Counterexample" << count << ".trc";
    1252           2 :       const std::string filename(filename_s.str());
    1253           2 :       mcrl2::trace::Trace i_trace= *i;
    1254           1 :       i_trace.save(filename,mcrl2::trace::tfPlain);
    1255           1 :       mCRL2log(mcrl2::log::info) << "Saved counterexample to: \"" << filename << "\"" << std::endl;
    1256             :     }
    1257             :   }
    1258          36 :   return bisim_part.in_same_class(l1.initial_state(),init_l2);
    1259             : }
    1260             : 
    1261             : }
    1262             : }
    1263             : }
    1264             : #endif

Generated by: LCOV version 1.13