mCRL2
Loading...
Searching...
No Matches
liblts_branching_bisim_minimal_depth.h
Go to the documentation of this file.
1// Author(s): Jan Martens and Maurice Laveaux
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 MCRl2_LTS_LIBLTS_BRANCHING_BISIM_MINIMAL_DEPTH
16#define MCRl2_LTS_LIBLTS_BRANCHING_BISIM_MINIMAL_DEPTH
17
18
22#include "mcrl2/lts/lts_aut.h"
23#include "mcrl2/lts/lts_dot.h"
24#include "mcrl2/lts/lts_fsm.h"
27
28#include <fstream>
29
30namespace mcrl2::lts::detail
31{
32
33template <class LTS_TYPE>
35{
36public:
44 branching_bisim_partitioner_minimal_depth(LTS_TYPE& l, const std::size_t init_l2)
45 : m_lts(l),
46 initial_l2(init_l2)
47 {
48
49 for (transition trans : m_lts.get_transitions())
50 {
51 trans_out[trans.from()].push_back(std::make_pair(trans.label(), trans.to()));
52 if (is_tau(trans.label()))
53 {
54 silent_out[trans.from()].insert(trans.to());
55 silent_in[trans.to()].insert(trans.from());
56 }
57 }
58
59 for (state_type s = 0; s < m_lts.num_states(); s++)
60 {
61 state2block[s] = 0;
62
63 if (silent_out[s].size() == 0)
64 {
65 bottom_states.push_back(s);
66 }
67 }
68
69
70
71 // Initialize the partition with a single block.
72 blocks.push_back(block());
73 blocks[0].state_index = 0;
74 blocks[0].block_index = 0;
75 blocks[0].parent_block_index = 0;
76 blocks[0].level = 0;
77 level2blocksidx[0].insert(0);
78
79 // Now we can start refining the partition.
80 std::size_t num_old_blocks = 0;
81 std::size_t num_blocks_created = 1;
82 std::size_t level = 0;
83
84 while (num_blocks_created > num_old_blocks && in_same_class(m_lts.initial_state(), initial_l2))
85 {
86 level += 1;
87 num_old_blocks = num_blocks_created;
88 num_blocks_created = refine_partition();
89 assert(level2blocksidx[level].size() == num_blocks_created);
90 state2sig = std::map<state_type, signature_type>();
91 mCRL2log(mcrl2::log::verbose) << "Refined partition to " << num_blocks_created
92 << " blocks on level " << level << "."
93 << std::endl;
94 }
95 }
96
107 {
108 assert(s == m_lts.initial_state() && t == initial_l2);
109 assert(state2block[s] != state2block[t]);
110 std::pair<block_index_type, block_index_type> b1b2 = min_split_blockpair(state2block[s], state2block[t]);
111 return dist_formula(b1b2.first, b1b2.second);
112 }
113
114 bool in_same_class(const std::size_t s, const std::size_t t) { return state2block[s] == state2block[t]; }
115
116
117private:
118 LTS_TYPE& m_lts;
121 typedef std::size_t block_index_type;
122 typedef std::size_t level_type;
123 // This tuple is meant for an observation (s', a, s'') such that s -(silent)-> s' -a-> s''.
124 typedef std::tuple<block_index_type, label_type, block_index_type> branching_observation_type;
125 typedef std::set<branching_observation_type> signature_type;
126 typedef std::pair<label_type, state_type> observation;
127 typedef std::pair<block_index_type, block_index_type> blockpair_type;
128
129 std::map<state_type, std::set<state_type>> silent_in;
130 std::map<state_type, std::set<state_type>> silent_out;
131 std::map<state_type, std::vector<observation>> trans_out;
132 std::map<state_type, std::size_t> state2num_touched;
133 std::map<state_type, block_index_type> state2block;
134 std::map<state_type, signature_type> state2sig;
135 std::vector<state_type> bottom_states;
136 std::map<level_type, std::set<block_index_type>> level2blocksidx;
137
138 std::map<std::pair<block_index_type, block_index_type>, mcrl2::state_formulas::state_formula> blockpair2formula;
139 std::map<std::pair<block_index_type, block_index_type>, std::set<block_index_type>> blockpair2truths;
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. If there is no parent block, this refers to the block itself.
146 level_type level; // The level of the block in the partition.
148
149 void swap(block& b)
150 {
155 }
156
157 bool operator==(const block& other)
158 {
159 return block_index == other.block_index;
160 }
161
162 bool operator!=(const block& other)
163 {
164 return !(*this == other);
165 }
166 };
167 std::vector<block> blocks;
168
169 /*
170 * Auxiliary function that computes whether a label is a tau index.
171 */
173 {
174 return m_lts.is_tau(m_lts.apply_hidden_label_map(l));
175 }
176
178 {
179 signature_type sig;
180 // Add the block index of the state to the signature.
181 sig.insert(std::make_tuple(state2block[s], m_lts.tau_label_index(), state2block[s]));
182 for (state_type target : silent_out[s])
183 {
184 sig.insert(state2sig[target].begin(), state2sig[target].end());
185 }
186 for (observation t : trans_out[s])
187 {
188 if (!is_tau(t.first) || state2block[s] != state2block[t.second])
189 {
190 sig.insert(std::make_tuple(state2block[s], t.first, state2block[t.second]));
191 }
192 }
193
194 state2sig[s] = sig;
195 return sig;
196 }
197
198 // Refine the partition exactly one level.
199 std::size_t refine_partition()
200 {
201 std::queue<state_type> frontier;
202 // start with bottom states.
203 for (auto s : bottom_states)
204 {
205 frontier.push(s);
206 }
207 std::map<signature_type, block_index_type> sig2block;
208 std::map<state_type, block_index_type> state2block_new;
209 std::size_t num_blocks_created = 0;
210 // Compute signatures in order of bottom states and reachability order.
211 while (!frontier.empty())
212 {
213 state_type state = frontier.front();
214 frontier.pop();
216 if (sig2block.find(sig) == sig2block.end())
217 {
218 // Create the new block
219 blocks.push_back(block());
220 num_blocks_created += 1;
221 block_index_type new_block_id = blocks.size() - 1;
222 sig2block[sig] = new_block_id;
223 blocks[new_block_id].state_index = state;
224 blocks[new_block_id].block_index = new_block_id;
225 blocks[new_block_id].parent_block_index = state2block[state];
226 blocks[new_block_id].level = blocks[state2block[state]].level + 1;
227 blocks[new_block_id].sig = sig;
228 level2blocksidx[blocks[new_block_id].level].insert(new_block_id);
229 }
230
231 state2block_new[state] = sig2block[sig];
233
234 for (state_type backward : silent_in[state])
235 {
236 size_t max_out = silent_out[backward].size();
237 state2num_touched[backward] += 1;
238 if (state2num_touched[backward] == max_out)
239 {
240 frontier.push(backward);
241 }
242 }
243 }
244 // Now we have computed the new blocks, we can redefine the partition.
245 state2block = state2block_new;
246 return num_blocks_created;
247 }
248
249 std::pair<block_index_type, block_index_type> min_split_blockpair(block_index_type b1, block_index_type b2)
250 {
251 assert(blocks[b1] != blocks[b2] && blocks[b1].level == blocks[b2].level);
252 while (blocks[b1].parent_block_index != blocks[b2].parent_block_index)
253 {
254 b1 = blocks[b1].parent_block_index;
255 b2 = blocks[b2].parent_block_index;
256 }
257 return std::make_pair(b1, b2);
258 }
259
265 mcrl2::state_formulas::state_formula conjunction(std::vector<mcrl2::state_formulas::state_formula>& conjunctions)
266 {
267 return utilities::detail::join<mcrl2::state_formulas::state_formula>(
268 conjunctions.begin(),
269 conjunctions.end(),
271 { return mcrl2::state_formulas::and_(a, b); },
273 }
274
276 {
277 return regular_formulas::alt(f,
279 }
280
288 {
289 // Copied from Olav no idea what it exactly does.
292 }
293
301 {
303 }
304
305 // Updates the truths values according the dist formula and the information in blockpair2truths.
306 void split_and_intersect(std::set<block_index_type>& truths, std::pair<block_index_type, block_index_type> liftedB1B2)
307 {
308 // Add the observation to the formula
309 level_type split_level = blocks[liftedB1B2.first].level;
310
311 std::set<block_index_type> truths_new;
312 for (block_index_type b_og : truths)
313 {
314 block_index_type b = b_og;
315 // Check if b in phi (maybe lift the level)
316 while (blocks[b].level > split_level)
317 {
318 b = blocks[b].parent_block_index;
319 }
320 if (blockpair2truths[liftedB1B2].find(b) != blockpair2truths[liftedB1B2].end())
321 {
322 truths_new.insert(b_og);
323 }
324 }
325 truths = truths_new;
326 }
327
335 bool is_dist(std::set<blockpair_type>& dist_blockpairs,
336 std::set<block_index_type>& to_dist)
337 {
338 if (to_dist.empty())
339 {
340 return true;
341 }
342 std::set<block_index_type> truths = level2blocksidx[blocks[*to_dist.begin()].level];
343 return is_dist(dist_blockpairs, to_dist, truths);
344 }
345
346
350 bool is_dist(const std::set<blockpair_type>& dist_blockpairs,const std::set<block_index_type>& to_dist, std::set<block_index_type>& truths)
351 {
352 if (to_dist.empty())
353 {
354 return true;
355 }
356
357 truths = level2blocksidx[blocks[*to_dist.begin()].level];
358 for (blockpair_type b1_b2 : dist_blockpairs)
359 {
360 split_and_intersect(truths, b1_b2);
361 }
362 for (block_index_type b : to_dist)
363 {
364 if (truths.find(b) != truths.end())
365 {
366 return false;
367 }
368 }
369 return true;
370 }
371
372
373 std::vector<mcrl2::state_formulas::state_formula> filtered_dist_conjunction(
374 std::map<blockpair_type, mcrl2::state_formulas::state_formula>& Phi,
375 std::set<block_index_type>& Tdist,
376 std::set<block_index_type>& Truths)
377 {
378 std::vector<mcrl2::state_formulas::state_formula> returnPhi;
379 std::set<blockpair_type> phi_pairs_og;
380 for (auto& phi_pair : Phi) {
381 phi_pairs_og.insert(phi_pair.first);
382 }
383
384 for (auto& phi_pair : Phi) {
385 // Remove the phi_pair from the formula.
386 phi_pairs_og.erase(phi_pair.first);
387 // Only add conjunct, if it wouldn't be distinguishing without.
388 if (!is_dist(phi_pairs_og, Tdist))
389 {
390 phi_pairs_og.insert(phi_pair.first);
391 returnPhi.push_back(phi_pair.second);
392 }
393 }
394 is_dist(phi_pairs_og, Tdist, Truths);
395
396 return returnPhi;
397 }
398
399 // This function computes the distinguishing state formula for two blocks.
400 // Precondition is that the blocks are not the same, are on the same level and have the same parent block.
402 {
403 assert(block_index1 != block_index2);
404 if (blockpair2formula.find(std::make_pair(block_index1, block_index2)) != blockpair2formula.end())
405 {
406 // We computed this already ( probably won't happen much in practice but guarantees polynomial runtime).
407 return blockpair2formula[std::make_pair(block_index1, block_index2)];
408 }
409
410 block block1 = blocks[block_index1];
411 block block2 = blocks[block_index2];
412
413 // make blocks same level
414 assert(block1.level == block2.level); // This should be true, otherwise need to make them same level.
415 assert(block1.parent_block_index == block2.parent_block_index); // This should be true, otherwise need to make them same level.)
416
417 signature_type ds = block1.sig;
418 signature_type dt = block2.sig;
419
420 // Find a distinguishing observation s- tau ->> s' -a-> s''
421 std::tuple<block_index_type, label_type, block_index_type> dist_obs;
422 bool found_obs = false;
423 for (auto path : ds)
424 {
425 if (!is_tau(std::get<1>(path)) or std::get<0>(path) != std::get<2>(path))
426 {
427 if (dt.find(path) == dt.end())
428 {
429 dist_obs = path;
430 found_obs = true;
431 break;
432 }
433 }
434 }
435 // If no such observation exists, we flip the blocks.
436 if (!found_obs)
437 {
439 blockpair2formula[std::make_pair(block1.block_index, block2.block_index)] = phi;
440 // Compute the truth values \sem{!\phi} = lvl2blocksidx[lvl] - \sem{\phi}
441 std::set_difference(level2blocksidx[block1.level].begin(),
442 level2blocksidx[block1.level].end(),
443 blockpair2truths[std::make_pair(block2.block_index, block1.block_index)].begin(),
444 blockpair2truths[std::make_pair(block2.block_index, block1.block_index)].end(),
445 std::inserter(blockpair2truths[std::make_pair(block1.block_index, block2.block_index)],
446 blockpair2truths[std::make_pair(block1.block_index, block2.block_index)].begin()));
447 return phi;
448 }
449
450
451 // We have a distinguishing observation, start constructing the formula.
452 label_type dist_label = std::get<1>(dist_obs);
453 block_index_type B1 = std::get<0>(dist_obs);
454 block_index_type B2 = std::get<2>(dist_obs);
455 // Log the observation for debugging purposes.
456 std::vector<std::pair<block_index_type, block_index_type>> T;
457
458 for (auto path : dt)
459 {
460 if (std::get<1>(path) == dist_label and (!is_tau(dist_label) or std::get<0>(path) != std::get<2>(path)))
461 {
462 // we might have B_1 -\tau -> B_1, I don't think its a problem.
463 T.push_back(std::make_pair(std::get<0>(path), std::get<2>(path)));
464 if (is_tau(dist_label))
465 {
466 // the following observation: block2 -\tau->> path2 -(tau)-> path2.
467 T.push_back(std::make_pair(std::get<2>(path), std::get<2>(path)));
468 }
469 }
470 }
471 if (is_tau(dist_label))
472 {
473 // the following observation: block2 -\tau->> path2 -(tau)-> path2.
474 T.push_back(std::make_pair(block2.parent_block_index, block2.parent_block_index));
475 }
476
477 //Keep a copy of T for backwards filtering in postprocessing.
478 std::set<blockpair_type> T_og;
479 for (auto t : T)
480 {
481 T_og.insert(t);
482 }
483
484 // TODO: Remove this part and make T a set.
485 // Sort T, such that the block with the highest distlevel in s'' get dealt with first.
486 // This is a heuristic, no idea if it improves much or can be improved
487 std::sort(T.begin(), T.end(),
488 [this, B2](std::pair<block_index_type, block_index_type> a, std::pair<block_index_type, block_index_type> b)
489 {
490 if (a.second == B2) {
491 return false;
492 }
493 if (b.second == B2)
494 {
495 return true;
496 }
497 auto alift = min_split_blockpair(a.second, B2);
498 auto blift = min_split_blockpair(b.second, B2);
499 return blocks[alift.first].level < blocks[blift.first].level;
500 });
501
502 // <tau*>(<dist_label> phi1 && phi2), We remember the original keys for truth values and backwards filtering.
503 std::map<blockpair_type, mcrl2::state_formulas::state_formula> Phi1;
504 std::map<blockpair_type, mcrl2::state_formulas::state_formula> Phi2;
505
506 // Track truth values for the formula s -\tau -> Truths2 [phi2] -dist_label-> Truths1 [phi1]
507 // This is a bit confusing, we flip order here in the path to the formula.
508 std::set<block_index_type> Truths1 = level2blocksidx[block1.level - 1];
509 std::set<block_index_type> Truths2 = level2blocksidx[block1.level - 1];
510
511 while (!T.empty())
512 {
513 std::pair<block_index_type, block_index_type> Bt1_Bt2 = T.back();
514 // We could pop_back here on T, but the computation of the truth also handles this.
515 if (Bt1_Bt2.second != B2)
516 {
517 std::pair<block_index_type, block_index_type> liftedPair = min_split_blockpair(B2, Bt1_Bt2.second);
518 Phi1[liftedPair] = dist_formula(liftedPair.first, liftedPair.second);
519 // Update truthvalues for the formula <(dist_label)> phi1.
520 split_and_intersect(Truths1, liftedPair);
521 }
522 else
523 {
524 std::pair<block_index_type, block_index_type> liftedPair = min_split_blockpair(B1, Bt1_Bt2.first);
525 Phi2[liftedPair] = dist_formula(liftedPair.first, liftedPair.second);
526 // Update truthvalues for the formula phi2.
527 split_and_intersect(Truths2, liftedPair);
528 }
529 // Remove observations (Bt1, Bt2) from T of which Bt2 is not in phi1 or Bt1 is not in phi2
530 std::vector<std::pair<block_index_type, block_index_type>> T_new;
531 for (auto bt1_bt2 : T)
532 {
533 // T_new only consists stuch that both Bt1 and Bt2 are still not distinguished.
534 if (Truths1.find(bt1_bt2.second) != Truths1.end() && Truths2.find(bt1_bt2.first) != Truths2.end())
535 {
536 T_new.push_back(bt1_bt2);
537 }
538 }
539 T = T_new;
540 }
541
542 // Backwards filtering, remove each formula and see if it is still distinguishing, starting with Phi2.
543 std::set<block_index_type> Tset;
544 //We assume Phi2.
545 for (auto B_Bp : T_og)
546 {
547 if (Truths2.find(B_Bp.first) != Truths2.end()) {
548 Tset.insert(B_Bp.second);
549 }
550 }
551
552 std::vector<mcrl2::state_formulas::state_formula> returnPhi1 = filtered_dist_conjunction(Phi1, Tset, Truths1);
553
554
555 Tset.clear();
556 //Now we assume phi1.
557 for (auto B_Bp : T_og)
558 {
559 if (Truths1.find(B_Bp.second) != Truths1.end()) {
560 Tset.insert(B_Bp.first);
561 }
562 }
563 std::vector<mcrl2::state_formulas::state_formula> returnPhi2 = filtered_dist_conjunction(Phi2, Tset, Truths2);
564
565 //Done with formula, set the truth values for the formula.
566 // Initialize the truth values for the formula
567 blockpair2truths[std::make_pair(block_index1, block_index2)] = std::set<block_index_type>();
568 for (block_index_type b : level2blocksidx[block1.level])
569 {
570 signature_type sig = blocks[b].sig;
571 for (auto path : sig)
572 {
573 if (std::get<1>(path) == dist_label)
574 {
575 block_index_type Bt1 = std::get<0>(path);
576 block_index_type Bt2 = std::get<2>(path);
577 if (Truths1.find(Bt2) != Truths1.end() && Truths2.find(Bt1) != Truths2.end())
578 {
579 blockpair2truths[std::make_pair(block1.block_index, block2.block_index)].insert(b);
580 break;
581 }
582 }
583 }
584 }
585
586 // Consruct the regular formula for the diamond operator
588 // If the action is tau, we need to add the tau_hat operator.
589 if (is_tau(dist_label))
590 {
591 // we mimic <\hat{tau}> phi := <tau> phi || phi , by <tau+false*> phi.
592 diamond = make_tau_hat(diamond);
593 }
594
595 // diamond formula <dist_label> phi1
597 // diamond formula: <dist_label>phi1 && phi2
598 if (!returnPhi2.empty())
599 {
600 returnPhi = mcrl2::state_formulas::and_(returnPhi, conjunction(returnPhi2));
601 }
602
603 // <tau*> (<dist_label> phi1 && phi2)
604 blockpair2formula[std::make_pair(block1.block_index, block2.block_index)]
606 create_regular_formula(m_lts.action_label(0))), returnPhi);
607 return blockpair2formula[std::make_pair(block1.block_index, block2.block_index)];
608 }
609
610};
611
612template <class LTS_TYPE>
614 LTS_TYPE& l2,
615 const std::string& counter_example_file)
616{
617 std::size_t init_l2 = l2.initial_state() + l1.num_states();
619 l2.clear(); // No use for l2 anymore.
620
621 // First remove tau loops in case of branching bisimulation
622 bool preserve_divergences = false;
624 scc_part.replace_transition_system(preserve_divergences);
625
626 init_l2 = scc_part.get_eq_class(init_l2);
627
628 // Run a faster branching bisimulation algorithm as preprocessing, no preversing of loops.
629 detail::bisim_partitioner_dnj branching_bisim_part(l1, true, preserve_divergences);
630 if (branching_bisim_part.in_same_class(l1.initial_state(), init_l2))
631 {
632 return true;
633 }
634
635 init_l2 = branching_bisim_part.get_eq_class(init_l2);
636 branching_bisim_part.finalize_minimized_LTS();
637
638 //Start the new debugging to get minimal depth splitting information.
639 branching_bisim_partitioner_minimal_depth<LTS_TYPE> branching_bisim_min(l1, init_l2);
640
641 //Min-depth partitioner should agree with dnj.
642 assert(!branching_bisim_min.in_same_class(l1.initial_state(), init_l2));
643
644 // LTSs are not bisimilar, we can create a counter example.
645 std::string filename = "Counterexample.mcf";
646 if (!counter_example_file.empty())
647 {
648 filename = counter_example_file;
649 }
650
651 mcrl2::state_formulas::state_formula counter_example_formula
652 = branching_bisim_min.dist_formula_mindepth(l1.initial_state(), init_l2);
653
654 std::ofstream counter_file(filename);
655 counter_file << mcrl2::state_formulas::pp(counter_example_formula);
656 mCRL2log(mcrl2::log::info) << "Saved counterexample to: \"" << filename << "\"" << std::endl;
657 return false;
658}
659
660} // namespace mcrl2::lts::detail
661#endif // MCRl2_LTS_LIBLTS_BRANCHING_BISIM_MINIMAL_DEPTH
Read-only balanced binary tree of terms.
A list of aterm objects.
Definition aterm_list.h:24
\brief The value false for action formulas
\brief The multi action for action formulas
\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.
implements the main algorithm for the branching bisimulation quotient
bool in_same_class(state_type const s, state_type const t) const
Check whether two states are in the same equivalence class.
state_type get_eq_class(state_type const s) const
Get the equivalence class of a state.
void finalize_minimized_LTS()
Adapt the LTS after minimisation.
mcrl2::state_formulas::state_formula conjunction(std::vector< mcrl2::state_formulas::state_formula > &conjunctions)
conjunction Creates a conjunction of state formulas
regular_formulas::regular_formula make_tau_hat(regular_formulas::regular_formula &f)
void split_and_intersect(std::set< block_index_type > &truths, std::pair< block_index_type, block_index_type > liftedB1B2)
branching_bisim_partitioner_minimal_depth(LTS_TYPE &l, const std::size_t init_l2)
Creates a branching bisimulation partitioner for an LTS.
mcrl2::state_formulas::state_formula dist_formula(block_index_type block_index1, block_index_type block_index2)
std::map< std::pair< block_index_type, block_index_type >, std::set< block_index_type > > blockpair2truths
std::map< std::pair< block_index_type, block_index_type >, mcrl2::state_formulas::state_formula > blockpair2formula
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
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
bool is_dist(std::set< blockpair_type > &dist_blockpairs, std::set< block_index_type > &to_dist)
is_dist Checks if a given conjunction correctly exludes a set of blocks.
std::vector< mcrl2::state_formulas::state_formula > filtered_dist_conjunction(std::map< blockpair_type, mcrl2::state_formulas::state_formula > &Phi, std::set< block_index_type > &Tdist, std::set< block_index_type > &Truths)
mcrl2::state_formulas::state_formula dist_formula_mindepth(size_t s, size_t t)
Creates a state formula that distinguishes state s from state t.
bool is_dist(const std::set< blockpair_type > &dist_blockpairs, const std::set< block_index_type > &to_dist, std::set< block_index_type > &truths)
is_dist overloaded to also maintain the truth values computed at the end.
std::tuple< block_index_type, label_type, block_index_type > branching_observation_type
std::pair< block_index_type, block_index_type > min_split_blockpair(block_index_type b1, block_index_type b2)
This class contains an scc partitioner removing inert tau loops.
Definition liblts_scc.h:128
std::size_t get_eq_class(const std::size_t s) const
Gives the equivalence class number of a state. The equivalence class numbers range from 0 upto (and e...
Definition liblts_scc.h:307
void replace_transition_system(const bool preserve_divergence_loops)
The lts for which this partioner is created is replaced by the lts modulo the calculated partition.
Definition liblts_scc.h:248
A class containing triples, source label and target representing transitions.
Definition transition.h:43
\brief An action label
\brief The alt operator for regular formulas
\brief The 'trans or nil' operator for regular formulas
\brief The and operator for state formulas
\brief The may operator for state formulas
\brief The not operator for state formulas
\brief The value true for state formulas
O(m log n)-time branching bisimulation algorithm.
#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.
@ verbose
Definition logger.h:35
atermpp::term_balanced_tree< data::data_expression > state
Definition state.h:24
A base class for the lts_dot labelled transition system.
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
bool destructive_branching_bisimulation_compare_minimal_depth(LTS_TYPE &l1, LTS_TYPE &l2, const std::string &counter_example_file)
std::size_t state_type
type used to store state (numbers and) counts
std::size_t label_type
type used to store label numbers and counts
void pp(const T &t, std::ostream &out)
Prints the object t to a stream.
Definition print.h:668
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.