mCRL2
Loading...
Searching...
No Matches
liblts_merge.h
Go to the documentation of this file.
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>
33#include "mcrl2/lts/lts.h"
34
35namespace mcrl2
36{
37namespace lts
38{
39namespace detail
40{
41
42template <class LTS_TYPE>
43void merge(LTS_TYPE& l1, const LTS_TYPE& l2)
44{
45 const std::size_t old_nstates=l1.num_states();
46 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 if (l1.has_state_info() && l2.has_state_info())
51 {
52 for (std::size_t i=0; i<l2.num_states(); ++i)
53 {
54 l1.add_state(l2.state_label(i));
55 }
56 }
57 else
58 {
59 // remove state information from this LTS, if any
60 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 std::map < action_label_type,label_index > labs;
71
72 // Put the labels of the LTS l1 in a map.
73 for (std::size_t i = 0; i < l1.num_action_labels(); ++i)
74 {
75 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 for (std::size_t i=0; i<l2.num_action_labels(); ++i)
86 {
87 typename LTS_TYPE::labels_size_type new_index;
88 const insert_type it=labs.insert(std::pair < action_label_type,label_index >
89 (l2.action_label(i),l1.num_action_labels()));
90 if (it.second)
91 {
92 // New element has been inserted.
93 new_index=l1.add_action(l2.action_label(i));
94 if (l2.is_tau(l2.apply_hidden_label_map(i)))
95 {
96 l1.hidden_label_set().insert(new_index);
97 }
98
99 }
100 else
101 {
102 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 if (l1.is_tau(l1.apply_hidden_label_map(new_index)) != l2.is_tau(l2.apply_hidden_label_map(i)))
106 {
107 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 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 std::vector<transition>& trans1=l1.get_transitions();
118 for (std::vector<transition>::iterator r=trans1.begin(); r!=trans1.end(); ++r)
119 {
120 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 const std::vector<transition>& trans2=l2.get_transitions();
128 for (std::vector<transition>::const_iterator r=trans2.begin(); r!=trans2.end(); ++r)
129 {
130 const transition transition_to_add=*r;
131 l1.add_transition(transition(transition_to_add.from()+old_nstates,
132 labs[l2.action_label(transition_to_add.label())],
133 transition_to_add.to()+old_nstates));
134 }
135
136}
137} // namespace detail
138} // namespace lts
139} // namespace mcrl2
140
141
142#endif
A class containing triples, source label and target representing transitions.
Definition transition.h:43
size_type from() const
The source of the transition.
Definition transition.h:77
size_type label() const
The label of the transition.
Definition transition.h:83
size_type to() const
The target of the transition.
Definition transition.h:90
Standard exception class for reporting runtime errors.
Definition exception.h:27
Exception classes for use in libraries and tools.
The file containing the core class for transition systems.
std::string pp(const detail::lhs_t &lhs)
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72