mCRL2
Loading...
Searching...
No Matches
liblts_bisim_minimal_depth.h
Go to the documentation of this file.
1// Author(s): Jan Martens
2//
3// Copyright: see the accompanying file COPYING or copy at
4// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
5//
6// Distributed under the Boost Software License, Version 1.0.
7// (See accompanying file LICENSE_1_0.txt or copy at
8// http://www.boost.org/LICENSE_1_0.txt)
15#ifndef _LIBLTS_BISIM_M
16#define _LIBLTS_BISIM_M
17
20#include "mcrl2/lts/lts_aut.h"
21#include "mcrl2/lts/lts_dot.h"
22#include "mcrl2/lts/lts_fsm.h"
25#include <fstream>
26
27namespace mcrl2
28{
29namespace lts
30{
31namespace detail
32{
33template <class LTS_TYPE>
35{
36public:
44 bisim_partitioner_minimal_depth(LTS_TYPE& l, const std::size_t init_l2)
45 : initial_l2(init_l2),
47 aut(l)
48 {
49 to_be_processed.clear();
50 block initial_block = block();
51 for (state_type i = 0; i < aut.num_states(); i++)
52 {
53 initial_block.states.push_back(i);
54 }
55 sort_transitions(aut.get_transitions(), aut.hidden_label_set(), mcrl2::lts::lbl_tgt_src);
56 const std::vector<transition>& trans = aut.get_transitions();
57 for (std::vector<transition>::const_iterator r = trans.begin(); r != trans.end(); ++r)
58 {
59 initial_block.transitions.push_back(*r);
60 }
61 initial_block.block_index = 0;
62 initial_block.state_index = 0;
64 initial_block.parent_block_index = 0;
65 initial_block.level = 0;
66 blocks.emplace_back(initial_block);
67
68 block_index_of_a_state = std::vector<block_index_type>(aut.num_states(), 0);
69 block_flags.push_back(false);
70 state_flags = std::vector<bool>(aut.num_states(), false);
71 to_be_processed.push_back(0);
72 BL.clear();
73 // finished creating initial data structures
74
75 bool splitted = true;
76 level_type lvl = 1;
77 while (splitted && block_index_of_a_state[initial_l2] == block_index_of_a_state[aut.initial_state()])
78 {
79 splitted = refine_partition(lvl);
80 lvl++;
81
82 for (typename std::vector<block>::reverse_iterator i = blocks.rbegin();
83 i != blocks.rend() && (*i).level == lvl - 1;
84 ++i)
85 {
86 to_be_processed.push_back((*i).block_index);
87 }
88 }
89
90 for (state_type i = 0; i < aut.num_states(); i++)
91 {
93 if (!block_flags[bid])
94 {
95 block_flags[bid] = true;
96 partition.insert(bid);
97 }
98 }
99 mCRL2log(mcrl2::log::info) << "Partition refinement done, partition contains: " << partition.size()
100 << " blocks, the history contains " << lvl - 1 << " levels." << std::endl;
102 }
103
106
116 mcrl2::state_formulas::state_formula dist_formula_mindepth(const std::size_t s, const std::size_t t)
117 {
119 mCRL2log(mcrl2::log::info) << "done with formula \n";
120 return convert_formula(f);
121 };
122
123 bool in_same_class(const std::size_t s, const std::size_t t)
124 {
126 }
127
128
129private:
130 typedef std::size_t block_index_type;
131 typedef std::size_t state_type;
132 typedef std::size_t level_type;
133 typedef std::size_t formula_index_type;
134 typedef std::size_t label_type;
136
138 LTS_TYPE& aut;
139 std::set<block_index_type> partition;
140
141 struct block
142 {
143 state_type state_index; // The state number that represent the states in this block
144 block_index_type block_index; // The sequence number of this block.
145 block_index_type parent_block_index; // Index of the parent block.
147
148 // If there is no parent block, this refers to the block itself.
149 std::vector<state_type> states;
150 std::vector<transition> transitions;
151 std::set<std::pair<label_type, block_index_type>> outgoing_observations;
152
153 void swap(block& b)
154 {
159 states.swap(b.states);
160 transitions.swap(b.transitions);
161 }
162 };
163
164 struct formula
165 {
169 std::vector<formula> conjunctions;
170 std::set<block_index_type> truths;
171
172 int depth()
173 {
174 int max_depth = 0;
175 for (formula f : conjunctions)
176 {
177 max_depth = std::max(max_depth, f.depth() + 1);
178 }
179 return max_depth;
180 }
181 };
182
183 std::vector<block> blocks;
184 // Blocks that are split become inactive.
185 std::vector<state_type> block_index_of_a_state;
186 std::vector<bool> block_flags;
187 std::vector<bool> state_flags;
188
189 std::vector<block_index_type> to_be_processed;
190 std::vector<block_index_type> BL;
191 typedef std::pair<label_type, block_index_type> observation_t;
192 typedef std::set<observation_t> derivatives_t;
193 std::map<std::pair<block_index_type, block_index_type>, level_type> greatest_common_ancestor;
194
195 /* Post processes the partition structure to save outgoing transitions per block */
197 {
198 for (transition t : aut.get_transitions())
199 {
200 block_index_type sourceBlock = block_index_of_a_state[t.from()];
201 block_index_type targetBlock = block_index_of_a_state[t.to()];
202
203 blocks[sourceBlock].outgoing_observations.insert(std::make_pair(aut.apply_hidden_label_map(t.label()), targetBlock));
204 }
205 }
206
212 {
213 std::set<block_index_type> image_truths;
214 std::set<block_index_type> pre_image_truths;
215 std::set<block_index_type> intersection;
216
217 image_truths = std::set(partition);
218
219 for (formula df : f.conjunctions)
220 {
221 std::set_intersection(image_truths.begin(),
222 image_truths.end(),
223 df.truths.begin(),
224 df.truths.end(),
225 std::inserter(intersection, intersection.begin()));
226 image_truths.swap(intersection);
227 intersection.clear();
228 }
229
230 // Now compute preimage according to label
231 for (block_index_type B : image_truths)
232 {
233 for (transition t : blocks[B].transitions)
234 {
235 if (aut.apply_hidden_label_map(t.label()) == f.label && (pre_image_truths.find(block_index_of_a_state[t.from()]) == pre_image_truths.end()))
236 {
237 pre_image_truths.insert(block_index_of_a_state[t.from()]);
238 }
239 }
240 }
241
242 if (f.negated)
243 {
244 image_truths.swap(pre_image_truths);
245 pre_image_truths.clear();
246 std::set_difference(partition.begin(),
247 partition.end(),
248 image_truths.begin(),
249 image_truths.end(),
250 std::inserter(pre_image_truths, pre_image_truths.begin()));
251 }
252 f.truths.swap(pre_image_truths);
253 }
254
255 // Refine the partition to a certain lvl.
257 {
258 if (to_be_processed.empty())
259 {
260 return false;
261 }
262 block_index_type splitter_index;
263 while (!to_be_processed.empty())
264 {
265 splitter_index = to_be_processed.front();
266
267 to_be_processed.erase(to_be_processed.begin());
268 if (blocks[splitter_index].level == lvl)
269 {
270 return true;
271 }
272
273 std::vector<transition> transitions_to_process = blocks[splitter_index].transitions;
274 for (std::vector<transition>::const_iterator i = transitions_to_process.begin();
275 i != transitions_to_process.end();
276 ++i)
277 {
278 transition t = *i;
279 state_flags[t.from()] = true;
280 const block_index_type marked_block_index = block_index_of_a_state[t.from()];
281 if (block_flags[marked_block_index] == false)
282 {
283 block_flags[marked_block_index] = true;
284 BL.push_back(marked_block_index);
285 }
286 // If the label of the next action is different, we must carry out the splitting.
287 if ((i != transitions_to_process.end() && next(i) == transitions_to_process.end())
288 || aut.apply_hidden_label_map(t.label()) != aut.apply_hidden_label_map(next(i)->label()))
289 {
290 split_BL(lvl);
291 BL.clear();
292 }
293 }
294 }
295 return true;
296 }
297
300 {
301 for (block_index_type Bsplit : BL)
302 {
303 block_flags[Bsplit] = false;
304 std::vector<state_type> flagged_states;
305 std::vector<state_type> non_flagged_states;
306 std::vector<state_type> Bsplit_states;
307 Bsplit_states.swap(blocks[Bsplit].states);
308 for (state_type s : Bsplit_states)
309 {
310 if (state_flags[s])
311 {
312 // state is flagged.
313 flagged_states.push_back(s);
314 }
315 else
316 {
317 // state is not flagged. It will be moved to a new block.
318 non_flagged_states.push_back(s);
319 block_index_of_a_state[s] = blocks.size();
320 }
321 }
322 block_index_type Bparent = Bsplit;
323 // Set the correct parent
324 while (blocks[Bparent].level == lvl)
325 {
326 Bparent = blocks[Bparent].parent_block_index;
327 }
328
329 block_index_type reset_state_flags_block = Bsplit;
330 if (!non_flagged_states.empty())
331 {
332 // There are flagged and non flagged states. So, the block must be split.
333 // Move the unflagged states to the new block.
334 if (mCRL2logEnabled(log::debug))
335 {
336 const std::size_t m = static_cast<std::size_t>(
337 std::pow(10.0, std::floor(std::log10(static_cast<double>((blocks.size() + 1) / 2)))));
338 if ((blocks.size() + 1) / 2 % m == 0)
339 {
340 mCRL2log(log::debug) << "Bisimulation partitioner: create block " << (blocks.size() + 1) / 2 << std::endl;
341 }
342 }
343 // Create a first new block.
344 blocks.push_back(block());
345 block_index_type new_block1 = blocks.size() - 1;
346 blocks.back().state_index = max_state_index;
348 blocks.back().block_index = new_block1;
349 blocks.back().level = lvl;
350
351 blocks.back().parent_block_index = Bparent;
352 non_flagged_states.swap(blocks.back().states);
353
354 // The flag fields of the new blocks is set to false;
355 block_flags.push_back(false);
356 // distribute the transitions
357 // Finally the non-inert transitions are distributed over both blocks in the obvious way.
358 // Note that this must be done after all states are properly put into a new block.
359 std::vector<transition> old_transitions;
360 std::vector<transition> flagged_transitions;
361 std::vector<transition> non_flagged_transitions;
362
363 old_transitions = blocks[Bsplit].transitions;
364 for (std::vector<transition>::iterator k = old_transitions.begin(); k != old_transitions.end(); ++k)
365 {
366 if (state_flags[(*k).to()])
367 {
368 flagged_transitions.push_back(*k);
369 }
370 else
371 {
372 non_flagged_transitions.push_back(*k);
373 }
374 }
375
376 // Create a second new block.
377 block BlockLeft = block();
378
379 // block_is_active.push_back(true);
380 BlockLeft.state_index = blocks[Bsplit].state_index;
381 BlockLeft.level = lvl;
382 BlockLeft.parent_block_index = Bparent;
383 BlockLeft.transitions.swap(flagged_transitions);
384 BlockLeft.states.swap(flagged_states);
385 if (blocks[Bsplit].level == lvl)
386 {
387 BlockLeft.block_index = Bsplit;
388 BlockLeft.state_index = blocks[Bsplit].state_index;
389 blocks[Bsplit].swap(BlockLeft);
390 }
391 else
392 {
393 BlockLeft.block_index = blocks.size();
394 BlockLeft.state_index = max_state_index;
396 blocks.push_back(BlockLeft);
397 block_flags.push_back(false);
398 for (state_type s : BlockLeft.states)
399 {
400 block_index_of_a_state[s] = BlockLeft.block_index;
401 }
402 }
403
404 blocks[new_block1].transitions.swap(non_flagged_transitions);
405 reset_state_flags_block = BlockLeft.block_index;
406
407 if (BlockLeft.block_index != Bsplit)
408 {
409 std::vector<state_type>& reference_to_flagged_states_of_block2 = blocks.back().states;
410 for (std::vector<state_type>::const_iterator j = reference_to_flagged_states_of_block2.begin();
411 j != reference_to_flagged_states_of_block2.end();
412 ++j)
413 {
414 block_index_of_a_state[*j] = BlockLeft.block_index;
415 }
416 }
417 }
418 else
419 {
420 reset_state_flags_block = Bsplit;
421 blocks[Bsplit].states.swap(flagged_states);
422 }
423 // reset the state flags
424 std::vector<state_type>& flagged_states_to_be_unflagged = blocks[reset_state_flags_block].states;
425 for (state_type s : flagged_states_to_be_unflagged)
426 {
427 state_flags[s] = false;
428 }
429 BL.clear();
430 };
431 }
432
433 label_type label(observation_t obs) { return obs.first; }
434
435 block_index_type target(observation_t obs) { return obs.second; }
436
442 {
443 derivatives_t b2_delta;
444 observation_t dist_obs;
445
446 level_type lvl = gca_level(b1, b2);
447
448 for (observation_t obs : blocks[b2].outgoing_observations)
449 {
450 b2_delta.insert(std::make_pair(label(obs), lift_block(target(obs), lvl - 1)));
451 }
452
453 bool found_dist_obs = false;
454 for (observation_t obs : blocks[b1].outgoing_observations)
455 {
456 if (b2_delta.find(std::make_pair(label(obs), lift_block(target(obs), lvl - 1))) == b2_delta.end())
457 {
458 found_dist_obs = true;
459 dist_obs = obs;
460 break;
461 }
462 }
463
464 if (!found_dist_obs)
465 {
466 // Greedy strategy did not find negation free formula;
467 formula neg_phi = distinguish(b2, b1);
468 neg_phi.negated = true;
469 set_truths(neg_phi);
470 return neg_phi;
471 }
472
473 // Set of t derivates we need to take care of.
474 std::set<block_index_type> dT;
475 for (observation_t obs : blocks[b2].outgoing_observations)
476 {
477 if (label(obs) == label(dist_obs))
478 {
479 dT.insert(target(obs));
480 }
481 }
482 std::vector<formula> conjunctions;
483
484 while (!dT.empty())
485 {
486 level_type max_intersect = 0;
487 block_index_type splitBlock = *dT.begin();
488 for (block_index_type bid : dT)
489 {
490 if (gca_level(target(dist_obs), bid) > max_intersect)
491 {
492 splitBlock = bid;
493 max_intersect = gca_level(target(dist_obs), bid);
494 }
495 }
496 formula f = distinguish(target(dist_obs), splitBlock);
497 conjunctions.push_back(f);
498
499 std::set<block_index_type> dTleft;
500 std::set_intersection(dT.begin(),
501 dT.end(),
502 f.truths.begin(),
503 f.truths.end(),
504 std::inserter(dTleft, dTleft.begin()));
505 assert(dT.size() > dTleft.size());
506 dT.swap(dTleft);
507 }
508 formula returnf;
509 returnf.conjunctions.swap(conjunctions);
510 returnf.label = label(dist_obs);
511 returnf.negated = false;
512 set_truths(returnf);
513 return returnf;
514 }
515
519 {
520 block_index_type b1 = B1, b2 = B2;
521 if (B1 < B2)
522 {
523 b1 = B2;
524 b2 = B1;
525 }
526 std::pair<block_index_type, block_index_type> bpair(b1, b2);
527 if (greatest_common_ancestor.find(bpair) != greatest_common_ancestor.end())
528 {
529 return greatest_common_ancestor[bpair];
530 }
531 level_type lvl1 = blocks[b1].level, lvl2 = blocks[b2].level;
532 if (b1 == b2)
533 {
534 greatest_common_ancestor.emplace(bpair, lvl1);
535 return lvl1;
536 }
537 block_index_type B1parent = b1, B2parent = b2;
538
539 if (lvl1 <= lvl2)
540 {
541 B2parent = blocks[b2].parent_block_index;
542 }
543 if (lvl2 <= lvl1)
544 {
545 B1parent = blocks[b1].parent_block_index;
546 }
547 if (B1parent == B2parent)
548 {
549 lvl1 = blocks[b1].level;
550 }
551 else
552 {
553 lvl1 = gca_level(B1parent, B2parent);
554 }
555 greatest_common_ancestor.emplace(bpair, lvl1);
556 return lvl1;
557 }
558
560 {
561 block_index_type B = B1;
562 while (blocks[B].level > goal)
563 {
564 B = blocks[B].parent_block_index;
565 }
566 return B;
567 }
568
569 /*
570 * \brief Converts the private formula data type to the proper mCRL2 state_formula objects
571 * \param a formula f
572 * \return a state_formula equivalent to f
573 */
575 {
578
579 if (f.negated)
580 {
581 return mcrl2::state_formulas::not_(returnPhi);
582 }
583 return returnPhi;
584 }
585
591 mcrl2::state_formulas::state_formula conjunction(std::vector<formula>& conjunctions)
592 {
593 std::vector<mcrl2::state_formulas::state_formula> terms;
594 for (formula& f : conjunctions)
595 {
596 terms.push_back(convert_formula(f));
597 }
598 return utilities::detail::join<mcrl2::state_formulas::state_formula>(
599 terms.begin(),
600 terms.end(),
602 { return mcrl2::state_formulas::and_(a, b); },
604 }
605
613 {
616 }
617
625 {
627 }
628};
629
630template <class LTS_TYPE>
631bool destructive_bisimulation_compare_minimal_depth(LTS_TYPE& l1, LTS_TYPE& l2, const std::string& counter_example_file)
632{
633 std::size_t init_l2 = l2.initial_state() + l1.num_states();
635 l2.clear(); // No use for l2 anymore.
637 if (bisim_partitioner_minimal_depth.in_same_class(l1.initial_state(), init_l2))
638 {
639 return true;
640 }
641
642 // LTSs are not bisimilar, we can create a counter example.
643 std::string filename = "Counterexample.mcf";
644 if (!counter_example_file.empty())
645 {
646 filename = counter_example_file;
647 }
648
649 mcrl2::state_formulas::state_formula counter_example_formula
650 = bisim_partitioner_minimal_depth.dist_formula_mindepth(l1.initial_state(), init_l2);
651
652 std::ofstream counter_file(filename);
653 counter_file << mcrl2::state_formulas::pp(counter_example_formula);
654 counter_file.close();
655 mCRL2log(mcrl2::log::info) << "Saved counterexample to: \"" << filename << "\"" << std::endl;
656 return false;
657}
658
659} // namespace detail
660} // namespace lts
661} // namespace mcrl2
662#endif
A list of aterm objects.
Definition aterm_list.h:24
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
\brief The multi action for action formulas
const_iterator begin() const
\brief A timed multi-action
const process::action_list & actions() const
This class contains strings to be used as values for action labels in lts's.
void set_truths(formula &f)
Compute and set the truth values of a formula f.
std::pair< label_type, block_index_type > observation_t
level_type gca_level(const block_index_type B1, const block_index_type B2)
Auxiliarry function that computes the level of the greatest common ancestor. In other words a lvl i s...
regular_formulas::regular_formula create_regular_formula(const mcrl2::lts::action_label_string &a) const
create_regular_formula Creates a regular formula that represents action a
bisim_partitioner_minimal_depth(LTS_TYPE &l, const std::size_t init_l2)
Creates a bisimulation partitioner for an LTS.
mcrl2::state_formulas::state_formula dist_formula_mindepth(const std::size_t s, const std::size_t t)
Creates a state formula that distinguishes state s from state t.
formula distinguish(const block_index_type b1, const block_index_type b2)
Creates a formula that distinguishes a block b1 from the block b2.
~bisim_partitioner_minimal_depth()=default
Destroys this partitioner.
std::map< std::pair< block_index_type, block_index_type >, level_type > greatest_common_ancestor
regular_formulas::regular_formula create_regular_formula(const mcrl2::lps::multi_action &a) const
create_regular_formula Creates a regular formula that represents action a
bool in_same_class(const std::size_t s, const std::size_t t)
block_index_type lift_block(const block_index_type B1, level_type goal)
mcrl2::state_formulas::state_formula conjunction(std::vector< formula > &conjunctions)
conjunction Creates a conjunction of state formulas
mcrl2::state_formulas::state_formula convert_formula(formula &f)
void split_BL(level_type lvl)
Performs the splits based on the blocks in Bsplit and the flags set in state_flags.
A class containing triples, source label and target representing transitions.
Definition transition.h:43
size_type from() const
The source of the transition.
Definition transition.h:77
size_type label() const
The label of the transition.
Definition transition.h:83
\brief An action label
\brief The may operator for state formulas
\brief The not operator for state formulas
\brief The value true for state formulas
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
This file contains a class that contains labelled transition systems in aut format.
This file contains a class that contains labelled transition systems in dot format.
This file contains a class that contains labelled transition systems in fsm format.
This file contains some utility functions to manipulate lts's.
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
bool destructive_bisimulation_compare_minimal_depth(LTS_TYPE &l1, LTS_TYPE &l2, const std::string &counter_example_file)
void sort_transitions(std::vector< transition > &transitions, const std::set< transition::size_type > &hidden_label_set, transition_sort_style ts=src_lbl_tgt)
Sorts the transitions using a sort style.
void pp(const T &t, std::ostream &out)
Prints the object t to a stream.
Definition print.h:668
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
void swap(atermpp::unprotected_aterm_core &t1, atermpp::unprotected_aterm_core &t2) noexcept
Swaps two aterms.
Definition aterm.h:462
Add your file description here.
std::set< std::pair< label_type, block_index_type > > outgoing_observations