LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_pbisim_grv.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 428 432 99.1 %
Date: 2020-07-11 00:44:39 Functions: 47 50 94.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Hector Joao Rivera Verduzco, 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_pbisim.h
      10             : 
      11             : #ifndef _LIBLTS_PBISIM_GRV_H
      12             : #define _LIBLTS_PBISIM_GRV_H
      13             : #include "mcrl2/utilities/execution_timer.h"
      14             : #include "mcrl2/lts/detail/embedded_list.h"
      15             : #include "mcrl2/lts/detail/liblts_plts_merge.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace lts
      20             : {
      21             : namespace detail
      22             : {
      23             : 
      24             : template < class LTS_TYPE>
      25           7 : class prob_bisim_partitioner_grv  // Called after Groote, Rivera Verduzco and de Vink
      26             : {
      27             :   public:
      28             :     /** \brief Creates a probabilistic bisimulation partitioner for an PLTS.
      29             :     *  \details This bisimulation partitioner applies the algorithm described in "J.F. Groote, H.J. Rivera, E.P. de Vink, 
      30             :           *      An O(mlogn) algorithm for probabilistic bisimulation".
      31             :     */
      32           7 :     prob_bisim_partitioner_grv(LTS_TYPE& l, utilities::execution_timer& timer)
      33           7 :       : aut(l)
      34             :     {
      35           7 :       mCRL2log(log::verbose) << "Probabilistic bisimulation partitioner created for " <<
      36           0 :                                 l.num_states() << " states and " <<
      37             :                                 l.num_transitions() << " transitions\n";
      38           7 :       timer.start("bisimulation_reduce (grv)");
      39           7 :       create_initial_partition();
      40           7 :       refine_partition_until_it_becomes_stable();
      41           7 :       timer.finish("bisimulation_reduce (grv)");
      42           7 :     }
      43             : 
      44             :     /** \brief Gives the number of bisimulation equivalence classes of the LTS.
      45             :     *  \return The number of bisimulation equivalence classes of the LTS.
      46             :     */
      47           7 :     std::size_t num_eq_classes() const
      48             :     {
      49           7 :       return action_constellations.size();
      50             :     }
      51             : 
      52             :     /** \brief Gives the bisimulation equivalence class number of a state.
      53             :     *  \param[in] A state number.
      54             :     *  \return The number of the bisimulation equivalence class to which the state belongs to. */
      55         396 :     std::size_t get_eq_class(const std::size_t s)
      56             :     {
      57         396 :       assert(s < action_states.size());
      58         396 :       return action_states[s].parent_block;
      59             :     }
      60             : 
      61             :     /** \brief Gives the bisimulation equivalence probabilistic class number of a probabilistic state.
      62             :     *  \param[in] A probabilistic state number.
      63             :     *  \return The number of the probabilistic class to which the state belongs to. */
      64         292 :     std::size_t get_eq_probabilistic_class(const std::size_t s)
      65             :     {
      66         292 :       assert(s<probabilistic_states.size());
      67         292 :       return probabilistic_states[s].parent_block; // The block index is the state number of the block.
      68             :     }
      69             : 
      70             :     /** \brief Replaces the transition relation of the current lts by the transitions
      71             :     *         of the bisimulation reduced transition system.
      72             :     * \pre The bisimulation equivalence classes have been computed. */
      73           7 :     void replace_transitions()
      74             :     {
      75          14 :       std::set<transition> resulting_transitions;
      76             : 
      77           7 :       const std::vector<transition>& trans = aut.get_transitions();
      78         299 :       for (const transition& t : trans)
      79             :       {
      80         292 :         resulting_transitions.insert(
      81             :           transition(
      82             :             get_eq_class(t.from()),
      83             :             t.label(),
      84             :             get_eq_probabilistic_class(t.to())));
      85             :       }
      86             :       // Remove the old transitions
      87           7 :       aut.clear_transitions();
      88             : 
      89             :       // Copy the transitions from the set into the transition system.
      90          47 :       for (const transition& t : resulting_transitions)
      91             :       {
      92          40 :         aut.add_transition(t);
      93             :       }
      94           7 :     }
      95             : 
      96             :     /** \brief Replaces the probabilistic states of the current lts by the probabilistic
      97             :     *         states of the bisimulation reduced transition system.
      98             :     * \pre The bisimulation classes have been computed. */
      99           7 :     void replace_probabilistic_states()
     100             :     {
     101          14 :       std::vector<typename LTS_TYPE::probabilistic_state_t> new_probabilistic_states;
     102             : 
     103             :       // get the equivalent probabilistic state of each probabilistic block and add it to aut
     104          38 :       for (probabilistic_block_type& prob_block : probabilistic_blocks)
     105             :       {
     106          62 :         typename LTS_TYPE::probabilistic_state_t equivalent_ps = calculate_equivalent_probabilistic_state(prob_block);
     107          31 :         new_probabilistic_states.push_back(equivalent_ps);
     108             :       }
     109             : 
     110             :       /* Remove old probabilistic states */
     111           7 :       aut.clear_probabilistic_states();
     112             : 
     113             :       // Add new prob states to aut
     114          38 :       for (const typename LTS_TYPE::probabilistic_state_t& new_ps : new_probabilistic_states)
     115             :       {
     116          31 :         aut.add_probabilistic_state(new_ps);
     117             :       }
     118             : 
     119          14 :       typename LTS_TYPE::probabilistic_state_t old_initial_prob_state = aut.initial_probabilistic_state();
     120          14 :       typename LTS_TYPE::probabilistic_state_t new_initial_prob_state = calculate_new_probabilistic_state(old_initial_prob_state);
     121           7 :       aut.set_initial_probabilistic_state(new_initial_prob_state);
     122           7 :     }
     123             : 
     124             :     /** \brief Returns whether two states are in the same probabilistic bisimulation equivalence class.
     125             :     *  \param[in] s A state number.
     126             :     *  \param[in] t A state number.
     127             :     *  \retval true if \e s and \e t are in the same bisimulation equivalence class;
     128             :     *  \retval false otherwise. */
     129             :     bool in_same_probabilistic_class_grv(const std::size_t s, const std::size_t t)
     130             :     {
     131             :       return get_eq_probabilistic_class(s) == get_eq_probabilistic_class(t);
     132             :     }
     133             : 
     134             : 
     135             :   protected:
     136             : 
     137             :     // --------------- BEGIN DECLARATION OF DATA TYPES ---------------------------------------------------------------
     138             :     
     139             :     typedef std::size_t block_key_type;
     140             :     typedef std::size_t constellation_key_type;
     141             :     typedef std::size_t transition_key_type;
     142             :     typedef std::size_t state_key_type;
     143             :     typedef std::size_t label_type;
     144             :     // typedef probabilistic_arbitrary_precision_fraction probability_label_type;
     145             :     typedef typename LTS_TYPE::probabilistic_state_t::probability_t probability_label_type;
     146             :     // typedef probabilistic_arbitrary_precision_fraction probability_fraction_type;
     147             :     typedef typename LTS_TYPE::probabilistic_state_t::probability_t probability_fraction_type;
     148             : 
     149             :     struct action_transition_type : public embedded_list_node <action_transition_type>
     150             :     {
     151             :       state_key_type from;
     152             :       label_type label;
     153             :       state_key_type to;
     154             :       std::size_t* state_to_constellation_count_ptr;
     155             :     };
     156             : 
     157        1144 :     struct probabilistic_transition_type : public embedded_list_node < probabilistic_transition_type >
     158             :     {
     159             :       state_key_type from;
     160             :       probability_label_type label;
     161             :       state_key_type to;
     162             :     };
     163             : 
     164         604 :     struct action_state_type : public embedded_list_node < action_state_type >
     165             :     {
     166             :       block_key_type parent_block;
     167             :       std::vector<probabilistic_transition_type*> incoming_transitions;
     168             : 
     169             :       // Temporary
     170             :       bool mark_state;
     171             :       std::size_t residual_transition_cnt;
     172             :       std::size_t* transition_count_ptr;
     173             :     };
     174             : 
     175         356 :     struct probabilistic_state_type : public embedded_list_node < probabilistic_state_type >
     176             :     {
     177             :       block_key_type parent_block;
     178             :       std::vector<action_transition_type*> incoming_transitions;
     179             : 
     180             :       // Temporary.
     181             :       bool mark_state;
     182             :       probability_label_type cumulative_probability;
     183             :     };
     184             : 
     185             :     // Prototype.
     186             :     struct action_mark_type;
     187             : 
     188             :     struct action_block_type : public embedded_list_node <action_block_type>
     189             :     {
     190             :       constellation_key_type parent_constellation;
     191             :       embedded_list<action_state_type> states;
     192             :       embedded_list<probabilistic_transition_type> incoming_probabilistic_transitions;
     193             :       action_mark_type* marking;  // This value is nullptr if the block is not marked.
     194             : 
     195          42 :       action_block_type() : marking(nullptr){}
     196             :     };
     197             : 
     198             :     struct action_mark_type
     199             :     {
     200             :       action_block_type* action_block;
     201             :       embedded_list<action_state_type> left;
     202             :       embedded_list<action_state_type> middle;
     203             :       embedded_list<action_state_type> right;
     204             :       embedded_list<action_state_type>* large_block_ptr;
     205             : 
     206          45 :       action_mark_type(action_block_type& B) 
     207             :        : action_block(&B), 
     208          45 :          large_block_ptr(nullptr)
     209          45 :       {}
     210             :     };
     211             : 
     212             :     // Prototype
     213             :     struct probabilistic_mark_type;
     214             : 
     215             :     struct probabilistic_block_type : public embedded_list_node <probabilistic_block_type>
     216             :     {
     217             :       constellation_key_type parent_constellation;
     218             :       embedded_list<probabilistic_state_type> states;
     219             :       probabilistic_mark_type* marking;
     220             : 
     221             :       // a probabilistic block has incoming action transitions ordered by label
     222             :       embedded_list<action_transition_type> incoming_action_transitions;
     223             : 
     224          31 :       probabilistic_block_type() : marking(nullptr){}
     225             :     };
     226             : 
     227          52 :     struct probabilistic_mark_type
     228             :     {
     229             :       probabilistic_block_type* probabilistic_block;
     230             :       embedded_list<probabilistic_state_type> left;
     231             :       std::vector< embedded_list<probabilistic_state_type> > middle;
     232             :       embedded_list<probabilistic_state_type> right;
     233             :       embedded_list<probabilistic_state_type>* large_block_ptr;
     234             : 
     235          52 :       probabilistic_mark_type(probabilistic_block_type& B) : probabilistic_block(&B), large_block_ptr(nullptr) {}
     236             :     };
     237             : 
     238          42 :     struct action_constellation_type 
     239             :     {
     240             :       embedded_list<action_block_type> blocks;
     241             :       std::size_t number_of_states;    // number of states in this constellation.
     242             :     }; 
     243             :     
     244          31 :     struct probabilistic_constellation_type 
     245             :     {
     246             :       embedded_list<probabilistic_block_type> blocks;
     247             :       std::size_t number_of_states;    // number of states in this constellation.
     248             :     };
     249             : 
     250             :     // --------------- END DECLARATION OF DATA TYPES ---------------------------------------------------------------
     251             : 
     252             :     // The class below is used to group transitions on action labels in linear space and time.
     253             :     // This makes use of the fact that action labels have a limited range, smaller than the number of transitions.
     254          14 :     class transitions_per_label_t
     255             :     {
     256             :       protected:
     257             :         // This is a vector that contains transitions with the same label at each entry.
     258             :         std::vector< embedded_list<action_transition_type> > m_transitions_per_label;
     259             :         // This stack indicates which positions in the vector above are occupied for efficient retrieval.
     260             :         std::stack<label_type> m_occupancy_indicator;
     261             :         
     262         562 :         void add_single_transition(action_transition_type& t) 
     263             :         {
     264         562 :           assert(t.label<m_transitions_per_label.size());
     265         562 :           if (m_transitions_per_label[t.label].size()==0)
     266             :           {
     267          44 :             m_occupancy_indicator.push(t.label);
     268             :           }
     269         562 :           m_transitions_per_label[t.label].push_back(t);
     270         562 :         }
     271             : 
     272             :       public:
     273             :         /* set the size of the vector m_transitions_per_label */
     274           7 :         void initialize(const std::size_t number_of_labels)
     275             :         { 
     276           7 :           m_transitions_per_label=std::vector< embedded_list<action_transition_type> >(number_of_labels);
     277           7 :         }
     278             : 
     279          14 :         const std::vector< embedded_list<action_transition_type> >& transitions() const
     280             :         {
     281          14 :           return m_transitions_per_label;
     282             :         }
     283             :         
     284             :         /* This function adds the transitions per label in order to the initial probabilistic block 
     285             :            and resets the occupancy array back to empty */
     286          75 :         void add_grouped_transitions_to_block(probabilistic_block_type& block)
     287             :         {
     288         119 :           while (!m_occupancy_indicator.empty())
     289             :           {
     290          44 :             const label_type action=m_occupancy_indicator.top();
     291          44 :             m_occupancy_indicator.pop();
     292             :             
     293             :             // The next operation resets m_transitions_per_label[action] to empty.
     294          44 :             assert(action<m_transitions_per_label.size());
     295          44 :             block.incoming_action_transitions.append(m_transitions_per_label[action]);
     296             :           } 
     297          31 :         }
     298             : 
     299          87 :         void move_incoming_transitions(probabilistic_state_type s, embedded_list<action_transition_type>& transition_list_with_t)
     300             :         {
     301         357 :           for(action_transition_type* t_ptr: s.incoming_transitions)
     302             :           {
     303         270 :             transition_list_with_t.erase(*t_ptr);
     304         270 :             add_single_transition(*t_ptr);
     305             :           }
     306          87 :         }
     307             : 
     308           7 :         void add_transitions(std::vector<action_transition_type>& transitions)
     309             :         {
     310         299 :           for(action_transition_type& t: transitions)
     311             :           {
     312         292 :             add_single_transition(t);
     313             :           }
     314           7 :         }
     315             :     };
     316             : 
     317             :     // The basic stores for all elementary data structures. The deque's are used intentionally
     318             :     // as there are pointers to their content. 
     319             :     std::vector<action_transition_type> action_transitions;
     320             :     std::deque<probabilistic_transition_type> probabilistic_transitions;
     321             :     std::vector<action_state_type> action_states;
     322             :     std::vector<probabilistic_state_type> probabilistic_states;
     323             :     std::deque<action_block_type> action_blocks;
     324             :     std::deque<probabilistic_block_type> probabilistic_blocks;
     325             :     std::deque<action_constellation_type> action_constellations;
     326             :     std::deque<probabilistic_constellation_type> probabilistic_constellations;
     327             : 
     328             :     // The storage to store the state_to_constellation counts for each transition. Transition refer with
     329             :     // a pointer to the elements in this deque. 
     330             :     std::deque<std::size_t> state_to_constellation_count;
     331             : 
     332             :     // The lists below contains all the non trivial constellations.
     333             :     std::stack<action_constellation_type*> non_trivial_action_constellations;
     334             :     std::stack<probabilistic_constellation_type*> non_trivial_probabilistic_constellations;
     335             :     
     336             :     // temporary data structures. declared here to prevent redeclaring these too often.
     337             :     std::deque<action_mark_type> marked_action_blocks;
     338             :     std::deque<probabilistic_mark_type> marked_probabilistic_blocks;
     339             :     std::vector< std::pair<probability_label_type, probabilistic_state_type*> > grouped_states_per_probability_in_block;
     340             :     
     341             :     // The following is a temporary data structure used to group incoming transitions on labels, which is declared
     342             :     // globally to avoid declaring it repeatedly which is time consuming.
     343             :     transitions_per_label_t transitions_per_label;
     344             : 
     345             : 
     346             :     LTS_TYPE& aut;
     347             : 
     348          49 :     bool check_data_structure()
     349             :     {
     350             :       // Check whether the constellation count in action transitions is ok. 
     351        3762 :       for(const action_transition_type& t: action_transitions)
     352             :       {
     353        3713 :         std::size_t constellation=probabilistic_blocks[probabilistic_states[t.to].parent_block].parent_constellation;
     354        3713 :         std::size_t count_state_to_constellation=0;
     355             :         
     356      814124 :         for(const action_transition_type& t1: action_transitions)
     357             :         {
     358     1624603 :           if (t.from==t1.from &&
     359      814168 :               t.label==t1.label &&
     360        3757 :               constellation==probabilistic_blocks[probabilistic_states[t1.to].parent_block].parent_constellation)
     361             :           {
     362        3741 :             count_state_to_constellation++;
     363             :           }
     364             :         }
     365        3713 :         if (count_state_to_constellation!=*t.state_to_constellation_count_ptr)
     366             :         {
     367           0 :           mCRL2log(log::error) << "Transition " << t.from << "--" << t.label << "->" << t.to << " has inconsistent constellation_count: " <<
     368           0 :                                 *t.state_to_constellation_count_ptr << ". Should be " << count_state_to_constellation << ".\n";
     369           0 :           return false;
     370             :                                   
     371             :         }
     372             :       }
     373             : 
     374             :       // Check whether the number of states in an action constellation are correct.
     375         258 :       for(const action_constellation_type& c: action_constellations)
     376             :       {
     377         209 :         std::size_t counted_states=0;
     378         503 :         for(const action_block_type& b: c.blocks)
     379             :         {
     380         294 :           counted_states=counted_states+b.states.size();
     381             :         }
     382         209 :         assert(counted_states==c.number_of_states);  // Number of states in this action constellation does not match the number of states in its blocks.
     383             :       }
     384             : 
     385             :       // Check whether the number of states in a probabilistic constellation are correct.
     386         234 :       for(const probabilistic_constellation_type& c: probabilistic_constellations)
     387             :       {
     388         185 :         std::size_t counted_states=0;
     389         383 :         for(const probabilistic_block_type& b: c.blocks)
     390             :         {
     391         198 :           counted_states=counted_states+b.states.size();
     392             :         }
     393         185 :         assert(counted_states==c.number_of_states); // Number of states in this probabilistic constellation does not match the number of states in its blocks.
     394             :       }
     395             : 
     396         343 :       for(const action_block_type& b: action_blocks)
     397             :       {
     398         294 :         assert(b.states.size()>0); // Action block contains no states.
     399             : 
     400         294 :         assert(b.marking==nullptr); // Action block's marking must be a null ptr.
     401             :       }
     402             : 
     403         247 :       for(const probabilistic_block_type& b: probabilistic_blocks)
     404             :       {
     405         198 :         assert(b.states.size()>0); // Probabilistic block contains no states.
     406             : 
     407         198 :         assert(b.marking==nullptr); // Probabilistic block's marking must be a null ptr.
     408             :       }
     409             : 
     410          49 :       return true;
     411             :     }
     412             : 
     413             :     void print_structure(const std::string& info)
     414             :     {
     415             :       std::cerr << info << " ---------------------------------------------------------------------- \n";
     416             :       std::cerr << "Number of action blocks " << action_blocks.size() << "\n";
     417             :       std::cerr << "Number of probabilistic blocks " << probabilistic_blocks.size() << "\n";
     418             :       std::cerr << "Number of action constellations " << action_constellations.size() << "\n";
     419             :       std::cerr << "Number of probabilistic constellations " << probabilistic_constellations.size() << "\n";
     420             :       for(const action_block_type b: action_blocks)
     421             :       {
     422             :         std::cerr << "ACTION BLOCK INFO ------------------------\n";
     423             :         std::cerr << "PARENT CONSTELLATION " << b.parent_constellation << "\n";
     424             :         std::cerr << "NR STATES " << b.states.size() << "\n";
     425             :         for(const probabilistic_transition_type t: b.incoming_probabilistic_transitions)
     426             :         {
     427             :           std::cerr << "INCOMING TRANS " << t.from << " --" << t.label << "-> " << t.to << "\n";
     428             :         }
     429             :       }
     430             : 
     431             :       for(const probabilistic_block_type b: probabilistic_blocks)
     432             :       {
     433             :         std::cerr << "probabilistic BLOCK INFO ------------------------\n";
     434             :         std::cerr << "PARENT CONSTELLATION " << b.parent_constellation << "\n";
     435             :         std::cerr << "NR STATES " << b.states.size() << "\n";
     436             :         for(const action_transition_type t: b.incoming_action_transitions)
     437             :         {
     438             :           std::cerr << "INCOMING TRANS " << t.from << " --" << t.label << "-> " << t.to << "\n";
     439             :         }
     440             :       }
     441             : 
     442             :     }
     443             : 
     444             :     /** Creates the initial partition.
     445             :     *  \details The blocks are initially partitioned based on the actions that can perform. 
     446             :     */
     447           7 :     void create_initial_partition(void)
     448             :     {
     449           7 :       transitions_per_label.initialize(aut.num_action_labels());
     450             :       
     451             :       // Preprocessing initialization. First we have to initialise the action/probabilistic states and
     452             :       // transitions.
     453           7 :       preprocessing_stage();
     454             : 
     455             :       // Add action transitions to its respective list grouped by label.
     456           7 :       transitions_per_label.add_transitions(action_transitions);
     457             : 
     458             :       // We start with all the action states in one block and then we refine this block
     459             :       // according to the outgoing transitions.
     460           7 :       action_block_type initial_action_block;
     461             : 
     462             :       // Link all the action states together to the initial block
     463         309 :       for (action_state_type& s: action_states)
     464             :       {
     465         302 :         s.parent_block = 0; // Initial block has number 0. 
     466         302 :         initial_action_block.states.push_back(s);
     467             :       }
     468           7 :       assert(aut.num_states()==initial_action_block.states.size());
     469             : 
     470             :       // Add the linked states to the list of states in the initial block
     471           7 :       action_blocks.push_back(initial_action_block);
     472             : 
     473             :       // Refine the initial action block based on the outgoing transitions.
     474             :       // This corresponds to line 5 of Algorithm 2 in [GRV].
     475           7 :       refine_initial_action_block(transitions_per_label.transitions());
     476             : 
     477             :       // Initialise the probabilistic block. Initally, there is only one block of probabilistic states.
     478           7 :       probabilistic_blocks.emplace_back();
     479             : 
     480           7 :       probabilistic_block_type& initial_probabilistic_block=probabilistic_blocks.back();
     481           7 :       initial_probabilistic_block.parent_constellation = 0;
     482             : 
     483             :       // Link all the probabilistic states together to the initial block
     484          98 :       for (probabilistic_state_type& s : probabilistic_states)
     485             :       {
     486          91 :         s.parent_block = 0; // The initial block has number zero.
     487          91 :         initial_probabilistic_block.states.push_back(s);
     488             :       }
     489           7 :       assert(aut.num_probabilistic_states()==initial_probabilistic_block.states.size());
     490             :       
     491             :       // Initialise the probabilistic and action constellations; they will contain
     492             :       // all the blocks.
     493           7 :       probabilistic_constellation_type initial_probabilistic_const;
     494           7 :       initial_probabilistic_const.number_of_states = aut.num_probabilistic_states();
     495             : 
     496             :       // Initially there is only one block in the probabilistic constellation.
     497             :       // initial_probabilistic_const.blocks.init(&probabilistic_blocks.front(), &probabilistic_blocks.front(), 1);
     498           7 :       initial_probabilistic_const.blocks.push_back(probabilistic_blocks.front());
     499           7 :       probabilistic_constellations.push_back(initial_probabilistic_const);
     500             : 
     501             :       // Initialise the initial action constellation.
     502           7 :       action_constellations.emplace_back();
     503           7 :       action_constellation_type& initial_action_const=action_constellations.back();
     504             : 
     505           7 :       initial_action_const.number_of_states = aut.num_states();
     506             : 
     507             :       // Construct the list of action blocks by linking them together.
     508          30 :       for(action_block_type& b : action_blocks)
     509             :       {
     510          23 :         b.parent_constellation = 0; // The initial constellation has number 0;
     511          23 :         initial_action_const.blocks.push_back(b);
     512             :       }
     513             : 
     514             : //-----------------------------------------------------------------------------
     515             :       // state_to_const_count_temp is used to keep track of the block to constellation count per label of each state.
     516          14 :       std::vector<std::size_t*> new_count_ptr(aut.num_states(),nullptr);
     517             :       
     518          31 :       for (const embedded_list<action_transition_type>& at_list_per_label : transitions_per_label.transitions())
     519             :       {
     520             :         // Create a new position in state_to_constellation_count if no such count exists for the parent block of the transition. 
     521             :         // Assign this position to t.state_to_constellation_count_ptr and increment its count.
     522         316 :         for(action_transition_type& t: at_list_per_label)
     523             :         {
     524         292 :           assert(t.from<new_count_ptr.size());
     525         292 :           if (new_count_ptr[t.from]==nullptr)
     526             :           {
     527         288 :             state_to_constellation_count.push_back(0);
     528         288 :             new_count_ptr[t.from] = &state_to_constellation_count.back();
     529             :           }
     530         292 :           t.state_to_constellation_count_ptr = new_count_ptr[t.from];
     531         292 :           (*new_count_ptr[t.from])++;
     532             :         }
     533             :     
     534             :         // Reset all the variables used to prepare to next iteration.
     535         316 :         for(const action_transition_type& t: at_list_per_label)
     536             :         {
     537         292 :           new_count_ptr[t.from] = nullptr;
     538             :         }
     539             :       } 
     540             : 
     541             : //-----------------------------------------------------------------------------
     542             : 
     543             :       // Since the transitions are already grouped by label, add them to the
     544             :       // initial probabilistic block as incoming transitions.
     545           7 :       transitions_per_label.add_grouped_transitions_to_block(initial_probabilistic_block);
     546             : 
     547             :       // Initialise the incoming probabilistic transitions for all action blocks. To that end,
     548             :       // iterate over all probabilistic transitions and add it to its respective destination block.
     549         293 :       for(probabilistic_transition_type& t : probabilistic_transitions)
     550             :       {
     551         286 :         action_state_type& s = action_states[t.to];
     552         286 :         action_block_type& block = action_blocks[s.parent_block];
     553         286 :         block.incoming_probabilistic_transitions.push_back(t);
     554             :       }
     555             : 
     556           7 :       if (initial_action_const.blocks.size()>1) 
     557             :       {
     558           7 :         non_trivial_action_constellations.push(&initial_action_const);
     559             :       }
     560             : 
     561             : // print_structure("After init");
     562           7 :       assert(check_data_structure());
     563           7 :     }
     564             : 
     565             :     /* This function performs the preprocessing stage to prepare to apply the algorithm.
     566             :        It also initialises the action and probabilistic states and transitions.  */
     567           7 :     void preprocessing_stage()
     568             :     {
     569             :       // Allocate space for states and transitions
     570           7 :       action_states.resize(aut.num_states());
     571           7 :       probabilistic_states.resize(aut.num_probabilistic_states());
     572           7 :       action_transitions.resize(aut.num_transitions());
     573             : 
     574             :       // Initialise the action transitions
     575           7 :       transition_key_type t_key = 0;
     576         299 :       for (const transition& t : aut.get_transitions())
     577             :       {
     578         292 :         action_transition_type& at = action_transitions[t_key];
     579         292 :         at.from = t.from();
     580         292 :         at.label = t.label();
     581         292 :         at.to = t.to();
     582         292 :         at.state_to_constellation_count_ptr = nullptr;
     583             : 
     584             :         // save incoming transition in state
     585         292 :         probabilistic_states[at.to].incoming_transitions.push_back(&at);
     586             : 
     587         292 :         t_key++;
     588             :       }
     589             : 
     590             :       // Initialise the probabilistic transitions. To this end, we have to iterate over
     591             :       // all probabilistic states.
     592          98 :       for (std::size_t i = 0; i < aut.num_probabilistic_states(); i++)
     593             :       {
     594          91 :         const typename LTS_TYPE::probabilistic_state_t& ps = aut.probabilistic_state(i);
     595             : 
     596             :         // for (const lts_aut_base::state_probability_pair& sp_pair : ps)
     597         377 :         for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : ps)
     598             :         {
     599         572 :           probabilistic_transition_type pt;
     600         286 :           pt.from = i;
     601         286 :           pt.label = sp_pair.probability();
     602         286 :           pt.to = sp_pair.state();
     603         286 :           probabilistic_transitions.push_back(pt);
     604             : 
     605             :           // save incoming transition in state
     606         286 :           action_states[pt.to].incoming_transitions.push_back(&probabilistic_transitions.back());
     607             :         }
     608             :       }
     609             : 
     610             :       // End of preprocessing.
     611           7 :     }
     612             : 
     613             :     /* Refine the initial block according to its outgoing transitions.
     614             :     */
     615           7 :     void refine_initial_action_block(const std::vector< embedded_list<action_transition_type> >& transitions_per_label)
     616             :     {
     617             :       // Iterate over all transitions ordered by label, and refine the block.
     618          31 :       for (const embedded_list<action_transition_type>& t_list : transitions_per_label)
     619             :       {
     620          24 :         marked_action_blocks.clear();
     621             :         // The line below garbage collects marked_action_blocks to avoid covering too much memory continuously;
     622          24 :         static std::size_t count=0; if (count++ == 1000) { marked_action_blocks.shrink_to_fit(); count=0; }
     623             : 
     624         316 :         for(const action_transition_type& t: t_list)
     625             :         {
     626         292 :           action_state_type& s = action_states[t.from];
     627         292 :           assert(s.parent_block<action_blocks.size());
     628         292 :           action_block_type& parent_block = action_blocks[s.parent_block];
     629             : 
     630             :           // Move state s to marked states if not already added.
     631         292 :           if (false == s.mark_state)
     632             :           {
     633             :             // Add parent block to the list of marked blocks if not yet added
     634         288 :             if (parent_block.marking==nullptr) 
     635             :             {
     636          18 :               marked_action_blocks.emplace_back(parent_block);
     637          18 :               parent_block.marking=&marked_action_blocks.back();
     638             :             }
     639             : 
     640         288 :             move_list_element_back<action_state_type>(s, parent_block.states, parent_block.marking->left);
     641         288 :             s.mark_state = true;
     642             :           }
     643             :         }
     644             :         
     645             :         // Split the marked blocks.
     646          42 :         for (action_mark_type& block_marking: marked_action_blocks)
     647             :         {
     648          18 :           if (0 == block_marking.action_block->states.size())
     649             :           {
     650             :             // If all states in the block are marked, then return all marked states to the block.
     651           2 :             block_marking.action_block->states = block_marking.left;
     652             :           }
     653             :           else
     654             :           {
     655             :             // Split the block if not all states are marked.
     656          16 :             action_blocks.emplace_back();
     657          16 :             action_block_type& new_block=action_blocks.back();
     658          16 :             new_block.states = block_marking.left;
     659             : 
     660             :             // Init parent block of each state in new block.
     661         254 :             for(action_state_type& s: new_block.states)
     662             :             {
     663         238 :               s.parent_block = action_blocks.size()-1; 
     664             :             }
     665             : 
     666             :           }
     667             :           
     668             :           // clean mark list
     669          18 :           block_marking.left.clear();
     670          18 :           block_marking.action_block->marking=nullptr;
     671             : 
     672             :         }
     673             : 
     674             :         // Clean the marked states.
     675         316 :         for(const action_transition_type& t: t_list)
     676             :         {
     677         292 :           action_states[t.from].mark_state = false;
     678             :         }
     679             :       }
     680             : 
     681           7 :     }
     682             : 
     683             :     /* Move an element of a list to the back of another list.
     684             :     */
     685             :     template <typename LIST_ELEMENT>
     686        1134 :     void move_list_element_back(LIST_ELEMENT& s, embedded_list<LIST_ELEMENT>& source_list, embedded_list<LIST_ELEMENT>& dest_list)
     687             :     {
     688        1134 :       source_list.erase(s);
     689        1134 :       dest_list.push_back(s);
     690        1134 :     }
     691             : 
     692             :     /** \brief Move an element of a list to the front of another the list.
     693             :     *  \details
     694             :     */
     695             :     template<typename LIST_ELEMENT>
     696             :     void move_list_element_front(LIST_ELEMENT& s, embedded_list<LIST_ELEMENT>& source_list, embedded_list<LIST_ELEMENT>& dest_list)
     697             :     {
     698             :       source_list.erase(s);
     699             :       dest_list.push_front(s);
     700             :     }
     701             : 
     702             :     /** \brief Refine partition until it becomes stable.
     703             :     *  \details
     704             :     */
     705          42 :     void refine_partition_until_it_becomes_stable(void)
     706             :     {
     707             : 
     708             :       // Refine until all the constellations are trivial.
     709          77 :       while (!non_trivial_probabilistic_constellations.empty() || !non_trivial_action_constellations.empty())
     710             :       {
     711          35 :         assert(check_data_structure());
     712             : 
     713             :         // Refine probabilistic blocks if a non-trivial action constellation exists.
     714          35 :         if (!non_trivial_action_constellations.empty())
     715             :         {
     716          35 :           action_constellation_type* non_trivial_action_const = non_trivial_action_constellations.top();
     717          35 :           non_trivial_action_constellations.pop();
     718          35 :           assert(non_trivial_action_const->blocks.size()>=2);
     719             : 
     720             : // print_structure("REFINE I");
     721             :           // Choose splitter block Bc of a non-trivial constellation C, such that |Bc| <= 1/2|C|.
     722             :           // And also split constellation C into BC and C\BC in the set of constellations.
     723          35 :           action_block_type* Bc_ptr = choose_action_splitter(non_trivial_action_const);
     724             : 
     725             :           // Derive the left, right and middle sets from mark function.
     726          35 :           marked_probabilistic_blocks.clear();
     727             :           // The line below garbage collects marked_action_blocks to avoid covering too much memory continuously;
     728          35 :           static std::size_t count=0; if (count++ == 1000) { marked_probabilistic_blocks.shrink_to_fit(); count=0; }
     729             : 
     730          35 :           mark_probabilistic(*Bc_ptr, marked_probabilistic_blocks);
     731             : 
     732             :           // Split every marked probabilistic block based on left, middle and right.
     733          87 :           for (probabilistic_mark_type& B : marked_probabilistic_blocks)
     734             :           {
     735             :             // We must know whether the current constellation is already on the stack.
     736          52 :             bool already_on_non_trivial_constellations_stack = probabilistic_constellations[B.probabilistic_block->parent_constellation].blocks.size()>1; 
     737             : 
     738             :             // First return the largest of left, middle or right to the states of current processed block.
     739          52 :             B.probabilistic_block->states = *B.large_block_ptr;
     740          52 :             B.large_block_ptr->clear();
     741             : 
     742             :             // Split left set of the block to another block if left has states and it is not
     743             :             // the largest block.
     744          52 :             if (B.left.size() > 0)
     745             :             {
     746          10 :               split_probabilistic_block(*B.probabilistic_block, B.left);
     747             :             }
     748             : 
     749             :             // Split right set of the block to another block if right has states and it is not
     750             :             // the largest block.
     751          52 :             if (B.right.size() > 0)
     752             :             {
     753           1 :               split_probabilistic_block(*B.probabilistic_block, B.right);
     754             :             }
     755             : 
     756             :             // Iterate over all middle sets. Split middle sets of the current block to another block if 
     757             :             //  the middle set has states and it is not the largest block.
     758         134 :             for (embedded_list<probabilistic_state_type>& middle : B.middle)
     759             :             {
     760          82 :               if (middle.size() > 0)
     761             :               {
     762          13 :                 split_probabilistic_block(*B.probabilistic_block, middle);
     763             :               }
     764             :             }
     765             : 
     766             :             // Move the parent constellation of the current block to the front of the
     767             :             // constellation list if it became unstable.
     768          52 :             if (!already_on_non_trivial_constellations_stack &&  probabilistic_constellations[B.probabilistic_block->parent_constellation].blocks.size()>1)
     769             :             {
     770          18 :               probabilistic_constellation_type& parent_const = probabilistic_constellations[B.probabilistic_block->parent_constellation];
     771          18 :               assert(parent_const.blocks.size()>1);
     772          18 :               non_trivial_probabilistic_constellations.push(&parent_const);
     773             :             }
     774             : 
     775             :             // Reset middle vector to prepare for the next mark process
     776          52 :             B.middle.clear();
     777             :           }
     778             :         }
     779             : 
     780             :         // Refine action blocks if a non-trivial probabilistic constellation exists.
     781          35 :         if (!non_trivial_probabilistic_constellations.empty())
     782             :         {
     783             : // print_structure("REFINE II");
     784             : 
     785          24 :           probabilistic_constellation_type* non_trivial_probabilistic_const = non_trivial_probabilistic_constellations.top();
     786          24 :           non_trivial_probabilistic_constellations.pop();
     787          24 :           assert(non_trivial_probabilistic_const->blocks.size()>=2);
     788             :           // Choose splitter block Bc of a non-trivial constellation C, such that |Bc| <= 1/2|C|.
     789             :           // And also split constellation C into BC and C\BC in the set of constellations.
     790          24 :           probabilistic_block_type* Bc_ptr = choose_probabilistic_splitter(non_trivial_probabilistic_const);
     791             :           
     792             :           // For all incoming labeled "a" transitions of each state in BC call the mark function and split the blocks.
     793          51 :           for (typename embedded_list<action_transition_type>::iterator i=Bc_ptr->incoming_action_transitions.begin(); 
     794          51 :                         i!=Bc_ptr->incoming_action_transitions.end() ;  )
     795             :           {
     796             :             // Derive the left, right and middle sets from mark function based on the incoming labeled "a" transitions.
     797          27 :             const label_type a = i->label;
     798          27 :             marked_action_blocks.clear();
     799          27 :             mark_action(marked_action_blocks, a, i, Bc_ptr->incoming_action_transitions.end());  // The iterator i is implicitly increased 
     800             :                                                                                           // to the position in the list with the next action.
     801             : 
     802             :             // Split every marked probabilistic block based on left, middle and right.
     803          54 :             for (action_mark_type& B : marked_action_blocks)
     804             :             {
     805             :               // We must know whether the current constellation is already on the stack.
     806          27 :               bool already_on_non_trivial_constellations_stack = action_constellations[B.action_block->parent_constellation].blocks.size()>1; 
     807             : 
     808             :               // First return the largest of left, middle or right to the states of current processed block.
     809          27 :               B.action_block->states = *B.large_block_ptr;
     810          27 :               B.large_block_ptr->clear();
     811             : 
     812             :               // Split left set of the block to another block if left has states and it is not the largest block.
     813          27 :               if (B.left.size() > 0)
     814             :               {
     815          16 :                 split_action_block(*B.action_block, B.left);
     816             :               }
     817             : 
     818             :               // Split right set of the block to another block if right has states and it is not the largest block.
     819          27 :               if (B.right.size() > 0)
     820             :               {
     821           2 :                 split_action_block(*B.action_block, B.right);
     822             :               }
     823             : 
     824             :               // Split middle set of the block to another block if middle has states and it is not
     825             :               // the largest block.
     826          27 :               if (B.middle.size() > 0)
     827             :               {
     828           1 :                 split_action_block(*B.action_block, B.middle);
     829             :               }
     830             : 
     831             :               // Move the parent constellation of the current block to the front of the
     832             :               // constellation list if it became unstable.
     833          27 :               if (!already_on_non_trivial_constellations_stack && action_constellations[B.action_block->parent_constellation].blocks.size()>1)
     834             :               {
     835          10 :                 action_constellation_type& parent_const = action_constellations[B.action_block->parent_constellation];
     836          10 :                 assert(parent_const.blocks.size()>1);
     837          10 :                 non_trivial_action_constellations.push(&parent_const);
     838             :               }
     839             : 
     840             :             }
     841             :           }
     842             :         }
     843             :       }
     844             :       // print_structure("END REFINE");
     845           7 :       assert(check_data_structure());
     846           7 :     }
     847             : 
     848             :     /** \brief Split a probabilistic block.
     849             :     *  \details Creates another block containing the states specified in states_of_new_block. It adds the new block
     850             :     *           to the same constellation as the current block to split.
     851             :     */
     852          24 :     void split_probabilistic_block(probabilistic_block_type& block_to_split, embedded_list<probabilistic_state_type>& states_of_new_block)
     853             :     {
     854             :       // First create the new block to be allocated, and initialise its parameters
     855          24 :       probabilistic_blocks.emplace_back();
     856          24 :       probabilistic_block_type& new_block=probabilistic_blocks.back();
     857             :       
     858          24 :       new_block.parent_constellation = block_to_split.parent_constellation; // The new block is in the same constellation as B
     859          24 :       new_block.states = states_of_new_block;
     860          24 :       states_of_new_block.clear();
     861             : 
     862             :       // Add the incoming action transition of the new block. To this end, iterate over all
     863             :       // states in the new block and add the incoming transitions of each state to the
     864             :       // incoming transitions of the new block. Also keep track of the labels of the incoming
     865             :       // transitions.
     866         111 :       for(probabilistic_state_type& s: new_block.states)
     867             :       {
     868             :         // Update the parent block of the state
     869          87 :         s.parent_block = probabilistic_blocks.size()-1; 
     870          87 :         transitions_per_label.move_incoming_transitions(s,block_to_split.incoming_action_transitions);  
     871             :       }
     872             : 
     873             :       // Since the transitions are already grouped by label, add them to the
     874             :       // initial probabilistic block as incoming transitions.
     875          24 :       transitions_per_label.add_grouped_transitions_to_block(new_block);
     876             : 
     877             :       // Add the new block to the back of the list of blocks in the parent constellation.
     878          24 :       probabilistic_constellation_type& parent_const = probabilistic_constellations[new_block.parent_constellation];
     879             : 
     880          24 :       parent_const.blocks.push_back(probabilistic_blocks.back());
     881          24 :     }
     882             : 
     883             :     /** \brief Split an action block.
     884             :     *  \details Creates another block containing the states specified in states_of_new_block. It adds the new block
     885             :     *           to the same constellation as the current block to split.
     886             :     */
     887          19 :     void split_action_block(action_block_type& block_to_split, embedded_list<action_state_type>& states_of_new_block)
     888             :     {
     889             :       // First create the new block to be allocated, and initialise its parameters
     890          19 :       action_blocks.emplace_back();
     891          19 :       action_block_type& new_block=action_blocks.back();
     892             : 
     893          19 :       new_block.parent_constellation = block_to_split.parent_constellation; // The new block is in the same constellation as block to split
     894          19 :       new_block.states = states_of_new_block;
     895          19 :       states_of_new_block.clear();
     896             : 
     897             :       // Add the incoming action transition of the new block. To this end, iterate over all
     898             :       // states in the new block and add the incoming transitions of each state to the
     899             :       // incoming transitions of the new block.
     900         180 :       for(action_state_type& s: new_block.states)
     901             :       {
     902             :         // Update the parent block of the state
     903         161 :         s.parent_block = action_blocks.size()-1;   
     904             : 
     905             :         // Iterate over all incoming transitions of the state, to add them to the new block
     906         319 :         for (probabilistic_transition_type* t : s.incoming_transitions)
     907             :         {
     908             :           // Move transition from list of transitions of previous block to new block
     909         158 :           move_list_element_back((*t), block_to_split.incoming_probabilistic_transitions,
     910             :             new_block.incoming_probabilistic_transitions);
     911             :         }
     912             :       }
     913             : 
     914             :       // Add the new block to the back of the list of blocks in the parent constellation.
     915          19 :       action_constellation_type& parent_const = action_constellations[new_block.parent_constellation];
     916             : 
     917          19 :       parent_const.blocks.push_back(action_blocks.back());
     918          19 :     }
     919             : 
     920             :     /** \brief Gives the probabilistic blocks that are marked by block Bc.
     921             :     *  \details Derives the left, middle and rigth sets of the marked probabilistic blocks, based on the
     922             :     *           incoming probabilistic transitions in block Bc.
     923             :     */
     924          35 :     void mark_probabilistic(const action_block_type& Bc, std::deque<probabilistic_mark_type>& marked_probabilistic_blocks)
     925             :     {
     926             :       // First, iterate over all incoming transitions of block Bc. Mark the blocks that are reached
     927             :       // and calculate the cumulative probability of the reached state. This is the probability of
     928             :       // a state to reach block Bc.
     929         317 :       for( probabilistic_transition_type& pt: Bc.incoming_probabilistic_transitions)
     930             :       {
     931         282 :         probabilistic_state_type& s = probabilistic_states[pt.from];
     932         282 :         const probability_label_type& p = pt.label;
     933         282 :         probabilistic_block_type& B = probabilistic_blocks[s.parent_block];
     934             : 
     935             :         // If the block was not previously marked, then mark the block and move all states to right
     936         282 :         if (nullptr == B.marking)
     937             :         {
     938          52 :           marked_probabilistic_blocks.emplace_back(B);
     939          52 :           B.marking = &marked_probabilistic_blocks.back();
     940          52 :           B.marking->right = B.states;
     941          52 :           B.states.clear(); 
     942             : 
     943             :           // Also initialise the larger block pointer to the right set and the maximum cumulative
     944             :           // probability of the block to p.
     945          52 :           B.marking->large_block_ptr = &B.marking->right;
     946             :         }
     947             : 
     948             :         // Since state s can reach block Bc, move state s to the left set if not yet added, and mark the state
     949         282 :         if (false == s.mark_state)
     950             :         {
     951             :           // State s is not yet marked. Mark the state and move it to left set. In addition, initialise
     952             :           // its cumulative probability.
     953         208 :           s.mark_state = true;
     954         208 :           s.cumulative_probability = p;
     955         208 :           move_list_element_back<probabilistic_state_type>(s, B.marking->right, B.marking->left);
     956             :         }
     957             :         else 
     958             :         {
     959             :           // State s was already added to left. Just update its cumulative probability.
     960          74 :           s.cumulative_probability = s.cumulative_probability + p;
     961             :         }
     962             :       }
     963             : 
     964             :       // Group all states with the same cumulative probability to construct the middle sets.
     965             :       // To this end, iterate over all marked blocks. For each block, first add all the states
     966             :       // with probability lower than the max_cumulative_probability of the block to the middle set.
     967          87 :       for (probabilistic_mark_type& B : marked_probabilistic_blocks)
     968             :       {
     969             :         // Clear this locally used data structure and reset it so now and then to avoid that it requires
     970             :         // too much data. 
     971          52 :         grouped_states_per_probability_in_block.clear();
     972          52 :         static std::size_t count=0; if (count++ == 1000) { marked_action_blocks.shrink_to_fit(); count=0; }
     973             : 
     974          52 :         embedded_list<probabilistic_state_type> middle_temp=B.left;
     975          52 :         B.left.clear();
     976             : 
     977             :         // First, add all states lower than max_cumulative_probability to the middle set.
     978         260 :         for(typename embedded_list<probabilistic_state_type>::iterator i=middle_temp.begin(); i!=middle_temp.end(); )
     979             :         {
     980         208 :           probabilistic_state_type& s= *i;
     981         208 :           i++; // Increment the iterator here, such that we can change the list. 
     982             : 
     983         208 :           if (s.cumulative_probability == probability_label_type().one()) 
     984             :           {
     985             :             // State s has probability lower than max_cumulative_probability. Add to the middle set.
     986          30 :             move_list_element_back<probabilistic_state_type>((s), middle_temp, B.left);
     987             :           }
     988             : 
     989             :           // Also reset the marked_state variable in the state here, taiking advantage that we
     990             :           // are iterating over all marked states
     991         208 :           s.mark_state = false;
     992             :         }
     993             : 
     994             :         // Add all the states corresponding to the bigger and smaller probability to middle.
     995             :         // Save the remaining states in a vector to sort them later.
     996         230 :         for(probabilistic_state_type& s: middle_temp)
     997             :         {
     998         178 :           grouped_states_per_probability_in_block.emplace_back(s.cumulative_probability, &s);
     999             :         }
    1000             : 
    1001             :         // Sort the probabilities of middle, not including the biggest and smallest probability
    1002          52 :         std::sort(grouped_states_per_probability_in_block.begin(), grouped_states_per_probability_in_block.end());
    1003             :         
    1004             :         // Construct the rest of the middle set based on the grouped probabilities. To this end, 
    1005             :         // traverse all the vector with the grouped states by probability. Store the states with
    1006             :         // the same probability to a new sub-set in middle set. current_probability is used to
    1007             :         // keep track of the probability that is currently being processed.
    1008         104 :         probability_label_type current_probability = probability_label_type().zero();
    1009             : 
    1010          52 :         if (grouped_states_per_probability_in_block.size()>0)
    1011             :         { 
    1012          40 :           B.middle.emplace_back();
    1013         218 :           for (const std::pair<probability_label_type, probabilistic_state_type*>& cumulative_prob_state_pair : grouped_states_per_probability_in_block)
    1014             :           {
    1015         178 :             probabilistic_state_type* s = cumulative_prob_state_pair.second;
    1016         178 :             if (current_probability != cumulative_prob_state_pair.first)
    1017             :             {
    1018             :               // The current state has a different probability as the current probability. Allocate
    1019             :               // another space in the middle to store this state and change the current probability.
    1020          42 :               current_probability = cumulative_prob_state_pair.first;
    1021          42 :               B.middle.emplace_back(); //put empty list at end of B.middle.
    1022             :             }
    1023             : 
    1024         178 :             move_list_element_back<probabilistic_state_type>((*s), middle_temp, B.middle.back());
    1025             :           }
    1026             :         }
    1027             : 
    1028             :         // Now that we have all the states in left, middle and right; we have to find the largest
    1029             :         // set. The large block is initialised to be the right set; hence, we only compare if
    1030             :         // left and middle are larger.
    1031          52 :         if (B.left.size() > B.large_block_ptr->size())
    1032             :         {
    1033           4 :           B.large_block_ptr = &B.left;
    1034             :         }
    1035             : 
    1036             :         // Iterate over all subsets of middle set to see if there is a one that is the largest.
    1037         134 :         for (embedded_list<probabilistic_state_type>& middle_set : B.middle)
    1038             :         {
    1039          82 :           if (middle_set.size() > B.large_block_ptr->size())
    1040             :           {
    1041          30 :             B.large_block_ptr = &middle_set;
    1042             :           }
    1043             :         }
    1044             : 
    1045             :         // Finally, reset the block_is_marked variable of the current block.
    1046          52 :         B.probabilistic_block->marking = nullptr; 
    1047             :       }
    1048          35 :     }
    1049             : 
    1050             :     /** \brief Gives the action blocks that are marked by probabilistic block Bc.
    1051             :     *  \details Derives the left, middle and rigth sets of the marked action blocks, based on the
    1052             :     *           incoming action transitions labeled with "a" in block Bc.
    1053             :     */
    1054          27 :     void mark_action(std::deque<action_mark_type>& marked_action_blocks, 
    1055             :                      const label_type& a, 
    1056             :                      typename embedded_list<action_transition_type>::iterator& action_walker_begin,
    1057             :                      const typename embedded_list<action_transition_type>::iterator action_walker_end)
    1058             :     {
    1059          27 :       assert(action_walker_begin!=action_walker_end && action_walker_begin->label==a);
    1060             : 
    1061             :       // For all incoming transitions with label "a" of block Bc calculate left, middle and right.
    1062             :       // To this end, first move all the states of the block that was reached by traversing the
    1063             :       // transition backwards to its right set, then move all the states that can reach block Bc with 
    1064             :       // an "a" action to left and decrement the residual transition count of the state.
    1065         297 :       for(typename embedded_list<action_transition_type>::iterator action_walker=action_walker_begin; 
    1066         297 :           action_walker!=action_walker_end && action_walker->label==a;  
    1067             :           action_walker++)
    1068             :       {
    1069         270 :         action_transition_type& t= *action_walker;
    1070         270 :         action_state_type& s = action_states[t.from];
    1071         270 :         action_block_type& B = action_blocks[s.parent_block];  
    1072             :         
    1073             :         // If the block was not previously marked, then mark the block and add all states to right.
    1074         270 :         if (nullptr == B.marking)
    1075             :         {
    1076          27 :           marked_action_blocks.emplace_back(B);
    1077          27 :           B.marking = &marked_action_blocks.back();
    1078          27 :           B.marking->right=B.states;
    1079          27 :           B.states.clear();
    1080             :           // Also initialise the larger block pointer to the right set.
    1081          27 :           B.marking->large_block_ptr = &B.marking->right;
    1082             :         }
    1083             : 
    1084             :         // Since state s can reach block Bc, move state s to the left set if not yet added, and mark the state
    1085         270 :         if (false == s.mark_state)
    1086             :         {
    1087             :           // State s is not yet marked. Mark the state and move it to left set. In addition, initialise
    1088             :           // its residual transition count.
    1089         269 :           s.mark_state = true;
    1090         269 :           s.residual_transition_cnt = *t.state_to_constellation_count_ptr;
    1091         269 :           move_list_element_back<action_state_type>(s, B.marking->right, B.marking->left);
    1092             :         }
    1093             : 
    1094         270 :         s.residual_transition_cnt--;
    1095             :       }
    1096             : 
    1097             :       // Now, for all marked blocks, check the residual transition count of all the states in left. If the transition 
    1098             :       // count is zero, it means that the state only can reach block BC. If the transition count is greater than 
    1099             :       // zero, the state has transitions to the other part of the constellation; hence, those states have to be
    1100             :       // moved to middle.
    1101          54 :       for (action_mark_type& B : marked_action_blocks)
    1102             :       {
    1103             :         // Iterate over all left states in B and check whether the state has to be moved to middle.
    1104         296 :         for(typename embedded_list<action_state_type>::iterator i=B.left.begin(); i!=B.left.end(); )
    1105             :         {
    1106         269 :           action_state_type& s= *i; 
    1107         269 :           i++;  // This iterator is incremented here as s will be removed from the list over which iteration takes place.
    1108         269 :           if (s.residual_transition_cnt > 0)
    1109             :           {
    1110             :             // The transition count is greater than zero. Move state to middle set.
    1111           3 :             move_list_element_back<action_state_type>(s, B.left, B.middle);
    1112             :           }
    1113             : 
    1114             :           // Also reset the marked_state variable in the state here, taking advantage that we
    1115             :           // are iterating over all marked states
    1116         269 :           s.mark_state = false;
    1117             :         }
    1118             : 
    1119             :         // Find the largest set.
    1120          27 :         if (B.left.size() > B.large_block_ptr->size())
    1121             :         {
    1122          10 :           B.large_block_ptr = &B.left;
    1123             :         }
    1124          27 :         if (B.middle.size() > B.large_block_ptr->size())
    1125             :         {
    1126           1 :           B.large_block_ptr = &B.middle;
    1127             :         }
    1128             : 
    1129             :         // Finally, reset the block_is_marked variable of the current block.
    1130          27 :         B.action_block->marking = nullptr;
    1131             :       }
    1132             : 
    1133             :       // Update the state_to_constellation_count of each transition. Increment action_walker_begin
    1134             :       // such that it points to the next action after this loop. 
    1135         270 :       for( ;
    1136         297 :           action_walker_begin!=action_walker_end && action_walker_begin->label==a;  
    1137             :           action_walker_begin++)
    1138             :       {
    1139         270 :         action_transition_type& t= *action_walker_begin;
    1140         270 :         action_state_type& s = action_states[t.from];
    1141             : 
    1142             :         // If the residual_transition_cnt is greater than zero, it means that the state
    1143             :         // is in the middle set; hence, the state_to_constellation_count has to be updated.
    1144         270 :         if (s.residual_transition_cnt > 0)
    1145             :         {
    1146           3 :           std::size_t state_to_constellation_count_old = *t.state_to_constellation_count_ptr;
    1147             : 
    1148           3 :           if (state_to_constellation_count_old != s.residual_transition_cnt)
    1149             :           {
    1150             :             // This is the first transition from this state to a new block. 
    1151             :             // First update the state_to_constellation_count with the residual_transition_cnt 
    1152             :             // which is used by the transitions that we do not visit. Also the not yet 
    1153             :             // visited transitions are set to this value.
    1154           3 :             *t.state_to_constellation_count_ptr = s.residual_transition_cnt;
    1155             : 
    1156             :             // Now allocate another state_to_constellation_count for the Bc block
    1157           3 :             state_to_constellation_count.emplace_back(state_to_constellation_count_old - s.residual_transition_cnt);
    1158           3 :             s.transition_count_ptr = &state_to_constellation_count.back();
    1159             :           }
    1160           3 :           t.state_to_constellation_count_ptr = s.transition_count_ptr; 
    1161             :         }
    1162             :       }
    1163          27 :     }
    1164             : 
    1165             :     /** \brief Choose an splitter block from a non trivial constellation.
    1166             :     *  \details The number of states in the chosen splitter is always less than the half of the non 
    1167             :     *           trivial constellation. Furtheremore, the selected splitter is moved to a new constellation.
    1168             :     */
    1169          35 :     action_block_type* choose_action_splitter(action_constellation_type* non_trivial_action_const)
    1170             :     {
    1171          35 :       assert(non_trivial_action_const->blocks.size()>=2);
    1172             : 
    1173             :       // First, determine the block to split from constellation. It is the block |Bc| < 1/2|C|
    1174             :       // First try with the first block in the list.
    1175          35 :       action_block_type* Bc = &non_trivial_action_const->blocks.front();
    1176             : 
    1177          35 :       if (Bc->states.size() > (non_trivial_action_const->number_of_states / 2))
    1178             :       {
    1179             :         // The block is bigger than 1/2|C|. Choose another one.
    1180          16 :         Bc = &non_trivial_action_const->blocks.back();
    1181             :       }
    1182             : 
    1183             :       // Now split the block of the constellation.
    1184             :       // First unlink Bc from the list of blocks of the non trivial constellation.
    1185          35 :       non_trivial_action_const->blocks.erase(*Bc);
    1186             : 
    1187             :       // Update the number of states and blocks of the non trivial block
    1188          35 :       non_trivial_action_const->number_of_states -= Bc->states.size();
    1189             : 
    1190             :       // Check if the constellation is still non-trivial; if not, move it to the non trivial constellation stack.
    1191          35 :       if (non_trivial_action_const->blocks.size() > 1)  
    1192             :       {
    1193             :         //The constellation is non trivial, put it in the stack of non_trivial_constellations.
    1194          18 :         non_trivial_action_constellations.push(non_trivial_action_const);
    1195             :       } 
    1196             : 
    1197             :       // Add Bc to a new constellation
    1198          35 :       action_constellations.emplace_back();
    1199          35 :       action_constellation_type& new_action_const=action_constellations.back();
    1200             : 
    1201          35 :       Bc->parent_constellation = action_constellations.size()-1;
    1202          35 :       new_action_const.blocks.push_back(*Bc);
    1203          35 :       new_action_const.number_of_states = Bc->states.size();
    1204             : 
    1205          35 :       return Bc;
    1206             :     }
    1207             : 
    1208             :     /** \brief Choose an splitter block from a non trivial constellation.
    1209             :     *  \details The number of states in the chosen splitter is always less than the half of the non
    1210             :     *           trivial constellation. Furtheremore, the selected splitter is moved to a new constellation.
    1211             :     */
    1212          24 :     probabilistic_block_type* choose_probabilistic_splitter(probabilistic_constellation_type* non_trivial_probabilistic_const)
    1213             :     {
    1214             :       // First, determine the block to split from constellation. It is the block |Bc| < 1/2|C|
    1215             :       // First try with the first block in the list.
    1216          24 :       probabilistic_block_type* Bc = &non_trivial_probabilistic_const->blocks.front();
    1217          24 :       if (Bc->states.size() > (non_trivial_probabilistic_const->number_of_states / 2))
    1218             :       {
    1219             :         // The block is bigger than 1/2|C|. Choose another one.
    1220          14 :         Bc = &non_trivial_probabilistic_const->blocks.back();
    1221             :       }
    1222             : 
    1223             :       // Now split the block of the constellation.
    1224             :       // First unlink Bc from the list of blocks of the non trivial constellation.
    1225          24 :       non_trivial_probabilistic_const->blocks.erase(*Bc);
    1226             : 
    1227             :       // Update the number of states and blocks of the non trivial block
    1228          24 :       non_trivial_probabilistic_const->number_of_states -= Bc->states.size();
    1229             : 
    1230             :       // Check if the constellation is still non-trivial; if not, move it to the trivial constellation stack.
    1231          24 :       if (non_trivial_probabilistic_const->blocks.size() > 1)
    1232             :       {
    1233             :         //The constellation is non trivial, put it in the stack of non_trivial_constellations.
    1234           6 :         non_trivial_probabilistic_constellations.push(non_trivial_probabilistic_const);
    1235             :       }
    1236             : 
    1237             :       // Add Bc to a new constellation
    1238          24 :       probabilistic_constellations.emplace_back();
    1239          24 :       probabilistic_constellation_type& new_probabilistic_const=probabilistic_constellations.back();
    1240          24 :       Bc->parent_constellation = probabilistic_constellations.size()-1;
    1241          24 :       new_probabilistic_const.blocks.push_back(*Bc); 
    1242          24 :       new_probabilistic_const.number_of_states = Bc->states.size();
    1243             : 
    1244          24 :       return Bc;
    1245             :     }
    1246             : 
    1247          38 :     typename LTS_TYPE::probabilistic_state_t calculate_new_probabilistic_state(typename LTS_TYPE::probabilistic_state_t ps)
    1248             :     {
    1249          38 :       typename LTS_TYPE::probabilistic_state_t new_prob_state;
    1250          76 :       std::map <state_key_type, probability_fraction_type> prob_state_map;
    1251             : 
    1252             :       /* Iterate over all state probability pairs in the selected probabilistic state*/
    1253         142 :       for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : ps)
    1254             :       {
    1255             :         /* Check the resulting action state in the final State partition */
    1256         104 :         state_key_type new_state = get_eq_class(sp_pair.state());
    1257             : 
    1258         104 :         if (prob_state_map.count(new_state) == 0)
    1259             :         {
    1260             :           /* The state is not yet in the mapping. Add the state with its probability*/
    1261          76 :           prob_state_map[new_state] = sp_pair.probability();
    1262             :         }
    1263             :         else
    1264             :         {
    1265             :           /* The state is already in the mapping. Sum up probabilities */
    1266          28 :           prob_state_map[new_state] = prob_state_map[new_state] + sp_pair.probability();
    1267             :         }
    1268             :       }
    1269             : 
    1270             :       /* Add all the state probabilities pairs in the mapping to its actual data type*/
    1271         114 :       for (typename std::map<state_key_type, probability_fraction_type>::iterator i = prob_state_map.begin(); i != prob_state_map.end(); i++)
    1272             :       {
    1273          76 :         new_prob_state.add(i->first, i->second);
    1274             :       }
    1275             : 
    1276          76 :       return new_prob_state;
    1277             :     }
    1278             : 
    1279          31 :     typename LTS_TYPE::probabilistic_state_t calculate_equivalent_probabilistic_state(probabilistic_block_type& pb)
    1280             :     {
    1281          31 :       typename LTS_TYPE::probabilistic_state_t equivalent_prob_state;
    1282             : 
    1283             :       // Select the first probabilistic state of the probabilistic block.
    1284          31 :       const probabilistic_state_type& s = pb.states.front();
    1285             : 
    1286             :       // Take the an incoming transition to know the key of the state
    1287          31 :       state_key_type s_key = s.incoming_transitions.back()->to;
    1288             : 
    1289          31 :       const typename LTS_TYPE::probabilistic_state_t& old_prob_state = aut.probabilistic_state(s_key);
    1290             : 
    1291          31 :       equivalent_prob_state = calculate_new_probabilistic_state(old_prob_state);
    1292             : 
    1293          31 :       return equivalent_prob_state;
    1294             :     }
    1295             : };
    1296             : 
    1297             : 
    1298             : /** \brief Reduce transition system l with respect to probabilistic bisimulation.
    1299             : * \param[in/out] l The transition system that is reduced.
    1300             : */
    1301             : template < class LTS_TYPE>
    1302             : void probabilistic_bisimulation_reduce_grv(LTS_TYPE& l, utilities::execution_timer& timer);
    1303             : 
    1304             : /** \brief Checks whether the two initial states of two plts's are probabilistic bisimilar.
    1305             : * \details This lts and the lts l2 are not usable anymore after this call.
    1306             : * \param[in/out] l1 A first probabilistic transition system.
    1307             : * \param[in/out] l2 A second probabilistic transition system.
    1308             : * \retval True iff the initial states of the current transition system and l2 are probabilistic bisimilar */
    1309             : template < class LTS_TYPE>
    1310             : bool destructive_probabilistic_bisimulation_compare_grv(LTS_TYPE& l1, LTS_TYPE& l2, utilities::execution_timer& timer);
    1311             : 
    1312             : /** \brief Checks whether the two initial states of two plts's are probabilistic bisimilar.
    1313             : *  \details The current transitions system and the lts l2 are first duplicated and subsequently
    1314             : *           reduced modulo bisimulation. If memory space is a concern, one could consider to
    1315             : *           use destructive_bisimulation_compare.
    1316             : * \param[in/out] l1 A first transition system.
    1317             : * \param[in/out] l2 A second transistion system.
    1318             : * \retval True iff the initial states of the current transition system and l2 are probabilistic bisimilar */
    1319             : template < class LTS_TYPE>
    1320             : bool probabilistic_bisimulation_compare_grv(const LTS_TYPE& l1, const LTS_TYPE& l2, utilities::execution_timer& timer);
    1321             : 
    1322             : template < class LTS_TYPE>
    1323           7 : void probabilistic_bisimulation_reduce_grv(LTS_TYPE& l, utilities::execution_timer& timer)
    1324             : {
    1325             :   // Apply the probabilistic bisimulation reduction algorithm.
    1326          14 :   detail::prob_bisim_partitioner_grv<LTS_TYPE> prob_bisim_part(l, timer);
    1327             : 
    1328             :   // Clear the state labels of the LTS l
    1329           7 :   l.clear_state_labels();
    1330             : 
    1331             :   // Assign the reduced LTS
    1332           7 :   l.set_num_states(prob_bisim_part.num_eq_classes());
    1333           7 :   prob_bisim_part.replace_transitions();
    1334           7 :   prob_bisim_part.replace_probabilistic_states();
    1335           7 : }
    1336             : 
    1337             : template < class LTS_TYPE>
    1338             : bool probabilistic_bisimulation_compare_grv(
    1339             :   const LTS_TYPE& l1,
    1340             :   const LTS_TYPE& l2,
    1341             :   utilities::execution_timer& timer)
    1342             : {
    1343             :   LTS_TYPE l1_copy(l1);
    1344             :   LTS_TYPE l2_copy(l2);
    1345             :   return destructive_probabilistic_bisimulation_compare_grv(l1_copy, l2_copy, timer);
    1346             : }
    1347             : 
    1348             : template < class LTS_TYPE>
    1349             : bool destructive_probabilistic_bisimulation_compare_grv(
    1350             :   LTS_TYPE& l1,
    1351             :   LTS_TYPE& l2,
    1352             :   utilities::execution_timer& timer)
    1353             : {
    1354             :   std::size_t initial_probabilistic_state_key_l1;
    1355             :   std::size_t initial_probabilistic_state_key_l2;
    1356             : 
    1357             :   // Merge states
    1358             :   mcrl2::lts::detail::plts_merge(l1, l2);
    1359             :   l2.clear(); // No use for l2 anymore.
    1360             : 
    1361             :   // The last two probabilistic states are the initial states of l2 and l1
    1362             :   // in the merged plts.
    1363             :   initial_probabilistic_state_key_l2 = l1.num_probabilistic_states() - 1;
    1364             :   initial_probabilistic_state_key_l1 = l1.num_probabilistic_states() - 2;
    1365             : 
    1366             :   detail::prob_bisim_partitioner_grv<LTS_TYPE> prob_bisim_part(l1,timer);
    1367             : 
    1368             :   return prob_bisim_part.in_same_probabilistic_class_grv(initial_probabilistic_state_key_l2,
    1369             :     initial_probabilistic_state_key_l1);
    1370             : }
    1371             : 
    1372             : } // end namespace detail
    1373             : } // end namespace lts
    1374             : } // end namespace mcrl2
    1375             : #endif //_LIBLTS_PBISIM_GRV_H

Generated by: LCOV version 1.13