mCRL2
Loading...
Searching...
No Matches
liblts_bisim_gjkw.h
Go to the documentation of this file.
1// Author(s): David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
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
22
23#ifndef _LIBLTS_BISIM_GJKW_H
24#define _LIBLTS_BISIM_GJKW_H
25
26#include <unordered_map> // used during initialisation
27#include <list> // for the list of B_to_C_descriptors
28
33
34namespace mcrl2
35{
36namespace lts
37{
38namespace detail
39{
40 #ifndef NDEBUG
47 #define ONLY_IF_DEBUG(...) __VA_ARGS__
48 #else
49 #define ONLY_IF_DEBUG(...)
50 #endif
51// state_type and trans_type are defined in check_complexity.h.
52
54typedef std::size_t label_type;
55
56
57
58
59
60/* ************************************************************************* */
61/* */
62/* R E F I N A B L E P A R T I T I O N */
63/* */
64/* ************************************************************************* */
65
66
67
68
69
112
113namespace bisim_gjkw
114{
115
116class state_info_entry;
117
120
131typedef permutation_t::iterator permutation_iter_t;
132typedef permutation_t::const_iterator permutation_const_iter_t;
133
134class block_t;
135class constln_t;
136
137class B_to_C_entry;
138class pred_entry;
139class succ_entry;
143
148typedef std::list<B_to_C_descriptor> B_to_C_desc_list;
149typedef B_to_C_desc_list::iterator B_to_C_desc_iter_t;
150typedef B_to_C_desc_list::const_iterator B_to_C_desc_const_iter_t;
151
164{
165 private:
170
175
178
181
184 public:
187
190
193 private:
196 public:
198 const constln_t* constln() const;
200
203 void set_current_constln(succ_iter_t const new_current_constln)
204 {
205 int_current_constln = new_current_constln; // current_constln points to a successor transition of this state:
206 assert(succ_begin() <= int_current_constln);
207 assert(int_current_constln <= succ_end());
208 // it points to a place where a constellation slice starts or ends:
209 // (This assertion cannot be tested because the types are not yet
210 // complete.)
211 // assert(succ_begin() == int_current_constln ||
212 // succ_end() == int_current_constln ||
213 // int_current_constln[-1].constln_slice !=
214 // int_current_constln->constln_slice);
215 // it points to the relevant constellation:
216 // The following assertions cannot be executed immediately after each
217 // call.
218 // assert(succ_begin() == current_constln() ||
219 // *current_constln()[-1].target->constln() <= *SpC);
220 // assert(succ_end() == current_constln() ||
221 // *SpC <= *current_constln()->target->constln());
222 }
223
227 void set_pred_begin(pred_iter_t new_in_begin)
228 {
229 state_in_begin = new_in_begin;
230 }
231
234 { assert(s_i_begin <= this); assert(this < s_i_end);
235 return this[1].state_in_begin;
236 }
238 { assert(s_i_begin <= this); assert(this < s_i_end);
239 return this[1].state_in_begin;
240 }
241 void set_pred_end(pred_iter_t new_in_end)
242 { assert(s_i_begin <= this); assert(this < s_i_end);
243 this[1].set_pred_begin(new_in_end);
244 }
245
249
253
257 void set_inert_pred_begin(pred_iter_t new_inert_in_begin)
258 {
259 state_inert_in_begin = new_inert_in_begin; assert(pred_begin() <= inert_pred_begin());
260 assert(inert_pred_begin() <= pred_end());
261 }
262
266
270 void set_succ_begin(succ_iter_t new_out_begin)
271 {
272 state_out_begin = new_out_begin;
273 }
274
277 { assert(s_i_begin <= this); assert(this < s_i_end);
278 return this[1].state_out_begin;
279 }
281 { assert(s_i_begin <= this); assert(this < s_i_end);
282 return this[1].state_out_begin;
283 }
284 void set_succ_end(succ_iter_t new_out_end)
285 { assert(s_i_begin <= this); assert(this < s_i_end);
286 this[1].set_succ_begin(new_out_end); assert(succ_begin() <= succ_end());
287 }
288
292 void set_inert_succ_begin(succ_iter_t const new_inert_out_begin)
293 { // The following assertions cannot be tested because the respective
294 // types are not yet complete.
295 // if (new_inert_out_begin > inert_succ_begin())
296 // {
297 // assert(*new_inert_out_begin[-1].target->constln()<=*constln());
298 // assert(new_inert_out_begin[-1].target->block != block);
299 // }
300 // else if (new_inert_out_begin < inert_succ_begin())
301 // {
302 // assert(new_inert_out_begin->target->block == block);
303 // }
304 state_inert_out_begin = new_inert_out_begin; assert(succ_begin() <= inert_succ_begin());
305 assert(inert_succ_begin() <= inert_succ_end());
306 }
307
311
313 succ_iter_t new_inert_out_end)
314 {
315 state_inert_out_begin = new_inert_out_begin;
316 state_inert_out_end = new_inert_out_end; assert(succ_begin() <= inert_succ_begin());
317 assert(inert_succ_begin() <= inert_succ_end());
318 assert(inert_succ_end() <= succ_end());
319 // The following assertions cannot be tested always, as the function
320 // may be called earlier than the assertions are reestablished.
321 // assert(succ_begin() == inert_succ_begin() ||
322 // *inert_succ_begin()[-1].target->constln() <= *constln());
323 // assert(succ_begin() == inert_succ_begin() ||
324 // inert_succ_begin()[-1].target->block != block);
325 // assert(inert_succ_begin() == inert_succ_end() ||
326 // (inert_succ_begin()->target->block == block &&
327 // inert_succ_end()[-1].target->block == block));
328 // assert(succ_end() == inert_succ_end() ||
329 // *constln() < *inert_succ_end()->target->constln());
330 }
331
332 bool surely_has_transition_to(const constln_t* SpC) const;
334 #ifndef NDEBUG
337 std::string debug_id_short() const
338 {
339 assert(s_i_begin <= this);
340 assert(this < s_i_end);
341 return std::to_string(this - s_i_begin);
342 }
343
346 std::string debug_id() const
347 {
348 return "state " + debug_id_short();
349 }
350 private:
353
360
361 friend class part_state_t;
362 public:
364 #endif
365};
366
367
371{
372 // swap contents of permutation array
373 std::swap(*s1, *s2);
374 // swap pointers to permutation array
375 (*s1)->pos = s1;
376 (*s2)->pos = s2;
377}
378
404{
405 private:
408
411
414
417
420
427
430 public:
438 private:
441
447
450
457
458#define BLOCK_NO_SEQNR ((state_type) -1)
459
460 public:
465
472 block_t(constln_t* const constln_, permutation_iter_t const begin_,
473 permutation_iter_t const end_)
474 : int_end(end_),
475 int_begin(begin_),
476 int_marked_nonbottom_begin(begin_), // no non-bottom state is marked
477 int_bottom_begin(begin_), // all states are bottom states
478 int_marked_bottom_begin(end_), // no bottom state is marked
479 // int_inert_begin -- is initialised by part_trans_t::create_new_block
480 // int_inert_end -- is initialised by part_trans_t::create_new_block
481 to_constln(), // empty list
482 int_constln(constln_),
483 refinable_next(nullptr),
485 { // The following assertions hold trivially.
486 // assert(int_begin <= int_marked_nonbottom_begin);
487 // assert(int_marked_nonbottom_begin <= int_bottom_begin);
488 // assert(int_bottom_begin <= int_marked_bottom_begin);
489 // assert(int_marked_bottom_begin <= int_end);
490 assert(int_bottom_begin < int_end);
491 // The following assertions cannot be tested because constln_t is not
492 // yet complete.
493 // assert(int_constln->begin() <= int_begin);
494 // assert(int_end <= int_constln->end());
495 }
496
498
501 { assert(BLOCK_NO_SEQNR == int_seqnr);
503 }
504
505 state_type seqnr() const { return int_seqnr; }
506
509
512 bool is_refinable() const { return nullptr != refinable_next; }
513
518 {
519 if (is_refinable())
520 {
521 return false;
522 }
523 refinable_next = nullptr == refinable_first ? this : refinable_first;
524 refinable_first = this;
525 return true;
526 }
527
533 { assert(refinable_first == this);
534 refinable_first = refinable_next == this ? nullptr : refinable_next;
535 refinable_next = nullptr;
536 }
537
539 state_type size() const { return int_end - int_begin; }
540
544 {
546 }
547
552 {
555 }
556
559 {
561 }
562
569 bool operator<(const block_t& other) const
570 {
571 return begin() < other.begin();
572 }
573
575 const constln_t* constln() const { return int_constln; }
577 void set_constln(constln_t* new_constln)
578 { // The following assertion cannot be tested because the type constln_t
579 int_constln = new_constln; // is not yet complete.
580 // assert(nullptr == int_constln ||
581 // (int_constln->begin() <= int_begin &&
582 // int_end <= int_constln->end()));
583 }
584
587
589 void SetFromRed(B_to_C_desc_iter_t new_fromred);
590
595 {
596 int_begin = new_begin; assert(int_begin <= int_marked_nonbottom_begin);
597 }
598
603 {
604 int_end = new_end; assert(int_marked_bottom_begin <= int_end); assert(int_bottom_begin < int_end);
605 }
606
610
614 void set_nonbottom_end(permutation_iter_t new_nonbottom_end)
615 {
616 int_bottom_begin = new_nonbottom_end; assert(int_marked_nonbottom_begin <= int_bottom_begin);
618 assert(int_bottom_begin < int_end);
619 }
620
625 {
626 int_bottom_begin = new_bottom_begin; assert(int_marked_nonbottom_begin <= int_bottom_begin);
628 // assert(int_bottom_begin < int_end);
629 }
630
634
638
641 {
643 }
645 {
647 }
649 new_unmarked_nonbottom_end)
650 {
651 int_marked_nonbottom_begin = new_unmarked_nonbottom_end; assert(int_begin <= int_marked_nonbottom_begin);
653 }
654
657 {
659 }
661 {
663 }
665 new_marked_nonbottom_begin)
666 {
667 int_marked_nonbottom_begin = new_marked_nonbottom_begin; assert(int_begin <= int_marked_nonbottom_begin);
669 }
670
673 {
674 return int_bottom_begin;
675 }
677
680 {
681 return int_bottom_begin;
682 }
684
687 {
689 }
691 void set_unmarked_bottom_end(permutation_iter_t new_unmarked_bottom_end)
692 {
693 int_marked_bottom_begin = new_unmarked_bottom_end; assert(int_bottom_begin <= int_marked_bottom_begin);
695 }
696
699 {
701 }
703 void set_marked_bottom_begin(permutation_iter_t new_marked_bottom_begin)
704 {
705 int_marked_bottom_begin = new_marked_bottom_begin; assert(int_bottom_begin <= int_marked_bottom_begin);
707 }
708
713
717 void set_inert_begin(B_to_C_iter_t new_inert_begin)
718 {
719 int_inert_begin = new_inert_begin; assert(int_inert_begin <= int_inert_end);
720 }
721
725 void set_inert_end(B_to_C_iter_t new_inert_end)
726 {
727 int_inert_end = new_inert_end; assert(int_inert_begin <= int_inert_end);
728 }
730 B_to_C_iter_t new_inert_end)
731 {
732 int_inert_begin = new_inert_begin;
733 int_inert_end = new_inert_end; assert(int_inert_begin <= int_inert_end);
734 }
735
742 { assert(s->pos < nonbottom_end()); assert(nonbottom_begin() <= s->pos);
743 if (marked_nonbottom_begin() <= s->pos) return false;
746 return true;
747 }
748
756 { assert(s->pos < end());
757 if (bottom_begin() <= s->pos)
758 {
759 if (marked_bottom_begin() <= s->pos) return false;
762 return true;
763 }
764 return mark_nonbottom(s);
765 }
766
773 block_t* split_off_blue(permutation_iter_t blue_nonbottom_end);
774
781 block_t* split_off_red(permutation_iter_t red_nonbottom_begin);
782 #ifndef NDEBUG
785 std::string debug_id() const
786 {
787 return "block [" + std::to_string(begin() - perm_begin) + "," +
788 std::to_string(end() - perm_begin) + ")" +
789 (BLOCK_NO_SEQNR != seqnr() ?" (#"+std::to_string(seqnr())+")" :"");
790 }
791
796
798 private:
800
801 friend class part_state_t;
802 #endif
803};
804
805
812{
813 private:
816
819
826
829 public:
842
846
854
859 permutation_iter_t end_, B_to_C_iter_t postprocess_none)
860 : int_end(end_),
861 int_begin(begin_),
862 nontrivial_next(nullptr),
863 postprocess_begin(postprocess_none),
864 postprocess_end(postprocess_none),
865 sort_key(sort_key_)
866 { assert(int_begin<int_end); assert((state_type)(int_end-int_begin)<=sort_key);
867 }
868
871
876
884
890 { assert(nontrivial_first == this);
892 nontrivial_next = nullptr;
893 }
894
898 {
899 if (nullptr == nontrivial_next)
900 {
901 nontrivial_next = nullptr == nontrivial_first ? this
903 nontrivial_first = this;
904 }
905 }
906
911 bool is_trivial() const
912 {
913 return nullptr == nontrivial_next;
914 }
915
922 {
923 int_begin = new_begin; assert(int_begin < int_end);
924 }
925
932 {
933 int_end = new_end; assert(int_begin < int_end);
934 }
935
937 state_type size() const { return int_end - int_begin; }
938
945 bool operator<(const constln_t& other) const
946 {
947 return sort_key < other.sort_key;
948 }
949 bool operator> (const constln_t& other) const { return other < *this; }
950 bool operator<=(const constln_t& other) const { return !(other < *this); }
951 bool operator>=(const constln_t& other) const { return !(*this < other); }
952
959 { assert(begin() < end());
960 block_t* const FirstB = (*begin())->block;
961 block_t* const LastB = end()[-1]->block; assert(FirstB != LastB);
962 if (FirstB->end() == LastB->begin()) { make_trivial(); } assert(FirstB->constln() == this); assert(LastB->constln() == this);
964 // 2.5: Choose a small splitter block SpB subset of SpC from P,
965 // i.e. |SpB| <= 1/2*|SpC|
970 if (FirstB->size() > LastB->size())
971 {
972 // 2.6: Create a new constellation NewC
973 // 2.6: ... and move SpB from SpC to NewC
974 constln_t* NewC =
975 new constln_t(sort_key - (LastB->begin() - begin()),
976 LastB->begin(), end(), postprocess_end);
977 set_end(LastB->begin());
978 LastB->set_constln(NewC);
979 return LastB;
980 }
981 else
982 {
983 // 2.6: Create a new constellation NewC
984 // 2.6: ... and move SpB from SpC to NewC
985 constln_t* NewC =
986 new constln_t(sort_key - (end() - FirstB->end()), begin(),
987 FirstB->end(), postprocess_end);
988 set_begin(FirstB->end());
989 FirstB->set_constln(NewC);
990 return FirstB;
991 }
992 }
993 #ifndef NDEBUG
995 std::string debug_id() const
996 {
997 return "constellation [" +
998 std::to_string(begin() - block_t::permutation_begin()) +
999 "," + std::to_string(end() - block_t::permutation_begin()) +
1000 ") (#" + std::to_string(sort_key) + ")";
1001 }
1002 #endif
1003};
1004
1005
1006template <class LTS_TYPE>
1007class bisim_partitioner_gjkw_initialise_helper;
1008
1009class part_trans_t;
1010
1016{
1017 public:
1024
1025 private:
1031
1032 template <class LTS_TYPE>
1034 public:
1042 : permutation(n),
1043 state_info(n+1) //< an additional ``state'' is needed to store pointers
1044 // to the end of the slices of transitions of the last state
1045 { assert(0 == block_t::nr_of_blocks);
1046 #ifndef NDEBUG
1050 #endif
1051 }
1052
1057 { assert(state_info.empty()); assert(permutation.empty());
1058 }
1059
1065 void clear()
1066 {
1067 // We have to deallocate constellations first because deallocating
1068 // blocks makes the constellations inaccessible.
1069 for (permutation_iter_t permutation_iter = permutation.end();
1070 permutation.begin() != permutation_iter; )
1071 {
1072 constln_t* const C = permutation_iter[-1]->constln(); assert(C->end() == permutation_iter);
1073 // permutation_iter[-1]->block->set_constln(nullptr); // assert that constellation is trivial:
1074 assert(permutation_iter[-1]->block->begin() == C->begin());
1075 permutation_iter = C->begin();
1076 delete C;
1077 }
1078 #ifndef NDEBUG
1079 state_type deleted_blocks = 0;
1080 #endif
1081 for (permutation_iter_t permutation_iter = permutation.end();
1082 permutation.begin() != permutation_iter; )
1083 {
1084 block_t* const B = permutation_iter[-1]->block; assert(B->end() == permutation_iter);
1085 permutation_iter = B->begin();
1086 #ifndef NDEBUG
1087 if (BLOCK_NO_SEQNR != B->seqnr()) ++deleted_blocks;
1088 else assert(0 == deleted_blocks);
1089 #endif
1090 delete B;
1091 } assert(deleted_blocks == block_t::nr_of_blocks);
1093 state_info.clear();
1094 permutation.clear();
1095 }
1096
1099 state_type state_size() const { return permutation.size(); }
1100
1104 const block_t* block(state_type s) const
1105 {
1106 return state_info[s].block;
1107 }
1108 #ifndef NDEBUG
1109 private:
1118 void print_block(const char* message, const block_t* B,
1120 public:
1126 void print_part(const part_trans_t& part_tr) const;
1127
1132 void print_trans() const;
1133 #endif
1134};
1135
1137
1138
1139
1140
1141
1142/* ************************************************************************* */
1143/* */
1144/* T R A N S I T I O N S */
1145/* */
1146/* ************************************************************************* */
1147
1148
1149
1150
1151
1181
1183
1184/* pred_entry, succ_entry, and B_to_C_entry contain the data that is stored
1185about a transition. Every transition has one of each data structure; the three
1186structures are linked through the iterators (used here as pointers). */
1188{
1189 public:
1192
1193 private:
1207 public:
1208
1210 {
1212 }
1213
1215 {
1217 }
1218
1220 {
1222 }
1223
1224
1226 {
1227 if (this < &*int_slice_begin_or_before_end)
1228 { assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end <= this);
1231 } assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end == this);
1233 }
1234
1236 {
1237 if (this < &*int_slice_begin_or_before_end)
1238 { assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end <= this);
1241 } assert(&*int_slice_begin_or_before_end->int_slice_begin_or_before_end == this);
1243 }
1244
1246 {
1247 if (this_ < this_->int_slice_begin_or_before_end)
1248 { assert(this_->int_slice_begin_or_before_end->
1250 return this_->int_slice_begin_or_before_end + 1;
1251 } assert(this_->int_slice_begin_or_before_end->
1253 // The following line requires an iterator but a normal method would
1254 // only have a pointer, not an iterator. That's why we need to jump
1255 // through the `static` hoop.
1256 return this_ + 1;
1257 }
1258
1260 {
1261 if (this_ < this_->int_slice_begin_or_before_end)
1262 { assert(this_->int_slice_begin_or_before_end->
1264 return this_->int_slice_begin_or_before_end + 1;
1265 } assert(this_->int_slice_begin_or_before_end->
1267 // The following line requires an iterator but a normal method would
1268 // only have a pointer, not an iterator. That's why we need to jump
1269 // through the `static` hoop.
1270 return this_ + 1;
1271 }
1272 #ifndef NDEBUG
1276 enum check_complexity::counter_type ctr, unsigned max_value);
1277 #endif
1278};
1279
1280
1282{
1283 public:
1286 #ifndef NDEBUG
1289 std::string debug_id_short() const
1290 {
1291 return "from " + source->debug_id_short() + " to " +
1292 succ->target->debug_id_short();
1293 }
1294
1297 std::string debug_id() const
1298 {
1299 return "transition " + debug_id_short();
1300 }
1301
1303 #endif
1304};
1305
1306
1308{
1309 public:
1312};
1313 #ifndef NDEBUG
1317 enum check_complexity::counter_type ctr, unsigned max_value)
1318 {
1319 succ_const_iter_t iter = this_->slice_begin();
1320 succ_const_iter_t end = slice_end(this_);
1321 assert(iter < end);
1322 mCRL2complexity(iter->B_to_C->pred, add_work(ctr, max_value), );
1323 while (++iter != end)
1324 {
1325 // treat temporary counters specially
1326 mCRL2complexity(iter->B_to_C->pred,
1327 add_work_notemporary(ctr, max_value), );
1328 }
1329 }
1330 #endif
1331/* B_to_C_descriptor is a data type that indicates which slice of states
1332belongs together. */
1334{
1335 public:
1337
1339 : end(end_),
1340 begin(begin_)
1341 { }
1342
1344 const block_t* from_block() const
1345 { assert(begin < end); assert(begin->pred->succ->B_to_C == begin);
1346 return begin->pred->source->block;
1347 }
1349 { assert(begin < end); assert(begin->pred->succ->B_to_C == begin);
1350 return begin->pred->source->block;
1351 }
1352
1354 const constln_t* to_constln() const
1355 { assert(begin < end); assert(begin->pred->succ->B_to_C == begin);
1356 return begin->pred->succ->target->constln();
1357 }
1359 { assert(begin < end); assert(begin->pred->succ->B_to_C == begin);
1360 return begin->pred->succ->target->constln();
1361 }
1362
1367 { assert(to_constln()->postprocess_end <= begin ||
1368 end <= to_constln()->postprocess_end);
1369 assert(to_constln()->postprocess_begin <= begin ||
1370 end <= to_constln()->postprocess_begin);
1371 return to_constln()->postprocess_begin <= begin &&
1373 }
1374 #ifndef NDEBUG
1377 std::string debug_id() const
1378 {
1379 assert(begin < end);
1380 std::string result("slice containing transition");
1381 if (end - begin > 1)
1382 result += "s ";
1383 else
1384 result += " ";
1386 assert(iter->pred->succ->B_to_C == iter);
1387 result += iter->pred->debug_id_short();
1388 if (end - iter > 4)
1389 {
1390 assert(iter[1].pred->succ->B_to_C == iter+1);
1391 result += ", ";
1392 result += iter[1].pred->debug_id_short();
1393 result += ", ...";
1394 iter = end - 3;
1395 }
1396 while (++iter != end)
1397 {
1398 assert(iter->pred->succ->B_to_C == iter);
1399 result += ", ";
1400 result += iter->pred->debug_id_short();
1401 }
1402 return result;
1403 }
1404
1414 unsigned max_value)
1415 {
1416 bool added = false;
1417
1418 for (B_to_C_const_iter_t iter = begin; iter != end; ++iter)
1419 {
1420 if (iter->pred->source->pos >=
1421 iter->pred->source->block->bottom_begin())
1422 {
1423 // source state of the transition is a bottom state
1424 mCRL2complexity(iter->pred, add_work(ctr, max_value), );
1425 added = true;
1426 }
1427 }
1428 return added;
1429 }
1430
1432 #endif
1433};
1434
1435
1436/* part_trans_t collects and organises all data for the transitions. */
1438{
1439 private:
1443
1444 template <class LTS_TYPE>
1446
1447 void swap_in(B_to_C_iter_t const pos1, B_to_C_iter_t const pos2)
1448 { assert(B_to_C.end() > pos1); assert(pos1->pred->succ->B_to_C == pos1);
1449 assert(B_to_C.end() > pos2); assert(pos2->pred->succ->B_to_C == pos2);
1450 // swap contents
1451 pred_entry const temp_entry(*pos1->pred);
1452 *pos1->pred = *pos2->pred;
1453 *pos2->pred = temp_entry;
1454 // swap pointers to contents
1455 pred_iter_t const temp_iter(pos1->pred);
1456 pos1->pred = pos2->pred;
1457 pos2->pred = temp_iter; assert(B_to_C.end() > pos1); assert(pos1->pred->succ->B_to_C == pos1);
1458 assert(B_to_C.end() > pos2); assert(pos2->pred->succ->B_to_C == pos2);
1459 }
1460
1461 void swap_out(pred_iter_t const pos1, pred_iter_t const pos2)
1462 { assert(pred.end() > pos1); assert(pos1->succ->B_to_C->pred == pos1);
1463 assert(pred.end() > pos2); assert(pos2->succ->B_to_C->pred == pos2);
1464 assert(pos1->succ->slice_begin() == pos2->succ->slice_begin());
1465 assert(succ_entry::slice_end(pos1->succ) == succ_entry::slice_end(pos2->succ));
1466 // swap contents, but do not swap slice_begin_or_before_end
1467 B_to_C_iter_t const temp_B_to_C(pos1->succ->B_to_C);
1468 state_info_ptr const temp_target(pos1->succ->target);
1469 pos1->succ->B_to_C = pos2->succ->B_to_C;
1470 pos1->succ->target = pos2->succ->target;
1471 pos2->succ->B_to_C = temp_B_to_C;
1472 pos2->succ->target = temp_target;
1473 // swap pointers to contents
1474 succ_iter_t const temp_iter(pos1->succ);
1475 pos1->succ = pos2->succ;
1476 pos2->succ = temp_iter; assert(pred.end() > pos1); assert(pos1->succ->B_to_C->pred == pos1);
1477 assert(pred.end() > pos2); assert(pos2->succ->B_to_C->pred == pos2);
1478 assert(pos1->succ->slice_begin() == pos2->succ->slice_begin());
1479 assert(succ_entry::slice_end(pos1->succ) == succ_entry::slice_end(pos2->succ));
1480 }
1481
1482 void swap_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2)
1483 { assert(succ.end() > pos1); assert(pos1->B_to_C->pred->succ == pos1);
1484 assert(succ.end() > pos2); assert(pos2->B_to_C->pred->succ == pos2);
1485 // swap contents
1486 B_to_C_entry const temp_entry(*pos1->B_to_C);
1487 *pos1->B_to_C = *pos2->B_to_C;
1488 *pos2->B_to_C = temp_entry;
1489 // swap pointers to contents
1490 B_to_C_iter_t const temp_iter(pos1->B_to_C);
1491 pos1->B_to_C = pos2->B_to_C;
1492 pos2->B_to_C = temp_iter; assert(succ.end() > pos1); assert(pos1->B_to_C->pred->succ == pos1);
1493 assert(succ.end() > pos2); assert(pos2->B_to_C->pred->succ == pos2);
1494 }
1495
1496 // *pos1 -> *pos2 -> *pos3 -> *pos1
1497 void swap3_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2,
1498 succ_iter_t const pos3)
1499 { assert(succ.end() > pos1); assert(pos1->B_to_C->pred->succ == pos1);
1500 assert(succ.end() > pos2); assert(pos2->B_to_C->pred->succ == pos2);
1501 assert(succ.end() > pos3); assert(pos3->B_to_C->pred->succ == pos3);
1502 assert(pos1 != pos2 || pos1 == pos3);
1503 // swap contents
1504 B_to_C_entry const temp_entry(*pos1->B_to_C);
1505 *pos1->B_to_C = *pos3->B_to_C;
1506 *pos3->B_to_C = *pos2->B_to_C;
1507 *pos2->B_to_C = temp_entry;
1508 // swap pointers to contents
1509 B_to_C_iter_t const temp_iter(pos2->B_to_C);
1510 pos2->B_to_C = pos3->B_to_C;
1511 pos3->B_to_C = pos1->B_to_C;
1512 pos1->B_to_C = temp_iter; assert(succ.end() > pos1); assert(pos1->B_to_C->pred->succ == pos1);
1513 assert(succ.end() > pos2); assert(pos2->B_to_C->pred->succ == pos2);
1514 assert(succ.end() > pos3); assert(pos3->B_to_C->pred->succ == pos3);
1515 }
1516 public:
1518 : pred(m),
1519 succ(m),
1520 B_to_C(m)
1521 { }
1523 { assert(B_to_C.empty()); assert(succ.empty()); assert(pred.empty());
1524 }
1525
1527 void clear()
1528 {
1529 // B_to_C_descriptors are deallocated when their respective lists are
1530 // deallocated by destructing the blocks.
1531 B_to_C.clear();
1532 succ.clear();
1533 pred.clear();
1534 }
1535
1536 trans_type trans_size() const { return pred.size(); }
1537
1538 /* split_inert_to_C splits the B_to_C slice of block b to its own
1539 constellation into two slices: one for the inert and one for the non-inert
1540 transitions. It is called with SpB just after a constellation is split, as
1541 the transitions from SpB to itself (= the inert transitions) now go to a
1542 different constellation than the other transitions from SpB to its old
1543 constellation. It does, however, not adapt the other transition arrays to
1544 reflect that noninert and inert transitions from block b would go to
1545 different constellations.
1546 Its time complexity is O(1+min {|out_noninert(b-->C)|, |out_inert(b)|}). */
1547 void split_inert_to_C(block_t* B);
1548
1549 /* part_trans_t::change_to_C has to be called after a transition target has
1550 changed its constellation. The member function will adapt the transition
1551 data structure. It assumes that the transition is non-inert and that the
1552 new constellation does not (yet) have inert incoming transitions. It
1553 returns the boundary between transitions to OldC and transitions to NewC in
1554 the state's outgoing transition array. */
1556 bool first_transition_of_state, bool first_transition_of_block);
1557
1558 /* split_s_inert_out splits the outgoing transitions from s to its own
1559 constellation into two: the inert transitions become transitions to the
1560 new constellation of which s is now part; the non-inert transitions remain
1561 transitions to OldC. It returns the boundary between transitions to
1562 OldC and transitions to NewC in the outgoing transition array of s.
1563 Its time complexity is O(1 + min { |out_\nottau(s)|, |out_\tau(s)| }). */
1565 );
1566
1567 /* part_trans_t::make_noninert makes the transition identified by succ_iter
1568 noninert. */
1569 void make_noninert(succ_iter_t const succ_iter)
1570 {
1571 // change B_to_C
1572 B_to_C_iter_t const other_B_to_C =
1573 succ_iter->B_to_C->pred->source->block->inert_begin(); assert(succ_iter->B_to_C->B_to_C_slice->begin <= other_B_to_C);
1574 assert(other_B_to_C <= succ_iter->B_to_C);
1575 assert(succ_iter->B_to_C < succ_iter->B_to_C->B_to_C_slice->end);
1576 swap_B_to_C(succ_iter, other_B_to_C->pred->succ);
1577 succ_iter->B_to_C->pred->source->block->set_inert_begin(other_B_to_C +
1578 1);
1579 // change pred
1580 pred_iter_t const other_pred = succ_iter->target->inert_pred_begin(); assert(succ_iter->target->pred_begin() <= other_pred);
1581 assert(other_pred <= succ_iter->B_to_C->pred);
1582 assert(succ_iter->B_to_C->pred < succ_iter->target->pred_end());
1583 swap_in(succ_iter->B_to_C, other_pred->succ->B_to_C);
1584 succ_iter->target->set_inert_pred_begin(other_pred + 1);
1585 // change succ
1586 succ_iter_t const other_succ =
1587 succ_iter->B_to_C->pred->source->inert_succ_begin(); assert(succ_iter->B_to_C->pred->source->succ_begin() <= other_succ);
1588 assert(other_succ <= succ_iter);
1589 assert(succ_iter < succ_iter->B_to_C->pred->source->succ_end());
1590 swap_out(succ_iter->B_to_C->pred, other_succ->B_to_C->pred);
1591 succ_iter->B_to_C->pred->source->set_inert_succ_begin(other_succ + 1);
1592 }
1593
1594 /* part_trans_t::new_block_created splits the B_to_C-slices to reflect that
1595 some transitions now start in the new block NewB. They can no longer be in
1596 the same slice as the transitions that start in the old block.
1597
1598 We need separate functions for blue and red blocks because the B_to_C-slice
1599 of the red block should come after the B_to_C-slice of the blue block,
1600 at least while postprocessing.
1601
1602 Its time complexity is O(1 + |out(NewB)|). */
1603 void new_blue_block_created(block_t* OldB, block_t* NewB);
1604 void new_red_block_created(block_t*OldB,block_t*NewB, bool postprocessing);
1605
1606 B_to_C_const_iter_t B_to_C_begin() const { return B_to_C.begin(); }
1607 B_to_C_iter_t B_to_C_end () { return B_to_C.end (); }
1608 pred_const_iter_t pred_end() const { return pred.end(); }
1609 succ_const_iter_t succ_end() const { return succ.end(); }
1610 #ifndef NDEBUG
1612 void assert_stability(const part_state_t& part_st) const;
1613 #endif
1614};
1615
1617
1618
1619
1620
1621
1622
1623/* ************************************************************************* */
1624/* */
1625/* A L G O R I T H M S */
1626/* */
1627/* ************************************************************************* */
1628
1629
1630
1631
1632
1636
1637
1638
1639/*=============================================================================
1640= create initial partition and data structures =
1641=============================================================================*/
1642
1643
1644
1654template<class LTS_TYPE>
1656{
1657 private:
1658 LTS_TYPE& aut;
1662
1663 // key and hash function for (action, target state) pair. Required since
1664 // unordered_map does not directly allow to use pair keys
1665 class Key
1666 {
1667 public:
1670
1671 Key(const label_type& f, const state_type& s)
1672 : first(f),
1673 second(s)
1674 {}
1675
1676 bool operator==(const Key &other) const
1677 {
1678 return first == other.first && second == other.second;
1679 }
1680 };
1681
1683 {
1684 public:
1685 std::size_t operator()(const Key& k) const
1686 {
1687 return std::hash<label_type>()(k.first) ^
1688 (std::hash<state_type>()(k.second) << 1);
1689 }
1690 };
1691 // Map used to convert LTS to Kripke structure
1692 // (also used when converting Kripke structure back to LTS)
1693 std::unordered_map<Key, state_type, KeyHasher> extra_kripke_states;
1694
1695 // temporary map to keep track of blocks. maps transition labels (different
1696 // from tau) to blocks
1697 std::unordered_map<label_type, state_type> action_block_map;
1698
1702 std::vector<state_type> states_per_block;
1704 public:
1705 bisim_partitioner_gjkw_initialise_helper(LTS_TYPE& l, bool branching,
1706 bool preserve_divergence);
1707
1709 void init_transitions(part_state_t& part_st, part_trans_t& part_tr,
1710 bool branching, bool preserve_divergence);
1711
1712 // replace_transition_system() replaces the transitions of the LTS stored here by
1713 // those of its bisimulation quotient. However, it does not change
1714 // anything else; in particular, it does not change the number of states of
1715 // the LTS.
1716 void replace_transition_system(const part_state_t& part_st, ONLY_IF_DEBUG( bool branching, )
1717 bool preserve_divergence);
1718
1721
1724};
1725
1726
1727
1728/*=============================================================================
1729= main class =
1730=============================================================================*/
1731
1732
1733
1734struct refine_shared_t;
1735
1736} // end namespace bisim_gjkw
1737
1740template <class LTS_TYPE>
1742{
1743 private:
1747 public:
1748 // The constructor constructs the data structures and immediately
1749 // calculates the bisimulation quotient. However, it does not change the
1750 // LTS.
1751 bisim_partitioner_gjkw(LTS_TYPE& l, bool branching = false,
1752 bool preserve_divergence = false)
1753 : init_helper(l, branching, preserve_divergence),
1754 part_st(init_helper.get_nr_of_states()),
1755 part_tr(init_helper.get_nr_of_transitions())
1756 { assert(branching || !preserve_divergence);
1757 create_initial_partition_gjkw(branching, preserve_divergence);
1759 }
1761 {
1762 part_tr.clear();
1763 part_st.clear();
1764 }
1765
1766 // replace_transition_system() replaces the transitions of the LTS stored here by
1767 // those of its bisimulation quotient. However, it does not change
1768 // anything else; in particular, it does not change the number of states of
1769 // the LTS.
1770 void replace_transition_system(bool branching, bool preserve_divergence)
1771 {
1772 (void) branching; // avoid warning about unused parameter.
1773 init_helper.replace_transition_system(part_st, ONLY_IF_DEBUG( branching, )
1774 preserve_divergence);
1775 }
1776
1778 {
1780 }
1781
1783 {
1784 return part_st.block(s)->seqnr();
1785 }
1786
1788 {
1789 return part_st.block(s) == part_st.block(t);
1790 }
1791
1792 private:
1793
1794 /*-------- dbStutteringEquivalence -- Algorithm 2 of [GJKW 2017] --------*/
1795
1796 void create_initial_partition_gjkw(bool branching,
1797 bool preserve_divergence);
1799
1800 /*----------------- Refine -- Algorithm 3 of [GJKW 2017] ----------------*/
1801
1803 const bisim_gjkw::constln_t* SpC,
1804 const bisim_gjkw::B_to_C_descriptor* FromRed,
1805 bool postprocessing ONLY_IF_DEBUG( , const bisim_gjkw::constln_t* NewC = nullptr )
1806 );
1807
1808 /*--------- PostprocessNewBottom -- Algorithm 4 of [GJKW 2017] ----------*/
1809
1811};
1812
1814
1815
1816
1817
1818
1819/* ************************************************************************* */
1820/* */
1821/* I N T E R F A C E */
1822/* */
1823/* ************************************************************************* */
1824
1825
1826
1827
1828
1834
1844template <class LTS_TYPE>
1845void bisimulation_reduce_gjkw(LTS_TYPE& l, bool branching = false,
1846 bool preserve_divergence = false);
1847
1861template <class LTS_TYPE>
1862bool destructive_bisimulation_compare_gjkw(LTS_TYPE& l1, LTS_TYPE& l2,
1863 bool branching = false, bool preserve_divergence = false,
1864 bool generate_counter_examples = false);
1865
1881template <class LTS_TYPE>
1882bool bisimulation_compare_gjkw(const LTS_TYPE& l1, const LTS_TYPE& l2,
1883 bool branching = false, bool preserve_divergence = false);
1884
1886template <class LTS_TYPE>
1887void bisimulation_reduce_gjkw(LTS_TYPE& l, bool const branching /* = false */,
1888 bool const preserve_divergence /* = false */)
1889{
1890 // First, remove tau loops in case of branching bisimulation.
1891 if (branching)
1892 {
1893 scc_reduce(l, preserve_divergence);
1894 }
1895
1896 // Second, apply the branching bisimulation reduction algorithm. If there are
1897 // no taus, this will automatically yield strong bisimulation.
1898 detail::bisim_partitioner_gjkw<LTS_TYPE> bisim_part(l, branching,
1899 preserve_divergence);
1900
1901 // Assign the reduced LTS
1902 bisim_part.replace_transition_system(branching, preserve_divergence);
1903}
1904
1905template <class LTS_TYPE>
1906inline bool bisimulation_compare_gjkw(const LTS_TYPE& l1, const LTS_TYPE& l2,
1907 bool branching /* = false */, bool preserve_divergence /* = false */)
1908{
1909 LTS_TYPE l1_copy(l1);
1910 LTS_TYPE l2_copy(l2);
1911 return destructive_bisimulation_compare_gjkw(l1_copy, l2_copy, branching,
1912 preserve_divergence);
1913}
1914
1915template <class LTS_TYPE>
1916bool destructive_bisimulation_compare_gjkw(LTS_TYPE& l1, LTS_TYPE& l2,
1917 bool branching /* = false */, bool preserve_divergence /* = false */,
1918 bool generate_counter_examples /* = false */,
1919 const std::string& /*counter_example_file = "" */,
1920 bool /*structured_output = false */)
1921{
1922 if (generate_counter_examples)
1923 {
1924 mCRL2log(log::warning) << "The GJKW branching bisimulation algorithm does "
1925 "not generate counterexamples.\n";
1926 }
1927 state_type init_l2 = l2.initial_state() + l1.num_states();
1929 l2.clear(); // No use for l2 anymore.
1930
1931 // First remove tau loops in case of branching bisimulation.
1932 if (branching)
1933 {
1935 scc_part.replace_transition_system(preserve_divergence);
1936 init_l2 = scc_part.get_eq_class(init_l2);
1937 }
1938
1939 detail::bisim_partitioner_gjkw<LTS_TYPE> bisim_part(l1, branching,
1940 preserve_divergence);
1941 return bisim_part.in_same_class(l1.initial_state(), init_l2);
1942}
1943
1945
1946
1947
1948
1949
1950/* ************************************************************************* */
1951/* */
1952/* I M P L E M E N T A T I O N S */
1953/* */
1954/* ************************************************************************* */
1955
1956
1957
1958
1959
1960// This section contains implementations of functions that refer to details of
1961// classes defined later, so they could not be defined at the point of
1962// declaration.
1963
1964namespace bisim_gjkw
1965{
1966
1969{
1970 return block->constln();
1971}
1972
1974{
1975 return block->constln();
1976}
1977
1980{
1981 if (!to_constln.empty() && to_constln.front().to_constln() == SpC)
1982 {
1983 return &*to_constln.begin();
1984 }
1985 else
1986 {
1987 #ifndef NDEBUG
1988 for (B_to_C_desc_const_iter_t iter = to_constln.begin();
1989 to_constln.end() != iter; ++iter)
1990 {
1991 assert(iter->from_block() == this);
1992 assert(iter->to_constln() != SpC);
1993 }
1994 #endif
1995 return nullptr;
1996 }
1997}
1998
1999
2001inline void block_t::SetFromRed(B_to_C_desc_iter_t const new_fromred)
2002{ assert(!to_constln.empty());
2003 if (to_constln.begin() != new_fromred)
2004 {
2005 to_constln.splice(to_constln.begin(), to_constln, new_fromred);
2006 } assert(new_fromred->from_block() == this);
2007}
2008
2009
2020 SpC) const
2021{ assert(succ_begin()<=current_constln()); assert(current_constln()<=succ_end());
2022 assert(succ_begin() == current_constln() || succ_end() == current_constln() ||
2023 *current_constln()[-1].target->constln() <
2024 *current_constln()->target->constln());
2025 assert(constln() != SpC);
2026 // either current_constln()->target or current_constln()[-1].target is in
2027 // SpC
2028 if (current_constln() != succ_end() &&
2029 current_constln()->target->constln() == SpC)
2030 {
2031 return true;
2032 }
2033 return false;
2034}
2035
2036
2048 const constln_t* const SpC) const
2049{ assert(succ_begin()<=current_constln()); assert(current_constln()<=succ_end());
2050 assert(succ_begin() == current_constln() || succ_end() == current_constln() ||
2051 *current_constln()[-1].target->constln() <
2052 *current_constln()->target->constln());
2053 assert(constln() != SpC);
2054 // condition:
2055 // current_constln()->target is in a constellation > SpC and
2056 // current_constln()[-1].target is in a constellation < SpC.
2057 if (current_constln() != succ_end() &&
2058 *current_constln()->target->constln() <= *SpC)
2059 {
2060 return false;
2061 }
2062 if (current_constln() != succ_begin() &&
2063 *SpC <= *current_constln()[-1].target->constln())
2064 {
2065 return false;
2066 }
2067 return true;
2068}
2069
2070
2071} // end namespace bisim_gjkw
2072} // end namespace detail
2073} // end namespace lts
2074} // end namespace mcrl2
2075
2076#endif // ifndef _LIBLTS_BISIM_GJKW_H
helper class for time complexity checks during test runs
#define mCRL2complexity(unit, call,...)
Assigns work to a counter and checks for errors.
helps with initialising the refinable partition data structure
stores information about a block
counter_type
Type for complexity budget counters.
stores information about a constellation
stores information about a single state
implements the main algorithm for the stutter equivalence quotient
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 vector class that cannot be moved while it is not empty
bool bisimulation_compare_gjkw(const LTS_TYPE &l1, const LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false)
Checks whether the two initial states of two LTSs are strong or branching bisimilar.
void bisimulation_reduce_gjkw(LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)
Reduce transition system l with respect to strong or (divergence preserving) branching bisimulation.
bool destructive_bisimulation_compare_gjkw(LTS_TYPE &l1, LTS_TYPE &l2, bool branching=false, bool preserve_divergence=false, bool generate_counter_examples=false)
Checks whether the two initial states of two LTSs are strong or branching bisimilar.
std::string debug_id() const
print a B_to_C slice identification for debugging
std::string debug_id() const
print a constellation identification for debugging
std::string debug_id() const
print a block identification for debugging
bisim_partitioner_gjkw(LTS_TYPE &l, bool branching=false, bool preserve_divergence=false)
check_complexity::trans_counter_t work_counter
succ_iter_t change_to_C(pred_iter_t pred_iter, ONLY_IF_DEBUG(constln_t *SpC, constln_t *NewC,) bool first_transition_of_state, bool first_transition_of_block)
transition target is moved to a new constellation
block_t * refinable_next
next block in the list of refinable blocks
static permutation_const_iter_t permutation_begin()
provide an iterator to the beginning of the permutation array
permutation_const_iter_t end() const
iterator past the last state in the block
void split_inert_to_C(block_t *B)
handle the transitions from the splitter to its own constellation
void set_inert_begin(B_to_C_iter_t new_inert_begin)
void replace_transition_system(bool branching, bool preserve_divergence)
void assert_stability(const part_state_t &part_st) const
assert that the data structure is consistent and stable
bisim_gjkw::bisim_partitioner_gjkw_initialise_helper< LTS_TYPE > init_helper
const constln_t * to_constln() const
compute the goal constellation of the transitions in this slice
static state_type nr_of_blocks
total number of blocks with unique sequence number allocated
state_type unmarked_bottom_size() const
provides the number of unmarked bottom states in the block
void replace_transition_system(const part_state_t &part_st, ONLY_IF_DEBUG(bool branching,) bool preserve_divergence)
Replaces the transition relation of the current LTS by the transitions of the bisimulation-reduced tr...
bool split_s_inert_out(state_info_ptr s ONLY_IF_DEBUG(, constln_t *OldC))
Split outgoing transitions of a state in the splitter.
void set_marked_bottom_begin(permutation_iter_t new_marked_bottom_begin)
void SetFromRed(B_to_C_desc_iter_t new_fromred)
set FromRed to an existing element in to_constln
void make_nontrivial()
makes a constellation non-trivial (i. e. inserts it into the respective list)
permutation_const_iter_t nonbottom_begin() const
iterator to the first non-bottom state in the block
pred_const_iter_t inert_pred_end() const
iterator one past the last inert incoming transition
static succ_const_iter_t slice_end(succ_const_iter_t this_)
const block_t * from_block() const
compute the source block of the transitions in this slice
block_t * split_off_small_block()
split off a single block from the constellation
bisim_gjkw::block_t * postprocess_new_bottom(bisim_gjkw::block_t *RedB)
Split a block with new bottom states as needed.
B_to_C_iter_t postprocess_begin
iterator to the first transition into this constellation that needs postprocessing
bool add_work_to_bottom_transns(enum check_complexity::counter_type ctr, unsigned max_value)
bool operator>(const constln_t &other) const
const constln_t * constln() const
get constellation where the state belongs
permutation_const_iter_t begin() const
iterator to the first state in the block
void make_trivial()
makes a constellation trivial (i. e. removes it from the respective list)
void swap_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2)
succ_iter_t state_inert_out_end
iterator past the last inert outgoing transition
B_to_C_descriptor(B_to_C_iter_t begin_, B_to_C_iter_t end_)
bool surely_has_no_transition_to(const constln_t *SpC) const
bool needs_postprocessing() const
returns true iff the slice is marked for postprocessing
void set_begin(permutation_iter_t new_begin)
permutation_const_iter_t marked_nonbottom_begin() const
iterator to the first marked non-bottom state in the block
permutation_iter_t pos
position of the state in the permutation array
state_type get_eq_class(state_type s) const
static constln_t * nontrivial_first
first constellation in the list of non-trivial constellations
bool operator>=(const constln_t &other) const
permutation_const_iter_t end() const
constant iterator past the last state in the constellation
permutation_const_iter_t unmarked_bottom_begin() const
iterator to the first unmarked bottom state in the block
void set_inert_begin_and_end(B_to_C_iter_t new_inert_begin, B_to_C_iter_t new_inert_end)
B_to_C_const_iter_t inert_begin() const
iterator to the first inert transition of the block
void make_nonrefinable()
makes a block non-refinable (i. e. removes it from the respective list)
permutation_const_iter_t marked_bottom_begin() const
iterator to the first marked bottom state in the block
pred_const_iter_t noninert_pred_begin() const
iterator to first non-inert incoming transition
bool mark_nonbottom(state_info_ptr s)
mark a non-bottom state
permutation_const_iter_t bottom_begin() const
iterator to the first bottom state in the block
std::string debug_id_short() const
print a short state identification for debugging
permutation_iter_t int_marked_bottom_begin
iterator to the first marked bottom state of the block
void swap_out(pred_iter_t const pos1, pred_iter_t const pos2)
state_type size() const
provides the number of states in the block
void init_transitions(part_state_t &part_st, part_trans_t &part_tr, bool branching, bool preserve_divergence)
initialise the state in part_st and the transitions in part_tr
permutation_iter_t int_begin
iterator to the first state in the constellation
succ_iter_t int_current_constln
iterator to first outgoing transition to the constellation of interest
block_t * split_off_blue(permutation_iter_t blue_nonbottom_end)
refine the block (the blue subblock is smaller)
permutation_iter_t int_bottom_begin
iterator to the first bottom state of the block
permutation_const_iter_t marked_bottom_end() const
iterator past the last marked bottom state in the block
void set_slice_begin_or_before_end(succ_iter_t new_value)
state_type notblue
number of inert transitions to non-blue states
permutation_const_iter_t marked_nonbottom_end() const
iterator one past the last marked non-bottom state in the block
check_complexity::state_counter_t work_counter
const state_type sort_key
sort key to order constellation-related information
state_type marked_bottom_size() const
provides the number of marked bottom states in the block
bool is_trivial() const
returns true iff the constellation is trivial
permutation_iter_t int_marked_nonbottom_begin
iterator to the first marked non-bottom state of the block
void make_noninert(succ_iter_t const succ_iter)
permutation_iter_t int_end
iterator past the last state of the block
B_to_C_desc_list to_constln
list of B_to_C with transitions from this block
state_type get_nr_of_states() const
provides the number of states in the Kripke structure
static block_t * get_some_refinable()
provides an arbitrary refinable block
static succ_iter_t slice_end(succ_iter_t this_)
block_t * block
block where the state belongs
void create_initial_partition_gjkw(bool branching, bool preserve_divergence)
const constln_t * get_nontrivial_next() const
provides the next non-trivial constellation
void set_constln(constln_t *new_constln)
void set_marked_nonbottom_begin(permutation_iter_t new_marked_nonbottom_begin)
#define BLOCK_NO_SEQNR
static permutation_const_iter_t perm_begin
bool operator<(const constln_t &other) const
compares two constellations for ordering them
bool make_refinable()
makes a block refinable (i. e. inserts it into the respective list)
fixed_vector< state_info_entry > state_info
array with all other information about states
state_type state_size() const
provide size of state space
state_type size() const
returns number of states in the constellation
B_to_C_const_iter_t inert_end() const
iterator past the last inert transition of the block
const constln_t * constln() const
constellation where the block belongs to
constln_t * int_constln
constellation to which the block belongs
permutation_const_iter_t bottom_end() const
iterator past the last bottom state in the block
static block_t * refinable_first
first block in the list of refinable blocks
static void slice_add_work_to_transns(succ_const_iter_t this_, enum check_complexity::counter_type ctr, unsigned max_value)
void swap_in(B_to_C_iter_t const pos1, B_to_C_iter_t const pos2)
state_type int_seqnr
unique sequence number of this block
succ_const_iter_t succ_begin() const
iterator to first outgoing transition
bool operator<=(const constln_t &other) const
void new_red_block_created(block_t *OldB, block_t *NewB, bool postprocessing)
handle B_to_C slices after a new red block has been created
void set_end(permutation_iter_t new_end)
void print_trans() const
print all transitions
bool is_refinable() const
checks whether the block is refinable
block_t * split_off_red(permutation_iter_t red_nonbottom_begin)
refine the block (the red subblock is smaller)
succ_iter_t int_slice_begin_or_before_end
points to the last or the first transition to the same constellation
succ_const_iter_t inert_succ_begin() const
iterator to first inert outgoing transition
permutation_const_iter_t begin() const
constant iterator to the first state in the constellation
pred_iter_t state_in_begin
iterator to first incoming transition
permutation_iter_t int_begin
iterator to the first state of the block
pred_iter_t state_inert_in_begin
iterator to first inert incoming transition
void assign_seqnr()
assigns a unique sequence number
std::unordered_map< Key, state_type, KeyHasher > extra_kripke_states
void new_blue_block_created(block_t *OldB, block_t *NewB)
handle B_to_C slices after a new blue block has been created
permutation_iter_t begin()
iterator to the first state in the constellation
static state_info_const_ptr s_i_begin
pointer at the first entry in the state_info array
check_complexity::B_to_C_counter_t work_counter
static constln_t * get_some_nontrivial()
provides an arbitrary non-trivial constellation
permutation_const_iter_t unmarked_bottom_end() const
iterator past the last unmarked bottom state in the block
bool operator<(const block_t &other) const
compares two blocks for ordering them
void set_bottom_begin(permutation_iter_t new_bottom_begin)
void set_nonbottom_end(permutation_iter_t new_nonbottom_end)
std::string debug_id() const
print a state identification for debugging
void set_inert_pred_begin(pred_iter_t new_inert_in_begin)
void clear()
deallocates constellations and blocks
bisim_gjkw::block_t * refine(bisim_gjkw::block_t *RfnB, const bisim_gjkw::constln_t *SpC, const bisim_gjkw::B_to_C_descriptor *FromRed, bool postprocessing ONLY_IF_DEBUG(, const bisim_gjkw::constln_t *NewC=nullptr))
refine a block into the part that can reach SpC and the part that cannot
constln_t(state_type sort_key_, permutation_iter_t begin_, permutation_iter_t end_, B_to_C_iter_t postprocess_none)
constructor
void set_inert_succ_begin_and_end(succ_iter_t new_inert_out_begin, succ_iter_t new_inert_out_end)
void swap3_B_to_C(succ_iter_t const pos1, succ_iter_t const pos2, succ_iter_t const pos3)
block_t(constln_t *const constln_, permutation_iter_t const begin_, permutation_iter_t const end_)
constructor
const block_t * block(state_type s) const
find block of a state
succ_const_iter_t inert_succ_end() const
iterator past the last inert outgoing transition
permutation_iter_t end()
iterator past the last state in the constellation
succ_const_iter_t slice_begin_or_before_end() const
check_complexity::block_counter_t work_counter
succ_iter_t state_out_begin
iterator to first outgoing transition
pred_const_iter_t inert_pred_begin() const
iterator to first inert incoming transition
std::string debug_id() const
print a transition identification for debugging
B_to_C_iter_t int_inert_begin
iterator to the first inert transition of the block
void set_unmarked_bottom_end(permutation_iter_t new_unmarked_bottom_end)
pred_const_iter_t noninert_pred_end() const
iterator past the last non-inert incoming transition
void set_inert_end(B_to_C_iter_t new_inert_end)
pred_const_iter_t pred_end() const
iterator past the last incoming transition
constln_t * nontrivial_next
next constellation in the list of non-trivial constellations
bool in_same_class(state_type s, state_type t) const
B_to_C_iter_t int_inert_end
iterator past the last inert transition of the block
static state_info_const_ptr s_i_end
pointer past the last actual entry in the state_info array
permutation_const_iter_t unmarked_nonbottom_begin() const
iterator to the first unmarked non-bottom state in the block
void set_end(permutation_iter_t new_end)
set the iterator past the last state in the constellation
permutation_const_iter_t nonbottom_end() const
iterator past the last non-bottom state in the block
succ_const_iter_t succ_end() const
iterator past the last outgoing transition
void set_unmarked_nonbottom_end(permutation_iter_t new_unmarked_nonbottom_end)
B_to_C_descriptor * FromRed(const constln_t *SpC)
read FromRed
std::string debug_id_short() const
print a short transition identification for debugging
permutation_const_iter_t unmarked_nonbottom_end() const
iterator past the last unmarked non-bottom state in the block
void print_block(const char *message, const block_t *B, permutation_const_iter_t begin, permutation_const_iter_t end) const
print a slice of the partition (typically a block)
state_type marked_size() const
provides the number of marked states in the block
B_to_C_iter_t postprocess_end
iterator past the last transition into this constellation that needs postprocessing
trans_type get_nr_of_transitions() const
provides the number of transitions in the Kripke structure
void print_part(const part_trans_t &part_tr) const
print the partition as a tree (per constellation and block)
permutation_iter_t int_end
iterator past the last state in the constellation
void set_current_constln(succ_iter_t const new_current_constln)
void set_inert_succ_begin(succ_iter_t const new_inert_out_begin)
bool mark(state_info_ptr s)
mark a state
succ_iter_t state_inert_out_begin
iterator to first inert outgoing transition
pred_const_iter_t pred_begin() const
iterator to first incoming transition
bool surely_has_transition_to(const constln_t *SpC) const
void set_begin(permutation_iter_t new_begin)
set the iterator to the first state in the constellation
#define ONLY_IF_DEBUG(...)
include something in Debug mode
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
@ warning
Definition logger.h:32
const state_info_entry * state_info_const_ptr
fixed_vector< pred_entry >::iterator pred_iter_t
fixed_vector< succ_entry >::const_iterator succ_const_iter_t
permutation_t::iterator permutation_iter_t
fixed_vector< pred_entry >::const_iterator pred_const_iter_t
fixed_vector< state_info_ptr > permutation_t
permutation_t::const_iterator permutation_const_iter_t
std::list< B_to_C_descriptor > B_to_C_desc_list
B_to_C_desc_list::const_iterator B_to_C_desc_const_iter_t
B_to_C_desc_list::iterator B_to_C_desc_iter_t
fixed_vector< B_to_C_entry >::iterator B_to_C_iter_t
fixed_vector< succ_entry >::iterator succ_iter_t
fixed_vector< B_to_C_entry >::const_iterator B_to_C_const_iter_t
static void swap_permutation(permutation_iter_t s1, permutation_iter_t s2)
swap two permutations
void merge(LTS_TYPE &l1, const LTS_TYPE &l2)
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
std::size_t trans_type
type used to store transition (numbers and) counts
void scc_reduce(LTS_TYPE &l, const bool preserve_divergence_loops=false)
Definition liblts_scc.h:362
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