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             : 
      10             : // This file contains the merge algorithm that merges two plts's.
      11             : // Merges an LTS L with this LTS (say K) and stores the resulting LTS
      12             : // (say M) in this LTS datastructure, effectively replacing K.
      13             : // Conceptually, we just take the union of the sets of states and the
      14             : // sets of transitions of K and L:
      15             : //   States_M      = States_K + States_L
      16             : //   Transitions_M = Transitions_K + Transitions_L
      17             : // where + denotes set union.
      18             : // However, this assumes that States_K and States_L are disjoint,
      19             : // which is generally not the case. More specifically we have:
      20             : //   States_K = { 0, ..., N_K - 1 }   and
      21             : //   States_L = { 0, ..., N_L - 1 }
      22             : // for some N_K, N_L > 0.
      23             : // Therefore, state i of L will be numbered |N_K| + i in the resulting
      24             : // LTS M and state i of K will be numbered i in M. This yields:
      25             : //   States_M = { 0, ..., N_K + N_L - 1 }.
      26             : 
      27             : 
      28             : #ifndef MCRL2_LTS_LIBLTS_PLTS_MERGE_H
      29             : #define MCRL2_LTS_LIBLTS_PLTS_MERGE_H
      30             : 
      31             : #include "mcrl2/lts/lts_aut.h"
      32             : #include "mcrl2/lts/lts_fsm.h"
      33             : #include "mcrl2/lts/lts_lts.h"
      34             : 
      35             : namespace mcrl2
      36             : {
      37             : namespace lts
      38             : {
      39             : namespace detail
      40             : {
      41             : 
      42             : template <class LTS_TYPE>
      43           6 : void plts_merge(LTS_TYPE& l1, const LTS_TYPE& l2)
      44             : {
      45           6 :   const std::size_t old_nstates=l1.num_states();
      46           6 :   const std::size_t old_n_prob_states = l1.num_probabilistic_states();
      47           6 :   l1.set_num_states(l1.num_states() + l2.num_states());
      48             : 
      49             :   // The resulting LTS will have state information only if BOTH LTSs
      50             :   // currently have state information.
      51           6 :   if (l1.has_state_info() && l2.has_state_info())
      52             :   {
      53           0 :     for (std::size_t i=0; i<l2.num_states(); ++i)
      54             :     {
      55           0 :       l1.add_state(l2.state_label(i));
      56             :     }
      57             :   }
      58             :   else
      59             :   {
      60             :     // remove state information from this LTS, if any
      61           6 :     l1.clear_state_labels();
      62             :   }
      63             : 
      64             :   // Before we can set the label data in a new transitions
      65             :   // array, we first have to collect the labels of both LTSs in a
      66             :   // map, of which the second element indicates the new index of each action label.
      67             : 
      68             :   typedef typename LTS_TYPE::action_label_t type1;
      69             :   typedef typename LTS_TYPE::labels_size_type type2;
      70             :   typedef typename std::pair< typename std::map < type1,type2 >::const_iterator, bool > insert_type;
      71           6 :   std::map < type1,type2 > labs;
      72             : 
      73             :   // Put the labels of the LTS l1 in a map.
      74          24 :   for (std::size_t i = 0; i < l1.num_action_labels(); ++i)
      75             :   {
      76          18 :     labs.insert(std::pair <typename LTS_TYPE::action_label_t,typename LTS_TYPE::labels_size_type>
      77             :                 (l1.action_label(i),i));
      78             :   }
      79             :   // Add the labels for the LTS l2, and put them there with a new index if it was
      80             :   // not added yet.
      81             :   // Furthermore, update the hidden_action_map. 
      82             :   // If label a1 is mapped on a2 in l2, then this must be the same
      83             :   // in l1. It may be that label a1 did not exist yet in which case it needs
      84             :   // to be added too.
      85             : 
      86             : 
      87          24 :   for (std::size_t i=0; i<l2.num_action_labels(); ++i)
      88             :   {
      89             :     typename LTS_TYPE::labels_size_type new_index;
      90          18 :     const insert_type it= labs.insert(std::pair < type1,type2 >
      91          18 :                                (l2.action_label(i),l1.num_action_labels()));
      92          18 :     if (it.second) 
      93             :     {
      94             :       // New element has been inserted.
      95           0 :       new_index=l1.add_action(l2.action_label(i));
      96           0 :       if (l2.is_tau(l2.apply_hidden_label_map(i)))
      97             :       {
      98           0 :         l1.hidden_label_set().insert(new_index);
      99             :       }
     100             :     }
     101             :     else 
     102             :     {
     103          18 :       new_index=it.first->second; // Old index to which i is mapped.
     104             :       // If label i occurred in l1 and were not both mapped to the hidden label, raise an exception.
     105          18 :       if (l1.is_tau(l1.apply_hidden_label_map(new_index)) != l2.is_tau(l2.apply_hidden_label_map(i)))
     106             :       {
     107           0 :         throw mcrl2::runtime_error("The action " + pp(l2.action_label(i)) + " has incompatible hidden actions " +
     108             :                                        pp(l1.action_label(l1.apply_hidden_label_map(new_index))) + " and " +
     109             :                                        pp(l2.action_label(l2.apply_hidden_label_map(i))) + ".");
     110             :       }
     111             : 
     112             :     }
     113          18 :     assert(new_index==it.first->second);
     114             :   }
     115             : 
     116             :   // Update the label numbers of all transitions of the LTS l1 to reflect
     117             :   // the new indices as given by labs.
     118           6 :   std::vector<transition> &trans1=l1.get_transitions();
     119          34 :   for (transition& t : trans1)
     120             :   {
     121          28 :     t.set_label(labs[l1.action_label(t.label())]);
     122             :   }
     123             : 
     124             :   // Now add the transition labels of LTS l2
     125             :   // Now add the source and target states of the transitions of LTS l2.
     126             :   // The labels will be added below, depending on whether there is label
     127             :   // information in both LTSs.
     128           6 :   const std::vector<transition> &trans2=l2.get_transitions();
     129          36 :   for (const transition transition_to_add : trans2)
     130             :   {
     131          30 :     l1.add_transition(transition(transition_to_add.from()+old_nstates,
     132          60 :                                  labs[l2.action_label(transition_to_add.label())],
     133          30 :                                  transition_to_add.to()+old_n_prob_states));
     134             :   }
     135             :   
     136             :   // Now update the state number for each probability pairs of all
     137             :   // probabilistic states
     138           6 :   const std::size_t n_prob_states_l2 = l2.num_probabilistic_states();
     139          18 :   for (std::size_t i = 0; i < n_prob_states_l2; ++i)
     140             :   {
     141          12 :     typename LTS_TYPE::probabilistic_state_t new_prob_state;
     142          12 :     const typename LTS_TYPE::probabilistic_state_t& old_prob_state = l2.probabilistic_state(i);
     143             : 
     144          12 :     if (old_prob_state.size()>1)
     145             :     {
     146          36 :       for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : old_prob_state)
     147             :       {
     148          24 :         new_prob_state.add(sp_pair.state()+ old_nstates, sp_pair.probability());
     149             :       }
     150             : 
     151             :     }
     152             :     else
     153             :     {
     154           0 :       new_prob_state.set(old_prob_state.get()+old_nstates);
     155             :     }
     156          12 :     l1.add_probabilistic_state(new_prob_state);
     157             :   }
     158             : 
     159             :   // Add the initial probabilistic state of both plts at the end of the merged plts.
     160             :   // First add the initia probabilistic state of l1
     161           6 :   l1.add_probabilistic_state(l1.initial_probabilistic_state());
     162             : 
     163             :   // Then add the initia probabilistic state of l2
     164           6 :   typename LTS_TYPE::probabilistic_state_t new_initial_prob_state_l2;
     165           6 :   if (l2.initial_probabilistic_state().size()<=1)
     166             :   {
     167           6 :     new_initial_prob_state_l2.set(l2.initial_probabilistic_state().get() + old_nstates);
     168             :   }
     169             :   else // If the initial state is a distribution with more than one state.
     170             :   {
     171           0 :     for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : l2.initial_probabilistic_state())
     172             :     {
     173           0 :       new_initial_prob_state_l2.add(sp_pair.state() + old_nstates, sp_pair.probability());
     174             :     }
     175             :   }
     176           6 :   l1.add_probabilistic_state(new_initial_prob_state_l2);
     177           6 : }
     178             : } // namespace detail
     179             : } // namespace lts
     180             : } // namespace mcrl2
     181             : 
     182             : 
     183             : #endif  // MCRL2_LTS_LIBLTS_PLTS_MERGE_H