spot 2.11.5.dev
acc.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2014-2023 Laboratoire de Recherche et Développement
3// de l'Epita.
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <functional>
23#include <sstream>
24#include <vector>
25#include <iostream>
26#include <algorithm>
27#include <numeric>
28#include <bddx.h>
29#include <tuple>
30#include <spot/misc/_config.h>
31#include <spot/misc/bitset.hh>
32#include <spot/misc/trival.hh>
33
34namespace spot
35{
36 namespace internal
37 {
38 class mark_container;
39
40 template<bool>
41 struct _32acc {};
42 template<>
43 struct _32acc<true>
44 {
45 SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t")
46 typedef unsigned value_t;
47 };
48 }
49
52
61 class SPOT_API acc_cond
62 {
63
64 public:
65 bool
66 has_parity_prefix(acc_cond& new_acc, std::vector<unsigned>& colors) const;
67
68#ifndef SWIG
69 private:
70 [[noreturn]] static void report_too_many_sets();
71#endif
72 public:
73
88 struct mark_t :
89 public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
90 {
91 private:
92 // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
93 typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
94 _value_t id;
95
96 mark_t(_value_t id) noexcept
97 : id(id)
98 {
99 }
100
101 public:
103 mark_t() = default;
104
105 mark_t
106 apply_permutation(std::vector<unsigned> permut);
107
108
109#ifndef SWIG
111 template<class iterator>
112 mark_t(const iterator& begin, const iterator& end)
113 : mark_t(_value_t::zero())
114 {
115 for (iterator i = begin; i != end; ++i)
116 if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
117 set(*i);
118 else
119 report_too_many_sets();
120 }
121
123 mark_t(std::initializer_list<unsigned> vals)
124 : mark_t(vals.begin(), vals.end())
125 {
126 }
127
128 SPOT_DEPRECATED("use brace initialization instead")
129 mark_t(unsigned i)
130 {
131 unsigned j = 0;
132 while (i)
133 {
134 if (i & 1U)
135 this->set(j);
136 ++j;
137 i >>= 1;
138 }
139 }
140#endif
141
147 constexpr static unsigned max_accsets()
148 {
149 return SPOT_MAX_ACCSETS;
150 }
151
157 static mark_t all()
158 {
159 return mark_t(_value_t::mone());
160 }
161
162 size_t hash() const noexcept
163 {
164 std::hash<decltype(id)> h;
165 return h(id);
166 }
167
168 SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
169 bool operator==(unsigned o) const
170 {
171 SPOT_ASSERT(o == 0U);
172 (void)o;
173 return !id;
174 }
175
176 SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
177 bool operator!=(unsigned o) const
178 {
179 SPOT_ASSERT(o == 0U);
180 (void)o;
181 return !!id;
182 }
183
184 bool operator==(mark_t o) const
185 {
186 return id == o.id;
187 }
188
189 bool operator!=(mark_t o) const
190 {
191 return id != o.id;
192 }
193
194 bool operator<(mark_t o) const
195 {
196 return id < o.id;
197 }
198
199 bool operator<=(mark_t o) const
200 {
201 return id <= o.id;
202 }
203
204 bool operator>(mark_t o) const
205 {
206 return id > o.id;
207 }
208
209 bool operator>=(mark_t o) const
210 {
211 return id >= o.id;
212 }
213
214 explicit operator bool() const
215 {
216 return !!id;
217 }
218
219 bool has(unsigned u) const
220 {
221 return !!this->operator&(mark_t({0}) << u);
222 }
223
224 void set(unsigned u)
225 {
226 id.set(u);
227 }
228
229 void clear(unsigned u)
230 {
231 id.clear(u);
232 }
233
234 mark_t& operator&=(mark_t r)
235 {
236 id &= r.id;
237 return *this;
238 }
239
240 mark_t& operator|=(mark_t r)
241 {
242 id |= r.id;
243 return *this;
244 }
245
246 mark_t& operator-=(mark_t r)
247 {
248 id &= ~r.id;
249 return *this;
250 }
251
252 mark_t& operator^=(mark_t r)
253 {
254 id ^= r.id;
255 return *this;
256 }
257
258 mark_t operator&(mark_t r) const
259 {
260 return id & r.id;
261 }
262
263 mark_t operator|(mark_t r) const
264 {
265 return id | r.id;
266 }
267
268 mark_t operator-(mark_t r) const
269 {
270 return id & ~r.id;
271 }
272
273 mark_t operator~() const
274 {
275 return ~id;
276 }
277
278 mark_t operator^(mark_t r) const
279 {
280 return id ^ r.id;
281 }
282
283#if SPOT_DEBUG || defined(SWIGPYTHON)
284# define SPOT_WRAP_OP(ins) \
285 try \
286 { \
287 ins; \
288 } \
289 catch (const std::runtime_error& e) \
290 { \
291 report_too_many_sets(); \
292 }
293#else
294# define SPOT_WRAP_OP(ins) ins;
295#endif
296 mark_t operator<<(unsigned i) const
297 {
298 SPOT_WRAP_OP(return id << i);
299 }
300
301 mark_t& operator<<=(unsigned i)
302 {
303 SPOT_WRAP_OP(id <<= i; return *this);
304 }
305
306 mark_t operator>>(unsigned i) const
307 {
308 SPOT_WRAP_OP(return id >> i);
309 }
310
311 mark_t& operator>>=(unsigned i)
312 {
313 SPOT_WRAP_OP(id >>= i; return *this);
314 }
315#undef SPOT_WRAP_OP
316
317 mark_t strip(mark_t y) const
318 {
319 // strip every bit of id that is marked in y
320 // 100101110100.strip(
321 // 001011001000)
322 // == 10 1 11 100
323 // == 10111100
324
325 auto xv = id; // 100101110100
326 auto yv = y.id; // 001011001000
327
328 while (yv && xv)
329 {
330 // Mask for everything after the last 1 in y
331 auto rm = (~yv) & (yv - 1); // 000000000111
332 // Mask for everything before the last 1 in y
333 auto lm = ~(yv ^ (yv - 1)); // 111111110000
334 xv = ((xv & lm) >> 1) | (xv & rm);
335 yv = (yv & lm) >> 1;
336 }
337 return xv;
338 }
339
342 bool subset(mark_t m) const
343 {
344 return !((*this) - m);
345 }
346
349 bool proper_subset(mark_t m) const
350 {
351 return *this != m && this->subset(m);
352 }
353
355 unsigned count() const
356 {
357 return id.count();
358 }
359
364 unsigned max_set() const
365 {
366 if (id)
367 return id.highest()+1;
368 else
369 return 0;
370 }
371
376 unsigned min_set() const
377 {
378 if (id)
379 return id.lowest()+1;
380 else
381 return 0;
382 }
383
389 {
390 return id & -id;
391 }
392
394 bool is_singleton() const
395 {
396#if __GNUC__
397 /* With GCC and Clang, count() is implemented using popcount. */
398 return count() == 1;
399#else
400 return id && !(id & (id - 1));
401#endif
402 }
403
405 bool has_many() const
406 {
407#if __GNUC__
408 /* With GCC and Clang, count() is implemented using popcount. */
409 return count() > 1;
410#else
411 return !!(id & (id - 1));
412#endif
413 }
414
418 mark_t& remove_some(unsigned n)
419 {
420 while (n--)
421 id &= id - 1;
422 return *this;
423 }
424
426 template<class iterator>
427 void fill(iterator here) const
428 {
429 auto a = *this;
430 unsigned level = 0;
431 while (a)
432 {
433 if (a.has(0))
434 *here++ = level;
435 ++level;
436 a >>= 1;
437 }
438 }
439
442
443 SPOT_API
444 friend std::ostream& operator<<(std::ostream& os, mark_t m);
445
446 std::string as_string() const
447 {
448 std::ostringstream os;
449 os << *this;
450 return os.str();
451 }
452 };
453
455 enum class acc_op : unsigned short
456 { Inf, Fin, InfNeg, FinNeg, And, Or };
457
466 {
467 mark_t mark;
468 struct {
469 acc_op op; // Operator
470 unsigned short size; // Size of the subtree (number of acc_word),
471 // not counting this node.
472 } sub;
473 };
474
487 struct SPOT_API acc_code: public std::vector<acc_word>
488 {
490 unit_propagation();
491
492 bool
493 has_parity_prefix(acc_cond& new_cond,
494 std::vector<unsigned>& colors) const;
495
496 bool
497 is_parity_max_equiv(std::vector<int>& permut,
498 unsigned new_color,
499 bool even) const;
500
501 bool operator==(const acc_code& other) const
502 {
503 unsigned pos = size();
504 if (other.size() != pos)
505 return false;
506 while (pos > 0)
507 {
508 auto op = (*this)[pos - 1].sub.op;
509 auto sz = (*this)[pos - 1].sub.size;
510 if (other[pos - 1].sub.op != op ||
511 other[pos - 1].sub.size != sz)
512 return false;
513 switch (op)
514 {
515 case acc_cond::acc_op::And:
516 case acc_cond::acc_op::Or:
517 --pos;
518 break;
519 case acc_cond::acc_op::Inf:
520 case acc_cond::acc_op::InfNeg:
521 case acc_cond::acc_op::Fin:
522 case acc_cond::acc_op::FinNeg:
523 pos -= 2;
524 if (other[pos].mark != (*this)[pos].mark)
525 return false;
526 break;
527 }
528 }
529 return true;
530 };
531
532 bool operator<(const acc_code& other) const
533 {
534 unsigned pos = size();
535 auto osize = other.size();
536 if (pos < osize)
537 return true;
538 if (pos > osize)
539 return false;
540 while (pos > 0)
541 {
542 auto op = (*this)[pos - 1].sub.op;
543 auto oop = other[pos - 1].sub.op;
544 if (op < oop)
545 return true;
546 if (op > oop)
547 return false;
548 auto sz = (*this)[pos - 1].sub.size;
549 auto osz = other[pos - 1].sub.size;
550 if (sz < osz)
551 return true;
552 if (sz > osz)
553 return false;
554 switch (op)
555 {
556 case acc_cond::acc_op::And:
557 case acc_cond::acc_op::Or:
558 --pos;
559 break;
560 case acc_cond::acc_op::Inf:
561 case acc_cond::acc_op::InfNeg:
562 case acc_cond::acc_op::Fin:
563 case acc_cond::acc_op::FinNeg:
564 {
565 pos -= 2;
566 auto m = (*this)[pos].mark;
567 auto om = other[pos].mark;
568 if (m < om)
569 return true;
570 if (m > om)
571 return false;
572 break;
573 }
574 }
575 }
576 return false;
577 }
578
579 bool operator>(const acc_code& other) const
580 {
581 return other < *this;
582 }
583
584 bool operator<=(const acc_code& other) const
585 {
586 return !(other < *this);
587 }
588
589 bool operator>=(const acc_code& other) const
590 {
591 return !(*this < other);
592 }
593
594 bool operator!=(const acc_code& other) const
595 {
596 return !(*this == other);
597 }
598
603 bool is_t() const
604 {
605 // We store "t" as an empty condition, or as Inf({}).
606 unsigned s = size();
607 return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
608 && !((*this)[s - 2].mark));
609 }
610
617 bool is_f() const
618 {
619 // We store "f" as Fin({}).
620 unsigned s = size();
621 return s > 1
622 && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
623 }
624
631 static acc_code f()
632 {
633 acc_code res;
634 res.resize(2);
635 res[0].mark = {};
636 res[1].sub.op = acc_op::Fin;
637 res[1].sub.size = 1;
638 return res;
639 }
640
645 static acc_code t()
646 {
647 return {};
648 }
649
658 {
659 acc_code res;
660 res.resize(2);
661 res[0].mark = m;
662 res[1].sub.op = acc_op::Fin;
663 res[1].sub.size = 1;
664 return res;
665 }
666
667 static acc_code fin(std::initializer_list<unsigned> vals)
668 {
669 return fin(mark_t(vals));
670 }
672
690 {
691 acc_code res;
692 res.resize(2);
693 res[0].mark = m;
694 res[1].sub.op = acc_op::FinNeg;
695 res[1].sub.size = 1;
696 return res;
697 }
698
699 static acc_code fin_neg(std::initializer_list<unsigned> vals)
700 {
701 return fin_neg(mark_t(vals));
702 }
704
714 {
715 acc_code res;
716 res.resize(2);
717 res[0].mark = m;
718 res[1].sub.op = acc_op::Inf;
719 res[1].sub.size = 1;
720 return res;
721 }
722
723 static acc_code inf(std::initializer_list<unsigned> vals)
724 {
725 return inf(mark_t(vals));
726 }
728
746 {
747 acc_code res;
748 res.resize(2);
749 res[0].mark = m;
750 res[1].sub.op = acc_op::InfNeg;
751 res[1].sub.size = 1;
752 return res;
753 }
754
755 static acc_code inf_neg(std::initializer_list<unsigned> vals)
756 {
757 return inf_neg(mark_t(vals));
758 }
760
765 {
766 return inf({0});
767 }
768
773 {
774 return fin({0});
775 }
776
782 static acc_code generalized_buchi(unsigned n)
783 {
784 if (n == 0)
785 return inf({});
786 acc_cond::mark_t m = mark_t::all();
787 m >>= mark_t::max_accsets() - n;
788 return inf(m);
789 }
790
797 {
798 if (n == 0)
799 return fin({});
800 acc_cond::mark_t m = mark_t::all();
801 m >>= mark_t::max_accsets() - n;
802 return fin(m);
803 }
804
809 static acc_code rabin(unsigned n)
810 {
811 acc_cond::acc_code res = f();
812 while (n > 0)
813 {
814 res |= inf({2*n - 1}) & fin({2*n - 2});
815 --n;
816 }
817 return res;
818 }
819
824 static acc_code streett(unsigned n)
825 {
826 acc_cond::acc_code res = t();
827 while (n > 0)
828 {
829 res &= inf({2*n - 1}) | fin({2*n - 2});
830 --n;
831 }
832 return res;
833 }
834
847 template<class Iterator>
848 static acc_code generalized_rabin(Iterator begin, Iterator end)
849 {
850 acc_cond::acc_code res = f();
851 unsigned n = 0;
852 for (Iterator i = begin; i != end; ++i)
853 {
854 unsigned f = n++;
855 acc_cond::mark_t m = {};
856 for (unsigned ni = *i; ni > 0; --ni)
857 m.set(n++);
858 auto pair = inf(m) & fin({f});
859 std::swap(pair, res);
860 res |= std::move(pair);
861 }
862 return res;
863 }
864
872 static acc_code parity(bool is_max, bool is_odd, unsigned sets);
873 static acc_code parity_max(bool is_odd, unsigned sets)
874 {
875 return parity(true, is_odd, sets);
876 }
877 static acc_code parity_max_odd(unsigned sets)
878 {
879 return parity_max(true, sets);
880 }
881 static acc_code parity_max_even(unsigned sets)
882 {
883 return parity_max(false, sets);
884 }
885 static acc_code parity_min(bool is_odd, unsigned sets)
886 {
887 return parity(false, is_odd, sets);
888 }
889 static acc_code parity_min_odd(unsigned sets)
890 {
891 return parity_min(true, sets);
892 }
893 static acc_code parity_min_even(unsigned sets)
894 {
895 return parity_min(false, sets);
896 }
898
915 static acc_code random(unsigned n, double reuse = 0.0);
916
919 {
920 if (is_t() || r.is_f())
921 {
922 *this = r;
923 return *this;
924 }
925 if (is_f() || r.is_t())
926 return *this;
927 unsigned s = size() - 1;
928 unsigned rs = r.size() - 1;
929 // We want to group all Inf(x) operators:
930 // Inf(a) & Inf(b) = Inf(a & b)
931 if (((*this)[s].sub.op == acc_op::Inf
932 && r[rs].sub.op == acc_op::Inf)
933 || ((*this)[s].sub.op == acc_op::InfNeg
934 && r[rs].sub.op == acc_op::InfNeg))
935 {
936 (*this)[s - 1].mark |= r[rs - 1].mark;
937 return *this;
938 }
939
940 // In the more complex scenarios, left and right may both
941 // be conjunctions, and Inf(x) might be a member of each
942 // side. Find it if it exists.
943 // left_inf points to the left Inf mark if any.
944 // right_inf points to the right Inf mark if any.
945 acc_word* left_inf = nullptr;
946 if ((*this)[s].sub.op == acc_op::And)
947 {
948 auto start = &(*this)[s] - (*this)[s].sub.size;
949 auto pos = &(*this)[s] - 1;
950 pop_back();
951 while (pos > start)
952 {
953 if (pos->sub.op == acc_op::Inf)
954 {
955 left_inf = pos - 1;
956 break;
957 }
958 pos -= pos->sub.size + 1;
959 }
960 }
961 else if ((*this)[s].sub.op == acc_op::Inf)
962 {
963 left_inf = &(*this)[s - 1];
964 }
965
966 const acc_word* right_inf = nullptr;
967 auto right_end = &r.back();
968 if (right_end->sub.op == acc_op::And)
969 {
970 auto start = &r[0];
971 auto pos = --right_end;
972 while (pos > start)
973 {
974 if (pos->sub.op == acc_op::Inf)
975 {
976 right_inf = pos - 1;
977 break;
978 }
979 pos -= pos->sub.size + 1;
980 }
981 }
982 else if (right_end->sub.op == acc_op::Inf)
983 {
984 right_inf = right_end - 1;
985 }
986
987 acc_cond::mark_t carry = {};
988 if (left_inf && right_inf)
989 {
990 carry = left_inf->mark;
991 auto pos = left_inf - &(*this)[0];
992 erase(begin() + pos, begin() + pos + 2);
993 }
994 auto sz = size();
995 insert(end(), &r[0], right_end + 1);
996 if (carry)
997 (*this)[sz + (right_inf - &r[0])].mark |= carry;
998
999 acc_word w;
1000 w.sub.op = acc_op::And;
1001 w.sub.size = size();
1002 emplace_back(w);
1003 return *this;
1004 }
1005
1008 {
1009 acc_code res = *this;
1010 res &= r;
1011 return res;
1012 }
1013
1014#ifndef SWIG
1017 {
1018 acc_code res = *this;
1019 res &= r;
1020 return res;
1021 }
1022#endif // SWIG
1023
1026 {
1027 if (is_t() || r.is_f())
1028 return *this;
1029 if (is_f() || r.is_t())
1030 {
1031 *this = r;
1032 return *this;
1033 }
1034 unsigned s = size() - 1;
1035 unsigned rs = r.size() - 1;
1036 // Fin(a) | Fin(b) = Fin(a | b)
1037 if (((*this)[s].sub.op == acc_op::Fin
1038 && r[rs].sub.op == acc_op::Fin)
1039 || ((*this)[s].sub.op == acc_op::FinNeg
1040 && r[rs].sub.op == acc_op::FinNeg))
1041 {
1042 (*this)[s - 1].mark |= r[rs - 1].mark;
1043 return *this;
1044 }
1045
1046 // In the more complex scenarios, left and right may both
1047 // be disjunctions, and Fin(x) might be a member of each
1048 // side. Find it if it exists.
1049 // left_inf points to the left Inf mark if any.
1050 // right_inf points to the right Inf mark if any.
1051 acc_word* left_fin = nullptr;
1052 if ((*this)[s].sub.op == acc_op::Or)
1053 {
1054 auto start = &(*this)[s] - (*this)[s].sub.size;
1055 auto pos = &(*this)[s] - 1;
1056 pop_back();
1057 while (pos > start)
1058 {
1059 if (pos->sub.op == acc_op::Fin)
1060 {
1061 left_fin = pos - 1;
1062 break;
1063 }
1064 pos -= pos->sub.size + 1;
1065 }
1066 }
1067 else if ((*this)[s].sub.op == acc_op::Fin)
1068 {
1069 left_fin = &(*this)[s - 1];
1070 }
1071
1072 const acc_word* right_fin = nullptr;
1073 auto right_end = &r.back();
1074 if (right_end->sub.op == acc_op::Or)
1075 {
1076 auto start = &r[0];
1077 auto pos = --right_end;
1078 while (pos > start)
1079 {
1080 if (pos->sub.op == acc_op::Fin)
1081 {
1082 right_fin = pos - 1;
1083 break;
1084 }
1085 pos -= pos->sub.size + 1;
1086 }
1087 }
1088 else if (right_end->sub.op == acc_op::Fin)
1089 {
1090 right_fin = right_end - 1;
1091 }
1092
1093 acc_cond::mark_t carry = {};
1094 if (left_fin && right_fin)
1095 {
1096 carry = left_fin->mark;
1097 auto pos = (left_fin - &(*this)[0]);
1098 this->erase(begin() + pos, begin() + pos + 2);
1099 }
1100 auto sz = size();
1101 insert(end(), &r[0], right_end + 1);
1102 if (carry)
1103 (*this)[sz + (right_fin - &r[0])].mark |= carry;
1104 acc_word w;
1105 w.sub.op = acc_op::Or;
1106 w.sub.size = size();
1107 emplace_back(w);
1108 return *this;
1109 }
1110
1111#ifndef SWIG
1114 {
1115 acc_code res = *this;
1116 res |= r;
1117 return res;
1118 }
1119#endif // SWIG
1120
1123 {
1124 acc_code res = *this;
1125 res |= r;
1126 return res;
1127 }
1128
1134 acc_code& operator<<=(unsigned sets)
1135 {
1136 if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1137 report_too_many_sets();
1138 if (empty())
1139 return *this;
1140 unsigned pos = size();
1141 do
1142 {
1143 switch ((*this)[pos - 1].sub.op)
1144 {
1145 case acc_cond::acc_op::And:
1146 case acc_cond::acc_op::Or:
1147 --pos;
1148 break;
1149 case acc_cond::acc_op::Inf:
1150 case acc_cond::acc_op::InfNeg:
1151 case acc_cond::acc_op::Fin:
1152 case acc_cond::acc_op::FinNeg:
1153 pos -= 2;
1154 (*this)[pos].mark <<= sets;
1155 break;
1156 }
1157 }
1158 while (pos > 0);
1159 return *this;
1160 }
1161
1165 acc_code operator<<(unsigned sets) const
1166 {
1167 acc_code res = *this;
1168 res <<= sets;
1169 return res;
1170 }
1171
1178 bool is_dnf() const;
1179
1186 bool is_cnf() const;
1187
1199
1207
1212 bdd to_bdd(const bdd* map) const;
1213
1222 std::vector<acc_code> top_disjuncts() const;
1223
1232 std::vector<acc_code> top_conjuncts() const;
1233
1245
1258
1271
1276 int fin_one() const;
1277
1298 std::pair<int, acc_code> fin_one_extract() const;
1299
1318 std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1320 std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1323
1336 std::vector<std::vector<int>>
1337 missing(mark_t inf, bool accepting) const;
1338
1341 bool accepting(mark_t inf) const;
1342
1348 bool inf_satisfiable(mark_t inf) const;
1349
1362 mark_t always_present) const;
1363
1374 std::vector<unsigned> symmetries() const;
1375
1389 acc_code remove(acc_cond::mark_t rem, bool missing) const;
1390
1395 acc_code strip(acc_cond::mark_t rem, bool missing) const;
1398
1401
1413 std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
1415
1423
1425 std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1426
1431 std::ostream&
1432 to_html(std::ostream& os,
1433 std::function<void(std::ostream&, int)>
1434 set_printer = nullptr) const;
1435
1440 std::ostream&
1441 to_text(std::ostream& os,
1442 std::function<void(std::ostream&, int)>
1443 set_printer = nullptr) const;
1444
1449 std::ostream&
1450 to_latex(std::ostream& os,
1451 std::function<void(std::ostream&, int)>
1452 set_printer = nullptr) const;
1453
1476 acc_code(const char* input);
1477
1482 {
1483 }
1484
1486 acc_code(const acc_word* other)
1487 : std::vector<acc_word>(other - other->sub.size, other + 1)
1488 {
1489 }
1490
1492 SPOT_API
1493 friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1494 };
1495
1503 acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1504 : num_(0U), all_({}), code_(code)
1505 {
1506 add_sets(n_sets);
1507 uses_fin_acceptance_ = check_fin_acceptance();
1508 }
1509
1514 acc_cond(const acc_code& code)
1515 : num_(0U), all_({}), code_(code)
1516 {
1517 add_sets(code.used_sets().max_set());
1518 uses_fin_acceptance_ = check_fin_acceptance();
1519 }
1520
1523 : num_(o.num_), all_(o.all_), code_(o.code_),
1524 uses_fin_acceptance_(o.uses_fin_acceptance_)
1525 {
1526 }
1527
1530 {
1531 num_ = o.num_;
1532 all_ = o.all_;
1533 code_ = o.code_;
1534 uses_fin_acceptance_ = o.uses_fin_acceptance_;
1535 return *this;
1536 }
1537
1538 ~acc_cond()
1539 {
1540 }
1541
1545 void set_acceptance(const acc_code& code)
1546 {
1547 code_ = code;
1548 uses_fin_acceptance_ = check_fin_acceptance();
1549 }
1550
1553 {
1554 return code_;
1555 }
1556
1559 {
1560 return code_;
1561 }
1562
1563 bool operator==(const acc_cond& other) const
1564 {
1565 return other.num_sets() == num_ && other.get_acceptance() == code_;
1566 }
1567
1568 bool operator!=(const acc_cond& other) const
1569 {
1570 return !(*this == other);
1571 }
1572
1575 {
1576 return uses_fin_acceptance_;
1577 }
1578
1580 bool is_t() const
1581 {
1582 return code_.is_t();
1583 }
1584
1589 bool is_all() const
1590 {
1591 return num_ == 0 && is_t();
1592 }
1593
1595 bool is_f() const
1596 {
1597 return code_.is_f();
1598 }
1599
1604 bool is_none() const
1605 {
1606 return num_ == 0 && is_f();
1607 }
1608
1613 bool is_buchi() const
1614 {
1615 unsigned s = code_.size();
1616 return num_ == 1 &&
1617 s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1618 }
1619
1624 bool is_co_buchi() const
1625 {
1626 return num_ == 1 && is_generalized_co_buchi();
1627 }
1628
1632 {
1633 set_acceptance(inf(all_sets()));
1634 }
1635
1639 {
1640 set_acceptance(fin(all_sets()));
1641 }
1642
1648 {
1649 unsigned s = code_.size();
1650 return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1651 && code_[0].mark == all_sets());
1652 }
1653
1659 {
1660 unsigned s = code_.size();
1661 return (s == 2 &&
1662 code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1663 }
1664
1676 int is_rabin() const;
1677
1689 int is_streett() const;
1690
1700 struct SPOT_API rs_pair
1701 {
1702#ifndef SWIG
1703 rs_pair() = default;
1704 rs_pair(const rs_pair&) = default;
1705 rs_pair& operator=(const rs_pair&) = default;
1706#endif
1707
1708 rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1709 fin(fin),
1710 inf(inf)
1711 {}
1712 acc_cond::mark_t fin;
1713 acc_cond::mark_t inf;
1714
1715 bool operator==(rs_pair o) const
1716 {
1717 return fin == o.fin && inf == o.inf;
1718 }
1719 bool operator!=(rs_pair o) const
1720 {
1721 return fin != o.fin || inf != o.inf;
1722 }
1723 bool operator<(rs_pair o) const
1724 {
1725 return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1726 }
1727 bool operator<=(rs_pair o) const
1728 {
1729 return !(o < *this);
1730 }
1731 bool operator>(rs_pair o) const
1732 {
1733 return o < *this;
1734 }
1735 bool operator>=(rs_pair o) const
1736 {
1737 return !(*this < o);
1738 }
1739 };
1750 bool is_streett_like(std::vector<rs_pair>& pairs) const;
1751
1762 bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1763
1773 bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1774
1787 bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1788
1798 bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1799
1800
1801 bool is_parity_max_equiv(std::vector<int>& permut, bool even) const;
1802
1805 bool is_parity() const
1806 {
1807 bool max;
1808 bool odd;
1809 return is_parity(max, odd);
1810 }
1811
1820 {
1821 return acc_cond(num_, code_.unit_propagation());
1822 }
1823
1824 // Return (true, m) if there exist some acceptance mark m that
1825 // does not satisfy the acceptance condition. Return (false, 0U)
1826 // otherwise.
1827 std::pair<bool, acc_cond::mark_t> unsat_mark() const
1828 {
1829 return sat_unsat_mark(false);
1830 }
1831 // Return (true, m) if there exist some acceptance mark m that
1832 // does satisfy the acceptance condition. Return (false, 0U)
1833 // otherwise.
1834 std::pair<bool, acc_cond::mark_t> sat_mark() const
1835 {
1836 return sat_unsat_mark(true);
1837 }
1838
1839 protected:
1840 bool check_fin_acceptance() const;
1841 std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1842
1843 public:
1852 static acc_code inf(mark_t mark)
1853 {
1854 return acc_code::inf(mark);
1855 }
1856
1857 static acc_code inf(std::initializer_list<unsigned> vals)
1858 {
1859 return inf(mark_t(vals.begin(), vals.end()));
1860 }
1862
1880 {
1881 return acc_code::inf_neg(mark);
1882 }
1883
1884 static acc_code inf_neg(std::initializer_list<unsigned> vals)
1885 {
1886 return inf_neg(mark_t(vals.begin(), vals.end()));
1887 }
1889
1897 static acc_code fin(mark_t mark)
1898 {
1899 return acc_code::fin(mark);
1900 }
1901
1902 static acc_code fin(std::initializer_list<unsigned> vals)
1903 {
1904 return fin(mark_t(vals.begin(), vals.end()));
1905 }
1907
1925 {
1926 return acc_code::fin_neg(mark);
1927 }
1928
1929 static acc_code fin_neg(std::initializer_list<unsigned> vals)
1930 {
1931 return fin_neg(mark_t(vals.begin(), vals.end()));
1932 }
1934
1939 unsigned add_sets(unsigned num)
1940 {
1941 if (num == 0)
1942 return -1U;
1943 unsigned j = num_;
1944 num += j;
1945 if (num > mark_t::max_accsets())
1946 report_too_many_sets();
1947 // Make sure we do not update if we raised an exception.
1948 num_ = num;
1949 all_ = all_sets_();
1950 return j;
1951 }
1952
1957 unsigned add_set()
1958 {
1959 return add_sets(1);
1960 }
1961
1963 mark_t mark(unsigned u) const
1964 {
1965 SPOT_ASSERT(u < num_sets());
1966 return mark_t({u});
1967 }
1968
1973 mark_t comp(const mark_t& l) const
1974 {
1975 return all_ ^ l;
1976 }
1977
1980 {
1981 return all_;
1982 }
1983
1984 acc_cond
1985 apply_permutation(std::vector<unsigned>permut)
1986 {
1987 return acc_cond(apply_permutation_aux(permut));
1988 }
1989
1990 acc_code
1991 apply_permutation_aux(std::vector<unsigned>permut)
1992 {
1993 auto conj = top_conjuncts();
1994 auto disj = top_disjuncts();
1995
1996 if (conj.size() > 1)
1997 {
1998 auto transformed = std::vector<acc_code>();
1999 for (auto elem : conj)
2000 transformed.push_back(elem.apply_permutation_aux(permut));
2001 std::sort(transformed.begin(), transformed.end());
2002 auto uniq = std::unique(transformed.begin(), transformed.end());
2003 auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(),
2004 [](acc_code c1, acc_code c2)
2005 {
2006 return c1 & c2;
2007 });
2008 return result;
2009 }
2010 else if (disj.size() > 1)
2011 {
2012 auto transformed = std::vector<acc_code>();
2013 for (auto elem : disj)
2014 transformed.push_back(elem.apply_permutation_aux(permut));
2015 std::sort(transformed.begin(), transformed.end());
2016 auto uniq = std::unique(transformed.begin(), transformed.end());
2017 auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(),
2018 [](acc_code c1, acc_code c2)
2019 {
2020 return c1 | c2;
2021 });
2022 return result;
2023 }
2024 else
2025 {
2026 if (code_.back().sub.op == acc_cond::acc_op::Fin)
2027 return fin(code_[0].mark.apply_permutation(permut));
2028 if (code_.back().sub.op == acc_cond::acc_op::Inf)
2029 return inf(code_[0].mark.apply_permutation(permut));
2030 }
2031 SPOT_ASSERT(false);
2032 return {};
2033 }
2034
2037 bool accepting(mark_t inf) const
2038 {
2039 return code_.accepting(inf);
2040 }
2041
2047 bool inf_satisfiable(mark_t inf) const
2048 {
2049 return code_.inf_satisfiable(inf);
2050 }
2051
2063 trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
2064 {
2065 return code_.maybe_accepting(infinitely_often, always_present);
2066 }
2067
2082
2083 // Deprecated since Spot 2.8
2084 SPOT_DEPRECATED("Use operator<< instead.")
2085 std::ostream& format(std::ostream& os, mark_t m) const
2086 {
2087 if (!m)
2088 return os;
2089 return os << m;
2090 }
2091
2092 // Deprecated since Spot 2.8
2093 SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
2094 std::string format(mark_t m) const
2095 {
2096 std::ostringstream os;
2097 if (m)
2098 os << m;
2099 return os.str();
2100 }
2101
2103 unsigned num_sets() const
2104 {
2105 return num_;
2106 }
2107
2115 template<class iterator>
2116 mark_t useless(iterator begin, iterator end) const
2117 {
2118 mark_t u = {}; // The set of useless sets
2119 for (unsigned x = 0; x < num_; ++x)
2120 {
2121 // Skip sets that are already known to be useless.
2122 if (u.has(x))
2123 continue;
2124 auto all = comp(u | mark_t({x}));
2125 // Iterate over all mark_t, and keep track of
2126 // set numbers that always appear with x.
2127 for (iterator y = begin; y != end; ++y)
2128 {
2129 const mark_t& v = *y;
2130 if (v.has(x))
2131 {
2132 all &= v;
2133 if (!all)
2134 break;
2135 }
2136 }
2137 u |= all;
2138 }
2139 return u;
2140 }
2141
2155 acc_cond remove(mark_t rem, bool missing) const
2156 {
2157 return {num_sets(), code_.remove(rem, missing)};
2158 }
2159
2164 acc_cond strip(mark_t rem, bool missing) const
2165 {
2166 return
2167 { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
2168 }
2169
2172 {
2173 return {num_sets(), code_.force_inf(m)};
2174 }
2175
2179 {
2180 return {num_sets(), code_.remove(all_sets() - rem, true)};
2181 }
2182
2194 std::string name(const char* fmt = "alo") const;
2195
2208 {
2209 return code_.fin_unit();
2210 }
2211
2224 {
2225 return code_.inf_unit();
2226 }
2227
2232 int fin_one() const
2233 {
2234 return code_.fin_one();
2235 }
2236
2257 std::pair<int, acc_cond> fin_one_extract() const
2258 {
2259 auto [f, c] = code_.fin_one_extract();
2260 return {f, {num_sets(), std::move(c)}};
2261 }
2262
2281 std::tuple<int, acc_cond, acc_cond>
2283 {
2284 auto [f, l, r] = code_.fin_unit_one_split();
2285 return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2286 }
2287 std::tuple<int, acc_cond, acc_cond>
2289 {
2290 auto [f, l, r] = code_.fin_unit_one_split_improved();
2291 return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2292 }
2294
2303 std::vector<acc_cond> top_disjuncts() const;
2304
2313 std::vector<acc_cond> top_conjuncts() const;
2314
2315 protected:
2316 mark_t all_sets_() const
2317 {
2318 return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2319 }
2320
2321 unsigned num_;
2322 mark_t all_;
2323 acc_code code_;
2324 bool uses_fin_acceptance_ = false;
2325
2326 };
2327
2329 typedef std::vector<acc_cond::rs_pair> rs_pairs;
2330
2331 // Creates view of pairs 'p' with restriction only to marks in 'm'
2332 explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2333 : pairs_(p), view_marks_(m) {}
2334
2335 // Creates view of pairs without restriction to marks
2336 explicit rs_pairs_view(const rs_pairs& p)
2338
2339 acc_cond::mark_t infs() const
2340 {
2341 return do_view([&](const acc_cond::rs_pair& p)
2342 {
2343 return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2344 });
2345 }
2346
2347 acc_cond::mark_t fins() const
2348 {
2349 return do_view([&](const acc_cond::rs_pair& p)
2350 {
2351 return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2352 });
2353 }
2354
2355 acc_cond::mark_t fins_alone() const
2356 {
2357 return do_view([&](const acc_cond::rs_pair& p)
2358 {
2359 return !visible(p.inf) && visible(p.fin) ? p.fin
2360 : acc_cond::mark_t({});
2361 });
2362 }
2363
2364 acc_cond::mark_t infs_alone() const
2365 {
2366 return do_view([&](const acc_cond::rs_pair& p)
2367 {
2368 return !visible(p.fin) && visible(p.inf) ? p.inf
2369 : acc_cond::mark_t({});
2370 });
2371 }
2372
2373 acc_cond::mark_t paired_with_fin(unsigned mark) const
2374 {
2375 acc_cond::mark_t res = {};
2376 for (const auto& p: pairs_)
2377 if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2378 res |= p.inf;
2379 return res;
2380 }
2381
2382 const rs_pairs& pairs() const
2383 {
2384 return pairs_;
2385 }
2386
2387 private:
2388 template<typename filter>
2389 acc_cond::mark_t do_view(const filter& filt) const
2390 {
2391 acc_cond::mark_t res = {};
2392 for (const auto& p: pairs_)
2393 res |= filt(p);
2394 return res;
2395 }
2396
2397 bool visible(const acc_cond::mark_t& v) const
2398 {
2399 return !!(view_marks_ & v);
2400 }
2401
2402 const rs_pairs& pairs_;
2403 acc_cond::mark_t view_marks_;
2404 };
2405
2406
2407 SPOT_API
2408 std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2409
2411
2412 namespace internal
2413 {
2414 class SPOT_API mark_iterator
2415 {
2416 public:
2417 typedef unsigned value_type;
2418 typedef const value_type& reference;
2419 typedef const value_type* pointer;
2420 typedef std::ptrdiff_t difference_type;
2421 typedef std::forward_iterator_tag iterator_category;
2422
2423 mark_iterator() noexcept
2424 : m_({})
2425 {
2426 }
2427
2429 : m_(m)
2430 {
2431 }
2432
2433 bool operator==(mark_iterator m) const
2434 {
2435 return m_ == m.m_;
2436 }
2437
2438 bool operator!=(mark_iterator m) const
2439 {
2440 return m_ != m.m_;
2441 }
2442
2443 value_type operator*() const
2444 {
2445 SPOT_ASSERT(m_);
2446 return m_.min_set() - 1;
2447 }
2448
2449 mark_iterator& operator++()
2450 {
2451 m_.clear(this->operator*());
2452 return *this;
2453 }
2454
2455 mark_iterator operator++(int)
2456 {
2457 mark_iterator it = *this;
2458 ++(*this);
2459 return it;
2460 }
2461 private:
2463 };
2464
2465 class SPOT_API mark_container
2466 {
2467 public:
2469 : m_(m)
2470 {
2471 }
2472
2473 mark_iterator begin() const
2474 {
2475 return {m_};
2476 }
2477 mark_iterator end() const
2478 {
2479 return {};
2480 }
2481 private:
2483 };
2484 }
2485
2487 {
2488 return {*this};
2489 }
2490
2491 inline acc_cond::mark_t
2492 acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut)
2493 {
2494 mark_t result { };
2495 for (auto color : sets())
2496 if (color < permut.size())
2497 result.set(permut[color]);
2498 return result;
2499 }
2500}
2501
2502namespace std
2503{
2504 template<>
2505 struct hash<spot::acc_cond::mark_t>
2506 {
2507 size_t operator()(spot::acc_cond::mark_t m) const noexcept
2508 {
2509 return m.hash();
2510 }
2511 };
2512}
An acceptance condition.
Definition: acc.hh:62
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1552
bool inf_satisfiable(mark_t inf) const
Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the co...
Definition: acc.hh:2047
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1979
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1924
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1879
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition: acc.hh:1819
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1638
std::pair< int, acc_cond > fin_one_extract() const
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it ...
Definition: acc.hh:2257
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1897
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1624
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
Definition: acc.hh:2037
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1852
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1647
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1929
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1857
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1957
bool is_parity(bool &max, bool &odd, bool equiv=false) const
check is the acceptance condition matches one of the four type of parity acceptance defined in the HO...
std::vector< acc_cond > top_disjuncts() const
Return the top-level disjuncts.
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1963
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1631
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:2171
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:2155
acc_op
Operators for acceptance formulas.
Definition: acc.hh:456
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1503
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1939
bool is_parity() const
check is the acceptance condition matches one of the four type of parity acceptance defined in the HO...
Definition: acc.hh:1805
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1580
bool is_generalized_rabin(std::vector< unsigned > &pairs) const
Is the acceptance condition generalized-Rabin?
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition: acc.hh:1973
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1529
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1558
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1902
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1658
std::tuple< int, acc_cond, acc_cond > fin_unit_one_split_improved() const
Split an acceptance condition, trying to select one unit-Fin.
Definition: acc.hh:2288
acc_cond restrict_to(mark_t rem) const
Restrict an acceptance condition to a subset of set numbers that are occurring at some point.
Definition: acc.hh:2178
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:2063
std::string name(const char *fmt="alo") const
Return the name of this acceptance condition, in the specified format.
bool is_none() const
Whether the acceptance condition is "none".
Definition: acc.hh:1604
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1545
int is_rabin() const
Check if the acceptance condition matches the Rabin acceptance of the HOA format.
bool is_rabin_like(std::vector< rs_pair > &pairs) const
Test whether an acceptance condition is Rabin-like and returns each Rabin pair in an std::vector<rs_p...
mark_t accepting_sets(mark_t inf) const
Return an accepting subset of inf.
bool is_all() const
Whether the acceptance condition is "all".
Definition: acc.hh:1589
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:2164
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:2232
mark_t useless(iterator begin, iterator end) const
Compute useless acceptance sets given a list of mark_t that occur in an SCC.
Definition: acc.hh:2116
int is_streett() const
Check if the acceptance condition matches the Streett acceptance of the HOA format.
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition: acc.hh:2207
bool is_generalized_streett(std::vector< unsigned > &pairs) const
Is the acceptance condition generalized-Streett?
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition: acc.hh:1514
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1522
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1884
bool is_streett_like(std::vector< rs_pair > &pairs) const
Test whether an acceptance condition is Streett-like and returns each Streett pair in an std::vector<...
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition: acc.hh:1613
std::vector< acc_cond > top_conjuncts() const
Return the top-level conjuncts.
std::tuple< int, acc_cond, acc_cond > fin_unit_one_split() const
Split an acceptance condition, trying to select one unit-Fin.
Definition: acc.hh:2282
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
Definition: acc.hh:2223
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1574
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1595
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2103
Definition: bitset.hh:39
Definition: acc.hh:2466
Definition: acc.hh:2415
A class implementing Kleene's three-valued logic.
Definition: trival.hh:34
op
Operator types.
Definition: formula.hh:79
@ Or
(omega-Rational) Or
@ U
until
@ And
(omega-Rational) And
SPOT_DEPRECATED("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence rec...
Definition: automata.hh:27
const mc_rvalue operator|(const mc_rvalue &lhs, const mc_rvalue &rhs)
This function helps to find the output value from a set of threads that may have different values.
Definition: mc.hh:131
An acceptance formula.
Definition: acc.hh:488
static acc_code parity_max(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:873
std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > fin_unit_one_split() const
Split an acceptance condition, trying to select one unit-Fin.
std::vector< std::vector< int > > missing(mark_t inf, bool accepting) const
Help closing accepting or rejecting cycle.
friend std::ostream & operator<<(std::ostream &os, const acc_code &code)
prints the acceptance formula as text
std::ostream & to_html(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as HTML.
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:713
acc_code to_cnf() const
Convert the acceptance formula into disjunctive normal form.
acc_code operator&(acc_code &&r) const
Conjunct the current condition with r.
Definition: acc.hh:1016
acc_code force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:755
std::vector< std::pair< acc_cond::mark_t, acc_cond::mark_t > > useless_colors_patterns() const
Find patterns of useless colors.
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1122
std::vector< acc_code > top_conjuncts() const
Return the top-level conjuncts.
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1113
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:667
bool is_dnf() const
Whether the acceptance formula is in disjunctive normal form.
std::vector< acc_code > top_disjuncts() const
Return the top-level disjuncts.
acc_code operator&(const acc_code &r) const
Conjunct the current condition with r.
Definition: acc.hh:1007
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:723
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:893
static acc_code parity(bool is_max, bool is_odd, unsigned sets)
Build a parity acceptance condition.
mark_t used_once_sets() const
Return the sets that appears only once in the acceptance.
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1134
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:617
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:782
static acc_code parity_min_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:889
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1486
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
static acc_code parity_max_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:881
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:631
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
static acc_code parity_max_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:877
std::ostream & to_latex(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as LaTeX.
std::pair< int, acc_code > fin_one_extract() const
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it ...
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:603
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1165
static acc_code random(unsigned n, double reuse=0.0)
Build a random acceptance condition.
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:809
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1481
std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > fin_unit_one_split_improved() const
Split an acceptance condition, trying to select one unit-Fin.
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:772
acc_code complement() const
Complement an acceptance formula.
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:745
bdd to_bdd(const bdd *map) const
Convert the acceptance formula into a BDD.
std::ostream & to_text(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as text.
int fin_one() const
Return one acceptance set i that appears as Fin(i) in the condition.
acc_cond::mark_t used_sets() const
Return the set of sets appearing in the condition.
std::pair< acc_cond::mark_t, acc_cond::mark_t > used_inf_fin_sets() const
Return the sets used as Inf or Fin in the acceptance condition.
acc_code strip(acc_cond::mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
acc_code(const char *input)
Construct an acc_code from a string.
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:699
acc_code & operator&=(const acc_code &r)
Conjunct the current condition in place with r.
Definition: acc.hh:918
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:824
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:645
std::vector< unsigned > symmetries() const
compute the symmetry class of the acceptance sets.
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:689
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:885
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:657
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:1025
bool inf_satisfiable(mark_t inf) const
Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the co...
bool is_cnf() const
Whether the acceptance formula is in conjunctive normal form.
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:764
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:796
acc_code remove(acc_cond::mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
acc_code to_dnf() const
Convert the acceptance formula into disjunctive normal form.
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition: acc.hh:848
An acceptance mark.
Definition: acc.hh:90
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:147
bool is_singleton() const
Whether the mark contains only one bit set.
Definition: acc.hh:394
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:388
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:364
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:418
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:157
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2486
bool proper_subset(mark_t m) const
Whether the set of bits represented by *this is a proper subset of those represented by m.
Definition: acc.hh:349
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:112
unsigned count() const
Number of bits sets.
Definition: acc.hh:355
mark_t()=default
Initialize an empty mark_t.
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:123
bool has_many() const
Whether the mark contains at least two bits set.
Definition: acc.hh:405
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:376
bool subset(mark_t m) const
Whether the set of bits represented by *this is a subset of those represented by m.
Definition: acc.hh:342
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:427
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1701
Definition: acc.hh:41
Definition: acc.hh:2328
A "node" in an acceptance formulas.
Definition: acc.hh:466

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4