mCRL2
Loading...
Searching...
No Matches
liblts_ready_sim.h
Go to the documentation of this file.
1
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//
11
12#ifndef MCRL2_LTS_LIBLTS_READY_SIM_H
13#define MCRL2_LTS_LIBLTS_READY_SIM_H
14
16
17
18namespace mcrl2
19{
20namespace lts
21{
22namespace detail
23{
24
25template <class LTS_TYPE>
26 class ready_sim_partitioner : public sim_partitioner<LTS_TYPE>
27{
28 public:
29 ready_sim_partitioner(LTS_TYPE& l) : sim_partitioner<LTS_TYPE>(l)
30 {
31 exists2 = new hash_table2(1000);
32 forall2 = new hash_table2(1000);
33 };
34
39 virtual void partitioning_algorithm();
42 private :
43 // Non inherited data members...
46
47 // Non inherited methods...
55
64 void refinei() ;
65
66 /*
67 * Induce P on Pi, then
68 * drops those pairs (alpha, beta)
69 * such that
70 * {N} E<-l- Beta and not {N} A<-l- Alpha
71 * \pre : refinei called
72 */
73 void updatei();
74
75
76 // Non inherited auxiliary methods...
77 std::string print_structure(hash_table2* struc);
78
79 // Inherited data members...
80 using sim_partitioner<LTS_TYPE>::aut;
81 using sim_partitioner<LTS_TYPE>::s_Pi;
82 using sim_partitioner<LTS_TYPE>::s_Sigma;
83 using sim_partitioner<LTS_TYPE>::block_Pi;
84 using sim_partitioner<LTS_TYPE>::children;
85 using sim_partitioner<LTS_TYPE>::parent;
86 using sim_partitioner<LTS_TYPE>::Q;
87 using sim_partitioner<LTS_TYPE>::P;
88 using sim_partitioner<LTS_TYPE>::contents_t;
89 using sim_partitioner<LTS_TYPE>::contents_u;
90 using sim_partitioner<LTS_TYPE>::touched_blocks;
91 using sim_partitioner<LTS_TYPE>::block_touched;
92 using sim_partitioner<LTS_TYPE>::state_buckets;
93
94 // Inherited methods
95 using sim_partitioner<LTS_TYPE>::induce_P_on_Pi;
96 using sim_partitioner<LTS_TYPE>::initialise_Sigma;
99 using sim_partitioner<LTS_TYPE>::touch;
100 using sim_partitioner<LTS_TYPE>::untouch;
101
102 // Auxiliary inherited methods
103 using sim_partitioner<LTS_TYPE>::print_relation;
104 using sim_partitioner<LTS_TYPE>::print_Sigma_P;
105 using sim_partitioner<LTS_TYPE>::print_Pi_Q;
106
107};
108
109
110/* Pre : true */
111template <class LTS_TYPE>
113{
114 initialise_datastructures();
115 refinei();
116 updatei();
117 s_Sigma = s_Pi; // <== Key!!
118 P.swap(Q); // <== Key!!
119 mCRL2log(log::debug) << "--------------------- READY PRE-REDUCTION-------------------------" << std::endl;
120 mCRL2log(log::debug) << " prereduction; number of blocks: " << s_Sigma << std::endl;
121}
122
123/* ----------------- PARTITIONING ALGORITHM ------------------------- */
124/* Pre : true */
125template <class LTS_TYPE>
127{
128 // ready_sim problem amounts to GCPP previous reduction
129 ready2sim_reduction();
130 partitioning_algorithmG();
131}
132
133/* ----------------- REFINE ----------------------------------------- */
134
135/* PRE: s_Sigma = s_Pi = 1 */
136template <class LTS_TYPE>
138{
139 using namespace mcrl2::core;
140 /* Initialise the parent and children functions */
141 std::vector<std::size_t> v;
142 children.clear();
143 children.assign(s_Pi,v);
144 parent.clear();
145 parent.assign(s_Pi,UNIVERSAL_PART);
146 std::size_t alpha;
147 for (alpha = 0; alpha < s_Pi; ++alpha)
148 {
149 children[alpha].push_back(alpha);
150 parent[alpha] = alpha;
151 }
152
153 if (mCRL2logEnabled(log::debug))
154 {
155 mCRL2log(log::debug) << "---------------- Refinei ---------------------------------------" << std::endl;
156 mCRL2log(log::debug) << print_Sigma_P();
157 }
158
159 /* Some local variables */
160 std::vector<std::size_t>::iterator alphai, last;
161 std::size_t l;
162
163 /* The main loop */
164 for (l = 0; l < aut.num_action_labels(); ++l)
165 {
166 mCRL2log(log::debug) << "---------------------------------------------------" << std::endl;
167 mCRL2log(log::debug) << "Label = \"" << mcrl2::lts::pp(aut.action_label(l)) << "\"" << std::endl;
168
169 touched_blocks.clear();
170 initialise_Sigma(UNIVERSAL_PART,l); // Interested on {N} E<-l- alpha
171
172 /* iterate over all alpha such that {N} E<-l- alpha */
173 last = touched_blocks.end();
174 for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
175 {
176 alpha = *alphai;
177 /* if {N} A<-l- alpha then alpha cannot be split */
178 if (contents_u[alpha] != LIST_END)
179 {
180 /* split alpha; new block will be s_Pi */
181 children[parent[alpha]].push_back(s_Pi);
182 parent.push_back(parent[alpha]);
183 block_touched.push_back(false);
184 contents_t.push_back(LIST_END);
185
186 /* assign the untouched contents of alpha to s_Pi */
187 contents_u.push_back(contents_u[alpha]);
188 contents_u[alpha] = LIST_END;
189
190 /* update the block information for the moved states */
191 for (ptrdiff_t i = contents_u[s_Pi]; i != LIST_END;
192 i = state_buckets[i].next)
193 {
194 block_Pi[i] = s_Pi;
195 }
196 ++s_Pi;
197 }
198 untouch(alpha);
199 }
200 }
201}
202
203
204/* ----------------- UPDATEI ----------------------------------------- */
205template <class LTS_TYPE>
207{
208 using namespace mcrl2::core;
209 mCRL2log(log::debug) << "--------------- Updatei ---------------------------------------" << std::endl;
210
211 std::size_t l,alpha,gamma;
212 std::vector<std::size_t>::iterator alphai, last;
213
214 induce_P_on_Pi();
215
216 exists2->clear();
217 forall2->clear();
218
219 for (l = 0; l < aut.num_action_labels(); ++l)
220 {
221 for (gamma = 0; gamma < s_Sigma; ++gamma)
222 {
223 touched_blocks.clear();
224 initialise_Sigma(gamma,l);
225 last = touched_blocks.end();
226 for (alphai = touched_blocks.begin(); alphai != last; ++alphai)
227 {
228 alpha = *alphai;
229 exists2->add(alpha,l);
230 if (contents_u[alpha] == LIST_END)
231 {
232 forall2->add(alpha,l);
233 }
234 untouch(alpha);
235 }
236 }
237 }
238
239 mCRL2log(log::debug) << "------ Before Filter ------\nExists2: ";
240 mCRL2log(log::debug) << print_structure(exists2);
241 mCRL2log(log::debug) << "\nForall2: ";
242 mCRL2log(log::debug) << print_structure(forall2);
243 mCRL2log(log::debug) << "\nReady Preorder: ";
244 mCRL2log(log::debug) << print_relation(s_Pi,Q);
245
246 std::size_t beta;
247
248 /* Apply the filtering to discard non "ready-init" pairs,
249 * in Q[alpha][beta], i.e., when
250 * {N} E<-l- Beta and not {N} A<-l- Alpha
251 */
252 for (l = 0; l < aut.num_action_labels(); ++l)
253 {
254 for (beta = 0; beta < s_Pi; ++beta)
255 {
256 if (exists2->find(beta,l))
257 {
258 for (alpha = 0; alpha < s_Pi; ++alpha)
259 if (Q[alpha][beta] && !forall2->find(alpha,l))
260 Q[alpha][beta] = false ;
261 }
262 }
263 };
264
265 mCRL2log(log::debug) << "----- After Filter ------\nExists2: ";
266 mCRL2log(log::debug) << print_structure(exists2);
267 mCRL2log(log::debug) << "\nForall2: ";
268 mCRL2log(log::debug) << print_structure(forall2);
269 mCRL2log(log::debug) << "\nReady Preorder: ";
270 mCRL2log(log::debug) << print_relation(s_Pi,Q);
271}
272
273template <class LTS_TYPE>
275{
276 using namespace mcrl2::core;
277 std::stringstream result;
278 result << "{";
279 hash_table2_iterator i(struc);
280 for (; !i.is_end(); ++i)
281 {
282 result << "(" << i.get_x() << "," << mcrl2::lts::pp(aut.action_label(i.get_y()))<< "),";
283 }
284 result << "}";
285 return result.str();
286}
287
288template <class LTS_TYPE>
290{
291 delete exists2;
292 delete forall2;
293}
294
295
296} // namespace detail
297} // namespace lts
298} // namespacemcrl2
299#endif
std::size_t get_x()
std::size_t get_y()
std::string print_structure(hash_table2 *struc)
std::vector< ptrdiff_t > contents_t
Definition liblts_sim.h:110
std::vector< std::size_t > touched_blocks
Definition liblts_sim.h:122
void initialise_Sigma(std::size_t gamma, std::size_t l)
Definition liblts_sim.h:341
std::vector< ptrdiff_t > contents_u
Definition liblts_sim.h:111
std::vector< bool > block_touched
Definition liblts_sim.h:105
std::vector< std::size_t > block_Pi
Definition liblts_sim.h:107
std::string print_relation(std::size_t s, std::vector< std::vector< bool > > &R)
std::vector< std::size_t > parent
Definition liblts_sim.h:108
std::vector< state_bucket > state_buckets
Definition liblts_sim.h:106
void touch(std::size_t a, std::size_t alpha)
Definition liblts_sim.h:490
std::vector< std::vector< bool > > P
Definition liblts_sim.h:118
void untouch(std::size_t alpha)
Definition liblts_sim.h:518
std::vector< std::vector< std::size_t > > children
Definition liblts_sim.h:109
std::vector< std::vector< bool > > Q
Definition liblts_sim.h:119
Header file for the simulation preorder algorithm.
#define LIST_END
Definition liblts_sim.h:157
#define UNIVERSAL_PART
Definition liblts_sim.h:158
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
std::string pp(const abstraction &x)
Definition data.cpp:39
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72