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 <map> 32 : #include "mcrl2/utilities/exception.h" 33 : #include "mcrl2/lts/lts.h" 34 : 35 : namespace mcrl2 36 : { 37 : namespace lts 38 : { 39 : namespace detail 40 : { 41 : 42 : template <class LTS_TYPE> 43 143 : void merge(LTS_TYPE& l1, const LTS_TYPE& l2) 44 : { 45 143 : const std::size_t old_nstates=l1.num_states(); 46 143 : l1.set_num_states(l1.num_states() + l2.num_states()); 47 : 48 : // The resulting LTS will have state information only if BOTH LTSs 49 : // currently have state information. 50 143 : if (l1.has_state_info() && l2.has_state_info()) 51 : { 52 61 : for (std::size_t i=0; i<l2.num_states(); ++i) 53 : { 54 46 : l1.add_state(l2.state_label(i)); 55 : } 56 : } 57 : else 58 : { 59 : // remove state information from this LTS, if any 60 128 : l1.clear_state_labels(); 61 : } 62 : 63 : // Before we can set the label data in a new transitions 64 : // array, we first have to collect the labels of both LTSs in a 65 : // map, of which the second element indicates the new index of each action label. 66 : 67 : typedef typename LTS_TYPE::action_label_t action_label_type; 68 : typedef typename LTS_TYPE::labels_size_type label_index; 69 : typedef typename std::pair< typename std::map < action_label_type,label_index >::const_iterator, bool > insert_type; 70 143 : std::map < action_label_type,label_index > labs; 71 : 72 : // Put the labels of the LTS l1 in a map. 73 726 : for (std::size_t i = 0; i < l1.num_action_labels(); ++i) 74 : { 75 583 : labs.insert(std::pair <typename LTS_TYPE::action_label_t,typename LTS_TYPE::labels_size_type> 76 : (l1.action_label(i),i)); 77 : } 78 : // Add the labels for the LTS l2, and put them there with a new index if it was 79 : // not added yet. 80 : // Furthermore, update the hidden_label_set. 81 : // If label a1 is mapped to a2 in l2, then this must be the same 82 : // in l1. It may be that label a1 did not exist yet in which case it needs 83 : // to be added too. 84 : 85 725 : for (std::size_t i=0; i<l2.num_action_labels(); ++i) 86 : { 87 : typename LTS_TYPE::labels_size_type new_index; 88 582 : const insert_type it=labs.insert(std::pair < action_label_type,label_index > 89 582 : (l2.action_label(i),l1.num_action_labels())); 90 582 : if (it.second) 91 : { 92 : // New element has been inserted. 93 8 : new_index=l1.add_action(l2.action_label(i)); 94 8 : if (l2.is_tau(l2.apply_hidden_label_map(i))) 95 : { 96 0 : l1.hidden_label_set().insert(new_index); 97 : } 98 : 99 : } 100 : else 101 : { 102 574 : new_index=it.first->second; // Old index to which i is mapped. 103 : 104 : // If label i occurred in l1 and both were not mapped to the hidden label, raise an exception. 105 574 : 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 582 : assert(new_index==it.first->second); 113 : } 114 : 115 : // Update the label numbers of all transitions of the LTS l1 to reflect 116 : // the new indices as given by labs. 117 143 : std::vector<transition>& trans1=l1.get_transitions(); 118 768 : for (std::vector<transition>::iterator r=trans1.begin(); r!=trans1.end(); ++r) 119 : { 120 625 : r->set_label(labs[l1.action_label(r->label())]); 121 : } 122 : 123 : // Now add the transition labels of LTS l2 124 : // Now add the source and target states of the transitions of LTS l2. 125 : // The labels will be added below, depending on whether there is label 126 : // information in both LTSs. 127 143 : const std::vector<transition>& trans2=l2.get_transitions(); 128 754 : for (std::vector<transition>::const_iterator r=trans2.begin(); r!=trans2.end(); ++r) 129 : { 130 611 : const transition transition_to_add=*r; 131 611 : l1.add_transition(transition(transition_to_add.from()+old_nstates, 132 1222 : labs[l2.action_label(transition_to_add.label())], 133 611 : transition_to_add.to()+old_nstates)); 134 : } 135 : 136 143 : } 137 : } // namespace detail 138 : } // namespace lts 139 : } // namespace mcrl2 140 : 141 : 142 : #endif