Line data Source code
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 : //
9 : /// \file lts/detail/liblts_pbisim.h
10 :
11 : #ifndef _LIBLTS_PBISIM_GRV_H
12 : #define _LIBLTS_PBISIM_GRV_H
13 : #include "mcrl2/utilities/execution_timer.h"
14 : #include "mcrl2/lts/detail/embedded_list.h"
15 : #include "mcrl2/lts/detail/liblts_plts_merge.h"
16 :
17 : namespace mcrl2
18 : {
19 : namespace lts
20 : {
21 : namespace detail
22 : {
23 :
24 : template < class LTS_TYPE>
25 : class prob_bisim_partitioner_grv // Called after Groote, Rivera Verduzco and de Vink
26 : {
27 : public:
28 : /** \brief Creates a probabilistic bisimulation partitioner for an PLTS.
29 : * \details This bisimulation partitioner applies the algorithm described in "J.F. Groote, H.J. Rivera, E.P. de Vink,
30 : * An O(mlogn) algorithm for probabilistic bisimulation".
31 : */
32 13 : prob_bisim_partitioner_grv(LTS_TYPE& l, utilities::execution_timer& timer)
33 13 : : aut(l)
34 : {
35 13 : mCRL2log(log::verbose) << "Probabilistic bisimulation partitioner created for " <<
36 0 : l.num_states() << " states and " <<
37 0 : l.num_transitions() << " transitions\n";
38 13 : timer.start("bisimulation_reduce (grv)");
39 13 : create_initial_partition();
40 13 : refine_partition_until_it_becomes_stable();
41 13 : timer.finish("bisimulation_reduce (grv)");
42 13 : }
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 action_constellations.size();
50 : }
51 :
52 : /** \brief Gives the bisimulation equivalence class number of a state.
53 : * \param[in] A state number.
54 : * \return The number of the bisimulation equivalence class to which the state belongs to. */
55 396 : std::size_t get_eq_class(const std::size_t s)
56 : {
57 396 : assert(s < action_states.size());
58 396 : return action_states[s].parent_block;
59 : }
60 :
61 : /** \brief Gives the bisimulation equivalence probabilistic class number of a probabilistic state.
62 : * \param[in] A probabilistic state number.
63 : * \return The number of the probabilistic class to which the state belongs to. */
64 304 : std::size_t get_eq_probabilistic_class(const std::size_t s)
65 : {
66 304 : assert(s<probabilistic_states.size());
67 304 : return probabilistic_states[s].parent_block; // The block index is the state number of the block.
68 : }
69 :
70 : /** \brief Replaces the transition relation of the current lts by the transitions
71 : * of the bisimulation reduced transition system.
72 : * \pre The bisimulation equivalence classes have been computed. */
73 7 : void replace_transitions()
74 : {
75 7 : std::set<transition> resulting_transitions;
76 :
77 7 : const std::vector<transition>& trans = aut.get_transitions();
78 299 : for (const transition& t : trans)
79 : {
80 292 : resulting_transitions.insert(
81 584 : transition(
82 : get_eq_class(t.from()),
83 : t.label(),
84 : get_eq_probabilistic_class(t.to())));
85 : }
86 : // Remove the old transitions
87 7 : aut.clear_transitions();
88 :
89 : // Copy the transitions from the set into the transition system.
90 47 : for (const transition& t : resulting_transitions)
91 : {
92 40 : aut.add_transition(t);
93 : }
94 7 : }
95 :
96 : /** \brief Replaces the probabilistic states of the current lts by the probabilistic
97 : * states of the bisimulation reduced transition system.
98 : * \pre The bisimulation classes have been computed. */
99 7 : void replace_probabilistic_states()
100 : {
101 7 : 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
104 38 : for (probabilistic_block_type& prob_block : probabilistic_blocks)
105 : {
106 31 : if (prob_block.states.size()>0)
107 : {
108 31 : typename LTS_TYPE::probabilistic_state_t equivalent_ps = calculate_equivalent_probabilistic_state(prob_block);
109 31 : new_probabilistic_states.push_back(equivalent_ps);
110 31 : }
111 : }
112 :
113 : /* Remove old probabilistic states */
114 7 : aut.clear_probabilistic_states();
115 :
116 : // Add new prob states to aut
117 38 : for (const typename LTS_TYPE::probabilistic_state_t& new_ps : new_probabilistic_states)
118 : {
119 31 : aut.add_probabilistic_state(new_ps);
120 : }
121 :
122 7 : typename LTS_TYPE::probabilistic_state_t old_initial_prob_state = aut.initial_probabilistic_state();
123 7 : typename LTS_TYPE::probabilistic_state_t new_initial_prob_state = calculate_new_probabilistic_state(old_initial_prob_state);
124 7 : aut.set_initial_probabilistic_state(new_initial_prob_state);
125 7 : }
126 :
127 : /** \brief Returns whether two states are in the same probabilistic bisimulation equivalence class.
128 : * \param[in] s A state number.
129 : * \param[in] t A state number.
130 : * \retval true if \e s and \e t are in the same bisimulation equivalence class;
131 : * \retval false otherwise. */
132 6 : bool in_same_probabilistic_class_grv(const std::size_t s, const std::size_t t)
133 : {
134 6 : return get_eq_probabilistic_class(s) == get_eq_probabilistic_class(t);
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 : {
154 : state_key_type from;
155 : label_type label;
156 : state_key_type to;
157 : std::size_t* state_to_constellation_count_ptr;
158 : };
159 :
160 : struct probabilistic_transition_type : public embedded_list_node < probabilistic_transition_type >
161 : {
162 : state_key_type from;
163 : probability_label_type label;
164 : state_key_type to;
165 : };
166 :
167 : struct action_state_type : public embedded_list_node < action_state_type >
168 : {
169 : block_key_type parent_block;
170 : std::vector<probabilistic_transition_type*> incoming_transitions;
171 :
172 : // Temporary
173 : bool mark_state;
174 : std::size_t residual_transition_cnt;
175 : std::size_t* transition_count_ptr;
176 : };
177 :
178 : struct probabilistic_state_type : public embedded_list_node < probabilistic_state_type >
179 : {
180 : block_key_type parent_block;
181 : std::vector<action_transition_type*> incoming_transitions;
182 :
183 : // Temporary.
184 : bool mark_state;
185 : probability_label_type cumulative_probability;
186 : };
187 :
188 : // Prototype.
189 : struct action_mark_type;
190 :
191 : struct action_block_type : public embedded_list_node <action_block_type>
192 : {
193 : constellation_key_type parent_constellation;
194 : embedded_list<action_state_type> states;
195 : embedded_list<probabilistic_transition_type> incoming_probabilistic_transitions;
196 : action_mark_type* marking; // This value is nullptr if the block is not marked.
197 :
198 60 : action_block_type() : marking(nullptr){}
199 : };
200 :
201 : struct action_mark_type
202 : {
203 : action_block_type* action_block;
204 : embedded_list<action_state_type> left;
205 : embedded_list<action_state_type> middle;
206 : embedded_list<action_state_type> right;
207 : embedded_list<action_state_type>* large_block_ptr;
208 :
209 63 : action_mark_type(action_block_type& B)
210 63 : : action_block(&B),
211 63 : large_block_ptr(nullptr)
212 63 : {}
213 : };
214 :
215 : // Prototype
216 : struct probabilistic_mark_type;
217 :
218 : struct probabilistic_block_type : public embedded_list_node <probabilistic_block_type>
219 : {
220 : constellation_key_type parent_constellation;
221 : embedded_list<probabilistic_state_type> states;
222 : probabilistic_mark_type* marking;
223 :
224 : // a probabilistic block has incoming action transitions ordered by label
225 : embedded_list<action_transition_type> incoming_action_transitions;
226 :
227 43 : probabilistic_block_type() : marking(nullptr){}
228 : };
229 :
230 : struct probabilistic_mark_type
231 : {
232 : probabilistic_block_type* probabilistic_block;
233 : embedded_list<probabilistic_state_type> left;
234 : std::vector< embedded_list<probabilistic_state_type> > middle;
235 : embedded_list<probabilistic_state_type> right;
236 : embedded_list<probabilistic_state_type>* large_block_ptr;
237 :
238 64 : probabilistic_mark_type(probabilistic_block_type& B) : probabilistic_block(&B), large_block_ptr(nullptr) {}
239 : };
240 :
241 : struct action_constellation_type
242 : {
243 : embedded_list<action_block_type> blocks;
244 : std::size_t number_of_states; // number of states in this constellation.
245 : };
246 :
247 : struct probabilistic_constellation_type
248 : {
249 : embedded_list<probabilistic_block_type> blocks;
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.
257 : class transitions_per_label_t
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 :
265 620 : void add_single_transition(action_transition_type& t)
266 : {
267 620 : assert(t.label<m_transitions_per_label.size());
268 620 : if (m_transitions_per_label[t.label].size()==0)
269 : {
270 56 : m_occupancy_indicator.push(t.label);
271 : }
272 620 : m_transitions_per_label[t.label].push_back(t);
273 620 : }
274 :
275 : public:
276 : /* set the size of the vector m_transitions_per_label */
277 13 : void initialize(const std::size_t number_of_labels)
278 : {
279 13 : m_transitions_per_label=std::vector< embedded_list<action_transition_type> >(number_of_labels);
280 13 : }
281 :
282 26 : const std::vector< embedded_list<action_transition_type> >& transitions() const
283 : {
284 26 : return m_transitions_per_label;
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 */
289 43 : void add_grouped_transitions_to_block(probabilistic_block_type& block)
290 : {
291 99 : while (!m_occupancy_indicator.empty())
292 : {
293 56 : const label_type action=m_occupancy_indicator.top();
294 56 : m_occupancy_indicator.pop();
295 :
296 : // The next operation resets m_transitions_per_label[action] to empty.
297 56 : assert(action<m_transitions_per_label.size());
298 56 : block.incoming_action_transitions.append(m_transitions_per_label[action]);
299 : }
300 43 : }
301 :
302 99 : void move_incoming_transitions(probabilistic_state_type s, embedded_list<action_transition_type>& transition_list_with_t)
303 : {
304 369 : for(action_transition_type* t_ptr: s.incoming_transitions)
305 : {
306 270 : transition_list_with_t.erase(*t_ptr);
307 270 : add_single_transition(*t_ptr);
308 : }
309 99 : }
310 :
311 13 : void add_transitions(std::vector<action_transition_type>& transitions)
312 : {
313 363 : for(action_transition_type& t: transitions)
314 : {
315 350 : add_single_transition(t);
316 : }
317 13 : }
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.
346 : transitions_per_label_t transitions_per_label;
347 :
348 :
349 : LTS_TYPE& aut;
350 :
351 73 : bool check_data_structure()
352 : {
353 : // Check whether the constellation count in action transitions is ok.
354 4018 : for(const action_transition_type& t: action_transitions)
355 : {
356 3945 : std::size_t constellation=probabilistic_blocks[probabilistic_states[t.to].parent_block].parent_constellation;
357 3945 : std::size_t count_state_to_constellation=0;
358 :
359 816604 : for(const action_transition_type& t1: action_transitions)
360 : {
361 1629427 : if (t.from==t1.from &&
362 816648 : t.label==t1.label &&
363 3989 : constellation==probabilistic_blocks[probabilistic_states[t1.to].parent_block].parent_constellation)
364 : {
365 3973 : count_state_to_constellation++;
366 : }
367 : }
368 3945 : if (count_state_to_constellation!=*t.state_to_constellation_count_ptr)
369 : {
370 0 : mCRL2log(log::error) << "Transition " << t.from << "--" << t.label << "->" << t.to << " has inconsistent constellation_count: " <<
371 0 : *t.state_to_constellation_count_ptr << ". Should be " << count_state_to_constellation << ".\n";
372 0 : return false;
373 :
374 : }
375 : }
376 :
377 : // Check whether the number of states in an action constellation are correct.
378 324 : for(const action_constellation_type& c: action_constellations)
379 : {
380 251 : std::size_t counted_states=0;
381 868 : for(const action_block_type& b: c.blocks)
382 : {
383 366 : counted_states=counted_states+b.states.size();
384 : }
385 251 : 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.
389 294 : for(const probabilistic_constellation_type& c: probabilistic_constellations)
390 : {
391 221 : std::size_t counted_states=0;
392 676 : for(const probabilistic_block_type& b: c.blocks)
393 : {
394 234 : counted_states=counted_states+b.states.size();
395 : }
396 221 : 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 439 : for(const action_block_type& b: action_blocks)
400 : {
401 366 : assert(b.states.size()>0); // Action block contains no states.
402 :
403 366 : assert(b.marking==nullptr); // Action block's marking must be a null ptr.
404 : }
405 :
406 307 : for(const probabilistic_block_type& b: probabilistic_blocks)
407 : {
408 234 : assert(b.marking==nullptr); // Probabilistic block's marking must be a null ptr.
409 : }
410 :
411 73 : 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 :
432 : for(const probabilistic_block_type b: probabilistic_blocks)
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 :
445 : /** Creates the initial partition.
446 : * \details The blocks are initially partitioned based on the actions that can perform.
447 : */
448 13 : void create_initial_partition(void)
449 : {
450 13 : transitions_per_label.initialize(aut.num_action_labels());
451 :
452 : // Preprocessing initialization. First we have to initialise the action/probabilistic states and
453 : // transitions.
454 13 : preprocessing_stage();
455 :
456 : // Add action transitions to its respective list grouped by label.
457 13 : transitions_per_label.add_transitions(action_transitions);
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 13 : action_block_type initial_action_block;
462 :
463 : // Link all the action states together to the initial block
464 361 : for (action_state_type& s: action_states)
465 : {
466 348 : s.parent_block = 0; // Initial block has number 0.
467 348 : initial_action_block.states.push_back(s);
468 : }
469 13 : 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 13 : 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].
476 13 : refine_initial_action_block(transitions_per_label.transitions());
477 :
478 : // Initialise the probabilistic block. Initally, there is only one block of probabilistic states.
479 13 : probabilistic_blocks.emplace_back();
480 :
481 13 : probabilistic_block_type& initial_probabilistic_block=probabilistic_blocks.back();
482 13 : initial_probabilistic_block.parent_constellation = 0;
483 :
484 : // Link all the probabilistic states together to the initial block
485 138 : for (probabilistic_state_type& s : probabilistic_states)
486 : {
487 125 : s.parent_block = 0; // The initial block has number zero.
488 125 : initial_probabilistic_block.states.push_back(s);
489 : }
490 13 : 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 13 : probabilistic_constellation_type initial_probabilistic_const;
495 13 : 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 13 : initial_probabilistic_const.blocks.push_back(probabilistic_blocks.front());
500 13 : probabilistic_constellations.push_back(initial_probabilistic_const);
501 :
502 : // Initialise the initial action constellation.
503 13 : action_constellations.emplace_back();
504 13 : action_constellation_type& initial_action_const=action_constellations.back();
505 :
506 13 : initial_action_const.number_of_states = aut.num_states();
507 :
508 : // Construct the list of action blocks by linking them together.
509 54 : for(action_block_type& b : action_blocks)
510 : {
511 41 : b.parent_constellation = 0; // The initial constellation has number 0;
512 41 : 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 13 : std::vector<std::size_t*> new_count_ptr(aut.num_states(),nullptr);
518 :
519 55 : for (const embedded_list<action_transition_type>& at_list_per_label : transitions_per_label.transitions())
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 434 : for(action_transition_type& t: at_list_per_label)
524 : {
525 350 : assert(t.from<new_count_ptr.size());
526 350 : if (new_count_ptr[t.from]==nullptr)
527 : {
528 346 : state_to_constellation_count.push_back(0);
529 346 : new_count_ptr[t.from] = &state_to_constellation_count.back();
530 : }
531 350 : t.state_to_constellation_count_ptr = new_count_ptr[t.from];
532 350 : (*new_count_ptr[t.from])++;
533 : }
534 :
535 : // Reset all the variables used to prepare to next iteration.
536 434 : for(const action_transition_type& t: at_list_per_label)
537 : {
538 350 : 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 13 : 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.
550 355 : for(probabilistic_transition_type& t : probabilistic_transitions)
551 : {
552 342 : action_state_type& s = action_states[t.to];
553 342 : action_block_type& block = action_blocks[s.parent_block];
554 342 : block.incoming_probabilistic_transitions.push_back(t);
555 : }
556 :
557 13 : if (initial_action_const.blocks.size()>1)
558 : {
559 13 : non_trivial_action_constellations.push(&initial_action_const);
560 : }
561 :
562 13 : assert(check_data_structure());
563 13 : }
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. */
567 13 : void preprocessing_stage()
568 : {
569 : // Allocate space for states and transitions
570 :
571 13 : action_states.resize(aut.num_states());
572 13 : probabilistic_states.resize(aut.num_probabilistic_states());
573 13 : action_transitions.resize(aut.num_transitions());
574 :
575 : // Initialise the action transitions
576 13 : transition_key_type t_key = 0;
577 363 : for (const transition& t : aut.get_transitions())
578 : {
579 350 : action_transition_type& at = action_transitions[t_key];
580 350 : at.from = t.from();
581 350 : at.label = t.label();
582 350 : at.to = t.to();
583 350 : at.state_to_constellation_count_ptr = nullptr;
584 :
585 : // save incoming transition in state
586 350 : probabilistic_states[at.to].incoming_transitions.push_back(&at);
587 :
588 350 : t_key++;
589 : }
590 :
591 : // Initialise the probabilistic transitions. To this end, we have to iterate over
592 : // all probabilistic states.
593 138 : for (std::size_t i = 0; i < aut.num_probabilistic_states(); i++)
594 : {
595 125 : const typename LTS_TYPE::probabilistic_state_t& ps = aut.probabilistic_state(i);
596 125 : probabilistic_transition_type pt;
597 125 : if (ps.size()>1) // The probabilistic state is stored as a vector.
598 : {
599 403 : for (const typename LTS_TYPE::probabilistic_state_t::state_probability_pair& sp_pair : ps)
600 : {
601 310 : pt.from = i;
602 310 : pt.label = sp_pair.probability();
603 310 : pt.to = sp_pair.state();
604 310 : probabilistic_transitions.push_back(pt);
605 :
606 : // save incoming transition in state
607 310 : 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 32 : pt.from = i;
613 32 : pt.label = LTS_TYPE::probabilistic_state_t::probability_t::one();
614 32 : pt.to = ps.get();
615 32 : probabilistic_transitions.push_back(pt);
616 : // save incoming transition in state
617 32 : action_states[pt.to].incoming_transitions.push_back(&probabilistic_transitions.back());
618 : }
619 : }
620 :
621 : // End of preprocessing.
622 13 : }
623 :
624 : /* Refine the initial block according to its outgoing transitions.
625 : */
626 13 : void refine_initial_action_block(const std::vector< embedded_list<action_transition_type> >& transitions_per_label)
627 : {
628 : // Iterate over all transitions ordered by label, and refine the block.
629 55 : for (const embedded_list<action_transition_type>& t_list : transitions_per_label)
630 : {
631 42 : marked_action_blocks.clear();
632 : // The line below garbage collects marked_action_blocks to avoid covering too much memory continuously;
633 42 : static std::size_t count=0; if (count++ == 1000) { marked_action_blocks.shrink_to_fit(); count=0; }
634 :
635 434 : for(const action_transition_type& t: t_list)
636 : {
637 350 : action_state_type& s = action_states[t.from];
638 350 : assert(s.parent_block<action_blocks.size());
639 350 : action_block_type& parent_block = action_blocks[s.parent_block];
640 :
641 : // Move state s to marked states if not already added.
642 350 : if (false == s.mark_state)
643 : {
644 : // Add parent block to the list of marked blocks if not yet added
645 346 : if (parent_block.marking==nullptr)
646 : {
647 36 : marked_action_blocks.emplace_back(parent_block);
648 36 : parent_block.marking=&marked_action_blocks.back();
649 : }
650 :
651 346 : move_list_element_back<action_state_type>(s, parent_block.states, parent_block.marking->left);
652 346 : s.mark_state = true;
653 : }
654 : }
655 :
656 : // Split the marked blocks.
657 78 : for (action_mark_type& block_marking: marked_action_blocks)
658 : {
659 36 : 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 8 : block_marking.action_block->states = block_marking.left;
663 : }
664 : else
665 : {
666 : // Split the block if not all states are marked.
667 28 : action_blocks.emplace_back();
668 28 : action_block_type& new_block=action_blocks.back();
669 28 : new_block.states = block_marking.left;
670 :
671 : // Init parent block of each state in new block.
672 330 : for(action_state_type& s: new_block.states)
673 : {
674 274 : s.parent_block = action_blocks.size()-1;
675 : }
676 :
677 : }
678 :
679 : // clean mark list
680 36 : block_marking.left.clear();
681 36 : block_marking.action_block->marking=nullptr;
682 :
683 : }
684 :
685 : // Clean the marked states.
686 434 : for(const action_transition_type& t: t_list)
687 : {
688 350 : action_states[t.from].mark_state = false;
689 : }
690 : }
691 :
692 13 : }
693 :
694 : /* Move an element of a list to the back of another list.
695 : */
696 : template <typename LIST_ELEMENT>
697 1280 : void move_list_element_back(LIST_ELEMENT& s, embedded_list<LIST_ELEMENT>& source_list, embedded_list<LIST_ELEMENT>& dest_list)
698 : {
699 1280 : source_list.erase(s);
700 1280 : dest_list.push_back(s);
701 1280 : }
702 :
703 : /** \brief Move an element of a list to the front of another the list.
704 : * \details
705 : */
706 : template<typename LIST_ELEMENT>
707 : void move_list_element_front(LIST_ELEMENT& s, embedded_list<LIST_ELEMENT>& source_list, embedded_list<LIST_ELEMENT>& dest_list)
708 : {
709 : source_list.erase(s);
710 : dest_list.push_front(s);
711 : }
712 :
713 : /** \brief Refine partition until it becomes stable.
714 : * \details
715 : */
716 13 : void refine_partition_until_it_becomes_stable(void)
717 : {
718 :
719 : // Refine until all the constellations are trivial.
720 60 : while (!non_trivial_probabilistic_constellations.empty() || !non_trivial_action_constellations.empty())
721 : {
722 47 : assert(check_data_structure());
723 :
724 : // Refine probabilistic blocks if a non-trivial action constellation exists.
725 47 : if (!non_trivial_action_constellations.empty())
726 : {
727 47 : action_constellation_type* non_trivial_action_const = non_trivial_action_constellations.top();
728 47 : non_trivial_action_constellations.pop();
729 47 : 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 47 : action_block_type* Bc_ptr = choose_action_splitter(non_trivial_action_const);
735 :
736 : // Derive the left, right and middle sets from mark function.
737 47 : marked_probabilistic_blocks.clear();
738 : // The line below garbage collects marked_action_blocks to avoid covering too much memory continuously;
739 47 : static std::size_t count=0; if (count++ == 1000) { marked_probabilistic_blocks.shrink_to_fit(); count=0; }
740 :
741 47 : mark_probabilistic(*Bc_ptr, marked_probabilistic_blocks);
742 :
743 : // Split every marked probabilistic block based on left, middle and right.
744 111 : for (probabilistic_mark_type& B : marked_probabilistic_blocks)
745 : {
746 : // We must know whether the current constellation is already on the stack.
747 64 : 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 64 : B.probabilistic_block->states = *B.large_block_ptr;
751 64 : 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 64 : if (B.left.size() > 0)
756 : {
757 10 : 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 64 : if (B.right.size() > 0)
763 : {
764 7 : 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 170 : for (embedded_list<probabilistic_state_type>& middle : B.middle)
770 : {
771 106 : if (middle.size() > 0)
772 : {
773 13 : 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 64 : if (!already_on_non_trivial_constellations_stack && probabilistic_constellations[B.probabilistic_block->parent_constellation].blocks.size()>1)
780 : {
781 24 : probabilistic_constellation_type& parent_const = probabilistic_constellations[B.probabilistic_block->parent_constellation];
782 24 : assert(parent_const.blocks.size()>1);
783 24 : non_trivial_probabilistic_constellations.push(&parent_const);
784 : }
785 :
786 : // Reset middle vector to prepare for the next mark process
787 64 : B.middle.clear();
788 : }
789 : }
790 :
791 : // Refine action blocks if a non-trivial probabilistic constellation exists.
792 47 : if (!non_trivial_probabilistic_constellations.empty())
793 : {
794 : // print_structure("REFINE II");
795 :
796 30 : probabilistic_constellation_type* non_trivial_probabilistic_const = non_trivial_probabilistic_constellations.top();
797 30 : non_trivial_probabilistic_constellations.pop();
798 30 : 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 30 : 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.
804 30 : for (typename embedded_list<action_transition_type>::iterator i=Bc_ptr->incoming_action_transitions.begin();
805 57 : 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 27 : const label_type a = i->label;
809 27 : marked_action_blocks.clear();
810 27 : 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.
814 54 : for (action_mark_type& B : marked_action_blocks)
815 : {
816 : // We must know whether the current constellation is already on the stack.
817 27 : 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 27 : B.action_block->states = *B.large_block_ptr;
821 27 : 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 27 : if (B.left.size() > 0)
825 : {
826 16 : 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 27 : if (B.right.size() > 0)
831 : {
832 2 : 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 27 : if (B.middle.size() > 0)
838 : {
839 1 : 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 27 : if (!already_on_non_trivial_constellations_stack && action_constellations[B.action_block->parent_constellation].blocks.size()>1)
845 : {
846 10 : action_constellation_type& parent_const = action_constellations[B.action_block->parent_constellation];
847 10 : assert(parent_const.blocks.size()>1);
848 10 : non_trivial_action_constellations.push(&parent_const);
849 : }
850 :
851 : }
852 : }
853 : }
854 : }
855 : // print_structure("END REFINE");
856 13 : assert(check_data_structure());
857 13 : }
858 :
859 : /** \brief Split a probabilistic block.
860 : * \details Creates another block containing the states specified in states_of_new_block. It adds the new block
861 : * to the same constellation as the current block to split.
862 : */
863 30 : void split_probabilistic_block(probabilistic_block_type& block_to_split, embedded_list<probabilistic_state_type>& states_of_new_block)
864 : {
865 : // First create the new block to be allocated, and initialise its parameters
866 30 : probabilistic_blocks.emplace_back();
867 30 : probabilistic_block_type& new_block=probabilistic_blocks.back();
868 :
869 30 : new_block.parent_constellation = block_to_split.parent_constellation; // The new block is in the same constellation as B
870 30 : new_block.states = states_of_new_block;
871 30 : 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 159 : for(probabilistic_state_type& s: new_block.states)
878 : {
879 : // Update the parent block of the state
880 99 : s.parent_block = probabilistic_blocks.size()-1;
881 99 : transitions_per_label.move_incoming_transitions(s,block_to_split.incoming_action_transitions);
882 : }
883 :
884 : // Since the transitions are already grouped by label, add them to the
885 : // initial probabilistic block as incoming transitions.
886 30 : transitions_per_label.add_grouped_transitions_to_block(new_block);
887 :
888 : // Add the new block to the back of the list of blocks in the parent constellation.
889 30 : probabilistic_constellation_type& parent_const = probabilistic_constellations[new_block.parent_constellation];
890 :
891 30 : parent_const.blocks.push_back(probabilistic_blocks.back());
892 30 : }
893 :
894 : /** \brief Split an action block.
895 : * \details Creates another block containing the states specified in states_of_new_block. It adds the new block
896 : * to the same constellation as the current block to split.
897 : */
898 19 : void split_action_block(action_block_type& block_to_split, embedded_list<action_state_type>& states_of_new_block)
899 : {
900 : // First create the new block to be allocated, and initialise its parameters
901 19 : action_blocks.emplace_back();
902 19 : action_block_type& new_block=action_blocks.back();
903 :
904 19 : new_block.parent_constellation = block_to_split.parent_constellation; // The new block is in the same constellation as block to split
905 19 : new_block.states = states_of_new_block;
906 19 : 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 199 : for(action_state_type& s: new_block.states)
912 : {
913 : // Update the parent block of the state
914 161 : 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 319 : for (probabilistic_transition_type* t : s.incoming_transitions)
918 : {
919 : // Move transition from list of transitions of previous block to new block
920 158 : move_list_element_back((*t), block_to_split.incoming_probabilistic_transitions,
921 158 : new_block.incoming_probabilistic_transitions);
922 : }
923 : }
924 :
925 : // Add the new block to the back of the list of blocks in the parent constellation.
926 19 : action_constellation_type& parent_const = action_constellations[new_block.parent_constellation];
927 :
928 19 : parent_const.blocks.push_back(action_blocks.back());
929 19 : }
930 :
931 : /** \brief Gives the probabilistic blocks that are marked by block Bc.
932 : * \details Derives the left, middle and rigth sets of the marked probabilistic blocks, based on the
933 : * incoming probabilistic transitions in block Bc.
934 : */
935 47 : 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.
940 420 : for( probabilistic_transition_type& pt: Bc.incoming_probabilistic_transitions)
941 : {
942 326 : probabilistic_state_type& s = probabilistic_states[pt.from];
943 326 : const probability_label_type& p = pt.label;
944 326 : probabilistic_block_type& B = probabilistic_blocks[s.parent_block];
945 :
946 : // If the block was not previously marked, then mark the block and move all states to right
947 326 : if (nullptr == B.marking)
948 : {
949 64 : marked_probabilistic_blocks.emplace_back(B);
950 64 : B.marking = &marked_probabilistic_blocks.back();
951 64 : B.marking->right = B.states;
952 64 : 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.
956 64 : B.marking->large_block_ptr = &B.marking->right;
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 326 : 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 252 : s.mark_state = true;
965 252 : s.cumulative_probability = p;
966 252 : 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.
971 74 : s.cumulative_probability = s.cumulative_probability + p;
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.
978 111 : for (probabilistic_mark_type& B : marked_probabilistic_blocks)
979 : {
980 : // Clear this locally used data structure and reset it so now and then to avoid that it requires
981 : // too much data.
982 64 : grouped_states_per_probability_in_block.clear();
983 64 : static std::size_t count=0; if (count++ == 1000) { marked_action_blocks.shrink_to_fit(); count=0; }
984 :
985 64 : embedded_list<probabilistic_state_type> middle_temp=B.left;
986 64 : B.left.clear();
987 :
988 : // First, add all states lower than max_cumulative_probability to the middle set.
989 316 : for(typename embedded_list<probabilistic_state_type>::iterator i=middle_temp.begin(); i!=middle_temp.end(); )
990 : {
991 252 : probabilistic_state_type& s= *i;
992 252 : i++; // Increment the iterator here, such that we can change the list.
993 :
994 252 : if (s.cumulative_probability == probability_label_type().one())
995 : {
996 : // State s has probability lower than max_cumulative_probability. Add to the middle set.
997 30 : 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 252 : 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 350 : for(probabilistic_state_type& s: middle_temp)
1008 : {
1009 222 : 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
1013 64 : std::sort(grouped_states_per_probability_in_block.begin(), grouped_states_per_probability_in_block.end());
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 64 : probability_label_type current_probability = probability_label_type().zero();
1020 :
1021 64 : if (grouped_states_per_probability_in_block.size()>0)
1022 : {
1023 52 : B.middle.emplace_back();
1024 274 : for (const std::pair<probability_label_type, probabilistic_state_type*>& cumulative_prob_state_pair : grouped_states_per_probability_in_block)
1025 : {
1026 222 : probabilistic_state_type* s = cumulative_prob_state_pair.second;
1027 222 : 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 54 : current_probability = cumulative_prob_state_pair.first;
1032 54 : B.middle.emplace_back(); //put empty list at end of B.middle.
1033 : }
1034 :
1035 222 : 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 64 : if (B.left.size() > B.large_block_ptr->size())
1043 : {
1044 4 : 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 170 : for (embedded_list<probabilistic_state_type>& middle_set : B.middle)
1049 : {
1050 106 : if (middle_set.size() > B.large_block_ptr->size())
1051 : {
1052 42 : B.large_block_ptr = &middle_set;
1053 : }
1054 : }
1055 :
1056 : // Finally, reset the block_is_marked variable of the current block.
1057 64 : B.probabilistic_block->marking = nullptr;
1058 : }
1059 47 : }
1060 :
1061 : /** \brief Gives the action blocks that are marked by probabilistic block Bc.
1062 : * \details Derives the left, middle and rigth sets of the marked action blocks, based on the
1063 : * incoming action transitions labeled with "a" in block Bc.
1064 : */
1065 27 : 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 27 : 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 27 : for(typename embedded_list<action_transition_type>::iterator action_walker=action_walker_begin;
1077 297 : action_walker!=action_walker_end && action_walker->label==a;
1078 270 : action_walker++)
1079 : {
1080 270 : action_transition_type& t= *action_walker;
1081 270 : action_state_type& s = action_states[t.from];
1082 270 : action_block_type& B = action_blocks[s.parent_block];
1083 :
1084 : // If the block was not previously marked, then mark the block and add all states to right.
1085 270 : if (nullptr == B.marking)
1086 : {
1087 27 : marked_action_blocks.emplace_back(B);
1088 27 : B.marking = &marked_action_blocks.back();
1089 27 : B.marking->right=B.states;
1090 27 : B.states.clear();
1091 : // Also initialise the larger block pointer to the right set.
1092 27 : B.marking->large_block_ptr = &B.marking->right;
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 270 : 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 269 : s.mark_state = true;
1101 269 : s.residual_transition_cnt = *t.state_to_constellation_count_ptr;
1102 269 : move_list_element_back<action_state_type>(s, B.marking->right, B.marking->left);
1103 : }
1104 :
1105 270 : s.residual_transition_cnt--;
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.
1112 54 : for (action_mark_type& B : marked_action_blocks)
1113 : {
1114 : // Iterate over all left states in B and check whether the state has to be moved to middle.
1115 296 : for(typename embedded_list<action_state_type>::iterator i=B.left.begin(); i!=B.left.end(); )
1116 : {
1117 269 : action_state_type& s= *i;
1118 269 : i++; // This iterator is incremented here as s will be removed from the list over which iteration takes place.
1119 269 : if (s.residual_transition_cnt > 0)
1120 : {
1121 : // The transition count is greater than zero. Move state to middle set.
1122 3 : 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 269 : s.mark_state = false;
1128 : }
1129 :
1130 : // Find the largest set.
1131 27 : if (B.left.size() > B.large_block_ptr->size())
1132 : {
1133 10 : B.large_block_ptr = &B.left;
1134 : }
1135 27 : if (B.middle.size() > B.large_block_ptr->size())
1136 : {
1137 1 : B.large_block_ptr = &B.middle;
1138 : }
1139 :
1140 : // Finally, reset the block_is_marked variable of the current block.
1141 27 : 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 27 : for( ;
1147 297 : action_walker_begin!=action_walker_end && action_walker_begin->label==a;
1148 270 : action_walker_begin++)
1149 : {
1150 270 : action_transition_type& t= *action_walker_begin;
1151 270 : action_state_type& s = action_states[t.from];
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 270 : if (s.residual_transition_cnt > 0)
1156 : {
1157 3 : std::size_t state_to_constellation_count_old = *t.state_to_constellation_count_ptr;
1158 :
1159 3 : 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.
1165 3 : *t.state_to_constellation_count_ptr = s.residual_transition_cnt;
1166 :
1167 : // Now allocate another state_to_constellation_count for the Bc block
1168 3 : state_to_constellation_count.emplace_back(state_to_constellation_count_old - s.residual_transition_cnt);
1169 3 : s.transition_count_ptr = &state_to_constellation_count.back();
1170 : }
1171 3 : t.state_to_constellation_count_ptr = s.transition_count_ptr;
1172 : }
1173 : }
1174 27 : }
1175 :
1176 : /** \brief Choose an splitter block from a non trivial constellation.
1177 : * \details The number of states in the chosen splitter is always less than the half of the non
1178 : * trivial constellation. Furtheremore, the selected splitter is moved to a new constellation.
1179 : */
1180 47 : action_block_type* choose_action_splitter(action_constellation_type* non_trivial_action_const)
1181 : {
1182 47 : 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 47 : action_block_type* Bc = &non_trivial_action_const->blocks.front();
1187 :
1188 47 : 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 16 : 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 47 : non_trivial_action_const->blocks.erase(*Bc);
1197 :
1198 : // Update the number of states and blocks of the non trivial block
1199 47 : 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 47 : 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 24 : non_trivial_action_constellations.push(non_trivial_action_const);
1206 : }
1207 :
1208 : // Add Bc to a new constellation
1209 47 : action_constellations.emplace_back();
1210 47 : action_constellation_type& new_action_const=action_constellations.back();
1211 :
1212 47 : Bc->parent_constellation = action_constellations.size()-1;
1213 47 : new_action_const.blocks.push_back(*Bc);
1214 47 : new_action_const.number_of_states = Bc->states.size();
1215 :
1216 47 : return Bc;
1217 : }
1218 :
1219 : /** \brief Choose an splitter block from a non trivial constellation.
1220 : * \details The number of states in the chosen splitter is always less than the half of the non
1221 : * trivial constellation. Furtheremore, the selected splitter is moved to a new constellation.
1222 : */
1223 30 : probabilistic_block_type* choose_probabilistic_splitter(probabilistic_constellation_type* non_trivial_probabilistic_const)
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 30 : probabilistic_block_type* Bc = &non_trivial_probabilistic_const->blocks.front();
1228 30 : 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 20 : 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 30 : non_trivial_probabilistic_const->blocks.erase(*Bc);
1237 :
1238 : // Update the number of states and blocks of the non trivial block
1239 30 : 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 30 : 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 6 : non_trivial_probabilistic_constellations.push(non_trivial_probabilistic_const);
1246 : }
1247 :
1248 : // Add Bc to a new constellation
1249 30 : probabilistic_constellations.emplace_back();
1250 30 : probabilistic_constellation_type& new_probabilistic_const=probabilistic_constellations.back();
1251 30 : Bc->parent_constellation = probabilistic_constellations.size()-1;
1252 30 : new_probabilistic_const.blocks.push_back(*Bc);
1253 30 : new_probabilistic_const.number_of_states = Bc->states.size();
1254 :
1255 30 : return Bc;
1256 : }
1257 :
1258 38 : typename LTS_TYPE::probabilistic_state_t calculate_new_probabilistic_state(typename LTS_TYPE::probabilistic_state_t ps)
1259 : {
1260 38 : typename LTS_TYPE::probabilistic_state_t new_prob_state;
1261 :
1262 : /* Iterate over all state probability pairs in the selected probabilistic state*/
1263 38 : if (ps.size()>1) // The state is stored as a vector of states and probabilities.
1264 : {
1265 23 : std::map <state_key_type, probability_fraction_type> prob_state_map;
1266 112 : 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 89 : state_key_type new_state = get_eq_class(sp_pair.state());
1270 :
1271 89 : 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 61 : prob_state_map[new_state] = sp_pair.probability();
1275 : }
1276 : else
1277 : {
1278 : /* The state is already in the mapping. Sum up probabilities */
1279 28 : 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 23 : typename std::map<state_key_type, probability_fraction_type>::iterator i = prob_state_map.begin();
1284 23 : if (++i==prob_state_map.end()) // There is only one state with probability one.
1285 : {
1286 5 : new_prob_state.set(prob_state_map.begin()->first);
1287 : }
1288 : else
1289 : {
1290 : // This probabilistic state has more components.
1291 74 : for (const auto& i: prob_state_map)
1292 : {
1293 56 : new_prob_state.add(i.first, i.second);
1294 : }
1295 : }
1296 23 : }
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 15 : new_prob_state.set(get_eq_class(ps.get()));
1301 : }
1302 38 : return new_prob_state;
1303 0 : }
1304 :
1305 31 : 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 31 : assert(pb.states.size()>0);
1309 31 : const probabilistic_state_type& s = pb.states.front();
1310 :
1311 31 : if (s.incoming_transitions.size()>0)
1312 : {
1313 : // Take an incoming transition to know the key of the state
1314 31 : state_key_type s_key = s.incoming_transitions.back()->to;
1315 :
1316 31 : const typename LTS_TYPE::probabilistic_state_t& old_prob_state = aut.probabilistic_state(s_key);
1317 :
1318 31 : return calculate_new_probabilistic_state(old_prob_state);
1319 : }
1320 : // else it is the initial proabilistic state.
1321 0 : return calculate_new_probabilistic_state(aut.initial_probabilistic_state());
1322 :
1323 : }
1324 : };
1325 :
1326 :
1327 : /** \brief Reduce transition system l with respect to probabilistic bisimulation.
1328 : * \param[in/out] l The transition system that is reduced.
1329 : */
1330 : template < class LTS_TYPE>
1331 : void probabilistic_bisimulation_reduce_grv(LTS_TYPE& l, utilities::execution_timer& timer);
1332 :
1333 : /** \brief Checks whether the two initial states of two plts's are probabilistic bisimilar.
1334 : * \details This lts and the lts l2 are not usable anymore after this call.
1335 : * \param[in/out] l1 A first probabilistic transition system.
1336 : * \param[in/out] l2 A second probabilistic transition system.
1337 : * \retval True iff the initial states of the current transition system and l2 are probabilistic bisimilar */
1338 : template < class LTS_TYPE>
1339 : bool destructive_probabilistic_bisimulation_compare_grv(LTS_TYPE& l1, LTS_TYPE& l2, utilities::execution_timer& timer);
1340 :
1341 : /** \brief Checks whether the two initial states of two plts's are probabilistic bisimilar.
1342 : * \details The current transitions system and the lts l2 are first duplicated and subsequently
1343 : * reduced modulo bisimulation. If memory space is a concern, one could consider to
1344 : * use destructive_bisimulation_compare.
1345 : * \param[in/out] l1 A first transition system.
1346 : * \param[in/out] l2 A second transistion system.
1347 : * \retval True iff the initial states of the current transition system and l2 are probabilistic bisimilar */
1348 : template < class LTS_TYPE>
1349 : bool probabilistic_bisimulation_compare_grv(const LTS_TYPE& l1, const LTS_TYPE& l2, utilities::execution_timer& timer);
1350 :
1351 : template < class LTS_TYPE>
1352 7 : void probabilistic_bisimulation_reduce_grv(LTS_TYPE& l, utilities::execution_timer& timer)
1353 : {
1354 : // Apply the probabilistic bisimulation reduction algorithm.
1355 7 : detail::prob_bisim_partitioner_grv<LTS_TYPE> prob_bisim_part(l, timer);
1356 :
1357 : // Clear the state labels of the LTS l
1358 7 : l.clear_state_labels();
1359 :
1360 : // Assign the reduced LTS
1361 7 : l.set_num_states(prob_bisim_part.num_eq_classes());
1362 7 : prob_bisim_part.replace_transitions();
1363 7 : prob_bisim_part.replace_probabilistic_states();
1364 7 : }
1365 :
1366 : template < class LTS_TYPE>
1367 6 : bool probabilistic_bisimulation_compare_grv(
1368 : const LTS_TYPE& l1,
1369 : const LTS_TYPE& l2,
1370 : utilities::execution_timer& timer)
1371 : {
1372 6 : LTS_TYPE l1_copy(l1);
1373 6 : LTS_TYPE l2_copy(l2);
1374 12 : return destructive_probabilistic_bisimulation_compare_grv(l1_copy, l2_copy, timer);
1375 6 : }
1376 :
1377 : template < class LTS_TYPE>
1378 6 : bool destructive_probabilistic_bisimulation_compare_grv(
1379 : LTS_TYPE& l1,
1380 : LTS_TYPE& l2,
1381 : utilities::execution_timer& timer)
1382 : {
1383 : std::size_t initial_probabilistic_state_key_l1;
1384 : std::size_t initial_probabilistic_state_key_l2;
1385 :
1386 : // Merge states
1387 6 : mcrl2::lts::detail::plts_merge(l1, l2);
1388 6 : 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 6 : initial_probabilistic_state_key_l2 = l1.num_probabilistic_states() - 1;
1393 6 : initial_probabilistic_state_key_l1 = l1.num_probabilistic_states() - 2;
1394 :
1395 6 : detail::prob_bisim_partitioner_grv<LTS_TYPE> prob_bisim_part(l1,timer);
1396 :
1397 6 : return prob_bisim_part.in_same_probabilistic_class_grv(initial_probabilistic_state_key_l2,
1398 12 : initial_probabilistic_state_key_l1);
1399 6 : }
1400 :
1401 : } // end namespace detail
1402 : } // end namespace lts
1403 : } // end namespace mcrl2
1404 : #endif //_LIBLTS_PBISIM_GRV_H
|
