Line data Source code
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 : /// \file lts/detail/liblts_pbisim_bem.h
10 :
11 : #ifndef _LIBLTS_PBISIM_BEM_H
12 : #define _LIBLTS_PBISIM_BEM_H
13 : #include "mcrl2/utilities/execution_timer.h"
14 : #include "mcrl2/lts/detail/liblts_plts_merge.h"
15 :
16 : namespace mcrl2
17 : {
18 : namespace lts
19 : {
20 : namespace detail
21 : {
22 :
23 : template < class LTS_TYPE>
24 : class prob_bisim_partitioner_bem
25 : {
26 :
27 : public:
28 : /** \brief Creates a probabilistic bisimulation partitioner for an PLTS.
29 : * \details This bisimulation partitioner applies the algorithm defined in C. Baier, B. Engelen and M. Majster-Cederbaum.
30 : * Deciding Bisimilarity and Similarity for Probabilistic Processes. In Journal of Computer and System Sciences 60, 187-237 (2000)
31 : */
32 7 : prob_bisim_partitioner_bem(LTS_TYPE& l, utilities::execution_timer& timer):aut(l)
33 : {
34 7 : mCRL2log(log::verbose) << "Probabilistic bisimulation partitioner created for "
35 0 : << l.num_states() << " states and " <<
36 0 : l.num_transitions() << " transitions\n";
37 7 : timer.start("bisimulation_reduce (bem)");
38 7 : create_initial_partition();
39 7 : refine_partition_until_it_becomes_stable();
40 7 : timer.finish("bisimulation_reduce (bem)");
41 7 : postprocessing_stage();
42 7 : }
43 :
44 : /** \brief Gives the number of bisimulation equivalence classes of the LTS.
45 : * \return The number of bisimulation equivalence classes of the LTS.
46 : */
47 7 : std::size_t num_eq_classes() const
48 : {
49 7 : return state_partition.size();
50 : }
51 :
52 : /** \brief Gives the bisimulation equivalence class number of a state.
53 : * \param[in] s A state number.
54 : * \return The number of the bisimulation equivalence class to which \e s belongs. */
55 485 : std::size_t get_eq_class(const std::size_t s) const
56 : {
57 485 : assert(s<block_index_of_a_state.size());
58 485 : return block_index_of_a_state[s]; // The block index is the state number of the block.
59 : }
60 :
61 : /** \brief Gives the bisimulation equivalence step class number of a probabilistic state.
62 : * \param[in] s A probabilistic state number.
63 : * \return The number of the step class to which s belongs. */
64 292 : std::size_t get_eq_step_class(const std::size_t d) const
65 : {
66 292 : assert(d < step_class_index_of_a_distribution.size());
67 292 : assert(step_class_index_of_a_distribution[d] < step_classes.size());
68 292 : assert(step_classes[step_class_index_of_a_distribution[d]].equivalent_step_class < step_classes.size());
69 292 : return step_classes[step_class_index_of_a_distribution[d]].equivalent_step_class;
70 : }
71 :
72 : /** \brief Replaces the transition relation of the current lts by the transitions
73 : * of the bisimulation reduced transition system.
74 : * \pre The bisimulation equivalence classes have been computed. */
75 7 : void replace_transitions()
76 : {
77 7 : std::set < transition > resulting_transitions;
78 :
79 7 : const std::vector<transition>& trans = aut.get_transitions();
80 299 : for (const transition& t : trans)
81 : {
82 292 : resulting_transitions.insert(
83 584 : transition(
84 : get_eq_class(t.from()),
85 : t.label(),
86 : get_eq_step_class(t.to())));
87 : }
88 : // Remove the old transitions
89 7 : aut.clear_transitions();
90 :
91 : // Copy the transitions from the set into the transition system.
92 47 : for (const transition& t : resulting_transitions)
93 : {
94 40 : aut.add_transition(t);
95 : }
96 7 : }
97 :
98 : /** \brief Replaces the probabilistic states of the current lts by the probabilistic
99 : * states of the bisimulation reduced transition system.
100 : * \pre The bisimulation step classes have been computed. */
101 7 : void replace_probabilistic_states()
102 : {
103 7 : std::vector<typename LTS_TYPE::probabilistic_state_t> new_probabilistic_states;
104 :
105 : // get the equivalent probabilistic state of each probabilistic block and add it to aut
106 38 : for (step_class_type& sc : equivalent_step_classes)
107 : {
108 31 : typename LTS_TYPE::probabilistic_state_t equivalent_ps = calculate_equivalent_probabilistic_state(sc);
109 31 : new_probabilistic_states.push_back(equivalent_ps);
110 : }
111 :
112 : /* Remove old probabilistic states */
113 7 : aut.clear_probabilistic_states();
114 :
115 : // Add new prob states to aut
116 38 : for (const typename LTS_TYPE::probabilistic_state_t& new_ps : new_probabilistic_states)
117 : {
118 31 : aut.add_probabilistic_state(new_ps);
119 : }
120 :
121 7 : typename LTS_TYPE::probabilistic_state_t old_initial_prob_state = aut.initial_probabilistic_state();
122 7 : typename LTS_TYPE::probabilistic_state_t new_initial_prob_state = calculate_new_probabilistic_state(old_initial_prob_state);
123 7 : aut.set_initial_probabilistic_state(new_initial_prob_state);
124 7 : }
125 :
126 : /** \brief Returns whether two states are in the same probabilistic bisimulation equivalence class.
127 : * \param[in] s A state number.
128 : * \param[in] t A state number.
129 : * \retval true if \e s and \e t are in the same bisimulation equivalence class;
130 : * \retval false otherwise. */
131 : bool in_same_probabilistic_class(const std::size_t s, const std::size_t t) const
132 : {
133 : return get_eq_step_class(s) == get_eq_step_class(t);
134 : }
135 :
136 : private:
137 :
138 : typedef std::size_t block_key_type;
139 : typedef std::size_t step_class_key_type;
140 : typedef std::size_t state_type;
141 : typedef std::size_t label_type;
142 : typedef std::size_t distribution_key_type;
143 : typedef typename LTS_TYPE::probabilistic_state_t::probability_t probability_fraction_type;
144 :
145 : struct distribution_type
146 : {
147 : distribution_key_type key;
148 : std::vector< std::list<transition*> > incoming_transitions_per_label; // Incoming transitions organized per label
149 : };
150 :
151 : struct block_type
152 : {
153 : block_key_type key;
154 : std::list<state_type> states; // The states in the block
155 : bool is_in_new_blocks;
156 : };
157 :
158 : struct step_class_type {
159 : step_class_key_type key;
160 : label_type action; // action label of the pair <a,M>.
161 : std::list<distribution_type*> distributions; // The distributions in the step class <a,M>.
162 : std::vector< bool > prev_states; // Previous states that can reach step_class <a,M>
163 : bool is_in_new_step_classes;
164 : std::size_t equivalent_step_class;
165 : };
166 :
167 : std::list<block_type*> state_partition;
168 : std::list<step_class_type*> step_partition;
169 : std::vector<distribution_type> distributions;
170 : std::deque<step_class_type> step_classes;
171 : std::deque<step_class_type> equivalent_step_classes;
172 : std::deque<block_type> blocks;
173 : std::vector<block_key_type> block_index_of_a_state;
174 : std::vector<step_class_key_type> step_class_index_of_a_distribution;
175 :
176 : LTS_TYPE& aut;
177 :
178 : struct tree_type
179 : {
180 : std::list<state_type> states;
181 : std::size_t count;
182 : tree_type* left;
183 : tree_type* right;
184 :
185 63 : void init_node()
186 : {
187 63 : count = 0;
188 63 : left = NULL;
189 63 : right = NULL;
190 63 : }
191 : };
192 :
193 : /** \brief Creates the initial partition of step classes and blocks.
194 : * \detail The blocks are initially partitioned based on the actions that can perform.
195 : * The step classes are partitioned based on the action that leads to the probabilistic state */
196 7 : void create_initial_partition (void)
197 : {
198 7 : std::vector< std::vector< std::list<distribution_type*> > > steps; // Representation of transition in 2-d array
199 7 : std::vector<transition>& transitions = aut.get_transitions();
200 7 : std::vector< std::vector<bool> > distribution_per_step_class;
201 :
202 7 : distribution_per_step_class.resize(aut.num_action_labels());
203 31 : for (std::vector<bool>& i : distribution_per_step_class)
204 : {
205 24 : i.resize(aut.num_probabilistic_states());
206 : }
207 :
208 : //---- Preprocessing stage to transform the PLTS to the data structures suggested by Baier ---- //
209 :
210 : // Construct vector of distributions
211 7 : distributions.resize(aut.num_probabilistic_states());
212 7 : std::size_t key = 0;
213 98 : for (distribution_type& distribution : distributions)
214 : {
215 91 : distribution.key = key;
216 91 : distribution.incoming_transitions_per_label.resize(aut.num_action_labels());
217 91 : key++;
218 : }
219 :
220 : // Initialize the Steps bi-dimientional array
221 7 : steps.resize(aut.num_states());
222 309 : for (std::size_t i = 0; i < steps.size(); i++)
223 : {
224 302 : steps[i].resize(aut.num_action_labels());
225 : }
226 :
227 299 : for (transition& t : transitions)
228 : {
229 292 : steps[t.from()][t.label()].push_back(&distributions[t.to()]);
230 292 : distributions[t.to()].incoming_transitions_per_label[t.label()].push_back(&t);
231 : }
232 :
233 : //---- Start the initialization process (page 207. Fig. 10. Baier) ---- //
234 :
235 : // Initially there are as many step classes as lables
236 7 : step_classes.resize(aut.num_action_labels());
237 :
238 31 : for (step_class_type& sc : step_classes)
239 : {
240 24 : sc.prev_states.resize(aut.num_states());
241 : }
242 :
243 : // create tree structure to group action states based on the outgoing transitions
244 7 : std::size_t max_block_size = 0;
245 7 : tree_type* max_block = nullptr;
246 7 : std::deque<tree_type> tree_nodes;
247 7 : std::vector<tree_type*> leaves;
248 7 : tree_type v0;
249 7 : v0.init_node();
250 7 : tree_nodes.push_back(v0);
251 :
252 : // For all s in S do
253 309 : for (state_type s = 0; s < aut.num_states(); s++)
254 : {
255 : // (1) Create pointer to root of the tree
256 302 : tree_type* v = &tree_nodes[0];
257 :
258 : // (2) Construct tree
259 1494 : for (std::size_t i = 0; i < aut.num_action_labels(); i++)
260 : {
261 1192 : step_classes[i].key = i;
262 1192 : step_classes[i].action = i;
263 1192 : if (steps[s][i].size() > 0)
264 : {
265 580 : for (distribution_type* d : steps[s][i])
266 : {
267 292 : if (distribution_per_step_class[i][d->key] == false)
268 : {
269 118 : step_classes[i].distributions.push_back(d);
270 118 : distribution_per_step_class[i][d->key] = true;
271 : }
272 : }
273 :
274 288 : step_classes[i].prev_states[s] = true;
275 :
276 288 : if (v->left == NULL)
277 : {
278 : // create left node
279 18 : tree_type w;
280 18 : w.init_node();
281 18 : tree_nodes.push_back(w);
282 18 : v->left = &tree_nodes.back();
283 :
284 : // add new node to the leaf nodes if it is a leaf
285 18 : if (i == aut.num_action_labels() - 1)
286 : {
287 7 : leaves.push_back(v->left);
288 : }
289 :
290 18 : }
291 288 : v = v->left;
292 : }
293 : else
294 : {
295 904 : if (v->right == NULL)
296 : {
297 : // create left node
298 38 : tree_type w;
299 38 : w.init_node();
300 38 : tree_nodes.push_back(w);
301 38 : v->right = &tree_nodes.back();
302 :
303 : // add new node to the leaf nodes if it is a leaf
304 38 : if (i == aut.num_action_labels() - 1)
305 : {
306 16 : leaves.push_back(v->right);
307 : }
308 38 : }
309 904 : v = v->right;
310 : }
311 : }
312 :
313 : // (3) Add the state to the leaf and increment its state counter
314 302 : v->states.push_back(s);
315 302 : v->count++;
316 :
317 : // (4) Keep track of the leave containing more states
318 302 : if (v->count > max_block_size)
319 : {
320 178 : max_block = v;
321 178 : max_block_size = v->count;
322 : }
323 : }
324 :
325 : // insert all states of the leaves to blocks
326 7 : blocks.resize(leaves.size());
327 :
328 7 : key = 0;
329 7 : std::size_t larger_key = 0;
330 30 : for (tree_type* leaf_ptr : leaves)
331 : {
332 23 : block_type& block = blocks[key];
333 23 : block.key = key;
334 23 : block.states.splice(block.states.end(), leaf_ptr->states);
335 :
336 23 : if (leaf_ptr == max_block)
337 : {
338 7 : larger_key = key;
339 : }
340 :
341 23 : key++;
342 : }
343 :
344 : // Add all blocks to the state partition.
345 : // Initially only the larger block has to be at the end of the list
346 30 : for (block_type& b : blocks)
347 : {
348 23 : if (b.key != larger_key)
349 : {
350 : // Push the non-larger blocks to the front of the list. This are the so called new blocks
351 16 : b.is_in_new_blocks = true;
352 16 : state_partition.push_front(&b);
353 : }
354 : else
355 : {
356 : // push the larger block to the end of the list
357 7 : b.is_in_new_blocks = false;
358 7 : state_partition.push_back(&b);
359 : }
360 : }
361 :
362 : // Add all step classes to the step partition.
363 : // Initially all are new step classes
364 31 : for (step_class_type& sc : step_classes)
365 : {
366 24 : if (sc.distributions.size() > 0)
367 : {
368 18 : step_partition.push_front(&sc);
369 18 : sc.is_in_new_step_classes = true;
370 : }
371 : }
372 :
373 7 : block_index_of_a_state.resize(aut.num_states());
374 30 : for (const block_type& b : blocks)
375 : {
376 325 : for (const state_type s : b.states)
377 : {
378 302 : block_index_of_a_state[s] = b.key;
379 : }
380 : }
381 :
382 7 : }
383 :
384 : /** \brief Calculates the probability to reach block b from distribution d.
385 : * \param[in] d is a probabilistic state (distribution).
386 : * b is a block of states.
387 : * \return The probability to reach block b. */
388 1189 : probability_fraction_type probability_to_block(distribution_type& d, block_type& b)
389 : {
390 1189 : probability_fraction_type prob_to_block;
391 1189 : const typename LTS_TYPE::probabilistic_state_t& prob_state = aut.probabilistic_state(d.key);
392 :
393 : /* Check whether the state is in the distribution d and add up the probability*/
394 1189 : if (prob_state.size()>1) // The state is stored as a vector of states/probabilities.
395 : {
396 5208 : for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& prob_pair : prob_state)
397 : {
398 4153 : const state_type s = prob_pair.state();
399 4153 : if (block_index_of_a_state[s] == b.key)
400 : {
401 355 : prob_to_block = prob_to_block + prob_pair.probability();
402 : }
403 : }
404 : }
405 : else // The state consists of a number with implicit probability 1.
406 : {
407 134 : const state_type s = prob_state.get();
408 134 : if (block_index_of_a_state[s] == b.key)
409 : {
410 16 : prob_to_block = prob_to_block + LTS_TYPE::probabilistic_state_t::probability_t::one();
411 : }
412 : }
413 :
414 1189 : return prob_to_block;
415 0 : }
416 :
417 77 : typename LTS_TYPE::probabilistic_state_t calculate_new_probabilistic_state(typename LTS_TYPE::probabilistic_state_t ps)
418 : {
419 77 : typename LTS_TYPE::probabilistic_state_t new_prob_state;
420 :
421 : /* Iterate over all state probability pairs in the selected probabilistic state*/
422 77 : if (ps.size()>1) // The state is stored as a vector of states/probabilities.
423 : {
424 44 : std::map<state_type, probability_fraction_type> prob_state_map;
425 204 : for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : ps)
426 : {
427 : /* Check the resulting action state in the final State partition */
428 160 : state_type new_state = get_eq_class(sp_pair.state());
429 :
430 160 : if (prob_state_map.count(new_state) == 0)
431 : {
432 : /* The state is not yet in the mapping. Add the state with its probability*/
433 112 : prob_state_map[new_state] = sp_pair.probability();
434 : }
435 : else
436 : {
437 : /* The state is already in the mapping. Sum up probabilities */
438 48 : prob_state_map[new_state] = prob_state_map[new_state] + sp_pair.probability();
439 : }
440 : }
441 : /* Add all the state probabilities pairs in the mapping to its actual data type*/
442 : /* Add all the state probabilities pairs in the mapping to its actual data type*/
443 44 : typename std::map<state_type, probability_fraction_type>::const_iterator i = prob_state_map.begin();
444 44 : if (++i==prob_state_map.end()) // There is only one state with probability 1.
445 : {
446 13 : new_prob_state.set(prob_state_map.begin()->first);
447 : }
448 : else
449 : {
450 : // This probabilistic state has more components.
451 130 : for (const std::pair<const state_type, probability_fraction_type>& i: prob_state_map)
452 : {
453 99 : new_prob_state.add(i.first, i.second);
454 : }
455 : }
456 :
457 44 : }
458 : else // The state consists of a number with implicit probability 1.
459 : {
460 : /* Check the resulting action state in the final State partition */
461 33 : new_prob_state.set(get_eq_class(ps.get()));
462 : }
463 :
464 77 : return new_prob_state;
465 0 : }
466 :
467 70 : typename LTS_TYPE::probabilistic_state_t calculate_equivalent_probabilistic_state(step_class_type& sc)
468 : {
469 70 : typename LTS_TYPE::probabilistic_state_t equivalent_prob_state;
470 :
471 : /* Select the first probabilistic state of the step class */
472 70 : distribution_type* d = sc.distributions.front();
473 :
474 70 : typename LTS_TYPE::probabilistic_state_t old_prob_state = aut.probabilistic_state(d->key);
475 :
476 70 : equivalent_prob_state = calculate_new_probabilistic_state(old_prob_state);
477 :
478 140 : return equivalent_prob_state;
479 70 : }
480 :
481 : /** \brief Two-phased partitioning algorithm described in page 204. Fig 9. Baier.
482 : * \detail Refinement of state partition and step partition until no new blocks/step classes
483 : * are in front of the partition lists
484 : */
485 7 : void refine_partition_until_it_becomes_stable (void)
486 : {
487 7 : std::list<step_class_type*> step_partition_old;
488 7 : std::list<block_type*> state_partition_old;
489 :
490 : // Repeat until no new blocks in front of the partition lists
491 71 : while (state_partition.front()->is_in_new_blocks == true ||
492 24 : (step_partition.size()>0 && step_partition.front()->is_in_new_step_classes == true))
493 : {
494 : // Phase 1: Splitting of step_partition via split(M,C)
495 40 : if (state_partition.front()->is_in_new_blocks == true)
496 : {
497 : // Choose a new block in front of the state partition and change it to the back of the list
498 35 : block_type* c_block = state_partition.front();
499 35 : state_partition.pop_front();
500 35 : state_partition.push_back(c_block);
501 35 : c_block->is_in_new_blocks = false;
502 :
503 : // swap elements of step_partition (M) to step_partition_old (M_old)
504 35 : step_partition_old.swap(step_partition);
505 :
506 : // vector to add the new step classes
507 35 : static std::vector<typename std::list<step_class_type*>::iterator> pending_new_step_classes;
508 35 : pending_new_step_classes.clear();
509 :
510 : // iterate over all step classes
511 35 : for (typename std::list<step_class_type*>::iterator sc_iter = step_partition_old.begin();
512 264 : sc_iter != step_partition_old.end(); ++sc_iter)
513 : {
514 229 : step_class_type* sc_ptr = *sc_iter;
515 :
516 : // Mapping to sort the distributions based on its probability to reach a block, instead of using
517 : // an ordered balanced tree as suggsted in Baier
518 229 : static std::map< probability_fraction_type, std::list<distribution_type*> > distributions_ordered_by_prob;
519 229 : distributions_ordered_by_prob.clear();
520 :
521 : // Iterate over all distributions d of the step class and add probability to block to vector
522 1418 : for (distribution_type* d : sc_ptr->distributions)
523 : {
524 1189 : probability_fraction_type probability = probability_to_block(*d, *c_block);
525 1189 : distributions_ordered_by_prob[probability].push_back(d);
526 : }
527 :
528 : // if there are multiple elements in the distributions_ordered_by_prob then we have to
529 : // add them to the step partition as a new step class
530 229 : if (distributions_ordered_by_prob.size() >= 2)
531 : {
532 : step_class_type* new_step_class_ptr;
533 :
534 19 : step_classes.resize(step_classes.size() + distributions_ordered_by_prob.size() - 1);
535 : // iterate over mapping
536 19 : std::size_t new_class_count = 0;
537 59 : for (std::pair< probability_fraction_type, std::list<distribution_type*> > ordered_dist : distributions_ordered_by_prob)
538 : {
539 40 : std::list<distribution_type*>& distribution_list = ordered_dist.second;
540 :
541 40 : if (new_class_count == 0)
542 : {
543 : // if it is the first element of the mapping then we do not create a new step class; instead, we
544 : // add its elements into the current step class that is being split.
545 19 : sc_ptr->distributions.swap(distribution_list);
546 :
547 : // clear the prev states of the current step class
548 2538 : for (std::size_t i = 0; i < sc_ptr->prev_states.size(); i++)
549 : {
550 2519 : sc_ptr->prev_states[i] = false;
551 : }
552 :
553 : // recalculate prev states based on incoming transitions of each distribution
554 215 : for (distribution_type* d : sc_ptr->distributions)
555 : {
556 664 : for (transition* t_ptr : d->incoming_transitions_per_label[sc_ptr->action])
557 : {
558 468 : sc_ptr->prev_states[t_ptr->from()] = true;
559 : }
560 : }
561 :
562 : // add to the front of the step partition (as a new step class) if not yet added
563 19 : if (sc_ptr->is_in_new_step_classes == false)
564 : {
565 : // since we are iterating over this step class, we save its iterator in a pending vector,
566 : // so later we can add it to the front of the step partition (outside the loop)
567 1 : pending_new_step_classes.push_back(sc_iter);
568 1 : sc_ptr->is_in_new_step_classes = true;
569 : }
570 : }
571 : else
572 : {
573 21 : new_step_class_ptr = &step_classes[step_classes.size() - new_class_count];
574 :
575 : //init new step class
576 21 : new_step_class_ptr->key = step_classes.size() - new_class_count;
577 21 : new_step_class_ptr->action = sc_ptr->action;
578 21 : new_step_class_ptr->is_in_new_step_classes = true;
579 21 : new_step_class_ptr->prev_states.resize(aut.num_states());
580 21 : new_step_class_ptr->distributions.swap(distribution_list);
581 :
582 : // recalculate prev states based ont incoming transitions of each distribution
583 101 : for (distribution_type* d : new_step_class_ptr->distributions)
584 : {
585 290 : for (transition* t_ptr : d->incoming_transitions_per_label[new_step_class_ptr->action])
586 : {
587 210 : new_step_class_ptr->prev_states[t_ptr->from()] = true;
588 : }
589 : }
590 :
591 : // add new step class to step partition and new_step_classes
592 21 : step_partition.push_front(new_step_class_ptr);
593 : }
594 40 : new_class_count++;
595 : }
596 : }
597 : }
598 :
599 : // Add the pending new blocks to the front of the list
600 36 : for (typename std::list<step_class_type*>::iterator sc_iter : pending_new_step_classes)
601 : {
602 1 : step_partition.splice(step_partition.begin(), step_partition_old, sc_iter);
603 : }
604 :
605 : // move remaining step classes to the end of step partition
606 35 : step_partition.splice(step_partition.end(), step_partition_old);
607 : }
608 :
609 : // Phase 2: Refinment of state_partition via Refine(X,a,M)
610 40 : if (step_partition.front()->is_in_new_step_classes == true)
611 : {
612 : // Choose some step class <a,M> in new_step_classes and remove it from new_step_classes
613 40 : step_class_type* step_class = step_partition.front();
614 40 : step_partition.pop_front();
615 40 : step_class->is_in_new_step_classes = false;
616 40 : step_partition.push_back(step_class);
617 :
618 : // swap elements of state_partition (X) to state_partition_old (X_old)
619 40 : state_partition_old.swap(state_partition);
620 :
621 40 : static std::vector<typename std::list<block_type*>::iterator > blocks_to_move_to_front;
622 40 : static std::vector<block_type*> new_blocks_to_move_to_front;
623 40 : blocks_to_move_to_front.clear();
624 40 : new_blocks_to_move_to_front.clear();
625 : // for all blocks B in X_old
626 : //for (block_type* b_to_split : state_partition_old)
627 309 : for (typename std::list<block_type*>::iterator block_iter = state_partition_old.begin();
628 309 : block_iter != state_partition_old.end(); ++block_iter)
629 : {
630 269 : block_type* b_to_split = *block_iter;
631 269 : block_type new_block;
632 269 : new_block.is_in_new_blocks = false;
633 269 : block_type temp_block;
634 : block_type* new_block_ptr;
635 269 : new_block.key = blocks.size();
636 :
637 : // iterate over all states in the block to split
638 3955 : for (state_type s : b_to_split->states)
639 : {
640 : // if block b can reach step class <a,M> starting from state s then we move it to antoher block
641 3686 : if (step_class->prev_states[s] == true)
642 : {
643 323 : new_block.states.push_back(s);
644 : }
645 : else
646 : {
647 3363 : temp_block.states.push_back(s);
648 : }
649 : }
650 :
651 : // if both, the new block and temp block has elements, then we add a new block into the state partition
652 269 : if (new_block.states.size() > 0 && temp_block.states.size() > 0)
653 : {
654 :
655 : // First update the block_index_of_a_state by iterating over all states of the new block
656 182 : for (state_type s : new_block.states)
657 : {
658 163 : block_index_of_a_state[s] = new_block.key;
659 : }
660 :
661 19 : blocks.push_back(new_block);
662 19 : new_block_ptr = &blocks.back();
663 :
664 : // return states from temp_block to b_to_split
665 19 : b_to_split->states.swap(temp_block.states);
666 :
667 : // if the current block is not currently a new block then add the smaller
668 : // block (between new block and current block) to the list of new blocks;
669 : // hence, in front of state partition
670 19 : if (b_to_split->is_in_new_blocks == false)
671 : {
672 14 : if (new_block_ptr->states.size() < b_to_split->states.size())
673 : {
674 11 : new_blocks_to_move_to_front.push_back(new_block_ptr);
675 11 : new_block_ptr->is_in_new_blocks = true;
676 : }
677 : else
678 : {
679 3 : b_to_split->is_in_new_blocks = true;
680 3 : blocks_to_move_to_front.push_back(block_iter);
681 :
682 : // add new block to the back of the state_partition list
683 3 : state_partition.push_back(new_block_ptr);
684 : }
685 : }
686 : else
687 : {
688 : // the current block is already in new blocks; hence, just add the new block
689 : // to the front of the partition as well.
690 :
691 : //new_blocks.push_back(new_block_ptr);
692 5 : new_block_ptr->is_in_new_blocks = true;
693 :
694 : // add new block to the back of the state_partition list
695 5 : new_blocks_to_move_to_front.push_back(new_block_ptr);
696 : }
697 : }
698 : }
699 :
700 : // move the remaning blocks to the end of state_partition
701 40 : state_partition.splice(state_partition.begin(), state_partition_old);
702 :
703 : // move the blocks that should be in new blocks to the begining of the list
704 43 : for (typename std::list<block_type*>::iterator block_iter : blocks_to_move_to_front)
705 : {
706 3 : state_partition.splice(state_partition.begin(), state_partition, block_iter);
707 : }
708 :
709 : // move the blocks that are new to the front of state_partition
710 56 : for (block_type* block_ptr : new_blocks_to_move_to_front)
711 : {
712 16 : state_partition.push_front(block_ptr);
713 : }
714 :
715 : }
716 : }
717 7 : }
718 :
719 7 : void postprocessing_stage(void)
720 : {
721 : //---- Post processing to keep track of the parent block of each state ----//
722 : //block_index_of_a_state.resize(aut.num_states());
723 49 : for (const block_type& b : blocks)
724 : {
725 344 : for (const state_type s : b.states)
726 : {
727 302 : block_index_of_a_state[s] = b.key;
728 : }
729 : }
730 :
731 7 : step_class_index_of_a_distribution.resize(aut.num_probabilistic_states());
732 52 : for (step_class_type& sc : step_classes)
733 : {
734 45 : sc.equivalent_step_class = sc.key;
735 :
736 163 : for (const distribution_type* d : sc.distributions)
737 : {
738 118 : step_class_index_of_a_distribution[d->key] = sc.key;
739 : }
740 : }
741 :
742 : // Merge equivalent step classes in step partition. The algorithm initially separates classes by actions,
743 : // but it is possible that a probabilistic sate has multiple incoming actions, hence it will be repeated
744 : // among multiple step classes
745 7 : typename LTS_TYPE::probabilistic_state_t new_prob_state;
746 7 : std::unordered_map<typename LTS_TYPE::probabilistic_state_t, std::vector<step_class_type*> > reduced_step_partition;
747 :
748 : /* Iterate over all step classes of Step_partition*/
749 52 : for (step_class_type& sc : step_classes)
750 : {
751 45 : if (sc.distributions.size() > 0)
752 : {
753 39 : typename LTS_TYPE::probabilistic_state_t new_prob_state = calculate_equivalent_probabilistic_state(sc);
754 :
755 : /* Add the step class index to the new probability state*/
756 39 : reduced_step_partition[new_prob_state].push_back(&sc);
757 39 : }
758 : }
759 :
760 7 : step_class_key_type equivalent_class_key = 0;
761 7 : for (typename std::unordered_map<typename LTS_TYPE::probabilistic_state_t,
762 7 : std::vector<step_class_type*> >::iterator i = reduced_step_partition.begin();
763 38 : i != reduced_step_partition.end(); ++i)
764 : {
765 31 : std::vector<step_class_type*>& sc_vector = i->second;
766 :
767 31 : equivalent_step_classes.push_back(*sc_vector[0]);
768 70 : for (step_class_type* sc :sc_vector)
769 : {
770 39 : sc->equivalent_step_class = equivalent_class_key;
771 : }
772 31 : equivalent_class_key++;
773 : }
774 :
775 7 : }
776 : };
777 :
778 :
779 : /** \brief Reduce transition system l with respect to probabilistic bisimulation.
780 : * \param[in/out] l The transition system that is reduced.
781 : * \param[in/out] timer A timer that can be used to report benchmarking results.
782 : */
783 : template < class LTS_TYPE>
784 : void probabilistic_bisimulation_reduce_bem(LTS_TYPE& l, utilities::execution_timer& timer);
785 :
786 : /** \brief Checks whether the two initial states of two plts's are probabilistic bisimilar.
787 : * \details This lts and the lts l2 are not usable anymore after this call.
788 : * \param[in/out] l1 A first probabilistic transition system.
789 : * \param[in/out] l2 A second probabilistic transition system.
790 : * \retval True iff the initial states of the current transition system and l2 are probabilistic bisimilar */
791 : template < class LTS_TYPE>
792 : bool destructive_probabilistic_bisimulation_compare_bem(LTS_TYPE& l1, LTS_TYPE& l2, utilities::execution_timer& timer);
793 :
794 :
795 : /** \brief Checks whether the two initial states of two plts's are probabilistic bisimilar.
796 : * \details The current transitions system and the lts l2 are first duplicated and subsequently
797 : * reduced modulo bisimulation. If memory space is a concern, one could consider to
798 : * use destructive_bisimulation_compare.
799 : * \param[in/out] l1 A first transition system.
800 : * \param[in/out] l2 A second transistion system.
801 : * \retval True iff the initial states of the current transition system and l2 are probabilistic bisimilar */
802 : template < class LTS_TYPE>
803 : bool probabilistic_bisimulation_compare_bem(const LTS_TYPE& l1, const LTS_TYPE& l2, utilities::execution_timer& timer);
804 :
805 :
806 : template < class LTS_TYPE>
807 7 : void probabilistic_bisimulation_reduce_bem(LTS_TYPE& l, utilities::execution_timer& timer)
808 : {
809 :
810 : // Apply the probabilistic bisimulation reduction algorithm.
811 7 : detail::prob_bisim_partitioner_bem<LTS_TYPE> prob_bisim_part(l,timer);
812 :
813 : // Clear the state labels of the LTS l
814 7 : l.clear_state_labels();
815 :
816 : // Assign the reduced LTS
817 7 : l.set_num_states(prob_bisim_part.num_eq_classes());
818 7 : prob_bisim_part.replace_transitions();
819 7 : prob_bisim_part.replace_probabilistic_states();
820 7 : }
821 :
822 : template < class LTS_TYPE>
823 : bool probabilistic_bisimulation_compare_bem(
824 : const LTS_TYPE& l1,
825 : const LTS_TYPE& l2,
826 : utilities::execution_timer& timer)
827 : {
828 : LTS_TYPE l1_copy(l1);
829 : LTS_TYPE l2_copy(l2);
830 : return destructive_probabilistic_bisimulation_compare_bem(l1_copy, l2_copy, timer);
831 : }
832 :
833 : template < class LTS_TYPE>
834 : bool destructive_probabilistic_bisimulation_compare_bem(
835 : LTS_TYPE& l1,
836 : LTS_TYPE& l2,
837 : utilities::execution_timer& timer)
838 : {
839 : std::size_t initial_probabilistic_state_key_l1;
840 : std::size_t initial_probabilistic_state_key_l2;
841 :
842 : // Merge states
843 : mcrl2::lts::detail::plts_merge(l1, l2);
844 : l2.clear(); // No use for l2 anymore.
845 :
846 : // The last two probabilistic states are the initial states of l2 and l1
847 : // in the merged plts
848 : initial_probabilistic_state_key_l2 = l1.num_probabilistic_states() - 1;
849 : initial_probabilistic_state_key_l1 = l1.num_probabilistic_states() - 2;
850 :
851 : detail::prob_bisim_partitioner_bem<LTS_TYPE> prob_bisim_part(l1, timer);
852 :
853 : return prob_bisim_part.in_same_probabilistic_class(initial_probabilistic_state_key_l2,
854 : initial_probabilistic_state_key_l1);
855 : }
856 :
857 : } // namespace detail
858 : } // namespace lts
859 : } // namespace mcrl2
860 :
861 : #endif // _LIBLTS_PBISIM_BEM_H
|
