mCRL2
Loading...
Searching...
No Matches
liblts_plts_merge.h
Go to the documentation of this file.
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
35namespace mcrl2
36{
37namespace lts
38{
39namespace detail
40{
41
42template <class LTS_TYPE>
43void plts_merge(LTS_TYPE& l1, const LTS_TYPE& l2)
44{
45 const std::size_t old_nstates=l1.num_states();
46 const std::size_t old_n_prob_states = l1.num_probabilistic_states();
47 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 if (l1.has_state_info() && l2.has_state_info())
52 {
53 for (std::size_t i=0; i<l2.num_states(); ++i)
54 {
55 l1.add_state(l2.state_label(i));
56 }
57 }
58 else
59 {
60 // remove state information from this LTS, if any
61 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 std::map < type1,type2 > labs;
72
73 // Put the labels of the LTS l1 in a map.
74 for (std::size_t i = 0; i < l1.num_action_labels(); ++i)
75 {
76 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 for (std::size_t i=0; i<l2.num_action_labels(); ++i)
88 {
89 typename LTS_TYPE::labels_size_type new_index;
90 const insert_type it= labs.insert(std::pair < type1,type2 >
91 (l2.action_label(i),l1.num_action_labels()));
92 if (it.second)
93 {
94 // New element has been inserted.
95 new_index=l1.add_action(l2.action_label(i));
96 if (l2.is_tau(l2.apply_hidden_label_map(i)))
97 {
98 l1.hidden_label_set().insert(new_index);
99 }
100 }
101 else
102 {
103 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 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 }
113 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 std::vector<transition> &trans1=l1.get_transitions();
119 for (transition& t : trans1)
120 {
121 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 const std::vector<transition> &trans2=l2.get_transitions();
129 for (const transition transition_to_add : trans2)
130 {
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_n_prob_states));
134 }
135
136 // Now update the state number for each probability pairs of all
137 // probabilistic states
138 const std::size_t n_prob_states_l2 = l2.num_probabilistic_states();
139 for (std::size_t i = 0; i < n_prob_states_l2; ++i)
140 {
141 typename LTS_TYPE::probabilistic_state_t new_prob_state;
142 const typename LTS_TYPE::probabilistic_state_t& old_prob_state = l2.probabilistic_state(i);
143
144 if (old_prob_state.size()>1)
145 {
146 for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : old_prob_state)
147 {
148 new_prob_state.add(sp_pair.state()+ old_nstates, sp_pair.probability());
149 }
150
151 }
152 else
153 {
154 new_prob_state.set(old_prob_state.get()+old_nstates);
155 }
156 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 l1.add_probabilistic_state(l1.initial_probabilistic_state());
162
163 // Then add the initia probabilistic state of l2
164 typename LTS_TYPE::probabilistic_state_t new_initial_prob_state_l2;
165 if (l2.initial_probabilistic_state().size()<=1)
166 {
167 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 for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : l2.initial_probabilistic_state())
172 {
173 new_initial_prob_state_l2.add(sp_pair.state() + old_nstates, sp_pair.probability());
174 }
175 }
176 l1.add_probabilistic_state(new_initial_prob_state_l2);
177}
178} // namespace detail
179} // namespace lts
180} // namespace mcrl2
181
182
183#endif // MCRL2_LTS_LIBLTS_PLTS_MERGE_H
A class containing triples, source label and target representing transitions.
Definition transition.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
This file contains a class that contains labelled transition systems in aut format.
This file contains a class that contains labelled transition systems in fsm format.
This file contains a class that contains labelled transition systems in lts (mcrl2) format.
std::string pp(const detail::lhs_t &lhs)
void plts_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