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

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg, Jan Friso Groote
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : 
      10             : // This file contains the merge algorithm that merges two lts'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_MERGE_H
      29             : #define MCRL2_LTS_LIBLTS_MERGE_H
      30             : 
      31             : #include "mcrl2/utilities/exception.h"
      32             : #include "mcrl2/lts/lts.h"
      33             : 
      34             : namespace mcrl2
      35             : {
      36             : namespace lts
      37             : {
      38             : namespace detail
      39             : {
      40             : 
      41             : template <class LTS_TYPE>
      42         140 : void merge(LTS_TYPE& l1, const LTS_TYPE& l2)
      43             : {
      44         140 :   const std::size_t old_nstates=l1.num_states();
      45         140 :   l1.set_num_states(l1.num_states() + l2.num_states());
      46             : 
      47             :   // The resulting LTS will have state information only if BOTH LTSs
      48             :   // currently have state information.
      49         140 :   if (l1.has_state_info() && l2.has_state_info())
      50             :   {
      51           0 :     for (std::size_t i=0; i<l2.num_states(); ++i)
      52             :     {
      53           0 :       l1.add_state(l2.state_label(i));
      54             :     }
      55             :   }
      56             :   else
      57             :   {
      58             :     // remove state information from this LTS, if any
      59         140 :     l1.clear_state_labels();
      60             :   }
      61             : 
      62             :   // Before we can set the label data in a new transitions
      63             :   // array, we first have to collect the labels of both LTSs in a
      64             :   // map, of which the second element indicates the new index of each action label.
      65             : 
      66             :   typedef typename LTS_TYPE::action_label_t action_label_type;
      67             :   typedef typename LTS_TYPE::labels_size_type label_index;
      68             :   typedef typename std::pair< typename std::map < action_label_type,label_index >::const_iterator, bool > insert_type;
      69         280 :   std::map < action_label_type,label_index > labs;
      70             : 
      71             :   // Put the labels of the LTS l1 in a map.
      72         713 :   for (std::size_t i = 0; i < l1.num_action_labels(); ++i)
      73             :   {
      74         573 :     labs.insert(std::pair <typename LTS_TYPE::action_label_t,typename LTS_TYPE::labels_size_type>
      75             :                 (l1.action_label(i),i));
      76             :   }
      77             :   // Add the labels for the LTS l2, and put them there with a new index if it was
      78             :   // not added yet.
      79             :   // Furthermore, update the hidden_label_map. 
      80             :   // If label a1 is mapped to a2 in l2, then this must be the same
      81             :   // in l1. It may be that label a1 did not exist yet in which case it needs
      82             :   // to be added too.
      83             : 
      84         712 :   for (std::size_t i=0; i<l2.num_action_labels(); ++i)
      85             :   {
      86             :     typename LTS_TYPE::labels_size_type new_index;
      87         572 :     const insert_type it=labs.insert(std::pair < action_label_type,label_index >
      88             :                                (l2.action_label(i),l1.num_action_labels()));
      89         572 :     if (it.second) 
      90             :     {
      91             :       // New element has been inserted.
      92           8 :       new_index=l1.add_action(l2.action_label(i));
      93           8 :       if (l2.is_tau(l2.apply_hidden_label_map(i)))
      94             :       {
      95           0 :         l1.hidden_label_map()[new_index]=l1.tau_label_index();
      96             :       }
      97             : 
      98             :     }
      99             :     else 
     100             :     {
     101         564 :       new_index=it.first->second; // Old index to which i is mapped.
     102             : 
     103             :       // If label i occurred in l1 and was not mapped to the same hidden label, raise an exception.
     104         564 :       if (l1.is_tau(l1.apply_hidden_label_map(new_index)) != l2.is_tau(l2.apply_hidden_label_map(i)))
     105             :       {
     106             :         throw mcrl2::runtime_error("The action " + pp(l2.action_label(i)) + " has incompatible hidden actions " +
     107             :                                        pp(l1.action_label(l1.apply_hidden_label_map(new_index))) + " and " + 
     108           0 :                                        pp(l2.action_label(l2.apply_hidden_label_map(i))) + ".");
     109             :       }
     110             :     }
     111         572 :     assert(new_index==it.first->second);
     112             :   }
     113             : 
     114             :   // Update the label numbers of all transitions of the LTS l1 to reflect
     115             :   // the new indices as given by labs.
     116         140 :   std::vector<transition>& trans1=l1.get_transitions();
     117         745 :   for (std::vector<transition>::iterator r=trans1.begin(); r!=trans1.end(); ++r)
     118             :   {
     119         605 :     r->set_label(labs[l1.action_label(r->label())]);
     120             :   }
     121             : 
     122             :   // Now add the transition labels of LTS l2
     123             :   // Now add the source and target states of the transitions of LTS l2.
     124             :   // The labels will be added below, depending on whether there is label
     125             :   // information in both LTSs.
     126         140 :   const std::vector<transition>& trans2=l2.get_transitions();
     127         732 :   for (std::vector<transition>::const_iterator r=trans2.begin(); r!=trans2.end(); ++r)
     128             :   {
     129         592 :     const transition transition_to_add=*r;
     130        1776 :     l1.add_transition(transition(transition_to_add.from()+old_nstates,
     131        1184 :                                  labs[l2.action_label(transition_to_add.label())],
     132         592 :                                  transition_to_add.to()+old_nstates));
     133             :   }
     134             : 
     135         140 : }
     136             : } // namespace detail
     137             : } // namespace lts
     138             : } // namespace mcrl2
     139             : 
     140             : 
     141             : #endif

Generated by: LCOV version 1.13