mCRL2
Loading...
Searching...
No Matches
liblts_pbisim_grv.h
Go to the documentation of this file.
1// Author(s): Hector Joao Rivera Verduzco, 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//
10
11#ifndef _LIBLTS_PBISIM_GRV_H
12#define _LIBLTS_PBISIM_GRV_H
16
17namespace mcrl2
18{
19namespace lts
20{
21namespace detail
22{
23
24template < class LTS_TYPE>
25class prob_bisim_partitioner_grv // Called after Groote, Rivera Verduzco and de Vink
26{
27 public:
33 : aut(l)
34 {
35 mCRL2log(log::verbose) << "Probabilistic bisimulation partitioner created for " <<
36 l.num_states() << " states and " <<
37 l.num_transitions() << " transitions\n";
38 timer.start("bisimulation_reduce (grv)");
41 timer.finish("bisimulation_reduce (grv)");
42 }
43
47 std::size_t num_eq_classes() const
48 {
49 return action_constellations.size();
50 }
51
55 std::size_t get_eq_class(const std::size_t s)
56 {
57 assert(s < action_states.size());
58 return action_states[s].parent_block;
59 }
60
64 std::size_t get_eq_probabilistic_class(const std::size_t s)
65 {
66 assert(s<probabilistic_states.size());
67 return probabilistic_states[s].parent_block; // The block index is the state number of the block.
68 }
69
74 {
75 std::set<transition> resulting_transitions;
76
77 const std::vector<transition>& trans = aut.get_transitions();
78 for (const transition& t : trans)
79 {
80 resulting_transitions.insert(
82 get_eq_class(t.from()),
83 t.label(),
85 }
86 // Remove the old transitions
87 aut.clear_transitions();
88
89 // Copy the transitions from the set into the transition system.
90 for (const transition& t : resulting_transitions)
91 {
92 aut.add_transition(t);
93 }
94 }
95
100 {
101 std::vector<typename LTS_TYPE::probabilistic_state_t> new_probabilistic_states;
102
103 // get the equivalent probabilistic state of each probabilistic block and add it to aut
105 {
106 if (prob_block.states.size()>0)
107 {
108 typename LTS_TYPE::probabilistic_state_t equivalent_ps = calculate_equivalent_probabilistic_state(prob_block);
109 new_probabilistic_states.push_back(equivalent_ps);
110 }
111 }
112
113 /* Remove old probabilistic states */
114 aut.clear_probabilistic_states();
115
116 // Add new prob states to aut
117 for (const typename LTS_TYPE::probabilistic_state_t& new_ps : new_probabilistic_states)
118 {
119 aut.add_probabilistic_state(new_ps);
120 }
121
122 typename LTS_TYPE::probabilistic_state_t old_initial_prob_state = aut.initial_probabilistic_state();
123 typename LTS_TYPE::probabilistic_state_t new_initial_prob_state = calculate_new_probabilistic_state(old_initial_prob_state);
124 aut.set_initial_probabilistic_state(new_initial_prob_state);
125 }
126
132 bool in_same_probabilistic_class_grv(const std::size_t s, const std::size_t t)
133 {
135 }
136
137
138 protected:
139
140 // --------------- BEGIN DECLARATION OF DATA TYPES ---------------------------------------------------------------
141
142 typedef std::size_t block_key_type;
143 typedef std::size_t constellation_key_type;
144 typedef std::size_t transition_key_type;
145 typedef std::size_t state_key_type;
146 typedef std::size_t label_type;
147 // typedef probabilistic_arbitrary_precision_fraction probability_label_type;
148 typedef typename LTS_TYPE::probabilistic_state_t::probability_t probability_label_type;
149 // typedef probabilistic_arbitrary_precision_fraction probability_fraction_type;
150 typedef typename LTS_TYPE::probabilistic_state_t::probability_t probability_fraction_type;
151
152 struct action_transition_type : public embedded_list_node <action_transition_type>
153 {
158 };
159
160 struct probabilistic_transition_type : public embedded_list_node < probabilistic_transition_type >
161 {
165 };
166
167 struct action_state_type : public embedded_list_node < action_state_type >
168 {
170 std::vector<probabilistic_transition_type*> incoming_transitions;
171
172 // Temporary
176 };
177
178 struct probabilistic_state_type : public embedded_list_node < probabilistic_state_type >
179 {
181 std::vector<action_transition_type*> incoming_transitions;
182
183 // Temporary.
186 };
187
188 // Prototype.
189 struct action_mark_type;
190
191 struct action_block_type : public embedded_list_node <action_block_type>
192 {
196 action_mark_type* marking; // This value is nullptr if the block is not marked.
197
199 };
200
202 {
208
210 : action_block(&B),
211 large_block_ptr(nullptr)
212 {}
213 };
214
215 // Prototype
216 struct probabilistic_mark_type;
217
218 struct probabilistic_block_type : public embedded_list_node <probabilistic_block_type>
219 {
223
224 // a probabilistic block has incoming action transitions ordered by label
226
228 };
229
231 {
234 std::vector< embedded_list<probabilistic_state_type> > middle;
237
239 };
240
242 {
244 std::size_t number_of_states; // number of states in this constellation.
245 };
246
248 {
250 std::size_t number_of_states; // number of states in this constellation.
251 };
252
253 // --------------- END DECLARATION OF DATA TYPES ---------------------------------------------------------------
254
255 // The class below is used to group transitions on action labels in linear space and time.
256 // This makes use of the fact that action labels have a limited range, smaller than the number of transitions.
258 {
259 protected:
260 // This is a vector that contains transitions with the same label at each entry.
261 std::vector< embedded_list<action_transition_type> > m_transitions_per_label;
262 // This stack indicates which positions in the vector above are occupied for efficient retrieval.
263 std::stack<label_type> m_occupancy_indicator;
264
266 {
267 assert(t.label<m_transitions_per_label.size());
268 if (m_transitions_per_label[t.label].size()==0)
269 {
271 }
272 m_transitions_per_label[t.label].push_back(t);
273 }
274
275 public:
276 /* set the size of the vector m_transitions_per_label */
277 void initialize(const std::size_t number_of_labels)
278 {
279 m_transitions_per_label=std::vector< embedded_list<action_transition_type> >(number_of_labels);
280 }
281
282 const std::vector< embedded_list<action_transition_type> >& transitions() const
283 {
285 }
286
287 /* This function adds the transitions per label in order to the initial probabilistic block
288 and resets the occupancy array back to empty */
290 {
291 while (!m_occupancy_indicator.empty())
292 {
293 const label_type action=m_occupancy_indicator.top();
295
296 // The next operation resets m_transitions_per_label[action] to empty.
297 assert(action<m_transitions_per_label.size());
298 block.incoming_action_transitions.append(m_transitions_per_label[action]);
299 }
300 }
301
303 {
305 {
306 transition_list_with_t.erase(*t_ptr);
307 add_single_transition(*t_ptr);
308 }
309 }
310
311 void add_transitions(std::vector<action_transition_type>& transitions)
312 {
314 {
316 }
317 }
318 };
319
320 // The basic stores for all elementary data structures. The deque's are used intentionally
321 // as there are pointers to their content.
322 std::vector<action_transition_type> action_transitions;
323 std::deque<probabilistic_transition_type> probabilistic_transitions;
324 std::vector<action_state_type> action_states;
325 std::vector<probabilistic_state_type> probabilistic_states;
326 std::deque<action_block_type> action_blocks;
327 std::deque<probabilistic_block_type> probabilistic_blocks;
328 std::deque<action_constellation_type> action_constellations;
329 std::deque<probabilistic_constellation_type> probabilistic_constellations;
330
331 // The storage to store the state_to_constellation counts for each transition. Transition refer with
332 // a pointer to the elements in this deque.
333 std::deque<std::size_t> state_to_constellation_count;
334
335 // The lists below contains all the non trivial constellations.
336 std::stack<action_constellation_type*> non_trivial_action_constellations;
337 std::stack<probabilistic_constellation_type*> non_trivial_probabilistic_constellations;
338
339 // temporary data structures. declared here to prevent redeclaring these too often.
340 std::deque<action_mark_type> marked_action_blocks;
341 std::deque<probabilistic_mark_type> marked_probabilistic_blocks;
342 std::vector< std::pair<probability_label_type, probabilistic_state_type*> > grouped_states_per_probability_in_block;
343
344 // The following is a temporary data structure used to group incoming transitions on labels, which is declared
345 // globally to avoid declaring it repeatedly which is time consuming.
347
348
349 LTS_TYPE& aut;
350
352 {
353 // Check whether the constellation count in action transitions is ok.
355 {
356 std::size_t constellation=probabilistic_blocks[probabilistic_states[t.to].parent_block].parent_constellation;
357 std::size_t count_state_to_constellation=0;
358
360 {
361 if (t.from==t1.from &&
362 t.label==t1.label &&
363 constellation==probabilistic_blocks[probabilistic_states[t1.to].parent_block].parent_constellation)
364 {
365 count_state_to_constellation++;
366 }
367 }
368 if (count_state_to_constellation!=*t.state_to_constellation_count_ptr)
369 {
370 mCRL2log(log::error) << "Transition " << t.from << "--" << t.label << "->" << t.to << " has inconsistent constellation_count: " <<
371 *t.state_to_constellation_count_ptr << ". Should be " << count_state_to_constellation << ".\n";
372 return false;
373
374 }
375 }
376
377 // Check whether the number of states in an action constellation are correct.
379 {
380 std::size_t counted_states=0;
381 for(const action_block_type& b: c.blocks)
382 {
383 counted_states=counted_states+b.states.size();
384 }
385 assert(counted_states==c.number_of_states); // Number of states in this action constellation does not match the number of states in its blocks.
386 }
387
388 // Check whether the number of states in a probabilistic constellation are correct.
390 {
391 std::size_t counted_states=0;
392 for(const probabilistic_block_type& b: c.blocks)
393 {
394 counted_states=counted_states+b.states.size();
395 }
396 assert(counted_states==c.number_of_states); // Number of states in this probabilistic constellation does not match the number of states in its blocks.
397 }
398
399 for(const action_block_type& b: action_blocks)
400 {
401 assert(b.states.size()>0); // Action block contains no states.
402
403 assert(b.marking==nullptr); // Action block's marking must be a null ptr.
404 }
405
407 {
408 assert(b.marking==nullptr); // Probabilistic block's marking must be a null ptr.
409 }
410
411 return true;
412 }
413
414 void print_structure(const std::string& info)
415 {
416 std::cerr << info << " ---------------------------------------------------------------------- \n";
417 std::cerr << "Number of action blocks " << action_blocks.size() << "\n";
418 std::cerr << "Number of probabilistic blocks " << probabilistic_blocks.size() << "\n";
419 std::cerr << "Number of action constellations " << action_constellations.size() << "\n";
420 std::cerr << "Number of probabilistic constellations " << probabilistic_constellations.size() << "\n";
421 for(const action_block_type b: action_blocks)
422 {
423 std::cerr << "ACTION BLOCK INFO ------------------------\n";
424 std::cerr << "PARENT CONSTELLATION " << b.parent_constellation << "\n";
425 std::cerr << "NR STATES " << b.states.size() << "\n";
426 for(const probabilistic_transition_type t: b.incoming_probabilistic_transitions)
427 {
428 std::cerr << "INCOMING TRANS " << t.from << " --" << t.label << "-> " << t.to << "\n";
429 }
430 }
431
433 {
434 std::cerr << "probabilistic BLOCK INFO ------------------------\n";
435 std::cerr << "PARENT CONSTELLATION " << b.parent_constellation << "\n";
436 std::cerr << "NR STATES " << b.states.size() << "\n";
437 for(const action_transition_type t: b.incoming_action_transitions)
438 {
439 std::cerr << "INCOMING TRANS " << t.from << " --" << t.label << "-> " << t.to << "\n";
440 }
441 }
442
443 }
444
449 {
450 transitions_per_label.initialize(aut.num_action_labels());
451
452 // Preprocessing initialization. First we have to initialise the action/probabilistic states and
453 // transitions.
455
456 // Add action transitions to its respective list grouped by label.
458
459 // We start with all the action states in one block and then we refine this block
460 // according to the outgoing transitions.
461 action_block_type initial_action_block;
462
463 // Link all the action states together to the initial block
465 {
466 s.parent_block = 0; // Initial block has number 0.
467 initial_action_block.states.push_back(s);
468 }
469 assert(aut.num_states()==initial_action_block.states.size());
470
471 // Add the linked states to the list of states in the initial block
472 action_blocks.push_back(initial_action_block);
473
474 // Refine the initial action block based on the outgoing transitions.
475 // This corresponds to line 5 of Algorithm 2 in [GRV].
477
478 // Initialise the probabilistic block. Initally, there is only one block of probabilistic states.
479 probabilistic_blocks.emplace_back();
480
481 probabilistic_block_type& initial_probabilistic_block=probabilistic_blocks.back();
482 initial_probabilistic_block.parent_constellation = 0;
483
484 // Link all the probabilistic states together to the initial block
486 {
487 s.parent_block = 0; // The initial block has number zero.
488 initial_probabilistic_block.states.push_back(s);
489 }
490 assert(aut.num_probabilistic_states()==initial_probabilistic_block.states.size());
491
492 // Initialise the probabilistic and action constellations; they will contain
493 // all the blocks.
494 probabilistic_constellation_type initial_probabilistic_const;
495 initial_probabilistic_const.number_of_states = aut.num_probabilistic_states();
496
497 // Initially there is only one block in the probabilistic constellation.
498 // initial_probabilistic_const.blocks.init(&probabilistic_blocks.front(), &probabilistic_blocks.front(), 1);
499 initial_probabilistic_const.blocks.push_back(probabilistic_blocks.front());
500 probabilistic_constellations.push_back(initial_probabilistic_const);
501
502 // Initialise the initial action constellation.
503 action_constellations.emplace_back();
504 action_constellation_type& initial_action_const=action_constellations.back();
505
506 initial_action_const.number_of_states = aut.num_states();
507
508 // Construct the list of action blocks by linking them together.
510 {
511 b.parent_constellation = 0; // The initial constellation has number 0;
512 initial_action_const.blocks.push_back(b);
513 }
514
515//-----------------------------------------------------------------------------
516 // state_to_const_count_temp is used to keep track of the block to constellation count per label of each state.
517 std::vector<std::size_t*> new_count_ptr(aut.num_states(),nullptr);
518
520 {
521 // Create a new position in state_to_constellation_count if no such count exists for the parent block of the transition.
522 // Assign this position to t.state_to_constellation_count_ptr and increment its count.
523 for(action_transition_type& t: at_list_per_label)
524 {
525 assert(t.from<new_count_ptr.size());
526 if (new_count_ptr[t.from]==nullptr)
527 {
528 state_to_constellation_count.push_back(0);
529 new_count_ptr[t.from] = &state_to_constellation_count.back();
530 }
531 t.state_to_constellation_count_ptr = new_count_ptr[t.from];
532 (*new_count_ptr[t.from])++;
533 }
534
535 // Reset all the variables used to prepare to next iteration.
536 for(const action_transition_type& t: at_list_per_label)
537 {
538 new_count_ptr[t.from] = nullptr;
539 }
540 }
541
542//-----------------------------------------------------------------------------
543
544 // Since the transitions are already grouped by label, add them to the
545 // initial probabilistic block as incoming transitions.
546 transitions_per_label.add_grouped_transitions_to_block(initial_probabilistic_block);
547
548 // Initialise the incoming probabilistic transitions for all action blocks. To that end,
549 // iterate over all probabilistic transitions and add it to its respective destination block.
551 {
554 block.incoming_probabilistic_transitions.push_back(t);
555 }
556
557 if (initial_action_const.blocks.size()>1)
558 {
559 non_trivial_action_constellations.push(&initial_action_const);
560 }
561
562 assert(check_data_structure());
563 }
564
565 /* This function performs the preprocessing stage to prepare to apply the algorithm.
566 It also initialises the action and probabilistic states and transitions. */
568 {
569 // Allocate space for states and transitions
570
571 action_states.resize(aut.num_states());
572 probabilistic_states.resize(aut.num_probabilistic_states());
573 action_transitions.resize(aut.num_transitions());
574
575 // Initialise the action transitions
576 transition_key_type t_key = 0;
577 for (const transition& t : aut.get_transitions())
578 {
580 at.from = t.from();
581 at.label = t.label();
582 at.to = t.to();
584
585 // save incoming transition in state
586 probabilistic_states[at.to].incoming_transitions.push_back(&at);
587
588 t_key++;
589 }
590
591 // Initialise the probabilistic transitions. To this end, we have to iterate over
592 // all probabilistic states.
593 for (std::size_t i = 0; i < aut.num_probabilistic_states(); i++)
594 {
595 const typename LTS_TYPE::probabilistic_state_t& ps = aut.probabilistic_state(i);
597 if (ps.size()>1) // The probabilistic state is stored as a vector.
598 {
599 for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : ps)
600 {
601 pt.from = i;
602 pt.label = sp_pair.probability();
603 pt.to = sp_pair.state();
604 probabilistic_transitions.push_back(pt);
605
606 // save incoming transition in state
607 action_states[pt.to].incoming_transitions.push_back(&probabilistic_transitions.back());
608 }
609 }
610 else // The probabilistic state is stored as a single state number with implicit probability 1.
611 {
612 pt.from = i;
613 pt.label = LTS_TYPE::probabilistic_state_t::probability_t::one();
614 pt.to = ps.get();
615 probabilistic_transitions.push_back(pt);
616 // save incoming transition in state
617 action_states[pt.to].incoming_transitions.push_back(&probabilistic_transitions.back());
618 }
619 }
620
621 // End of preprocessing.
622 }
623
624 /* Refine the initial block according to its outgoing transitions.
625 */
627 {
628 // Iterate over all transitions ordered by label, and refine the block.
630 {
631 marked_action_blocks.clear();
632 // The line below garbage collects marked_action_blocks to avoid covering too much memory continuously;
633 static std::size_t count=0; if (count++ == 1000) { marked_action_blocks.shrink_to_fit(); count=0; }
634
635 for(const action_transition_type& t: t_list)
636 {
637 action_state_type& s = action_states[t.from];
638 assert(s.parent_block<action_blocks.size());
640
641 // Move state s to marked states if not already added.
642 if (false == s.mark_state)
643 {
644 // Add parent block to the list of marked blocks if not yet added
645 if (parent_block.marking==nullptr)
646 {
647 marked_action_blocks.emplace_back(parent_block);
648 parent_block.marking=&marked_action_blocks.back();
649 }
650
651 move_list_element_back<action_state_type>(s, parent_block.states, parent_block.marking->left);
652 s.mark_state = true;
653 }
654 }
655
656 // Split the marked blocks.
657 for (action_mark_type& block_marking: marked_action_blocks)
658 {
659 if (0 == block_marking.action_block->states.size())
660 {
661 // If all states in the block are marked, then return all marked states to the block.
662 block_marking.action_block->states = block_marking.left;
663 }
664 else
665 {
666 // Split the block if not all states are marked.
667 action_blocks.emplace_back();
668 action_block_type& new_block=action_blocks.back();
669 new_block.states = block_marking.left;
670
671 // Init parent block of each state in new block.
672 for(action_state_type& s: new_block.states)
673 {
674 s.parent_block = action_blocks.size()-1;
675 }
676
677 }
678
679 // clean mark list
680 block_marking.left.clear();
681 block_marking.action_block->marking=nullptr;
682
683 }
684
685 // Clean the marked states.
686 for(const action_transition_type& t: t_list)
687 {
688 action_states[t.from].mark_state = false;
689 }
690 }
691
692 }
693
694 /* Move an element of a list to the back of another list.
695 */
696 template <typename LIST_ELEMENT>
698 {
699 source_list.erase(s);
700 dest_list.push_back(s);
701 }
702
706 template<typename LIST_ELEMENT>
708 {
709 source_list.erase(s);
710 dest_list.push_front(s);
711 }
712
717 {
718
719 // Refine until all the constellations are trivial.
721 {
722 assert(check_data_structure());
723
724 // Refine probabilistic blocks if a non-trivial action constellation exists.
726 {
727 action_constellation_type* non_trivial_action_const = non_trivial_action_constellations.top();
729 assert(non_trivial_action_const->blocks.size()>=2);
730
731// print_structure("REFINE I");
732 // Choose splitter block Bc of a non-trivial constellation C, such that |Bc| <= 1/2|C|.
733 // And also split constellation C into BC and C\BC in the set of constellations.
734 action_block_type* Bc_ptr = choose_action_splitter(non_trivial_action_const);
735
736 // Derive the left, right and middle sets from mark function.
738 // The line below garbage collects marked_action_blocks to avoid covering too much memory continuously;
739 static std::size_t count=0; if (count++ == 1000) { marked_probabilistic_blocks.shrink_to_fit(); count=0; }
740
742
743 // Split every marked probabilistic block based on left, middle and right.
745 {
746 // We must know whether the current constellation is already on the stack.
747 bool already_on_non_trivial_constellations_stack = probabilistic_constellations[B.probabilistic_block->parent_constellation].blocks.size()>1;
748
749 // First return the largest of left, middle or right to the states of current processed block.
750 B.probabilistic_block->states = *B.large_block_ptr;
751 B.large_block_ptr->clear();
752
753 // Split left set of the block to another block if left has states and it is not
754 // the largest block.
755 if (B.left.size() > 0)
756 {
757 split_probabilistic_block(*B.probabilistic_block, B.left);
758 }
759
760 // Split right set of the block to another block if right has states and it is not
761 // the largest block.
762 if (B.right.size() > 0)
763 {
764 split_probabilistic_block(*B.probabilistic_block, B.right);
765 }
766
767 // Iterate over all middle sets. Split middle sets of the current block to another block if
768 // the middle set has states and it is not the largest block.
769 for (embedded_list<probabilistic_state_type>& middle : B.middle)
770 {
771 if (middle.size() > 0)
772 {
773 split_probabilistic_block(*B.probabilistic_block, middle);
774 }
775 }
776
777 // Move the parent constellation of the current block to the front of the
778 // constellation list if it became unstable.
779 if (!already_on_non_trivial_constellations_stack && probabilistic_constellations[B.probabilistic_block->parent_constellation].blocks.size()>1)
780 {
781 probabilistic_constellation_type& parent_const = probabilistic_constellations[B.probabilistic_block->parent_constellation];
782 assert(parent_const.blocks.size()>1);
784 }
785
786 // Reset middle vector to prepare for the next mark process
787 B.middle.clear();
788 }
789 }
790
791 // Refine action blocks if a non-trivial probabilistic constellation exists.
793 {
794// print_structure("REFINE II");
795
796 probabilistic_constellation_type* non_trivial_probabilistic_const = non_trivial_probabilistic_constellations.top();
798 assert(non_trivial_probabilistic_const->blocks.size()>=2);
799 // Choose splitter block Bc of a non-trivial constellation C, such that |Bc| <= 1/2|C|.
800 // And also split constellation C into BC and C\BC in the set of constellations.
801 probabilistic_block_type* Bc_ptr = choose_probabilistic_splitter(non_trivial_probabilistic_const);
802
803 // For all incoming labeled "a" transitions of each state in BC call the mark function and split the blocks.
805 i!=Bc_ptr->incoming_action_transitions.end() ; )
806 {
807 // Derive the left, right and middle sets from mark function based on the incoming labeled "a" transitions.
808 const label_type a = i->label;
809 marked_action_blocks.clear();
810 mark_action(marked_action_blocks, a, i, Bc_ptr->incoming_action_transitions.end()); // The iterator i is implicitly increased
811 // to the position in the list with the next action.
812
813 // Split every marked probabilistic block based on left, middle and right.
815 {
816 // We must know whether the current constellation is already on the stack.
817 bool already_on_non_trivial_constellations_stack = action_constellations[B.action_block->parent_constellation].blocks.size()>1;
818
819 // First return the largest of left, middle or right to the states of current processed block.
820 B.action_block->states = *B.large_block_ptr;
821 B.large_block_ptr->clear();
822
823 // Split left set of the block to another block if left has states and it is not the largest block.
824 if (B.left.size() > 0)
825 {
826 split_action_block(*B.action_block, B.left);
827 }
828
829 // Split right set of the block to another block if right has states and it is not the largest block.
830 if (B.right.size() > 0)
831 {
832 split_action_block(*B.action_block, B.right);
833 }
834
835 // Split middle set of the block to another block if middle has states and it is not
836 // the largest block.
837 if (B.middle.size() > 0)
838 {
839 split_action_block(*B.action_block, B.middle);
840 }
841
842 // Move the parent constellation of the current block to the front of the
843 // constellation list if it became unstable.
844 if (!already_on_non_trivial_constellations_stack && action_constellations[B.action_block->parent_constellation].blocks.size()>1)
845 {
846 action_constellation_type& parent_const = action_constellations[B.action_block->parent_constellation];
847 assert(parent_const.blocks.size()>1);
848 non_trivial_action_constellations.push(&parent_const);
849 }
850
851 }
852 }
853 }
854 }
855 // print_structure("END REFINE");
856 assert(check_data_structure());
857 }
858
864 {
865 // First create the new block to be allocated, and initialise its parameters
866 probabilistic_blocks.emplace_back();
868
869 new_block.parent_constellation = block_to_split.parent_constellation; // The new block is in the same constellation as B
870 new_block.states = states_of_new_block;
871 states_of_new_block.clear();
872
873 // Add the incoming action transition of the new block. To this end, iterate over all
874 // states in the new block and add the incoming transitions of each state to the
875 // incoming transitions of the new block. Also keep track of the labels of the incoming
876 // transitions.
877 for(probabilistic_state_type& s: new_block.states)
878 {
879 // Update the parent block of the state
880 s.parent_block = probabilistic_blocks.size()-1;
882 }
883
884 // Since the transitions are already grouped by label, add them to the
885 // initial probabilistic block as incoming transitions.
887
888 // Add the new block to the back of the list of blocks in the parent constellation.
890
891 parent_const.blocks.push_back(probabilistic_blocks.back());
892 }
893
899 {
900 // First create the new block to be allocated, and initialise its parameters
901 action_blocks.emplace_back();
902 action_block_type& new_block=action_blocks.back();
903
904 new_block.parent_constellation = block_to_split.parent_constellation; // The new block is in the same constellation as block to split
905 new_block.states = states_of_new_block;
906 states_of_new_block.clear();
907
908 // Add the incoming action transition of the new block. To this end, iterate over all
909 // states in the new block and add the incoming transitions of each state to the
910 // incoming transitions of the new block.
911 for(action_state_type& s: new_block.states)
912 {
913 // Update the parent block of the state
914 s.parent_block = action_blocks.size()-1;
915
916 // Iterate over all incoming transitions of the state, to add them to the new block
917 for (probabilistic_transition_type* t : s.incoming_transitions)
918 {
919 // Move transition from list of transitions of previous block to new block
922 }
923 }
924
925 // Add the new block to the back of the list of blocks in the parent constellation.
927
928 parent_const.blocks.push_back(action_blocks.back());
929 }
930
935 void mark_probabilistic(const action_block_type& Bc, std::deque<probabilistic_mark_type>& marked_probabilistic_blocks)
936 {
937 // First, iterate over all incoming transitions of block Bc. Mark the blocks that are reached
938 // and calculate the cumulative probability of the reached state. This is the probability of
939 // a state to reach block Bc.
941 {
943 const probability_label_type& p = pt.label;
945
946 // If the block was not previously marked, then mark the block and move all states to right
947 if (nullptr == B.marking)
948 {
949 marked_probabilistic_blocks.emplace_back(B);
951 B.marking->right = B.states;
952 B.states.clear();
953
954 // Also initialise the larger block pointer to the right set and the maximum cumulative
955 // probability of the block to p.
957 }
958
959 // Since state s can reach block Bc, move state s to the left set if not yet added, and mark the state
960 if (false == s.mark_state)
961 {
962 // State s is not yet marked. Mark the state and move it to left set. In addition, initialise
963 // its cumulative probability.
964 s.mark_state = true;
966 move_list_element_back<probabilistic_state_type>(s, B.marking->right, B.marking->left);
967 }
968 else
969 {
970 // State s was already added to left. Just update its cumulative probability.
972 }
973 }
974
975 // Group all states with the same cumulative probability to construct the middle sets.
976 // To this end, iterate over all marked blocks. For each block, first add all the states
977 // with probability lower than the max_cumulative_probability of the block to the middle set.
979 {
980 // Clear this locally used data structure and reset it so now and then to avoid that it requires
981 // too much data.
983 static std::size_t count=0; if (count++ == 1000) { marked_action_blocks.shrink_to_fit(); count=0; }
984
986 B.left.clear();
987
988 // First, add all states lower than max_cumulative_probability to the middle set.
989 for(typename embedded_list<probabilistic_state_type>::iterator i=middle_temp.begin(); i!=middle_temp.end(); )
990 {
992 i++; // Increment the iterator here, such that we can change the list.
993
995 {
996 // State s has probability lower than max_cumulative_probability. Add to the middle set.
997 move_list_element_back<probabilistic_state_type>((s), middle_temp, B.left);
998 }
999
1000 // Also reset the marked_state variable in the state here, taiking advantage that we
1001 // are iterating over all marked states
1002 s.mark_state = false;
1003 }
1004
1005 // Add all the states corresponding to the bigger and smaller probability to middle.
1006 // Save the remaining states in a vector to sort them later.
1007 for(probabilistic_state_type& s: middle_temp)
1008 {
1009 grouped_states_per_probability_in_block.emplace_back(s.cumulative_probability, &s);
1010 }
1011
1012 // Sort the probabilities of middle, not including the biggest and smallest probability
1014
1015 // Construct the rest of the middle set based on the grouped probabilities. To this end,
1016 // traverse all the vector with the grouped states by probability. Store the states with
1017 // the same probability to a new sub-set in middle set. current_probability is used to
1018 // keep track of the probability that is currently being processed.
1019 probability_label_type current_probability = probability_label_type().zero();
1020
1022 {
1023 B.middle.emplace_back();
1024 for (const std::pair<probability_label_type, probabilistic_state_type*>& cumulative_prob_state_pair : grouped_states_per_probability_in_block)
1025 {
1026 probabilistic_state_type* s = cumulative_prob_state_pair.second;
1027 if (current_probability != cumulative_prob_state_pair.first)
1028 {
1029 // The current state has a different probability as the current probability. Allocate
1030 // another space in the middle to store this state and change the current probability.
1031 current_probability = cumulative_prob_state_pair.first;
1032 B.middle.emplace_back(); //put empty list at end of B.middle.
1033 }
1034
1035 move_list_element_back<probabilistic_state_type>((*s), middle_temp, B.middle.back());
1036 }
1037 }
1038
1039 // Now that we have all the states in left, middle and right; we have to find the largest
1040 // set. The large block is initialised to be the right set; hence, we only compare if
1041 // left and middle are larger.
1042 if (B.left.size() > B.large_block_ptr->size())
1043 {
1044 B.large_block_ptr = &B.left;
1045 }
1046
1047 // Iterate over all subsets of middle set to see if there is a one that is the largest.
1048 for (embedded_list<probabilistic_state_type>& middle_set : B.middle)
1049 {
1050 if (middle_set.size() > B.large_block_ptr->size())
1051 {
1052 B.large_block_ptr = &middle_set;
1053 }
1054 }
1055
1056 // Finally, reset the block_is_marked variable of the current block.
1057 B.probabilistic_block->marking = nullptr;
1058 }
1059 }
1060
1065 void mark_action(std::deque<action_mark_type>& marked_action_blocks,
1066 const label_type& a,
1067 typename embedded_list<action_transition_type>::iterator& action_walker_begin,
1068 const typename embedded_list<action_transition_type>::iterator action_walker_end)
1069 {
1070 assert(action_walker_begin!=action_walker_end && action_walker_begin->label==a);
1071
1072 // For all incoming transitions with label "a" of block Bc calculate left, middle and right.
1073 // To this end, first move all the states of the block that was reached by traversing the
1074 // transition backwards to its right set, then move all the states that can reach block Bc with
1075 // an "a" action to left and decrement the residual transition count of the state.
1076 for(typename embedded_list<action_transition_type>::iterator action_walker=action_walker_begin;
1077 action_walker!=action_walker_end && action_walker->label==a;
1078 action_walker++)
1079 {
1080 action_transition_type& t= *action_walker;
1083
1084 // If the block was not previously marked, then mark the block and add all states to right.
1085 if (nullptr == B.marking)
1086 {
1087 marked_action_blocks.emplace_back(B);
1088 B.marking = &marked_action_blocks.back();
1089 B.marking->right=B.states;
1090 B.states.clear();
1091 // Also initialise the larger block pointer to the right set.
1093 }
1094
1095 // Since state s can reach block Bc, move state s to the left set if not yet added, and mark the state
1096 if (false == s.mark_state)
1097 {
1098 // State s is not yet marked. Mark the state and move it to left set. In addition, initialise
1099 // its residual transition count.
1100 s.mark_state = true;
1102 move_list_element_back<action_state_type>(s, B.marking->right, B.marking->left);
1103 }
1104
1106 }
1107
1108 // Now, for all marked blocks, check the residual transition count of all the states in left. If the transition
1109 // count is zero, it means that the state only can reach block BC. If the transition count is greater than
1110 // zero, the state has transitions to the other part of the constellation; hence, those states have to be
1111 // moved to middle.
1113 {
1114 // Iterate over all left states in B and check whether the state has to be moved to middle.
1115 for(typename embedded_list<action_state_type>::iterator i=B.left.begin(); i!=B.left.end(); )
1116 {
1117 action_state_type& s= *i;
1118 i++; // This iterator is incremented here as s will be removed from the list over which iteration takes place.
1119 if (s.residual_transition_cnt > 0)
1120 {
1121 // The transition count is greater than zero. Move state to middle set.
1122 move_list_element_back<action_state_type>(s, B.left, B.middle);
1123 }
1124
1125 // Also reset the marked_state variable in the state here, taking advantage that we
1126 // are iterating over all marked states
1127 s.mark_state = false;
1128 }
1129
1130 // Find the largest set.
1131 if (B.left.size() > B.large_block_ptr->size())
1132 {
1133 B.large_block_ptr = &B.left;
1134 }
1135 if (B.middle.size() > B.large_block_ptr->size())
1136 {
1137 B.large_block_ptr = &B.middle;
1138 }
1139
1140 // Finally, reset the block_is_marked variable of the current block.
1141 B.action_block->marking = nullptr;
1142 }
1143
1144 // Update the state_to_constellation_count of each transition. Increment action_walker_begin
1145 // such that it points to the next action after this loop.
1146 for( ;
1147 action_walker_begin!=action_walker_end && action_walker_begin->label==a;
1148 action_walker_begin++)
1149 {
1150 action_transition_type& t= *action_walker_begin;
1152
1153 // If the residual_transition_cnt is greater than zero, it means that the state
1154 // is in the middle set; hence, the state_to_constellation_count has to be updated.
1155 if (s.residual_transition_cnt > 0)
1156 {
1157 std::size_t state_to_constellation_count_old = *t.state_to_constellation_count_ptr;
1158
1159 if (state_to_constellation_count_old != s.residual_transition_cnt)
1160 {
1161 // This is the first transition from this state to a new block.
1162 // First update the state_to_constellation_count with the residual_transition_cnt
1163 // which is used by the transitions that we do not visit. Also the not yet
1164 // visited transitions are set to this value.
1166
1167 // Now allocate another state_to_constellation_count for the Bc block
1168 state_to_constellation_count.emplace_back(state_to_constellation_count_old - s.residual_transition_cnt);
1170 }
1172 }
1173 }
1174 }
1175
1181 {
1182 assert(non_trivial_action_const->blocks.size()>=2);
1183
1184 // First, determine the block to split from constellation. It is the block |Bc| < 1/2|C|
1185 // First try with the first block in the list.
1186 action_block_type* Bc = &non_trivial_action_const->blocks.front();
1187
1188 if (Bc->states.size() > (non_trivial_action_const->number_of_states / 2))
1189 {
1190 // The block is bigger than 1/2|C|. Choose another one.
1191 Bc = &non_trivial_action_const->blocks.back();
1192 }
1193
1194 // Now split the block of the constellation.
1195 // First unlink Bc from the list of blocks of the non trivial constellation.
1196 non_trivial_action_const->blocks.erase(*Bc);
1197
1198 // Update the number of states and blocks of the non trivial block
1199 non_trivial_action_const->number_of_states -= Bc->states.size();
1200
1201 // Check if the constellation is still non-trivial; if not, move it to the non trivial constellation stack.
1202 if (non_trivial_action_const->blocks.size() > 1)
1203 {
1204 //The constellation is non trivial, put it in the stack of non_trivial_constellations.
1205 non_trivial_action_constellations.push(non_trivial_action_const);
1206 }
1207
1208 // Add Bc to a new constellation
1209 action_constellations.emplace_back();
1210 action_constellation_type& new_action_const=action_constellations.back();
1211
1213 new_action_const.blocks.push_back(*Bc);
1214 new_action_const.number_of_states = Bc->states.size();
1215
1216 return Bc;
1217 }
1218
1224 {
1225 // First, determine the block to split from constellation. It is the block |Bc| < 1/2|C|
1226 // First try with the first block in the list.
1227 probabilistic_block_type* Bc = &non_trivial_probabilistic_const->blocks.front();
1228 if (Bc->states.size() > (non_trivial_probabilistic_const->number_of_states / 2))
1229 {
1230 // The block is bigger than 1/2|C|. Choose another one.
1231 Bc = &non_trivial_probabilistic_const->blocks.back();
1232 }
1233
1234 // Now split the block of the constellation.
1235 // First unlink Bc from the list of blocks of the non trivial constellation.
1236 non_trivial_probabilistic_const->blocks.erase(*Bc);
1237
1238 // Update the number of states and blocks of the non trivial block
1239 non_trivial_probabilistic_const->number_of_states -= Bc->states.size();
1240
1241 // Check if the constellation is still non-trivial; if not, move it to the trivial constellation stack.
1242 if (non_trivial_probabilistic_const->blocks.size() > 1)
1243 {
1244 //The constellation is non trivial, put it in the stack of non_trivial_constellations.
1245 non_trivial_probabilistic_constellations.push(non_trivial_probabilistic_const);
1246 }
1247
1248 // Add Bc to a new constellation
1249 probabilistic_constellations.emplace_back();
1250 probabilistic_constellation_type& new_probabilistic_const=probabilistic_constellations.back();
1252 new_probabilistic_const.blocks.push_back(*Bc);
1253 new_probabilistic_const.number_of_states = Bc->states.size();
1254
1255 return Bc;
1256 }
1257
1258 typename LTS_TYPE::probabilistic_state_t calculate_new_probabilistic_state(typename LTS_TYPE::probabilistic_state_t ps)
1259 {
1260 typename LTS_TYPE::probabilistic_state_t new_prob_state;
1261
1262 /* Iterate over all state probability pairs in the selected probabilistic state*/
1263 if (ps.size()>1) // The state is stored as a vector of states and probabilities.
1264 {
1265 std::map <state_key_type, probability_fraction_type> prob_state_map;
1266 for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : ps)
1267 {
1268 /* Check the resulting action state in the final State partition */
1269 state_key_type new_state = get_eq_class(sp_pair.state());
1270
1271 if (prob_state_map.count(new_state) == 0)
1272 {
1273 /* The state is not yet in the mapping. Add the state with its probability*/
1274 prob_state_map[new_state] = sp_pair.probability();
1275 }
1276 else
1277 {
1278 /* The state is already in the mapping. Sum up probabilities */
1279 prob_state_map[new_state] = prob_state_map[new_state] + sp_pair.probability();
1280 }
1281 }
1282 /* Add all the state probabilities pairs in the mapping to its actual data type*/
1283 typename std::map<state_key_type, probability_fraction_type>::iterator i = prob_state_map.begin();
1284 if (++i==prob_state_map.end()) // There is only one state with probability one.
1285 {
1286 new_prob_state.set(prob_state_map.begin()->first);
1287 }
1288 else
1289 {
1290 // This probabilistic state has more components.
1291 for (const auto& i: prob_state_map)
1292 {
1293 new_prob_state.add(i.first, i.second);
1294 }
1295 }
1296 }
1297 else // The state is stored as a number with implicit probability 1.
1298 {
1299 /* Check the resulting action state in the final State partition */
1300 new_prob_state.set(get_eq_class(ps.get()));
1301 }
1302 return new_prob_state;
1303 }
1304
1305 typename LTS_TYPE::probabilistic_state_t calculate_equivalent_probabilistic_state(probabilistic_block_type& pb)
1306 {
1307 // Select the first probabilistic state of the probabilistic block.
1308 assert(pb.states.size()>0);
1309 const probabilistic_state_type& s = pb.states.front();
1310
1311 if (s.incoming_transitions.size()>0)
1312 {
1313 // Take an incoming transition to know the key of the state
1314 state_key_type s_key = s.incoming_transitions.back()->to;
1315
1316 const typename LTS_TYPE::probabilistic_state_t& old_prob_state = aut.probabilistic_state(s_key);
1317
1318 return calculate_new_probabilistic_state(old_prob_state);
1319 }
1320 // else it is the initial proabilistic state.
1321 return calculate_new_probabilistic_state(aut.initial_probabilistic_state());
1322
1323 }
1324};
1325
1326
1330template < class LTS_TYPE>
1331void probabilistic_bisimulation_reduce_grv(LTS_TYPE& l, utilities::execution_timer& timer);
1332
1338template < class LTS_TYPE>
1339bool destructive_probabilistic_bisimulation_compare_grv(LTS_TYPE& l1, LTS_TYPE& l2, utilities::execution_timer& timer);
1340
1348template < class LTS_TYPE>
1349bool probabilistic_bisimulation_compare_grv(const LTS_TYPE& l1, const LTS_TYPE& l2, utilities::execution_timer& timer);
1350
1351template < class LTS_TYPE>
1353{
1354 // Apply the probabilistic bisimulation reduction algorithm.
1355 detail::prob_bisim_partitioner_grv<LTS_TYPE> prob_bisim_part(l, timer);
1356
1357 // Clear the state labels of the LTS l
1358 l.clear_state_labels();
1359
1360 // Assign the reduced LTS
1361 l.set_num_states(prob_bisim_part.num_eq_classes());
1362 prob_bisim_part.replace_transitions();
1363 prob_bisim_part.replace_probabilistic_states();
1364}
1365
1366template < class LTS_TYPE>
1368 const LTS_TYPE& l1,
1369 const LTS_TYPE& l2,
1371{
1372 LTS_TYPE l1_copy(l1);
1373 LTS_TYPE l2_copy(l2);
1374 return destructive_probabilistic_bisimulation_compare_grv(l1_copy, l2_copy, timer);
1375}
1376
1377template < class LTS_TYPE>
1379 LTS_TYPE& l1,
1380 LTS_TYPE& l2,
1382{
1383 std::size_t initial_probabilistic_state_key_l1;
1384 std::size_t initial_probabilistic_state_key_l2;
1385
1386 // Merge states
1388 l2.clear(); // No use for l2 anymore.
1389
1390 // The last two probabilistic states are the initial states of l2 and l1
1391 // in the merged plts.
1392 initial_probabilistic_state_key_l2 = l1.num_probabilistic_states() - 1;
1393 initial_probabilistic_state_key_l1 = l1.num_probabilistic_states() - 2;
1394
1395 detail::prob_bisim_partitioner_grv<LTS_TYPE> prob_bisim_part(l1,timer);
1396
1397 return prob_bisim_part.in_same_probabilistic_class_grv(initial_probabilistic_state_key_l2,
1398 initial_probabilistic_state_key_l1);
1399}
1400
1401} // end namespace detail
1402} // end namespace lts
1403} // end namespace mcrl2
1404#endif //_LIBLTS_PBISIM_GRV_H
std::vector< embedded_list< action_transition_type > > m_transitions_per_label
void add_transitions(std::vector< action_transition_type > &transitions)
void move_incoming_transitions(probabilistic_state_type s, embedded_list< action_transition_type > &transition_list_with_t)
const std::vector< embedded_list< action_transition_type > > & transitions() const
std::deque< action_mark_type > marked_action_blocks
std::vector< std::pair< probability_label_type, probabilistic_state_type * > > grouped_states_per_probability_in_block
std::deque< probabilistic_block_type > probabilistic_blocks
void refine_partition_until_it_becomes_stable(void)
Refine partition until it becomes stable.
void split_action_block(action_block_type &block_to_split, embedded_list< action_state_type > &states_of_new_block)
Split an action block.
std::stack< action_constellation_type * > non_trivial_action_constellations
LTS_TYPE::probabilistic_state_t calculate_new_probabilistic_state(typename LTS_TYPE::probabilistic_state_t ps)
LTS_TYPE::probabilistic_state_t calculate_equivalent_probabilistic_state(probabilistic_block_type &pb)
std::size_t get_eq_probabilistic_class(const std::size_t s)
Gives the bisimulation equivalence probabilistic class number of a probabilistic state.
void move_list_element_back(LIST_ELEMENT &s, embedded_list< LIST_ELEMENT > &source_list, embedded_list< LIST_ELEMENT > &dest_list)
LTS_TYPE::probabilistic_state_t::probability_t probability_label_type
std::vector< probabilistic_state_type > probabilistic_states
bool in_same_probabilistic_class_grv(const std::size_t s, const std::size_t t)
Returns whether two states are in the same probabilistic bisimulation equivalence class.
std::stack< probabilistic_constellation_type * > non_trivial_probabilistic_constellations
std::vector< action_transition_type > action_transitions
void mark_probabilistic(const action_block_type &Bc, std::deque< probabilistic_mark_type > &marked_probabilistic_blocks)
Gives the probabilistic blocks that are marked by block Bc.
probabilistic_block_type * choose_probabilistic_splitter(probabilistic_constellation_type *non_trivial_probabilistic_const)
Choose an splitter block from a non trivial constellation.
LTS_TYPE::probabilistic_state_t::probability_t probability_fraction_type
action_block_type * choose_action_splitter(action_constellation_type *non_trivial_action_const)
Choose an splitter block from a non trivial constellation.
prob_bisim_partitioner_grv(LTS_TYPE &l, utilities::execution_timer &timer)
Creates a probabilistic bisimulation partitioner for an PLTS.
std::size_t get_eq_class(const std::size_t s)
Gives the bisimulation equivalence class number of a state.
void mark_action(std::deque< action_mark_type > &marked_action_blocks, const label_type &a, typename embedded_list< action_transition_type >::iterator &action_walker_begin, const typename embedded_list< action_transition_type >::iterator action_walker_end)
Gives the action blocks that are marked by probabilistic block Bc.
std::deque< probabilistic_transition_type > probabilistic_transitions
std::deque< action_constellation_type > action_constellations
std::vector< action_state_type > action_states
void replace_transitions()
Replaces the transition relation of the current lts by the transitions of the bisimulation reduced tr...
std::deque< action_block_type > action_blocks
void refine_initial_action_block(const std::vector< embedded_list< action_transition_type > > &transitions_per_label)
void replace_probabilistic_states()
Replaces the probabilistic states of the current lts by the probabilistic states of the bisimulation ...
std::deque< probabilistic_constellation_type > probabilistic_constellations
void split_probabilistic_block(probabilistic_block_type &block_to_split, embedded_list< probabilistic_state_type > &states_of_new_block)
Split a probabilistic block.
std::size_t num_eq_classes() const
Gives the number of bisimulation equivalence classes of the LTS.
std::deque< probabilistic_mark_type > marked_probabilistic_blocks
void move_list_element_front(LIST_ELEMENT &s, embedded_list< LIST_ELEMENT > &source_list, embedded_list< LIST_ELEMENT > &dest_list)
Move an element of a list to the front of another the list.
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
void probabilistic_bisimulation_reduce_grv(LTS_TYPE &l, utilities::execution_timer &timer)
Reduce transition system l with respect to probabilistic bisimulation.
bool probabilistic_bisimulation_compare_grv(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.
void plts_merge(LTS_TYPE &l1, const LTS_TYPE &l2)
bool destructive_probabilistic_bisimulation_compare_grv(LTS_TYPE &l1, LTS_TYPE &l2, utilities::execution_timer &timer)
Checks whether the two initial states of two plts's are probabilistic bisimilar.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
embedded_list< probabilistic_transition_type > incoming_probabilistic_transitions
std::vector< probabilistic_transition_type * > incoming_transitions
std::vector< embedded_list< probabilistic_state_type > > middle