Line data Source code
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)
9 : /// \file lts/detail/liblts_bisim_m.h
10 : ///
11 : /// \brief Partition refinement algorithm for guaruanteed minimal depth
12 : /// counter-examples.
13 : ///
14 : /// \details
15 : #ifndef _LIBLTS_BISIM_M
16 : #define _LIBLTS_BISIM_M
17 :
18 : #include "mcrl2/lts/detail/liblts_merge.h"
19 : #include "mcrl2/lts/detail/liblts_scc.h"
20 : #include "mcrl2/lts/lts_aut.h"
21 : #include "mcrl2/lts/lts_dot.h"
22 : #include "mcrl2/lts/lts_fsm.h"
23 : #include "mcrl2/lts/lts_utilities.h"
24 : #include "mcrl2/modal_formula/state_formula.h"
25 : #include <fstream>
26 :
27 : namespace mcrl2
28 : {
29 : namespace lts
30 : {
31 : namespace detail
32 : {
33 : template <class LTS_TYPE>
34 : class bisim_partitioner_minimal_depth
35 : {
36 : public:
37 : /** \brief Creates a bisimulation partitioner for an LTS.
38 : * \details This partitioner is specifically for creating minimal depth counter-examples for strong bisimulation.
39 : * It guarantees stability w.r.t. the old partition before consideren new splitter blocks. This might cause
40 : * this implementation to be less efficient than other partitioners. \param l Reference to the LTS. \param init_l2
41 : * reference to the initial state of lts2. */
42 1 : bisim_partitioner_minimal_depth(LTS_TYPE &l, const std::size_t init_l2)
43 1 : : initial_l2(init_l2),
44 1 : max_state_index(0),
45 1 : aut(l)
46 : {
47 1 : to_be_processed.clear();
48 1 : block initial_block = block();
49 5 : for (state_type i = 0; i < aut.num_states(); i++)
50 : {
51 4 : initial_block.states.push_back(i);
52 : }
53 1 : sort_transitions(aut.get_transitions(), mcrl2::lts::lbl_tgt_src);
54 1 : const std::vector<transition> &trans = aut.get_transitions();
55 3 : for (std::vector<transition>::const_iterator r = trans.begin(); r != trans.end(); ++r)
56 : {
57 2 : initial_block.transitions.push_back(*r);
58 : }
59 1 : initial_block.block_index = 0;
60 1 : initial_block.state_index = 0;
61 1 : max_state_index = 1;
62 1 : initial_block.parent_block_index = 0;
63 1 : initial_block.level = 0;
64 1 : blocks.emplace_back(initial_block);
65 :
66 1 : block_index_of_a_state = std::vector<block_index_type>(aut.num_states(), 0);
67 1 : block_flags.push_back(false);
68 1 : state_flags = std::vector<bool>(aut.num_states(), false);
69 1 : to_be_processed.push_back(0);
70 1 : BL.clear();
71 : // finished creating initial data structures
72 :
73 1 : bool splitted = true;
74 1 : level_type lvl = 1;
75 2 : while (splitted && block_index_of_a_state[initial_l2] == block_index_of_a_state[aut.initial_state()])
76 : {
77 1 : splitted = refine_partition(lvl);
78 1 : lvl++;
79 1 : for (typename std::vector<block>::reverse_iterator i = blocks.rbegin();
80 4 : i != blocks.rend() && (*i).level == lvl - 1;
81 3 : ++i)
82 : {
83 3 : to_be_processed.push_back((*i).block_index);
84 : }
85 : }
86 :
87 5 : for (state_type i = 0; i < aut.num_states(); i++)
88 : {
89 4 : block_index_type bid = block_index_of_a_state[i];
90 4 : if (!block_flags[bid])
91 : {
92 3 : block_flags[bid] = true;
93 3 : partition.insert(bid);
94 : }
95 : }
96 2 : mCRL2log(mcrl2::log::info) << "Partition refinement done, partition contains: " << partition.size()
97 1 : << " blocks, the history contains " << lvl - 1 << " levels." << std::endl;
98 1 : save_transitions();
99 1 : }
100 :
101 : /** \brief Destroys this partitioner. */
102 1 : ~bisim_partitioner_minimal_depth() = default;
103 :
104 : /** \brief Creates a state formula that distinguishes state s from state t.
105 : * \details The states s and t are non bisimilar states. A distinguishign state formula phi is
106 : * returned, which has the property that s \in \sem{phi} and t \not\in\sem{phi}.
107 : * Based on the preprint "Computing minimal distinguishing Hennessey-Milner formulas is NP-hard
108 : * . But variants are tractable", 2023 by Jan Martens and Jan Friso Groote
109 : * \param[in] s The state number for which the resulting formula should be true
110 : * \param[in] t The state number for which the resulting formula should be false
111 : * \return A minimal observation depth distinguishing state formula, that is often also minimum negation-depth and
112 : * irreducible. */
113 1 : mcrl2::state_formulas::state_formula dist_formula_mindepth(const std::size_t s, const std::size_t t)
114 : {
115 1 : formula f = distinguish(block_index_of_a_state[s], block_index_of_a_state[t]);
116 1 : mCRL2log(mcrl2::log::info) << "done with formula \n";
117 2 : return convert_formula(f);
118 1 : };
119 :
120 1 : bool in_same_class(const std::size_t s, const std::size_t t)
121 : {
122 1 : return block_index_of_a_state[s] == block_index_of_a_state[t];
123 : }
124 :
125 :
126 : private:
127 : typedef std::size_t block_index_type;
128 : typedef std::size_t state_type;
129 : typedef std::size_t level_type;
130 : typedef std::size_t formula_index_type;
131 : typedef std::size_t label_type;
132 : state_type initial_l2;
133 :
134 : state_type max_state_index;
135 : LTS_TYPE &aut;
136 : std::set<block_index_type> partition;
137 :
138 : struct block
139 : {
140 : state_type state_index; // The state number that represent the states in this block
141 : block_index_type block_index; // The sequence number of this block.
142 : block_index_type parent_block_index; // Index of the parent block.
143 : level_type level;
144 :
145 : // If there is no parent block, this refers to the block itself.
146 : std::vector<state_type> states;
147 : std::vector<transition> transitions;
148 : std::set<std::pair<label_type, block_index_type>> outgoing_observations;
149 :
150 1 : void swap(block &b)
151 : {
152 1 : std::swap(b.state_index, state_index);
153 1 : std::swap(b.block_index, block_index);
154 1 : std::swap(b.parent_block_index, parent_block_index);
155 1 : std::swap(b.level, level);
156 1 : states.swap(b.states);
157 1 : transitions.swap(b.transitions);
158 1 : }
159 : };
160 :
161 : struct formula
162 : {
163 : formula_index_type index;
164 : label_type label;
165 : bool negated;
166 : std::vector<formula> conjunctions;
167 : std::set<block_index_type> truths;
168 :
169 : int depth()
170 : {
171 : int max_depth = 0;
172 : for (formula f : conjunctions)
173 : {
174 : max_depth = std::max(max_depth, f.depth() + 1);
175 : }
176 : return max_depth;
177 : }
178 : };
179 :
180 : std::vector<block> blocks;
181 : // Blocks that are split become inactive.
182 : std::vector<state_type> block_index_of_a_state;
183 : std::vector<bool> block_flags;
184 : std::vector<bool> state_flags;
185 :
186 : std::vector<block_index_type> to_be_processed;
187 : std::vector<block_index_type> BL;
188 : typedef std::pair<label_type, block_index_type> observation_t;
189 : typedef std::set<observation_t> derivatives_t;
190 : std::map<std::pair<block_index_type, block_index_type>, level_type> greatest_common_ancestor;
191 :
192 : /* Post processes the partition structure to save outgoing transitions per block */
193 1 : void save_transitions()
194 : {
195 3 : for (transition t : aut.get_transitions())
196 : {
197 2 : block_index_type sourceBlock = block_index_of_a_state[t.from()];
198 2 : block_index_type targetBlock = block_index_of_a_state[t.to()];
199 :
200 2 : blocks[sourceBlock].outgoing_observations.insert(std::make_pair(t.label(), targetBlock));
201 : }
202 1 : }
203 :
204 : /** \brief Compute and set the truth values of a formula f.
205 : * \details Given the formula f we compute the subset of blocks in which f is true.
206 : * the truthvalues are computed based on the truth values of the different conjuncts and
207 : * the modality which consists of the label and being negated or not. */
208 1 : void set_truths(formula &f)
209 : {
210 1 : std::set<block_index_type> image_truths;
211 1 : std::set<block_index_type> pre_image_truths;
212 1 : std::set<block_index_type> intersection;
213 :
214 1 : image_truths = std::set(partition);
215 :
216 1 : for (formula df : f.conjunctions)
217 : {
218 0 : std::set_intersection(image_truths.begin(),
219 : image_truths.end(),
220 : df.truths.begin(),
221 : df.truths.end(),
222 : std::inserter(intersection, intersection.begin()));
223 0 : image_truths.swap(intersection);
224 0 : intersection.clear();
225 : }
226 :
227 : // Now compute preimage according to label
228 4 : for (block_index_type B : image_truths)
229 : {
230 5 : for (transition t : blocks[B].transitions)
231 : {
232 2 : if (t.label() == f.label && (pre_image_truths.find(block_index_of_a_state[t.from()]) == pre_image_truths.end()))
233 : {
234 1 : pre_image_truths.insert(block_index_of_a_state[t.from()]);
235 : }
236 : }
237 : }
238 :
239 1 : if (f.negated)
240 : {
241 0 : image_truths.swap(pre_image_truths);
242 0 : pre_image_truths.clear();
243 0 : std::set_difference(partition.begin(),
244 : partition.end(),
245 : image_truths.begin(),
246 : image_truths.end(),
247 : std::inserter(pre_image_truths, pre_image_truths.begin()));
248 : }
249 1 : f.truths.swap(pre_image_truths);
250 1 : }
251 :
252 : // Refine the partition to a certain lvl.
253 1 : bool refine_partition(level_type lvl)
254 : {
255 1 : if (to_be_processed.empty())
256 : {
257 0 : return false;
258 : }
259 : block_index_type splitter_index;
260 3 : while (!to_be_processed.empty())
261 : {
262 1 : splitter_index = to_be_processed.front();
263 :
264 1 : to_be_processed.erase(to_be_processed.begin());
265 1 : if (blocks[splitter_index].level == lvl)
266 : {
267 0 : return true;
268 : }
269 :
270 1 : std::vector<transition> transitions_to_process;
271 1 : transitions_to_process = blocks[splitter_index].transitions;
272 1 : for (std::vector<transition>::const_iterator i = transitions_to_process.begin();
273 3 : i != transitions_to_process.end();
274 2 : ++i)
275 : {
276 2 : transition t = *i;
277 2 : state_flags[t.from()] = true;
278 2 : const block_index_type marked_block_index = block_index_of_a_state[t.from()];
279 2 : if (block_flags[marked_block_index] == false)
280 : {
281 2 : block_flags[marked_block_index] = true;
282 2 : BL.push_back(marked_block_index);
283 : }
284 : // If the label of the next action is different, we must carry out the splitting.
285 4 : if ((i != transitions_to_process.end() && next(i) == transitions_to_process.end())
286 4 : || t.label() != (*next(i)).label())
287 : {
288 2 : split_BL(lvl);
289 2 : BL.clear();
290 : }
291 : }
292 : }
293 1 : return true;
294 : }
295 :
296 : /** \brief Performs the splits based on the blocks in Bsplit and the flags set in state_flags. */
297 2 : void split_BL(level_type lvl)
298 : {
299 4 : for (block_index_type Bsplit : BL)
300 : {
301 2 : block_flags[Bsplit] = false;
302 2 : std::vector<state_type> flagged_states;
303 2 : std::vector<state_type> non_flagged_states;
304 2 : std::vector<state_type> Bsplit_states;
305 2 : Bsplit_states.swap(blocks[Bsplit].states);
306 9 : for (state_type s : Bsplit_states)
307 : {
308 7 : if (state_flags[s])
309 : {
310 : // state is flagged.
311 2 : flagged_states.push_back(s);
312 : }
313 : else
314 : {
315 : // state is not flagged. It will be moved to a new block.
316 5 : non_flagged_states.push_back(s);
317 5 : block_index_of_a_state[s] = blocks.size();
318 : }
319 : }
320 2 : block_index_type Bparent = Bsplit;
321 : // Set the correct parent
322 3 : while (blocks[Bparent].level == lvl)
323 : {
324 1 : Bparent = blocks[Bparent].parent_block_index;
325 : }
326 :
327 2 : block_index_type reset_state_flags_block = Bsplit;
328 2 : if (!non_flagged_states.empty())
329 : {
330 : // There are flagged and non flagged states. So, the block must be split.
331 : // Move the unflagged states to the new block.
332 2 : if (mCRL2logEnabled(log::debug))
333 : {
334 0 : const std::size_t m = static_cast<std::size_t>(
335 0 : std::pow(10.0, std::floor(std::log10(static_cast<double>((blocks.size() + 1) / 2)))));
336 0 : if ((blocks.size() + 1) / 2 % m == 0)
337 : {
338 0 : mCRL2log(log::debug) << "Bisimulation partitioner: create block " << (blocks.size() + 1) / 2 << std::endl;
339 : }
340 : }
341 : // Create a first new block.
342 2 : blocks.push_back(block());
343 2 : block_index_type new_block1 = blocks.size() - 1;
344 2 : blocks.back().state_index = max_state_index;
345 2 : max_state_index++;
346 2 : blocks.back().block_index = new_block1;
347 2 : blocks.back().level = lvl;
348 :
349 2 : blocks.back().parent_block_index = Bparent;
350 2 : non_flagged_states.swap(blocks.back().states);
351 :
352 : // The flag fields of the new blocks is set to false;
353 2 : block_flags.push_back(false);
354 : // distribute the transitions
355 : // Finally the non-inert transitions are distributed over both blocks in the obvious way.
356 : // Note that this must be done after all states are properly put into a new block.
357 2 : std::vector<transition> old_transitions;
358 2 : std::vector<transition> flagged_transitions;
359 2 : std::vector<transition> non_flagged_transitions;
360 :
361 2 : old_transitions = blocks[Bsplit].transitions;
362 6 : for (std::vector<transition>::iterator k = old_transitions.begin(); k != old_transitions.end(); ++k)
363 : {
364 4 : if (state_flags[(*k).to()])
365 : {
366 0 : flagged_transitions.push_back(*k);
367 : }
368 : else
369 : {
370 4 : non_flagged_transitions.push_back(*k);
371 : }
372 : }
373 :
374 : // Create a second new block.
375 2 : block BlockLeft = block();
376 :
377 : // block_is_active.push_back(true);
378 2 : BlockLeft.state_index = blocks[Bsplit].state_index;
379 2 : BlockLeft.level = lvl;
380 2 : BlockLeft.parent_block_index = Bparent;
381 2 : BlockLeft.transitions.swap(flagged_transitions);
382 2 : BlockLeft.states.swap(flagged_states);
383 2 : if (blocks[Bsplit].level == lvl)
384 : {
385 1 : BlockLeft.block_index = Bsplit;
386 1 : BlockLeft.state_index = blocks[Bsplit].state_index;
387 1 : blocks[Bsplit].swap(BlockLeft);
388 : }
389 : else
390 : {
391 1 : BlockLeft.block_index = blocks.size();
392 1 : BlockLeft.state_index = max_state_index;
393 1 : max_state_index++;
394 1 : blocks.push_back(BlockLeft);
395 1 : block_flags.push_back(false);
396 2 : for (state_type s : BlockLeft.states)
397 : {
398 1 : block_index_of_a_state[s] = BlockLeft.block_index;
399 : }
400 : }
401 :
402 2 : blocks[new_block1].transitions.swap(non_flagged_transitions);
403 2 : reset_state_flags_block = BlockLeft.block_index;
404 :
405 2 : if (BlockLeft.block_index != Bsplit)
406 : {
407 1 : std::vector<state_type> &reference_to_flagged_states_of_block2 = blocks.back().states;
408 1 : for (std::vector<state_type>::const_iterator j = reference_to_flagged_states_of_block2.begin();
409 2 : j != reference_to_flagged_states_of_block2.end();
410 1 : ++j)
411 : {
412 1 : block_index_of_a_state[*j] = BlockLeft.block_index;
413 : }
414 : }
415 2 : }
416 : else
417 : {
418 0 : reset_state_flags_block = Bsplit;
419 0 : blocks[Bsplit].states.swap(flagged_states);
420 : }
421 : // reset the state flags
422 2 : std::vector<state_type> &flagged_states_to_be_unflagged = blocks[reset_state_flags_block].states;
423 4 : for (state_type s : flagged_states_to_be_unflagged)
424 : {
425 2 : state_flags[s] = false;
426 : }
427 2 : BL.clear();
428 : };
429 2 : }
430 :
431 5 : label_type label(observation_t obs) { return obs.first; }
432 :
433 2 : block_index_type target(observation_t obs) { return obs.second; }
434 :
435 : /** \brief Creates a formula that distinguishes a block b1 from the block b2.
436 : * \details creates a minimal depth formula that distinguishes b1 and b2.
437 : * \return A minimal observation depth distinguishing state formula, that is often also minimum negation-depth and
438 : * irreducible. */
439 1 : formula distinguish(const block_index_type b1, const block_index_type b2)
440 : {
441 1 : derivatives_t b2_delta;
442 1 : observation_t dist_obs;
443 :
444 1 : level_type lvl = gca_level(b1, b2);
445 :
446 2 : for (observation_t obs : blocks[b2].outgoing_observations)
447 : {
448 1 : b2_delta.insert(std::make_pair(label(obs), lift_block(target(obs), lvl - 1)));
449 : }
450 :
451 1 : bool found_dist_obs = false;
452 1 : for (observation_t obs : blocks[b1].outgoing_observations)
453 : {
454 1 : if (b2_delta.find(std::make_pair(label(obs), lift_block(target(obs), lvl - 1))) == b2_delta.end())
455 : {
456 1 : found_dist_obs = true;
457 1 : dist_obs = obs;
458 1 : break;
459 : }
460 : }
461 :
462 1 : if (!found_dist_obs)
463 : {
464 : // Greedy strategy did not find negation free formula;
465 0 : formula neg_phi = distinguish(b2, b1);
466 0 : neg_phi.negated = true;
467 0 : set_truths(neg_phi);
468 0 : return neg_phi;
469 0 : }
470 :
471 : // Set of t derivates we need to take care of.
472 1 : std::set<block_index_type> dT;
473 2 : for (observation_t obs : blocks[b2].outgoing_observations)
474 : {
475 1 : if (label(obs) == label(dist_obs))
476 : {
477 0 : dT.insert(target(obs));
478 : }
479 : }
480 1 : std::vector<formula> conjunctions;
481 :
482 1 : while (!dT.empty())
483 : {
484 0 : level_type max_intersect = 0;
485 0 : block_index_type splitBlock = *dT.begin();
486 0 : for (block_index_type bid : dT)
487 : {
488 0 : if (gca_level(target(dist_obs), bid) > max_intersect)
489 : {
490 0 : splitBlock = bid;
491 0 : max_intersect = gca_level(target(dist_obs), bid);
492 : }
493 : }
494 0 : formula f = distinguish(target(dist_obs), splitBlock);
495 0 : conjunctions.push_back(f);
496 :
497 0 : std::set<block_index_type> dTleft;
498 0 : std::set_intersection(dT.begin(),
499 : dT.end(),
500 : f.truths.begin(),
501 : f.truths.end(),
502 : std::inserter(dTleft, dTleft.begin()));
503 0 : assert(dT.size() > dTleft.size());
504 0 : dT.swap(dTleft);
505 : }
506 1 : formula returnf;
507 1 : returnf.conjunctions.swap(conjunctions);
508 1 : returnf.label = label(dist_obs);
509 1 : returnf.negated = false;
510 1 : set_truths(returnf);
511 1 : return returnf;
512 1 : }
513 :
514 : /** \brief Auxiliarry function that computes the level of the greatest common ancestor.
515 : * In other words a lvl i such that B1 and B2 are i-bisimilar. */
516 1 : level_type gca_level(const block_index_type B1, const block_index_type B2)
517 : {
518 1 : block_index_type b1 = B1, b2 = B2;
519 1 : if (B1 < B2)
520 : {
521 0 : b1 = B2;
522 0 : b2 = B1;
523 : }
524 1 : std::pair<block_index_type, block_index_type> bpair(b1, b2);
525 1 : if (greatest_common_ancestor.find(bpair) != greatest_common_ancestor.end())
526 : {
527 0 : return greatest_common_ancestor[bpair];
528 : }
529 1 : level_type lvl1 = blocks[b1].level, lvl2 = blocks[b2].level;
530 1 : if (b1 == b2)
531 : {
532 0 : greatest_common_ancestor.emplace(bpair, lvl1);
533 0 : return lvl1;
534 : }
535 1 : block_index_type B1parent = b1, B2parent = b2;
536 :
537 1 : if (lvl1 <= lvl2)
538 : {
539 1 : B2parent = blocks[b2].parent_block_index;
540 : }
541 1 : if (lvl2 <= lvl1)
542 : {
543 1 : B1parent = blocks[b1].parent_block_index;
544 : }
545 1 : if (B1parent == B2parent)
546 : {
547 1 : lvl1 = blocks[b1].level;
548 : }
549 : else
550 : {
551 0 : lvl1 = gca_level(B1parent, B2parent);
552 : }
553 1 : greatest_common_ancestor.emplace(bpair, lvl1);
554 1 : return lvl1;
555 : }
556 :
557 2 : block_index_type lift_block(const block_index_type B1, level_type goal)
558 : {
559 2 : block_index_type B = B1;
560 4 : while (blocks[B].level > goal)
561 : {
562 2 : B = blocks[B].parent_block_index;
563 : }
564 2 : return B;
565 : }
566 :
567 : /*
568 : * \brief Converts the private formula data type to the proper mCRL2 state_formula objects
569 : * \param a formula f
570 : * \return a state_formula equivalent to f
571 : */
572 1 : mcrl2::state_formulas::state_formula convert_formula(formula &f)
573 : {
574 1 : mcrl2::state_formulas::state_formula returnPhi
575 2 : = mcrl2::state_formulas::may(create_regular_formula(aut.action_label(f.label)), conjunction(f.conjunctions));
576 :
577 1 : if (f.negated)
578 : {
579 0 : return mcrl2::state_formulas::not_(returnPhi);
580 : }
581 1 : return returnPhi;
582 1 : }
583 :
584 : /**
585 : * \brief conjunction Creates a conjunction of state formulas
586 : * \param terms The terms of the conjunction
587 : * \return The conjunctive state formula
588 : */
589 1 : mcrl2::state_formulas::state_formula conjunction(std::vector<formula> &conjunctions)
590 : {
591 1 : std::vector<mcrl2::state_formulas::state_formula> terms;
592 1 : for (formula &f : conjunctions)
593 : {
594 0 : terms.push_back(convert_formula(f));
595 : }
596 : return utilities::detail::join<mcrl2::state_formulas::state_formula>(
597 : terms.begin(),
598 : terms.end(),
599 0 : [](mcrl2::state_formulas::state_formula a, mcrl2::state_formulas::state_formula b)
600 0 : { return mcrl2::state_formulas::and_(a, b); },
601 2 : mcrl2::state_formulas::true_());
602 1 : }
603 :
604 : /**
605 : * \brief create_regular_formula Creates a regular formula that represents action a
606 : * \details In case the action comes from an LTS in the aut or fsm format.
607 : * \param a The action for which to create a regular formula
608 : * \return The created regular formula
609 : */
610 1 : regular_formulas::regular_formula create_regular_formula(const mcrl2::lts::action_label_string &a) const
611 : {
612 2 : return mcrl2::regular_formulas::regular_formula(mcrl2::action_formulas::multi_action(
613 4 : process::action_list({process::action(process::action_label(a, {}), {})})));
614 : }
615 :
616 : /**
617 : * \brief create_regular_formula Creates a regular formula that represents action a
618 : * \details In case the action comes from an LTS in the lts format.
619 : * \param a The action for which to create a regular formula
620 : * \return The created regular formula
621 : */
622 : regular_formulas::regular_formula create_regular_formula(const mcrl2::lps::multi_action &a) const
623 : {
624 : return regular_formulas::regular_formula(action_formulas::multi_action(a.actions()));
625 : }
626 : };
627 :
628 : template < class LTS_TYPE>
629 1 : bool destructive_bisimulation_compare_minimal_depth(
630 : LTS_TYPE & l1,
631 : LTS_TYPE & l2,
632 : const std::string & counter_example_file)
633 : {
634 1 : std::size_t init_l2 = l2.initial_state() + l1.num_states();
635 1 : mcrl2::lts::detail::merge(l1, l2);
636 1 : l2.clear(); // No use for l2 anymore.
637 1 : detail::bisim_partitioner_minimal_depth<LTS_TYPE> bisim_partitioner_minimal_depth(l1, init_l2);
638 1 : if (bisim_partitioner_minimal_depth.in_same_class(l1.initial_state(), init_l2))
639 : {
640 0 : return true;
641 : }
642 :
643 : // LTSs are not bisimilar, we can create a counter example.
644 1 : std::string filename = "Counterexample.mcf";
645 1 : if (!counter_example_file.empty()) {
646 0 : filename = counter_example_file;
647 : }
648 :
649 1 : mcrl2::state_formulas::state_formula counter_example_formula = bisim_partitioner_minimal_depth.dist_formula_mindepth(l1.initial_state(), init_l2);
650 :
651 1 : std::ofstream counter_file(filename);
652 1 : counter_file << mcrl2::state_formulas::pp(counter_example_formula);
653 1 : counter_file.close();
654 1 : mCRL2log(mcrl2::log::info) << "Saved counterexample to: \"" << filename << "\"" << std::endl;
655 1 : return false;
656 1 : }
657 :
658 :
659 : } // namespace detail
660 : } // namespace lts
661 : } // namespace mcrl2
662 : #endif
|
