mCRL2
Loading...
Searching...
No Matches
liblts_pbisim_bem.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//
10
11#ifndef _LIBLTS_PBISIM_BEM_H
12#define _LIBLTS_PBISIM_BEM_H
15
16namespace mcrl2
17{
18namespace lts
19{
20namespace detail
21{
22
23template < class LTS_TYPE>
25{
26
27 public:
33 {
34 mCRL2log(log::verbose) << "Probabilistic bisimulation partitioner created for "
35 << l.num_states() << " states and " <<
36 l.num_transitions() << " transitions\n";
37 timer.start("bisimulation_reduce (bem)");
40 timer.finish("bisimulation_reduce (bem)");
42 }
43
47 std::size_t num_eq_classes() const
48 {
49 return state_partition.size();
50 }
51
55 std::size_t get_eq_class(const std::size_t s) const
56 {
57 assert(s<block_index_of_a_state.size());
58 return block_index_of_a_state[s]; // The block index is the state number of the block.
59 }
60
64 std::size_t get_eq_step_class(const std::size_t d) const
65 {
66 assert(d < step_class_index_of_a_distribution.size());
68 assert(step_classes[step_class_index_of_a_distribution[d]].equivalent_step_class < step_classes.size());
69 return step_classes[step_class_index_of_a_distribution[d]].equivalent_step_class;
70 }
71
76 {
77 std::set < transition > resulting_transitions;
78
79 const std::vector<transition>& trans = aut.get_transitions();
80 for (const transition& t : trans)
81 {
82 resulting_transitions.insert(
84 get_eq_class(t.from()),
85 t.label(),
86 get_eq_step_class(t.to())));
87 }
88 // Remove the old transitions
89 aut.clear_transitions();
90
91 // Copy the transitions from the set into the transition system.
92 for (const transition& t : resulting_transitions)
93 {
94 aut.add_transition(t);
95 }
96 }
97
102 {
103 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
107 {
108 typename LTS_TYPE::probabilistic_state_t equivalent_ps = calculate_equivalent_probabilistic_state(sc);
109 new_probabilistic_states.push_back(equivalent_ps);
110 }
111
112 /* Remove old probabilistic states */
113 aut.clear_probabilistic_states();
114
115 // Add new prob states to aut
116 for (const typename LTS_TYPE::probabilistic_state_t& new_ps : new_probabilistic_states)
117 {
118 aut.add_probabilistic_state(new_ps);
119 }
120
121 typename LTS_TYPE::probabilistic_state_t old_initial_prob_state = aut.initial_probabilistic_state();
122 typename LTS_TYPE::probabilistic_state_t new_initial_prob_state = calculate_new_probabilistic_state(old_initial_prob_state);
123 aut.set_initial_probabilistic_state(new_initial_prob_state);
124 }
125
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
146 {
148 std::vector< std::list<transition*> > incoming_transitions_per_label; // Incoming transitions organized per label
149 };
150
152 {
154 std::list<state_type> states; // The states in the block
156 };
157
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>
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
179 {
180 std::list<state_type> states;
181 std::size_t count;
184
186 {
187 count = 0;
188 left = NULL;
189 right = NULL;
190 }
191 };
192
197 {
198 std::vector< std::vector< std::list<distribution_type*> > > steps; // Representation of transition in 2-d array
199 std::vector<transition>& transitions = aut.get_transitions();
200 std::vector< std::vector<bool> > distribution_per_step_class;
201
202 distribution_per_step_class.resize(aut.num_action_labels());
203 for (std::vector<bool>& i : distribution_per_step_class)
204 {
205 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 distributions.resize(aut.num_probabilistic_states());
212 std::size_t key = 0;
213 for (distribution_type& distribution : distributions)
214 {
215 distribution.key = key;
216 distribution.incoming_transitions_per_label.resize(aut.num_action_labels());
217 key++;
218 }
219
220 // Initialize the Steps bi-dimientional array
221 steps.resize(aut.num_states());
222 for (std::size_t i = 0; i < steps.size(); i++)
223 {
224 steps[i].resize(aut.num_action_labels());
225 }
226
227 for (transition& t : transitions)
228 {
229 steps[t.from()][t.label()].push_back(&distributions[t.to()]);
230 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 step_classes.resize(aut.num_action_labels());
237
238 for (step_class_type& sc : step_classes)
239 {
240 sc.prev_states.resize(aut.num_states());
241 }
242
243 // create tree structure to group action states based on the outgoing transitions
244 std::size_t max_block_size = 0;
245 tree_type* max_block = nullptr;
246 std::deque<tree_type> tree_nodes;
247 std::vector<tree_type*> leaves;
248 tree_type v0;
249 v0.init_node();
250 tree_nodes.push_back(v0);
251
252 // For all s in S do
253 for (state_type s = 0; s < aut.num_states(); s++)
254 {
255 // (1) Create pointer to root of the tree
256 tree_type* v = &tree_nodes[0];
257
258 // (2) Construct tree
259 for (std::size_t i = 0; i < aut.num_action_labels(); i++)
260 {
261 step_classes[i].key = i;
262 step_classes[i].action = i;
263 if (steps[s][i].size() > 0)
264 {
265 for (distribution_type* d : steps[s][i])
266 {
267 if (distribution_per_step_class[i][d->key] == false)
268 {
269 step_classes[i].distributions.push_back(d);
270 distribution_per_step_class[i][d->key] = true;
271 }
272 }
273
274 step_classes[i].prev_states[s] = true;
275
276 if (v->left == NULL)
277 {
278 // create left node
279 tree_type w;
280 w.init_node();
281 tree_nodes.push_back(w);
282 v->left = &tree_nodes.back();
283
284 // add new node to the leaf nodes if it is a leaf
285 if (i == aut.num_action_labels() - 1)
286 {
287 leaves.push_back(v->left);
288 }
289
290 }
291 v = v->left;
292 }
293 else
294 {
295 if (v->right == NULL)
296 {
297 // create left node
298 tree_type w;
299 w.init_node();
300 tree_nodes.push_back(w);
301 v->right = &tree_nodes.back();
302
303 // add new node to the leaf nodes if it is a leaf
304 if (i == aut.num_action_labels() - 1)
305 {
306 leaves.push_back(v->right);
307 }
308 }
309 v = v->right;
310 }
311 }
312
313 // (3) Add the state to the leaf and increment its state counter
314 v->states.push_back(s);
315 v->count++;
316
317 // (4) Keep track of the leave containing more states
318 if (v->count > max_block_size)
319 {
320 max_block = v;
321 max_block_size = v->count;
322 }
323 }
324
325 // insert all states of the leaves to blocks
326 blocks.resize(leaves.size());
327
328 key = 0;
329 std::size_t larger_key = 0;
330 for (tree_type* leaf_ptr : leaves)
331 {
332 block_type& block = blocks[key];
333 block.key = key;
334 block.states.splice(block.states.end(), leaf_ptr->states);
335
336 if (leaf_ptr == max_block)
337 {
338 larger_key = key;
339 }
340
341 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 for (block_type& b : blocks)
347 {
348 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 b.is_in_new_blocks = true;
352 state_partition.push_front(&b);
353 }
354 else
355 {
356 // push the larger block to the end of the list
357 b.is_in_new_blocks = false;
358 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 for (step_class_type& sc : step_classes)
365 {
366 if (sc.distributions.size() > 0)
367 {
368 step_partition.push_front(&sc);
369 sc.is_in_new_step_classes = true;
370 }
371 }
372
373 block_index_of_a_state.resize(aut.num_states());
374 for (const block_type& b : blocks)
375 {
376 for (const state_type s : b.states)
377 {
378 block_index_of_a_state[s] = b.key;
379 }
380 }
381
382 }
383
389 {
390 probability_fraction_type prob_to_block;
391 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 if (prob_state.size()>1) // The state is stored as a vector of states/probabilities.
395 {
396 for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& prob_pair : prob_state)
397 {
398 const state_type s = prob_pair.state();
399 if (block_index_of_a_state[s] == b.key)
400 {
401 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 const state_type s = prob_state.get();
408 if (block_index_of_a_state[s] == b.key)
409 {
410 prob_to_block = prob_to_block + LTS_TYPE::probabilistic_state_t::probability_t::one();
411 }
412 }
413
414 return prob_to_block;
415 }
416
417 typename LTS_TYPE::probabilistic_state_t calculate_new_probabilistic_state(typename LTS_TYPE::probabilistic_state_t ps)
418 {
419 typename LTS_TYPE::probabilistic_state_t new_prob_state;
420
421 /* Iterate over all state probability pairs in the selected probabilistic state*/
422 if (ps.size()>1) // The state is stored as a vector of states/probabilities.
423 {
424 std::map<state_type, probability_fraction_type> prob_state_map;
425 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 state_type new_state = get_eq_class(sp_pair.state());
429
430 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 prob_state_map[new_state] = sp_pair.probability();
434 }
435 else
436 {
437 /* The state is already in the mapping. Sum up probabilities */
438 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 typename std::map<state_type, probability_fraction_type>::const_iterator i = prob_state_map.begin();
444 if (++i==prob_state_map.end()) // There is only one state with probability 1.
445 {
446 new_prob_state.set(prob_state_map.begin()->first);
447 }
448 else
449 {
450 // This probabilistic state has more components.
451 for (const std::pair<const state_type, probability_fraction_type>& i: prob_state_map)
452 {
453 new_prob_state.add(i.first, i.second);
454 }
455 }
456
457 }
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 new_prob_state.set(get_eq_class(ps.get()));
462 }
463
464 return new_prob_state;
465 }
466
467 typename LTS_TYPE::probabilistic_state_t calculate_equivalent_probabilistic_state(step_class_type& sc)
468 {
469 typename LTS_TYPE::probabilistic_state_t equivalent_prob_state;
470
471 /* Select the first probabilistic state of the step class */
472 distribution_type* d = sc.distributions.front();
473
474 typename LTS_TYPE::probabilistic_state_t old_prob_state = aut.probabilistic_state(d->key);
475
476 equivalent_prob_state = calculate_new_probabilistic_state(old_prob_state);
477
478 return equivalent_prob_state;
479 }
480
486 {
487 std::list<step_class_type*> step_partition_old;
488 std::list<block_type*> state_partition_old;
489
490 // Repeat until no new blocks in front of the partition lists
491 while (state_partition.front()->is_in_new_blocks == true ||
492 (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 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 block_type* c_block = state_partition.front();
499 state_partition.pop_front();
500 state_partition.push_back(c_block);
501 c_block->is_in_new_blocks = false;
502
503 // swap elements of step_partition (M) to step_partition_old (M_old)
504 step_partition_old.swap(step_partition);
505
506 // vector to add the new step classes
507 static std::vector<typename std::list<step_class_type*>::iterator> pending_new_step_classes;
508 pending_new_step_classes.clear();
509
510 // iterate over all step classes
511 for (typename std::list<step_class_type*>::iterator sc_iter = step_partition_old.begin();
512 sc_iter != step_partition_old.end(); ++sc_iter)
513 {
514 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 static std::map< probability_fraction_type, std::list<distribution_type*> > distributions_ordered_by_prob;
519 distributions_ordered_by_prob.clear();
520
521 // Iterate over all distributions d of the step class and add probability to block to vector
522 for (distribution_type* d : sc_ptr->distributions)
523 {
524 probability_fraction_type probability = probability_to_block(*d, *c_block);
525 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 if (distributions_ordered_by_prob.size() >= 2)
531 {
532 step_class_type* new_step_class_ptr;
533
534 step_classes.resize(step_classes.size() + distributions_ordered_by_prob.size() - 1);
535 // iterate over mapping
536 std::size_t new_class_count = 0;
537 for (std::pair< probability_fraction_type, std::list<distribution_type*> > ordered_dist : distributions_ordered_by_prob)
538 {
539 std::list<distribution_type*>& distribution_list = ordered_dist.second;
540
541 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 sc_ptr->distributions.swap(distribution_list);
546
547 // clear the prev states of the current step class
548 for (std::size_t i = 0; i < sc_ptr->prev_states.size(); i++)
549 {
550 sc_ptr->prev_states[i] = false;
551 }
552
553 // recalculate prev states based on incoming transitions of each distribution
554 for (distribution_type* d : sc_ptr->distributions)
555 {
556 for (transition* t_ptr : d->incoming_transitions_per_label[sc_ptr->action])
557 {
558 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 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 pending_new_step_classes.push_back(sc_iter);
568 sc_ptr->is_in_new_step_classes = true;
569 }
570 }
571 else
572 {
573 new_step_class_ptr = &step_classes[step_classes.size() - new_class_count];
574
575 //init new step class
576 new_step_class_ptr->key = step_classes.size() - new_class_count;
577 new_step_class_ptr->action = sc_ptr->action;
578 new_step_class_ptr->is_in_new_step_classes = true;
579 new_step_class_ptr->prev_states.resize(aut.num_states());
580 new_step_class_ptr->distributions.swap(distribution_list);
581
582 // recalculate prev states based ont incoming transitions of each distribution
583 for (distribution_type* d : new_step_class_ptr->distributions)
584 {
585 for (transition* t_ptr : d->incoming_transitions_per_label[new_step_class_ptr->action])
586 {
587 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 step_partition.push_front(new_step_class_ptr);
593 }
594 new_class_count++;
595 }
596 }
597 }
598
599 // Add the pending new blocks to the front of the list
600 for (typename std::list<step_class_type*>::iterator sc_iter : pending_new_step_classes)
601 {
602 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 step_partition.splice(step_partition.end(), step_partition_old);
607 }
608
609 // Phase 2: Refinment of state_partition via Refine(X,a,M)
610 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 step_class_type* step_class = step_partition.front();
614 step_partition.pop_front();
615 step_class->is_in_new_step_classes = false;
616 step_partition.push_back(step_class);
617
618 // swap elements of state_partition (X) to state_partition_old (X_old)
619 state_partition_old.swap(state_partition);
620
621 static std::vector<typename std::list<block_type*>::iterator > blocks_to_move_to_front;
622 static std::vector<block_type*> new_blocks_to_move_to_front;
623 blocks_to_move_to_front.clear();
624 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 for (typename std::list<block_type*>::iterator block_iter = state_partition_old.begin();
628 block_iter != state_partition_old.end(); ++block_iter)
629 {
630 block_type* b_to_split = *block_iter;
631 block_type new_block;
632 new_block.is_in_new_blocks = false;
633 block_type temp_block;
634 block_type* new_block_ptr;
635 new_block.key = blocks.size();
636
637 // iterate over all states in the block to split
638 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 if (step_class->prev_states[s] == true)
642 {
643 new_block.states.push_back(s);
644 }
645 else
646 {
647 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 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 for (state_type s : new_block.states)
657 {
658 block_index_of_a_state[s] = new_block.key;
659 }
660
661 blocks.push_back(new_block);
662 new_block_ptr = &blocks.back();
663
664 // return states from temp_block to b_to_split
665 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 if (b_to_split->is_in_new_blocks == false)
671 {
672 if (new_block_ptr->states.size() < b_to_split->states.size())
673 {
674 new_blocks_to_move_to_front.push_back(new_block_ptr);
675 new_block_ptr->is_in_new_blocks = true;
676 }
677 else
678 {
679 b_to_split->is_in_new_blocks = true;
680 blocks_to_move_to_front.push_back(block_iter);
681
682 // add new block to the back of the state_partition list
683 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 new_block_ptr->is_in_new_blocks = true;
693
694 // add new block to the back of the state_partition list
695 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 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 for (typename std::list<block_type*>::iterator block_iter : blocks_to_move_to_front)
705 {
706 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 for (block_type* block_ptr : new_blocks_to_move_to_front)
711 {
712 state_partition.push_front(block_ptr);
713 }
714
715 }
716 }
717 }
718
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 for (const block_type& b : blocks)
724 {
725 for (const state_type s : b.states)
726 {
727 block_index_of_a_state[s] = b.key;
728 }
729 }
730
731 step_class_index_of_a_distribution.resize(aut.num_probabilistic_states());
732 for (step_class_type& sc : step_classes)
733 {
734 sc.equivalent_step_class = sc.key;
735
736 for (const distribution_type* d : sc.distributions)
737 {
738 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 typename LTS_TYPE::probabilistic_state_t new_prob_state;
746 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 for (step_class_type& sc : step_classes)
750 {
751 if (sc.distributions.size() > 0)
752 {
753 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 reduced_step_partition[new_prob_state].push_back(&sc);
757 }
758 }
759
760 step_class_key_type equivalent_class_key = 0;
761 for (typename std::unordered_map<typename LTS_TYPE::probabilistic_state_t,
762 std::vector<step_class_type*> >::iterator i = reduced_step_partition.begin();
763 i != reduced_step_partition.end(); ++i)
764 {
765 std::vector<step_class_type*>& sc_vector = i->second;
766
767 equivalent_step_classes.push_back(*sc_vector[0]);
768 for (step_class_type* sc :sc_vector)
769 {
770 sc->equivalent_step_class = equivalent_class_key;
771 }
772 equivalent_class_key++;
773 }
774
775 }
776};
777
778
783template < class LTS_TYPE>
784void probabilistic_bisimulation_reduce_bem(LTS_TYPE& l, utilities::execution_timer& timer);
785
791template < class LTS_TYPE>
792bool destructive_probabilistic_bisimulation_compare_bem(LTS_TYPE& l1, LTS_TYPE& l2, utilities::execution_timer& timer);
793
794
802template < class LTS_TYPE>
803bool probabilistic_bisimulation_compare_bem(const LTS_TYPE& l1, const LTS_TYPE& l2, utilities::execution_timer& timer);
804
805
806template < class LTS_TYPE>
808{
809
810 // Apply the probabilistic bisimulation reduction algorithm.
811 detail::prob_bisim_partitioner_bem<LTS_TYPE> prob_bisim_part(l,timer);
812
813 // Clear the state labels of the LTS l
814 l.clear_state_labels();
815
816 // Assign the reduced LTS
817 l.set_num_states(prob_bisim_part.num_eq_classes());
818 prob_bisim_part.replace_transitions();
819 prob_bisim_part.replace_probabilistic_states();
820}
821
822template < class LTS_TYPE>
824 const LTS_TYPE& l1,
825 const LTS_TYPE& l2,
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
833template < class LTS_TYPE>
835 LTS_TYPE& l1,
836 LTS_TYPE& l2,
838{
839 std::size_t initial_probabilistic_state_key_l1;
840 std::size_t initial_probabilistic_state_key_l2;
841
842 // Merge states
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
LTS_TYPE::probabilistic_state_t::probability_t probability_fraction_type
std::size_t num_eq_classes() const
Gives the number of bisimulation equivalence classes of the LTS.
std::size_t get_eq_step_class(const std::size_t d) const
Gives the bisimulation equivalence step class number of a probabilistic state.
LTS_TYPE::probabilistic_state_t calculate_new_probabilistic_state(typename LTS_TYPE::probabilistic_state_t ps)
std::vector< block_key_type > block_index_of_a_state
void refine_partition_until_it_becomes_stable(void)
Two-phased partitioning algorithm described in page 204. Fig 9. Baier. \detail Refinement of state pa...
std::vector< step_class_key_type > step_class_index_of_a_distribution
void create_initial_partition(void)
Creates the initial partition of step classes and blocks. \detail The blocks are initially partitione...
probability_fraction_type probability_to_block(distribution_type &d, block_type &b)
Calculates the probability to reach block b from distribution d.
bool in_same_probabilistic_class(const std::size_t s, const std::size_t t) const
Returns whether two states are in the same probabilistic bisimulation equivalence class.
std::size_t get_eq_class(const std::size_t s) const
Gives the bisimulation equivalence class number of a state.
prob_bisim_partitioner_bem(LTS_TYPE &l, utilities::execution_timer &timer)
Creates a probabilistic bisimulation partitioner for an PLTS.
std::deque< step_class_type > equivalent_step_classes
void replace_transitions()
Replaces the transition relation of the current lts by the transitions of the bisimulation reduced tr...
LTS_TYPE::probabilistic_state_t calculate_equivalent_probabilistic_state(step_class_type &sc)
std::vector< distribution_type > distributions
void replace_probabilistic_states()
Replaces the probabilistic states of the current lts by the probabilistic states of the bisimulation ...
A class containing triples, source label and target representing transitions.
Definition transition.h:43
Simple timer to time the CPU time used by a piece of code.
void start(const std::string &timing_name)
Start measurement with a hint.
void finish(const std::string &timing_name)
Finish a measurement with a hint.
Class to obtain running times of code.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
@ verbose
Definition logger.h:35
bool probabilistic_bisimulation_compare_bem(const LTS_TYPE &l1, const LTS_TYPE &l2, utilities::execution_timer &timer)
Checks whether the two initial states of two plts's are probabilistic bisimilar.
bool destructive_probabilistic_bisimulation_compare_bem(LTS_TYPE &l1, LTS_TYPE &l2, utilities::execution_timer &timer)
Checks whether the two initial states of two plts's are probabilistic bisimilar.
void plts_merge(LTS_TYPE &l1, const LTS_TYPE &l2)
void probabilistic_bisimulation_reduce_bem(LTS_TYPE &l, utilities::execution_timer &timer)
Reduce transition system l with respect to probabilistic bisimulation.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
std::vector< std::list< transition * > > incoming_transitions_per_label