LCOV - code coverage report
Current view: top level - lts/include/mcrl2/lts/detail - liblts_pbisim_bem.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 285 286 99.7 %
Date: 2020-07-11 00:44:39 Functions: 26 27 96.3 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Hector Joao Rivera Verduzco
       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_bem.h
      10             : 
      11             : #ifndef _LIBLTS_PBISIM_BEM_H
      12             : #define _LIBLTS_PBISIM_BEM_H
      13             : #include "mcrl2/utilities/execution_timer.h"
      14             : #include "mcrl2/lts/detail/liblts_plts_merge.h"
      15             : 
      16             : namespace mcrl2
      17             : {
      18             : namespace lts
      19             : {
      20             : namespace detail
      21             : {
      22             : 
      23             : template < class LTS_TYPE>
      24           7 : class prob_bisim_partitioner_bem
      25             : {
      26             : 
      27             :   public:
      28             :     /** \brief Creates a probabilistic bisimulation partitioner for an PLTS.
      29             :      *  \details This bisimulation partitioner applies the algorithm defined in C. Baier, B. Engelen and M. Majster-Cederbaum. 
      30             :      *   Deciding Bisimilarity and Similarity for Probabilistic Processes. In Journal of Computer and System Sciences 60, 187-237 (2000)
      31             :      */
      32           7 :     prob_bisim_partitioner_bem(LTS_TYPE& l, utilities::execution_timer& timer):aut(l)
      33             :     {
      34           7 :       mCRL2log(log::verbose) << "Probabilistic bisimulation partitioner created for "
      35           0 :                   << l.num_states() << " states and " <<
      36             :                   l.num_transitions() << " transitions\n";
      37           7 :       timer.start("bisimulation_reduce (bem)");
      38           7 :       create_initial_partition();
      39           7 :       refine_partition_until_it_becomes_stable();
      40           7 :       timer.finish("bisimulation_reduce (bem)");
      41           7 :       postprocessing_stage();
      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 state_partition.size();
      50             :     }
      51             : 
      52             :     /** \brief Gives the bisimulation equivalence class number of a state.
      53             :      *  \param[in] s A state number.
      54             :      *  \return The number of the bisimulation equivalence class to which \e s belongs. */
      55         455 :     std::size_t get_eq_class(const std::size_t s) const
      56             :     {
      57         455 :       assert(s<block_index_of_a_state.size());
      58         455 :       return block_index_of_a_state[s]; // The block index is the state number of the block.
      59             :     }
      60             : 
      61             :     /** \brief Gives the bisimulation equivalence step class number of a probabilistic state.
      62             :     *  \param[in] s A probabilistic state number.
      63             :     *  \return The number of the step class to which s belongs. */
      64         292 :     std::size_t get_eq_step_class(const std::size_t d) const
      65             :     {
      66         292 :       assert(d < step_class_index_of_a_distribution.size());
      67         292 :       assert(step_class_index_of_a_distribution[d] < step_classes.size());
      68         292 :       assert(step_classes[step_class_index_of_a_distribution[d]].equivalent_step_class < step_classes.size());
      69         292 :       return step_classes[step_class_index_of_a_distribution[d]].equivalent_step_class;
      70             :     }
      71             : 
      72             :     /** \brief Replaces the transition relation of the current lts by the transitions
      73             :     *         of the bisimulation reduced transition system.
      74             :     * \pre The bisimulation equivalence classes have been computed. */
      75           7 :     void replace_transitions()
      76             :     {
      77          14 :       std::set < transition > resulting_transitions;
      78             : 
      79           7 :       const std::vector<transition>& trans = aut.get_transitions();
      80         299 :       for (const transition& t : trans)
      81             :       {
      82         292 :         resulting_transitions.insert(
      83             :           transition(
      84             :             get_eq_class(t.from()),
      85             :             t.label(),
      86             :             get_eq_step_class(t.to())));
      87             :       }
      88             :       // Remove the old transitions
      89           7 :       aut.clear_transitions();
      90             : 
      91             :       // Copy the transitions from the set into the transition system.
      92          47 :       for (const transition& t : resulting_transitions)
      93             :       {
      94          40 :         aut.add_transition(t);
      95             :       }
      96           7 :     }
      97             : 
      98             :     /** \brief Replaces the probabilistic states of the current lts by the probabilistic
      99             :     *         states of the bisimulation reduced transition system.
     100             :     * \pre The bisimulation step classes have been computed. */
     101           7 :     void replace_probabilistic_states()
     102             :     {
     103          14 :       std::vector<typename LTS_TYPE::probabilistic_state_t> new_probabilistic_states;
     104             : 
     105             :       // get the equivalent probabilistic state of each probabilistic block and add it to aut
     106          38 :       for (step_class_type& sc : equivalent_step_classes)
     107             :       {
     108          62 :         typename LTS_TYPE::probabilistic_state_t equivalent_ps;
     109             : 
     110          31 :         equivalent_ps = calculate_equivalent_probabilistic_state(sc);
     111          31 :         new_probabilistic_states.push_back(equivalent_ps);
     112             :       }
     113             : 
     114             :       /* Remove old probabilistic states */
     115           7 :       aut.clear_probabilistic_states();
     116             : 
     117             :       // Add new prob states to aut
     118          38 :       for (const typename LTS_TYPE::probabilistic_state_t& new_ps : new_probabilistic_states)
     119             :       {
     120          31 :         aut.add_probabilistic_state(new_ps);
     121             :       }
     122             : 
     123          14 :       typename LTS_TYPE::probabilistic_state_t old_initial_prob_state = aut.initial_probabilistic_state();
     124          14 :       typename LTS_TYPE::probabilistic_state_t new_initial_prob_state = calculate_new_probabilistic_state(old_initial_prob_state);
     125           7 :       aut.set_initial_probabilistic_state(new_initial_prob_state);
     126           7 :     }
     127             : 
     128             :     /** \brief Returns whether two states are in the same probabilistic bisimulation equivalence class.
     129             :     *  \param[in] s A state number.
     130             :     *  \param[in] t A state number.
     131             :     *  \retval true if \e s and \e t are in the same bisimulation equivalence class;
     132             :     *  \retval false otherwise. */
     133             :     bool in_same_probabilistic_class(const std::size_t s, const std::size_t t) const
     134             :     {
     135             :       return get_eq_step_class(s) == get_eq_step_class(t);
     136             :     }
     137             : 
     138             :   private:
     139             : 
     140             :   typedef std::size_t block_key_type;
     141             :   typedef std::size_t step_class_key_type;
     142             :   typedef std::size_t state_type;
     143             :   typedef std::size_t label_type;
     144             :   typedef std::size_t distribution_key_type;
     145             :   typedef typename LTS_TYPE::probabilistic_state_t::probability_t probability_fraction_type;
     146             : 
     147         182 :   struct distribution_type
     148             :   {
     149             :     distribution_key_type key;
     150             :     std::vector< std::list<transition*> > incoming_transitions_per_label; // Incoming transitions organized per label
     151             :   };
     152             :   
     153        1160 :   struct block_type
     154             :   {
     155             :     block_key_type key;
     156             :     std::list<state_type> states;        // The states in the block
     157             :     bool is_in_new_blocks;
     158             :   };
     159             : 
     160         152 :   struct step_class_type {
     161             :     step_class_key_type key;
     162             :     label_type action;                                // action label of the pair <a,M>.
     163             :     std::list<distribution_type*> distributions;      // The distributions in the step class <a,M>.
     164             :     std::vector< bool > prev_states;                  // Previous states that can reach step_class <a,M>
     165             :     bool is_in_new_step_classes;
     166             :     std::size_t equivalent_step_class;
     167             :   };
     168             : 
     169             :   std::list<block_type*> state_partition;
     170             :   std::list<step_class_type*> step_partition;
     171             :   std::vector<distribution_type> distributions;
     172             :   std::deque<step_class_type> step_classes;
     173             :   std::deque<step_class_type> equivalent_step_classes;
     174             :   std::deque<block_type> blocks;
     175             :   std::vector<block_key_type> block_index_of_a_state;
     176             :   std::vector<step_class_key_type> step_class_index_of_a_distribution;
     177             : 
     178             :   LTS_TYPE& aut;
     179             : 
     180         252 :   struct tree_type
     181             :   {
     182             :     std::list<state_type> states;
     183             :     std::size_t count;
     184             :     tree_type* left;
     185             :     tree_type* right;
     186             : 
     187          63 :     void init_node()
     188             :     {
     189          63 :       count = 0;
     190          63 :       left = NULL;
     191          63 :       right = NULL;
     192          63 :     }
     193             :   };
     194             : 
     195             :   /** \brief Creates the initial partition of step classes and blocks.
     196             :    *  \detail The blocks are initially partitioned based on the actions that can perform.
     197             :    *          The step classes are partitioned based on the action that leads to the probabilistic state */
     198           7 :   void create_initial_partition (void) 
     199             :   {
     200          14 :     std::vector< std::vector< std::list<distribution_type*> > > steps; // Representation of transition in 2-d array
     201           7 :     std::vector<transition>& transitions = aut.get_transitions();
     202          14 :     std::vector< std::vector<bool> > distribution_per_step_class;
     203             :     
     204           7 :     distribution_per_step_class.resize(aut.num_action_labels());
     205          31 :     for (std::vector<bool>& i : distribution_per_step_class)
     206             :     {
     207          24 :       i.resize(aut.num_probabilistic_states());
     208             :     }
     209             : 
     210             :     //---- Preprocessing stage to transform the PLTS to the data structures suggested by Baier ---- //
     211             : 
     212             :     // Construct vector of distributions
     213           7 :     distributions.resize(aut.num_probabilistic_states());
     214           7 :     std::size_t key = 0;
     215          98 :     for (distribution_type& distribution : distributions)
     216             :     {
     217          91 :       distribution.key = key;
     218          91 :       distribution.incoming_transitions_per_label.resize(aut.num_action_labels());
     219          91 :       key++;
     220             :     }
     221             : 
     222             :     // Initialize the Steps bi-dimientional array
     223           7 :     steps.resize(aut.num_states());
     224         309 :     for (std::size_t i = 0; i < steps.size(); i++)
     225             :     {
     226         302 :       steps[i].resize(aut.num_action_labels());
     227             :     }
     228             : 
     229         299 :     for (transition& t : transitions)
     230             :     {
     231         292 :       steps[t.from()][t.label()].push_back(&distributions[t.to()]);
     232         292 :       distributions[t.to()].incoming_transitions_per_label[t.label()].push_back(&t);
     233             :     }
     234             : 
     235             :     //---- Start the initialization process (page 207. Fig. 10. Baier) ---- //
     236             : 
     237             :     // Initially there are as many step classes as lables
     238           7 :     step_classes.resize(aut.num_action_labels());
     239             : 
     240          31 :     for (step_class_type& sc : step_classes)
     241             :     {
     242          24 :       sc.prev_states.resize(aut.num_states());
     243             :     }
     244             : 
     245             :     // create tree structure to group action states based on the outgoing transitions
     246           7 :     std::size_t max_block_size = 0;
     247           7 :     tree_type* max_block = nullptr;
     248          14 :     std::deque<tree_type> tree_nodes;
     249          14 :     std::vector<tree_type*> leaves;
     250          14 :     tree_type v0;
     251           7 :     v0.init_node();
     252           7 :     tree_nodes.push_back(v0);
     253             : 
     254             :     // For all s in S do
     255         309 :     for (state_type s = 0; s < aut.num_states(); s++)
     256             :     {
     257             :       // (1) Create pointer to root of the tree
     258         302 :       tree_type* v = &tree_nodes[0];
     259             : 
     260             :       // (2) Construct tree
     261        1494 :       for (std::size_t i = 0; i < aut.num_action_labels(); i++)
     262             :       {
     263        1192 :         step_classes[i].key = i;
     264        1192 :         step_classes[i].action = i;
     265        1192 :         if (steps[s][i].size() > 0)
     266             :         {
     267         580 :           for (distribution_type* d : steps[s][i])
     268             :           {
     269         292 :             if (distribution_per_step_class[i][d->key] == false)
     270             :             {
     271         118 :               step_classes[i].distributions.push_back(d);
     272         118 :               distribution_per_step_class[i][d->key] = true;
     273             :             }
     274             :           }
     275             :           
     276         288 :           step_classes[i].prev_states[s] = true;
     277             : 
     278         288 :           if (v->left == NULL)
     279             :           {
     280             :             // create left node
     281          36 :             tree_type w;
     282          18 :             w.init_node();
     283          18 :             tree_nodes.push_back(w);
     284          18 :             v->left = &tree_nodes.back();
     285             : 
     286             :             // add new node to the leaf nodes if it is a leaf
     287          18 :             if (i == aut.num_action_labels() - 1)
     288             :             {
     289           7 :               leaves.push_back(v->left);
     290             :             }
     291             : 
     292             :           }
     293         288 :           v = v->left;
     294             :         }
     295             :         else
     296             :         {
     297         904 :           if (v->right == NULL)
     298             :           {
     299             :             // create left node
     300          76 :             tree_type w;
     301          38 :             w.init_node();
     302          38 :             tree_nodes.push_back(w);
     303          38 :             v->right = &tree_nodes.back();
     304             : 
     305             :             // add new node to the leaf nodes if it is a leaf
     306          38 :             if (i == aut.num_action_labels() - 1)
     307             :             {
     308          16 :               leaves.push_back(v->right);
     309             :             }
     310             :           }
     311         904 :           v = v->right;
     312             :         }
     313             :       }
     314             : 
     315             :       // (3) Add the state to the leaf and increment its state counter
     316         302 :       v->states.push_back(s);
     317         302 :       v->count++;
     318             : 
     319             :       // (4) Keep track of the leave containing more states
     320         302 :       if (v->count > max_block_size)
     321             :       {
     322         178 :         max_block = v;
     323         178 :         max_block_size = v->count;
     324             :       }
     325             :     }
     326             : 
     327             :     // insert all states of the leaves to blocks
     328           7 :     blocks.resize(leaves.size());
     329             : 
     330           7 :     key = 0;
     331           7 :     std::size_t larger_key = 0;
     332          30 :     for (tree_type* leaf_ptr : leaves)
     333             :     {
     334          23 :       block_type& block = blocks[key];
     335          23 :       block.key = key;
     336          23 :       block.states.splice(block.states.end(), leaf_ptr->states);
     337             : 
     338          23 :       if (leaf_ptr == max_block)
     339             :       {
     340           7 :         larger_key = key;
     341             :       }
     342             : 
     343          23 :       key++;
     344             :     }
     345             : 
     346             :     // Add all blocks to the state partition.
     347             :     // Initially only the larger block has to be at the end of the list
     348          30 :     for (block_type& b : blocks)
     349             :     {
     350          23 :       if (b.key != larger_key)
     351             :       {
     352             :         // Push the non-larger blocks to the front of the list. This are the so called new blocks
     353          16 :         b.is_in_new_blocks = true;
     354          16 :         state_partition.push_front(&b);
     355             :       }
     356             :       else
     357             :       {
     358             :         // push the larger block to the end of the list
     359           7 :         b.is_in_new_blocks = false;
     360           7 :         state_partition.push_back(&b);
     361             :       }
     362             :     }
     363             :     
     364             :     // Add all step classes to the step partition.
     365             :     // Initially all are new step classes
     366          31 :     for (step_class_type& sc : step_classes)
     367             :     {
     368          24 :       if (sc.distributions.size() > 0)
     369             :       { 
     370          18 :         step_partition.push_front(&sc);
     371          18 :         sc.is_in_new_step_classes = true;
     372             :       }
     373             :     }
     374             : 
     375           7 :     block_index_of_a_state.resize(aut.num_states());
     376          30 :     for (const block_type& b : blocks)
     377             :     {
     378         325 :       for (const state_type s : b.states)
     379             :       {
     380         302 :         block_index_of_a_state[s] = b.key;
     381             :       }
     382             :     }
     383             : 
     384           7 :   }
     385             : 
     386             :   /** \brief Calculates the probability to reach block b from distribution d.
     387             :   *   \param[in] d is a probabilistic state (distribution).
     388             :   *              b is a block of states.
     389             :   *   \return The probability to reach block b. */
     390        1189 :   probability_fraction_type probability_to_block(distribution_type& d, block_type& b)
     391             :   {
     392        1189 :     probability_fraction_type prob_to_block;
     393        1189 :     const typename LTS_TYPE::probabilistic_state_t& prob_state = aut.probabilistic_state(d.key);
     394             : 
     395             :     /* Check whether the state is in the distribution d and add up the probability*/
     396        5476 :     for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& prob_pair : prob_state)
     397             :     {
     398        4287 :       const state_type& s = prob_pair.state();
     399        4287 :       if (block_index_of_a_state[s] == b.key)
     400             :       {
     401         371 :         prob_to_block = prob_to_block + prob_pair.probability();
     402             :       }
     403             :     }
     404             : 
     405        1189 :     return prob_to_block;
     406             :   }
     407             : 
     408          77 :   typename LTS_TYPE::probabilistic_state_t calculate_new_probabilistic_state(typename LTS_TYPE::probabilistic_state_t ps)
     409             :   {
     410          77 :     typename LTS_TYPE::probabilistic_state_t new_prob_state;
     411          77 :     static std::map<state_type, probability_fraction_type> prob_state_map;
     412          77 :     prob_state_map.clear();
     413             : 
     414             :     /* Iterate over all state probability pairs in the selected probabilistic state*/
     415         240 :     for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : ps)
     416             :     {
     417             :       /* Check the resulting action state in the final State partition */
     418         163 :       state_type new_state = get_eq_class(sp_pair.state());
     419             : 
     420         163 :       if (prob_state_map.count(new_state) == 0)
     421             :       {
     422             :         /* The state is not yet in the mapping. Add the state with its probability*/
     423         130 :         prob_state_map[new_state] = sp_pair.probability();
     424             :       }
     425             :       else
     426             :       {
     427             :         /* The state is already in the mapping. Sum up probabilities */
     428          33 :         prob_state_map[new_state] = prob_state_map[new_state] + sp_pair.probability();
     429             :       }
     430             :     }
     431             : 
     432             :     /* Add all the state probabilities pairs in the mapping to its actual data type*/
     433         207 :     for (const std::pair<state_type, probability_fraction_type>& i : prob_state_map)
     434             :     {
     435         130 :       new_prob_state.add(i.first, i.second);
     436             :     }
     437             : 
     438          77 :     return new_prob_state;
     439             :   }
     440             : 
     441          70 :   typename LTS_TYPE::probabilistic_state_t calculate_equivalent_probabilistic_state(step_class_type& sc)
     442             :   {
     443          70 :     typename LTS_TYPE::probabilistic_state_t equivalent_prob_state;
     444             : 
     445             :     /* Select the first probabilistic state of the step class */
     446          70 :     distribution_type* d = sc.distributions.front();
     447             : 
     448         140 :     typename LTS_TYPE::probabilistic_state_t old_prob_state = aut.probabilistic_state(d->key);
     449             : 
     450          70 :     equivalent_prob_state = calculate_new_probabilistic_state(old_prob_state);
     451             : 
     452         140 :     return equivalent_prob_state;
     453             :   }
     454             : 
     455             :   /** \brief  Two-phased partitioning algorithm described in page 204. Fig 9. Baier.
     456             :   *   \detail Refinement of state partition and step partition until no new blocks/step classes
     457             :   *           are in front of the partition lists
     458             :   */
     459           7 :   void refine_partition_until_it_becomes_stable (void) 
     460             :   {
     461          14 :     std::list<step_class_type*> step_partition_old;
     462          14 :     std::list<block_type*> state_partition_old;
     463             : 
     464             :     // Repeat until no new blocks in front of the partition lists
     465          87 :     while (state_partition.front()->is_in_new_blocks == true || step_partition.front()->is_in_new_step_classes == true)
     466             :     { 
     467             :       // Phase 1: Splitting of step_partition via split(M,C)
     468          40 :       if (state_partition.front()->is_in_new_blocks == true)
     469             :       {
     470             :         // Choose a new block in front of the state partition and change it to the back of the list
     471          35 :         block_type* c_block = state_partition.front();
     472          35 :         state_partition.pop_front();
     473          35 :         state_partition.push_back(c_block);
     474          35 :         c_block->is_in_new_blocks = false;
     475             : 
     476             :         // swap elements of step_partition (M) to step_partition_old (M_old)
     477          35 :         step_partition_old.swap(step_partition);
     478             : 
     479             :         // vector to add the new step classes
     480          35 :         static std::vector<typename std::list<step_class_type*>::iterator> pending_new_step_classes;
     481          35 :         pending_new_step_classes.clear();
     482             : 
     483             :         // iterate over all step classes
     484         264 :         for (typename std::list<step_class_type*>::iterator sc_iter = step_partition_old.begin(); 
     485         264 :           sc_iter != step_partition_old.end(); ++sc_iter)
     486             :         {
     487         229 :           step_class_type* sc_ptr = *sc_iter;
     488             : 
     489             :           // Mapping to sort the distributions based on its probability to reach a block, instead of using
     490             :           // an ordered balanced tree as suggsted in Baier
     491         229 :           static std::map< probability_fraction_type, std::list<distribution_type*> > distributions_ordered_by_prob;
     492         229 :           distributions_ordered_by_prob.clear();
     493             : 
     494             :           // Iterate over all distributions d of the step class and add probability to block to vector
     495        1418 :           for (distribution_type* d : sc_ptr->distributions)
     496             :           {
     497        2378 :             probability_fraction_type probability = probability_to_block(*d, *c_block);
     498        1189 :             distributions_ordered_by_prob[probability].push_back(d);
     499             :           }
     500             : 
     501             :           // if there are multiple elements in the distributions_ordered_by_prob then we have to 
     502             :           // add them to the step partition as a new step class
     503         229 :           if (distributions_ordered_by_prob.size() >= 2)
     504             :           {
     505             :             step_class_type* new_step_class_ptr;
     506             : 
     507          19 :             step_classes.resize(step_classes.size() + distributions_ordered_by_prob.size() - 1);
     508             :             // iterate over mapping
     509          19 :             std::size_t new_class_count = 0;
     510          59 :             for (std::pair< probability_fraction_type, std::list<distribution_type*> > ordered_dist : distributions_ordered_by_prob)
     511             :             {
     512          40 :               std::list<distribution_type*>& distribution_list = ordered_dist.second;
     513             :               
     514          40 :               if (new_class_count == 0)
     515             :               {
     516             :                 // if it is the first element of the mapping then we do not create a new step class; instead, we 
     517             :                 // add its elements into the current step class that is being split.
     518          19 :                 sc_ptr->distributions.swap(distribution_list);
     519             : 
     520             :                 // clear the prev states of the current step class
     521        2538 :                 for (std::size_t i = 0; i < sc_ptr->prev_states.size(); i++)
     522             :                 {
     523        2519 :                   sc_ptr->prev_states[i] = false;
     524             :                 }
     525             : 
     526             :                 // recalculate prev states based on incoming transitions of each distribution
     527         215 :                 for (distribution_type* d : sc_ptr->distributions)
     528             :                 {
     529         664 :                   for (transition* t_ptr : d->incoming_transitions_per_label[sc_ptr->action])
     530             :                   {
     531         468 :                     sc_ptr->prev_states[t_ptr->from()] = true;
     532             :                   }
     533             :                 }
     534             : 
     535             :                 // add to the front of the step partition (as a new step class) if not yet added 
     536          19 :                 if (sc_ptr->is_in_new_step_classes == false)
     537             :                 {
     538             :                   // since we are iterating over this step class, we save its iterator in a pending vector,
     539             :                   // so later we can add it to the front of the step partition (outside the loop)
     540           1 :                   pending_new_step_classes.push_back(sc_iter);
     541           1 :                   sc_ptr->is_in_new_step_classes = true;
     542             :                 }
     543             :               }
     544             :               else
     545             :               {
     546          21 :                 new_step_class_ptr = &step_classes[step_classes.size() - new_class_count];
     547             : 
     548             :                 //init new step class
     549          21 :                 new_step_class_ptr->key = step_classes.size() - new_class_count;
     550          21 :                 new_step_class_ptr->action = sc_ptr->action;
     551          21 :                 new_step_class_ptr->is_in_new_step_classes = true;
     552          21 :                 new_step_class_ptr->prev_states.resize(aut.num_states());
     553          21 :                 new_step_class_ptr->distributions.swap(distribution_list);
     554             : 
     555             :                 // recalculate prev states based ont incoming transitions of each distribution
     556         101 :                 for (distribution_type* d : new_step_class_ptr->distributions)
     557             :                 {
     558         290 :                   for (transition* t_ptr : d->incoming_transitions_per_label[new_step_class_ptr->action])
     559             :                   {
     560         210 :                     new_step_class_ptr->prev_states[t_ptr->from()] = true;
     561             :                   }
     562             :                 }
     563             : 
     564             :                 // add new step class to step partition and new_step_classes
     565          21 :                 step_partition.push_front(new_step_class_ptr);
     566             :               }
     567          40 :               new_class_count++;
     568             :             }
     569             :           }
     570             :         }
     571             : 
     572             :         // Add the pending new blocks to the front of the list
     573          36 :         for (typename std::list<step_class_type*>::iterator sc_iter : pending_new_step_classes)
     574             :         {
     575           1 :           step_partition.splice(step_partition.begin(), step_partition_old, sc_iter);
     576             :         }
     577             : 
     578             :         // move remaining step classes to the end of step partition
     579          35 :         step_partition.splice(step_partition.end(), step_partition_old);
     580             :       }
     581             : 
     582             :       // Phase 2: Refinment of state_partition via Refine(X,a,M)
     583          40 :       if (step_partition.front()->is_in_new_step_classes == true)
     584             :       {
     585             :         // Choose some step class <a,M> in new_step_classes and remove it from new_step_classes
     586          40 :         step_class_type* step_class = step_partition.front();
     587          40 :         step_partition.pop_front();
     588          40 :         step_class->is_in_new_step_classes = false;
     589          40 :         step_partition.push_back(step_class);
     590             : 
     591             :         // swap elements of state_partition (X) to state_partition_old (X_old)
     592          40 :         state_partition_old.swap(state_partition);
     593             : 
     594          40 :         static std::vector<typename std::list<block_type*>::iterator > blocks_to_move_to_front;
     595          40 :         static std::vector<block_type*> new_blocks_to_move_to_front;
     596          40 :         blocks_to_move_to_front.clear();
     597          40 :         new_blocks_to_move_to_front.clear();
     598             :         // for all blocks B in X_old
     599             :         //for (block_type* b_to_split : state_partition_old)
     600         309 :         for (typename std::list<block_type*>::iterator block_iter = state_partition_old.begin(); 
     601         309 :           block_iter != state_partition_old.end(); ++block_iter)
     602             :         {
     603         269 :           block_type* b_to_split = *block_iter;
     604         538 :           block_type new_block;
     605         269 :           new_block.is_in_new_blocks = false;
     606         538 :           block_type temp_block;
     607             :           block_type* new_block_ptr;
     608         269 :           new_block.key = blocks.size();
     609             : 
     610             :           // iterate over all states in the block to split
     611        3955 :           for (state_type s : b_to_split->states)
     612             :           {
     613             :             // if block b can reach step class <a,M> starting from state s then we move it to antoher block
     614        3686 :             if (step_class->prev_states[s] == true)
     615             :             {
     616         323 :               new_block.states.push_back(s);
     617             :             }
     618             :             else
     619             :             {
     620        3363 :               temp_block.states.push_back(s);
     621             :             }
     622             :           }
     623             : 
     624             :           // if both, the new block and temp block has elements, then we add a new block into the state partition
     625         269 :           if (new_block.states.size() > 0 && temp_block.states.size() > 0)
     626             :           {
     627             : 
     628             :             // First update the block_index_of_a_state by iterating over all states of the new block
     629         182 :             for (state_type s : new_block.states)
     630             :             {
     631         163 :               block_index_of_a_state[s] = new_block.key;
     632             :             }
     633             : 
     634          19 :             blocks.push_back(new_block);
     635          19 :             new_block_ptr = &blocks.back();
     636             : 
     637             :             // return states from temp_block to b_to_split
     638          19 :             b_to_split->states.swap(temp_block.states);
     639             :             
     640             :             // if the current block is not currently a new block then add the smaller
     641             :             // block (between new block and current block) to the list of new blocks; 
     642             :             // hence, in front of state partition
     643          19 :             if (b_to_split->is_in_new_blocks == false)
     644             :             {
     645          14 :               if (new_block_ptr->states.size() < b_to_split->states.size())
     646             :               {
     647          11 :                 new_blocks_to_move_to_front.push_back(new_block_ptr);
     648          11 :                 new_block_ptr->is_in_new_blocks = true;
     649             :               }
     650             :               else
     651             :               {
     652           3 :                 b_to_split->is_in_new_blocks = true;
     653           3 :                 blocks_to_move_to_front.push_back(block_iter);
     654             : 
     655             :                 // add new block to the back of the state_partition list
     656           3 :                 state_partition.push_back(new_block_ptr);
     657             :               }
     658             :             }
     659             :             else
     660             :             {
     661             :               // the current block is already in new blocks; hence, just add the new block
     662             :               // to the front of the partition as well.
     663             : 
     664             :               //new_blocks.push_back(new_block_ptr);
     665           5 :               new_block_ptr->is_in_new_blocks = true;
     666             : 
     667             :               // add new block to the back of the state_partition list
     668           5 :               new_blocks_to_move_to_front.push_back(new_block_ptr);
     669             :             }
     670             :           }
     671             :         }
     672             : 
     673             :         // move the remaning blocks to the end of state_partition
     674          40 :         state_partition.splice(state_partition.begin(), state_partition_old);
     675             : 
     676             :         // move the blocks that should be in new blocks to the begining of the list
     677          43 :         for (typename std::list<block_type*>::iterator block_iter : blocks_to_move_to_front)
     678             :         {
     679           3 :           state_partition.splice(state_partition.begin(), state_partition, block_iter);
     680             :         }
     681             : 
     682             :         // move the blocks that are new to the front of state_partition
     683          56 :         for (block_type* block_ptr : new_blocks_to_move_to_front)
     684             :         {
     685          16 :           state_partition.push_front(block_ptr);
     686             :         }
     687             : 
     688             :       }
     689             :     }
     690           7 :   }
     691             : 
     692           7 :   void postprocessing_stage(void)
     693             :   {
     694             :     //---- Post processing to keep track of the parent block of each state ----//
     695             :     //block_index_of_a_state.resize(aut.num_states());
     696          49 :     for (const block_type& b : blocks)
     697             :     {
     698         344 :       for (const state_type s : b.states)
     699             :       {
     700         302 :         block_index_of_a_state[s] = b.key;
     701             :       }
     702             :     }
     703             : 
     704           7 :     step_class_index_of_a_distribution.resize(aut.num_probabilistic_states());
     705          52 :     for (step_class_type& sc : step_classes)
     706             :     {
     707          45 :       sc.equivalent_step_class = sc.key;
     708             : 
     709         163 :       for (const distribution_type* d : sc.distributions)
     710             :       {
     711         118 :         step_class_index_of_a_distribution[d->key] = sc.key;
     712             :       }
     713             :     }
     714             : 
     715             :     // Merge equivalent step classes in step partition. The algorithm initially separates classes by actions,
     716             :     // but it is possible that a probabilistic sate has multiple incoming actions, hence it will be repeated
     717             :     // among multiple step classes
     718          14 :     typename LTS_TYPE::probabilistic_state_t new_prob_state;
     719          14 :     std::unordered_map<typename LTS_TYPE::probabilistic_state_t, std::vector<step_class_type*> > reduced_step_partition;
     720             : 
     721             :     /* Iterate over all step classes of Step_partition*/
     722          52 :     for (step_class_type& sc : step_classes)
     723             :     {
     724          45 :       if (sc.distributions.size() > 0)
     725             :       {
     726          78 :         typename LTS_TYPE::probabilistic_state_t new_prob_state = calculate_equivalent_probabilistic_state(sc);
     727             : 
     728             :         /* Add the step class index to the new probability state*/
     729          39 :         reduced_step_partition[new_prob_state].push_back(&sc);
     730             :       }
     731             :     }
     732             : 
     733           7 :     step_class_key_type equivalent_class_key = 0;
     734          31 :     for (typename std::unordered_map<typename LTS_TYPE::probabilistic_state_t,
     735           7 :           std::vector<step_class_type*> >::iterator i = reduced_step_partition.begin();
     736          38 :           i != reduced_step_partition.end(); ++i)
     737             :     {
     738          31 :       std::vector<step_class_type*>& sc_vector = i->second;
     739             : 
     740          31 :       equivalent_step_classes.push_back(*sc_vector[0]);
     741          70 :       for (step_class_type* sc :sc_vector)
     742             :       {
     743          39 :         sc->equivalent_step_class = equivalent_class_key;
     744             :       }
     745          31 :       equivalent_class_key++;
     746             :     }
     747             : 
     748           7 :   }
     749             : };
     750             : 
     751             : 
     752             : /** \brief Reduce transition system l with respect to probabilistic bisimulation.
     753             :  * \param[in/out] l The transition system that is reduced.
     754             :  * \param[in/out] timer A timer that can be used to report benchmarking results.
     755             :  */
     756             : template < class LTS_TYPE>
     757             : void probabilistic_bisimulation_reduce_bem(LTS_TYPE& l, utilities::execution_timer& timer);
     758             : 
     759             : /** \brief Checks whether the two initial states of two plts's are probabilistic bisimilar.
     760             : * \details This lts and the lts l2 are not usable anymore after this call.
     761             : * \param[in/out] l1 A first probabilistic transition system.
     762             : * \param[in/out] l2 A second probabilistic transition system.
     763             : * \retval True iff the initial states of the current transition system and l2 are probabilistic bisimilar */
     764             : template < class LTS_TYPE>
     765             : bool destructive_probabilistic_bisimulation_compare_bem(LTS_TYPE& l1, LTS_TYPE& l2, utilities::execution_timer& timer);
     766             : 
     767             : 
     768             : /** \brief Checks whether the two initial states of two plts's are probabilistic bisimilar.
     769             : *  \details The current transitions system and the lts l2 are first duplicated and subsequently
     770             : *           reduced modulo bisimulation. If memory space is a concern, one could consider to
     771             : *           use destructive_bisimulation_compare.
     772             : * \param[in/out] l1 A first transition system.
     773             : * \param[in/out] l2 A second transistion system.
     774             : * \retval True iff the initial states of the current transition system and l2 are probabilistic bisimilar */
     775             : template < class LTS_TYPE>
     776             : bool probabilistic_bisimulation_compare_bem(const LTS_TYPE& l1, const LTS_TYPE& l2, utilities::execution_timer& timer);
     777             : 
     778             : 
     779             : template < class LTS_TYPE>
     780           7 : void probabilistic_bisimulation_reduce_bem(LTS_TYPE& l, utilities::execution_timer& timer)
     781             : {
     782             : 
     783             :   // Apply the probabilistic bisimulation reduction algorithm.
     784          14 :   detail::prob_bisim_partitioner_bem<LTS_TYPE> prob_bisim_part(l,timer);
     785             : 
     786             :   // Clear the state labels of the LTS l
     787           7 :   l.clear_state_labels();
     788             : 
     789             :   // Assign the reduced LTS
     790           7 :   l.set_num_states(prob_bisim_part.num_eq_classes());
     791           7 :   prob_bisim_part.replace_transitions();
     792           7 :   prob_bisim_part.replace_probabilistic_states();
     793           7 : }
     794             : 
     795             : template < class LTS_TYPE>
     796             : bool probabilistic_bisimulation_compare_bem(
     797             :   const LTS_TYPE& l1,
     798             :   const LTS_TYPE& l2,
     799             :   utilities::execution_timer& timer)
     800             : {
     801             :   LTS_TYPE l1_copy(l1);
     802             :   LTS_TYPE l2_copy(l2);
     803             :   return destructive_probabilistic_bisimulation_compare_bem(l1_copy, l2_copy, timer);
     804             : }
     805             : 
     806             : template < class LTS_TYPE>
     807             : bool destructive_probabilistic_bisimulation_compare_bem(
     808             :   LTS_TYPE& l1,
     809             :   LTS_TYPE& l2,
     810             :   utilities::execution_timer& timer)
     811             : {
     812             :   std::size_t initial_probabilistic_state_key_l1;
     813             :   std::size_t initial_probabilistic_state_key_l2;
     814             : 
     815             :   // Merge states
     816             :   mcrl2::lts::detail::plts_merge(l1, l2);
     817             :   l2.clear(); // No use for l2 anymore.
     818             : 
     819             :               // The last two probabilistic states are the initial states of l2 and l1
     820             :               // in the merged plts
     821             :   initial_probabilistic_state_key_l2 = l1.num_probabilistic_states() - 1;
     822             :   initial_probabilistic_state_key_l1 = l1.num_probabilistic_states() - 2;
     823             : 
     824             :   detail::prob_bisim_partitioner_bem<LTS_TYPE> prob_bisim_part(l1, timer);
     825             : 
     826             :   return prob_bisim_part.in_same_probabilistic_class(initial_probabilistic_state_key_l2,
     827             :     initial_probabilistic_state_key_l1);
     828             : }
     829             : 
     830             : }  // namespace detail
     831             : }  // namespace lts
     832             : }  // namespace mcrl2
     833             : 
     834             : #endif // _LIBLTS_PBISIM_BEM_H

Generated by: LCOV version 1.13