spot  2.9.5
acc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2020 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 
29 #include <spot/misc/_config.h>
30 #include <spot/misc/bitset.hh>
31 #include <spot/misc/trival.hh>
32 
33 namespace spot
34 {
35  namespace internal
36  {
37  class mark_container;
38 
39  template<bool>
40  struct _32acc {};
41  template<>
42  struct _32acc<true>
43  {
44  SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t")
45  typedef unsigned value_t;
46  };
47  }
48 
51 
60  class SPOT_API acc_cond
61  {
62 
63  public:
64  bool
65  has_parity_prefix(acc_cond& new_acc, std::vector<unsigned>& colors) const;
66 
67 #ifndef SWIG
68  private:
69  [[noreturn]] static void report_too_many_sets();
70 #endif
71  public:
72 
87  struct mark_t :
88  public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
89  {
90  private:
91  // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
92  typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
93  _value_t id;
94 
95  mark_t(_value_t id) noexcept
96  : id(id)
97  {
98  }
99 
100  public:
102  mark_t() = default;
103 
104  mark_t
105  apply_permutation(std::vector<unsigned> permut);
106 
107 
108 #ifndef SWIG
109  template<class iterator>
111  mark_t(const iterator& begin, const iterator& end)
112  : mark_t(_value_t::zero())
113  {
114  for (iterator i = begin; i != end; ++i)
115  if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
116  set(*i);
117  else
118  report_too_many_sets();
119  }
120 
122  mark_t(std::initializer_list<unsigned> vals)
123  : mark_t(vals.begin(), vals.end())
124  {
125  }
126 
127  SPOT_DEPRECATED("use brace initialization instead")
128  mark_t(unsigned i)
129  {
130  unsigned j = 0;
131  while (i)
132  {
133  if (i & 1U)
134  this->set(j);
135  ++j;
136  i >>= 1;
137  }
138  }
139 #endif
140 
146  constexpr static unsigned max_accsets()
147  {
148  return SPOT_MAX_ACCSETS;
149  }
150 
156  static mark_t all()
157  {
158  return mark_t(_value_t::mone());
159  }
160 
161  size_t hash() const noexcept
162  {
163  std::hash<decltype(id)> h;
164  return h(id);
165  }
166 
167  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
168  bool operator==(unsigned o) const
169  {
170  SPOT_ASSERT(o == 0U);
171  (void)o;
172  return !id;
173  }
174 
175  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
176  bool operator!=(unsigned o) const
177  {
178  SPOT_ASSERT(o == 0U);
179  (void)o;
180  return !!id;
181  }
182 
183  bool operator==(mark_t o) const
184  {
185  return id == o.id;
186  }
187 
188  bool operator!=(mark_t o) const
189  {
190  return id != o.id;
191  }
192 
193  bool operator<(mark_t o) const
194  {
195  return id < o.id;
196  }
197 
198  bool operator<=(mark_t o) const
199  {
200  return id <= o.id;
201  }
202 
203  bool operator>(mark_t o) const
204  {
205  return id > o.id;
206  }
207 
208  bool operator>=(mark_t o) const
209  {
210  return id >= o.id;
211  }
212 
213  explicit operator bool() const
214  {
215  return !!id;
216  }
217 
218  bool has(unsigned u) const
219  {
220  return !!this->operator&(mark_t({0}) << u);
221  }
222 
223  void set(unsigned u)
224  {
225  id.set(u);
226  }
227 
228  void clear(unsigned u)
229  {
230  id.clear(u);
231  }
232 
233  mark_t& operator&=(mark_t r)
234  {
235  id &= r.id;
236  return *this;
237  }
238 
239  mark_t& operator|=(mark_t r)
240  {
241  id |= r.id;
242  return *this;
243  }
244 
245  mark_t& operator-=(mark_t r)
246  {
247  id &= ~r.id;
248  return *this;
249  }
250 
251  mark_t& operator^=(mark_t r)
252  {
253  id ^= r.id;
254  return *this;
255  }
256 
257  mark_t operator&(mark_t r) const
258  {
259  return id & r.id;
260  }
261 
262  mark_t operator|(mark_t r) const
263  {
264  return id | r.id;
265  }
266 
267  mark_t operator-(mark_t r) const
268  {
269  return id & ~r.id;
270  }
271 
272  mark_t operator~() const
273  {
274  return ~id;
275  }
276 
277  mark_t operator^(mark_t r) const
278  {
279  return id ^ r.id;
280  }
281 
282 #if SPOT_DEBUG || defined(SWIGPYTHON)
283 # define SPOT_WRAP_OP(ins) \
284  try \
285  { \
286  ins; \
287  } \
288  catch (const std::runtime_error& e) \
289  { \
290  report_too_many_sets(); \
291  }
292 #else
293 # define SPOT_WRAP_OP(ins) ins;
294 #endif
295  mark_t operator<<(unsigned i) const
296  {
297  SPOT_WRAP_OP(return id << i);
298  }
299 
300  mark_t& operator<<=(unsigned i)
301  {
302  SPOT_WRAP_OP(id <<= i; return *this);
303  }
304 
305  mark_t operator>>(unsigned i) const
306  {
307  SPOT_WRAP_OP(return id >> i);
308  }
309 
310  mark_t& operator>>=(unsigned i)
311  {
312  SPOT_WRAP_OP(id >>= i; return *this);
313  }
314 #undef SPOT_WRAP_OP
315 
316  mark_t strip(mark_t y) const
317  {
318  // strip every bit of id that is marked in y
319  // 100101110100.strip(
320  // 001011001000)
321  // == 10 1 11 100
322  // == 10111100
323 
324  auto xv = id; // 100101110100
325  auto yv = y.id; // 001011001000
326 
327  while (yv && xv)
328  {
329  // Mask for everything after the last 1 in y
330  auto rm = (~yv) & (yv - 1); // 000000000111
331  // Mask for everything before the last 1 in y
332  auto lm = ~(yv ^ (yv - 1)); // 111111110000
333  xv = ((xv & lm) >> 1) | (xv & rm);
334  yv = (yv & lm) >> 1;
335  }
336  return xv;
337  }
338 
341  bool subset(mark_t m) const
342  {
343  return !((*this) - m);
344  }
345 
348  bool proper_subset(mark_t m) const
349  {
350  return *this != m && this->subset(m);
351  }
352 
354  unsigned count() const
355  {
356  return id.count();
357  }
358 
363  unsigned max_set() const
364  {
365  if (id)
366  return id.highest()+1;
367  else
368  return 0;
369  }
370 
375  unsigned min_set() const
376  {
377  if (id)
378  return id.lowest()+1;
379  else
380  return 0;
381  }
382 
387  mark_t lowest() const
388  {
389  return id & -id;
390  }
391 
393  bool is_singleton() const
394  {
395 #if __GNUC__
396  /* With GCC and Clang, count() is implemented using popcount. */
397  return count() == 1;
398 #else
399  return id && !(id & (id - 1));
400 #endif
401  }
402 
404  bool has_many() const
405  {
406 #if __GNUC__
407  /* With GCC and Clang, count() is implemented using popcount. */
408  return count() > 1;
409 #else
410  return !!(id & (id - 1));
411 #endif
412  }
413 
417  mark_t& remove_some(unsigned n)
418  {
419  while (n--)
420  id &= id - 1;
421  return *this;
422  }
423 
425  template<class iterator>
426  void fill(iterator here) const
427  {
428  auto a = *this;
429  unsigned level = 0;
430  while (a)
431  {
432  if (a.has(0))
433  *here++ = level;
434  ++level;
435  a >>= 1;
436  }
437  }
438 
440  spot::internal::mark_container sets() const;
441 
442  SPOT_API
443  friend std::ostream& operator<<(std::ostream& os, mark_t m);
444 
445  std::string as_string() const
446  {
447  std::ostringstream os;
448  os << *this;
449  return os.str();
450  }
451  };
452 
454  enum class acc_op : unsigned short
455  { Inf, Fin, InfNeg, FinNeg, And, Or };
456 
464  union acc_word
465  {
466  mark_t mark;
467  struct {
468  acc_op op; // Operator
469  unsigned short size; // Size of the subtree (number of acc_word),
470  // not counting this node.
471  } sub;
472  };
473 
486  struct SPOT_API acc_code: public std::vector<acc_word>
487  {
488  acc_code
489  unit_propagation();
490 
491  bool
492  has_parity_prefix(acc_cond& new_cond,
493  std::vector<unsigned>& colors) const;
494 
495  bool
496  is_parity_max_equiv(std::vector<int>& permut,
497  unsigned new_color,
498  bool even) const;
499 
500  bool operator==(const acc_code& other) const
501  {
502  unsigned pos = size();
503  if (other.size() != pos)
504  return false;
505  while (pos > 0)
506  {
507  auto op = (*this)[pos - 1].sub.op;
508  auto sz = (*this)[pos - 1].sub.size;
509  if (other[pos - 1].sub.op != op ||
510  other[pos - 1].sub.size != sz)
511  return false;
512  switch (op)
513  {
514  case acc_cond::acc_op::And:
515  case acc_cond::acc_op::Or:
516  --pos;
517  break;
518  case acc_cond::acc_op::Inf:
519  case acc_cond::acc_op::InfNeg:
520  case acc_cond::acc_op::Fin:
521  case acc_cond::acc_op::FinNeg:
522  pos -= 2;
523  if (other[pos].mark != (*this)[pos].mark)
524  return false;
525  break;
526  }
527  }
528  return true;
529  };
530 
531  bool operator<(const acc_code& other) const
532  {
533  unsigned pos = size();
534  auto osize = other.size();
535  if (pos < osize)
536  return true;
537  if (pos > osize)
538  return false;
539  while (pos > 0)
540  {
541  auto op = (*this)[pos - 1].sub.op;
542  auto oop = other[pos - 1].sub.op;
543  if (op < oop)
544  return true;
545  if (op > oop)
546  return false;
547  auto sz = (*this)[pos - 1].sub.size;
548  auto osz = other[pos - 1].sub.size;
549  if (sz < osz)
550  return true;
551  if (sz > osz)
552  return false;
553  switch (op)
554  {
555  case acc_cond::acc_op::And:
556  case acc_cond::acc_op::Or:
557  --pos;
558  break;
559  case acc_cond::acc_op::Inf:
560  case acc_cond::acc_op::InfNeg:
561  case acc_cond::acc_op::Fin:
562  case acc_cond::acc_op::FinNeg:
563  {
564  pos -= 2;
565  auto m = (*this)[pos].mark;
566  auto om = other[pos].mark;
567  if (m < om)
568  return true;
569  if (m > om)
570  return false;
571  break;
572  }
573  }
574  }
575  return false;
576  }
577 
578  bool operator>(const acc_code& other) const
579  {
580  return other < *this;
581  }
582 
583  bool operator<=(const acc_code& other) const
584  {
585  return !(other < *this);
586  }
587 
588  bool operator>=(const acc_code& other) const
589  {
590  return !(*this < other);
591  }
592 
593  bool operator!=(const acc_code& other) const
594  {
595  return !(*this == other);
596  }
597 
602  bool is_t() const
603  {
604  // We store "t" as an empty condition, or as Inf({}).
605  unsigned s = size();
606  return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
607  && !((*this)[s - 2].mark));
608  }
609 
616  bool is_f() const
617  {
618  // We store "f" as Fin({}).
619  unsigned s = size();
620  return s > 1
621  && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
622  }
623 
630  static acc_code f()
631  {
632  acc_code res;
633  res.resize(2);
634  res[0].mark = {};
635  res[1].sub.op = acc_op::Fin;
636  res[1].sub.size = 1;
637  return res;
638  }
639 
644  static acc_code t()
645  {
646  return {};
647  }
648 
656  static acc_code fin(mark_t m)
657  {
658  acc_code res;
659  res.resize(2);
660  res[0].mark = m;
661  res[1].sub.op = acc_op::Fin;
662  res[1].sub.size = 1;
663  return res;
664  }
665 
666  static acc_code fin(std::initializer_list<unsigned> vals)
667  {
668  return fin(mark_t(vals));
669  }
671 
689  {
690  acc_code res;
691  res.resize(2);
692  res[0].mark = m;
693  res[1].sub.op = acc_op::FinNeg;
694  res[1].sub.size = 1;
695  return res;
696  }
697 
698  static acc_code fin_neg(std::initializer_list<unsigned> vals)
699  {
700  return fin_neg(mark_t(vals));
701  }
703 
712  static acc_code inf(mark_t m)
713  {
714  acc_code res;
715  res.resize(2);
716  res[0].mark = m;
717  res[1].sub.op = acc_op::Inf;
718  res[1].sub.size = 1;
719  return res;
720  }
721 
722  static acc_code inf(std::initializer_list<unsigned> vals)
723  {
724  return inf(mark_t(vals));
725  }
727 
745  {
746  acc_code res;
747  res.resize(2);
748  res[0].mark = m;
749  res[1].sub.op = acc_op::InfNeg;
750  res[1].sub.size = 1;
751  return res;
752  }
753 
754  static acc_code inf_neg(std::initializer_list<unsigned> vals)
755  {
756  return inf_neg(mark_t(vals));
757  }
759 
763  static acc_code buchi()
764  {
765  return inf({0});
766  }
767 
771  static acc_code cobuchi()
772  {
773  return fin({0});
774  }
775 
781  static acc_code generalized_buchi(unsigned n)
782  {
783  if (n == 0)
784  return inf({});
785  acc_cond::mark_t m = mark_t::all();
786  m >>= mark_t::max_accsets() - n;
787  return inf(m);
788  }
789 
795  static acc_code generalized_co_buchi(unsigned n)
796  {
797  if (n == 0)
798  return fin({});
799  acc_cond::mark_t m = mark_t::all();
800  m >>= mark_t::max_accsets() - n;
801  return fin(m);
802  }
803 
808  static acc_code rabin(unsigned n)
809  {
810  acc_cond::acc_code res = f();
811  while (n > 0)
812  {
813  res |= inf({2*n - 1}) & fin({2*n - 2});
814  --n;
815  }
816  return res;
817  }
818 
823  static acc_code streett(unsigned n)
824  {
825  acc_cond::acc_code res = t();
826  while (n > 0)
827  {
828  res &= inf({2*n - 1}) | fin({2*n - 2});
829  --n;
830  }
831  return res;
832  }
833 
846  template<class Iterator>
847  static acc_code generalized_rabin(Iterator begin, Iterator end)
848  {
849  acc_cond::acc_code res = f();
850  unsigned n = 0;
851  for (Iterator i = begin; i != end; ++i)
852  {
853  unsigned f = n++;
854  acc_cond::mark_t m = {};
855  for (unsigned ni = *i; ni > 0; --ni)
856  m.set(n++);
857  auto pair = inf(m) & fin({f});
858  std::swap(pair, res);
859  res |= std::move(pair);
860  }
861  return res;
862  }
863 
871  static acc_code parity(bool is_max, bool is_odd, unsigned sets);
872  static acc_code parity_max(bool is_odd, unsigned sets)
873  {
874  return parity(true, is_odd, sets);
875  }
876  static acc_code parity_max_odd(unsigned sets)
877  {
878  return parity_max(true, sets);
879  }
880  static acc_code parity_max_even(unsigned sets)
881  {
882  return parity_max(false, sets);
883  }
884  static acc_code parity_min(bool is_odd, unsigned sets)
885  {
886  return parity(false, is_odd, sets);
887  }
888  static acc_code parity_min_odd(unsigned sets)
889  {
890  return parity_min(true, sets);
891  }
892  static acc_code parity_min_even(unsigned sets)
893  {
894  return parity_min(false, sets);
895  }
897 
914  static acc_code random(unsigned n, double reuse = 0.0);
915 
917  acc_code& operator&=(const acc_code& r)
918  {
919  if (is_t() || r.is_f())
920  {
921  *this = r;
922  return *this;
923  }
924  if (is_f() || r.is_t())
925  return *this;
926  unsigned s = size() - 1;
927  unsigned rs = r.size() - 1;
928  // We want to group all Inf(x) operators:
929  // Inf(a) & Inf(b) = Inf(a & b)
930  if (((*this)[s].sub.op == acc_op::Inf
931  && r[rs].sub.op == acc_op::Inf)
932  || ((*this)[s].sub.op == acc_op::InfNeg
933  && r[rs].sub.op == acc_op::InfNeg))
934  {
935  (*this)[s - 1].mark |= r[rs - 1].mark;
936  return *this;
937  }
938 
939  // In the more complex scenarios, left and right may both
940  // be conjunctions, and Inf(x) might be a member of each
941  // side. Find it if it exists.
942  // left_inf points to the left Inf mark if any.
943  // right_inf points to the right Inf mark if any.
944  acc_word* left_inf = nullptr;
945  if ((*this)[s].sub.op == acc_op::And)
946  {
947  auto start = &(*this)[s] - (*this)[s].sub.size;
948  auto pos = &(*this)[s] - 1;
949  pop_back();
950  while (pos > start)
951  {
952  if (pos->sub.op == acc_op::Inf)
953  {
954  left_inf = pos - 1;
955  break;
956  }
957  pos -= pos->sub.size + 1;
958  }
959  }
960  else if ((*this)[s].sub.op == acc_op::Inf)
961  {
962  left_inf = &(*this)[s - 1];
963  }
964 
965  const acc_word* right_inf = nullptr;
966  auto right_end = &r.back();
967  if (right_end->sub.op == acc_op::And)
968  {
969  auto start = &r[0];
970  auto pos = --right_end;
971  while (pos > start)
972  {
973  if (pos->sub.op == acc_op::Inf)
974  {
975  right_inf = pos - 1;
976  break;
977  }
978  pos -= pos->sub.size + 1;
979  }
980  }
981  else if (right_end->sub.op == acc_op::Inf)
982  {
983  right_inf = right_end - 1;
984  }
985 
986  acc_cond::mark_t carry = {};
987  if (left_inf && right_inf)
988  {
989  carry = left_inf->mark;
990  auto pos = left_inf - &(*this)[0];
991  erase(begin() + pos, begin() + pos + 2);
992  }
993  auto sz = size();
994  insert(end(), &r[0], right_end + 1);
995  if (carry)
996  (*this)[sz + (right_inf - &r[0])].mark |= carry;
997 
998  acc_word w;
999  w.sub.op = acc_op::And;
1000  w.sub.size = size();
1001  emplace_back(w);
1002  return *this;
1003  }
1004 
1006  acc_code operator&(const acc_code& r) const
1007  {
1008  acc_code res = *this;
1009  res &= r;
1010  return res;
1011  }
1012 
1014  acc_code operator&(acc_code&& r) const
1015  {
1016  acc_code res = *this;
1017  res &= r;
1018  return res;
1019  }
1020 
1023  {
1024  if (is_t() || r.is_f())
1025  return *this;
1026  if (is_f() || r.is_t())
1027  {
1028  *this = r;
1029  return *this;
1030  }
1031  unsigned s = size() - 1;
1032  unsigned rs = r.size() - 1;
1033  // Fin(a) | Fin(b) = Fin(a | b)
1034  if (((*this)[s].sub.op == acc_op::Fin
1035  && r[rs].sub.op == acc_op::Fin)
1036  || ((*this)[s].sub.op == acc_op::FinNeg
1037  && r[rs].sub.op == acc_op::FinNeg))
1038  {
1039  (*this)[s - 1].mark |= r[rs - 1].mark;
1040  return *this;
1041  }
1042 
1043  // In the more complex scenarios, left and right may both
1044  // be disjunctions, and Fin(x) might be a member of each
1045  // side. Find it if it exists.
1046  // left_inf points to the left Inf mark if any.
1047  // right_inf points to the right Inf mark if any.
1048  acc_word* left_fin = nullptr;
1049  if ((*this)[s].sub.op == acc_op::Or)
1050  {
1051  auto start = &(*this)[s] - (*this)[s].sub.size;
1052  auto pos = &(*this)[s] - 1;
1053  pop_back();
1054  while (pos > start)
1055  {
1056  if (pos->sub.op == acc_op::Fin)
1057  {
1058  left_fin = pos - 1;
1059  break;
1060  }
1061  pos -= pos->sub.size + 1;
1062  }
1063  }
1064  else if ((*this)[s].sub.op == acc_op::Fin)
1065  {
1066  left_fin = &(*this)[s - 1];
1067  }
1068 
1069  const acc_word* right_fin = nullptr;
1070  auto right_end = &r.back();
1071  if (right_end->sub.op == acc_op::Or)
1072  {
1073  auto start = &r[0];
1074  auto pos = --right_end;
1075  while (pos > start)
1076  {
1077  if (pos->sub.op == acc_op::Fin)
1078  {
1079  right_fin = pos - 1;
1080  break;
1081  }
1082  pos -= pos->sub.size + 1;
1083  }
1084  }
1085  else if (right_end->sub.op == acc_op::Fin)
1086  {
1087  right_fin = right_end - 1;
1088  }
1089 
1090  acc_cond::mark_t carry = {};
1091  if (left_fin && right_fin)
1092  {
1093  carry = left_fin->mark;
1094  auto pos = (left_fin - &(*this)[0]);
1095  this->erase(begin() + pos, begin() + pos + 2);
1096  }
1097  auto sz = size();
1098  insert(end(), &r[0], right_end + 1);
1099  if (carry)
1100  (*this)[sz + (right_fin - &r[0])].mark |= carry;
1101  acc_word w;
1102  w.sub.op = acc_op::Or;
1103  w.sub.size = size();
1104  emplace_back(w);
1105  return *this;
1106  }
1107 
1110  {
1111  acc_code res = *this;
1112  res |= r;
1113  return res;
1114  }
1115 
1117  acc_code operator|(const acc_code& r) const
1118  {
1119  acc_code res = *this;
1120  res |= r;
1121  return res;
1122  }
1123 
1129  acc_code& operator<<=(unsigned sets)
1130  {
1131  if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1132  report_too_many_sets();
1133  if (empty())
1134  return *this;
1135  unsigned pos = size();
1136  do
1137  {
1138  switch ((*this)[pos - 1].sub.op)
1139  {
1140  case acc_cond::acc_op::And:
1141  case acc_cond::acc_op::Or:
1142  --pos;
1143  break;
1144  case acc_cond::acc_op::Inf:
1145  case acc_cond::acc_op::InfNeg:
1146  case acc_cond::acc_op::Fin:
1147  case acc_cond::acc_op::FinNeg:
1148  pos -= 2;
1149  (*this)[pos].mark <<= sets;
1150  break;
1151  }
1152  }
1153  while (pos > 0);
1154  return *this;
1155  }
1156 
1160  acc_code operator<<(unsigned sets) const
1161  {
1162  acc_code res = *this;
1163  res <<= sets;
1164  return res;
1165  }
1166 
1173  bool is_dnf() const;
1174 
1181  bool is_cnf() const;
1182 
1193  acc_code to_dnf() const;
1194 
1201  acc_code to_cnf() const;
1202 
1203 
1212  std::vector<acc_code> top_disjuncts() const;
1213 
1222  std::vector<acc_code> top_conjuncts() const;
1223 
1234  acc_code complement() const;
1235 
1247  mark_t fin_unit() const;
1248 
1253  int fin_one() const;
1254 
1267  std::vector<std::vector<int>>
1268  missing(mark_t inf, bool accepting) const;
1269 
1272  bool accepting(mark_t inf) const;
1273 
1279  bool inf_satisfiable(mark_t inf) const;
1280 
1292  trival maybe_accepting(mark_t infinitely_often,
1293  mark_t always_present) const;
1294 
1305  std::vector<unsigned> symmetries() const;
1306 
1320  acc_code remove(acc_cond::mark_t rem, bool missing) const;
1321 
1326  acc_code strip(acc_cond::mark_t rem, bool missing) const;
1328  acc_code force_inf(mark_t m) const;
1329 
1331  acc_cond::mark_t used_sets() const;
1332 
1339  mark_t used_once_sets() const;
1340 
1342  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1343 
1348  std::ostream&
1349  to_html(std::ostream& os,
1350  std::function<void(std::ostream&, int)>
1351  set_printer = nullptr) const;
1352 
1357  std::ostream&
1358  to_text(std::ostream& os,
1359  std::function<void(std::ostream&, int)>
1360  set_printer = nullptr) const;
1361 
1366  std::ostream&
1367  to_latex(std::ostream& os,
1368  std::function<void(std::ostream&, int)>
1369  set_printer = nullptr) const;
1370 
1393  acc_code(const char* input);
1394 
1399  {
1400  }
1401 
1403  acc_code(const acc_word* other)
1404  : std::vector<acc_word>(other - other->sub.size, other + 1)
1405  {
1406  }
1407 
1409  SPOT_API
1410  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1411  };
1412 
1420  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1421  : num_(0U), all_({}), code_(code)
1422  {
1423  add_sets(n_sets);
1424  uses_fin_acceptance_ = check_fin_acceptance();
1425  }
1426 
1431  acc_cond(const acc_code& code)
1432  : num_(0U), all_({}), code_(code)
1433  {
1434  add_sets(code.used_sets().max_set());
1435  uses_fin_acceptance_ = check_fin_acceptance();
1436  }
1437 
1439  acc_cond(const acc_cond& o)
1440  : num_(o.num_), all_(o.all_), code_(o.code_),
1441  uses_fin_acceptance_(o.uses_fin_acceptance_)
1442  {
1443  }
1444 
1447  {
1448  num_ = o.num_;
1449  all_ = o.all_;
1450  code_ = o.code_;
1451  uses_fin_acceptance_ = o.uses_fin_acceptance_;
1452  return *this;
1453  }
1454 
1455  ~acc_cond()
1456  {
1457  }
1458 
1462  void set_acceptance(const acc_code& code)
1463  {
1464  code_ = code;
1465  uses_fin_acceptance_ = check_fin_acceptance();
1466  }
1467 
1469  const acc_code& get_acceptance() const
1470  {
1471  return code_;
1472  }
1473 
1476  {
1477  return code_;
1478  }
1479 
1480  bool operator==(const acc_cond& other) const
1481  {
1482  return other.num_sets() == num_ && other.get_acceptance() == code_;
1483  }
1484 
1485  bool operator!=(const acc_cond& other) const
1486  {
1487  return !(*this == other);
1488  }
1489 
1491  bool uses_fin_acceptance() const
1492  {
1493  return uses_fin_acceptance_;
1494  }
1495 
1497  bool is_t() const
1498  {
1499  return code_.is_t();
1500  }
1501 
1506  bool is_all() const
1507  {
1508  return num_ == 0 && is_t();
1509  }
1510 
1512  bool is_f() const
1513  {
1514  return code_.is_f();
1515  }
1516 
1521  bool is_none() const
1522  {
1523  return num_ == 0 && is_f();
1524  }
1525 
1530  bool is_buchi() const
1531  {
1532  unsigned s = code_.size();
1533  return num_ == 1 &&
1534  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1535  }
1536 
1541  bool is_co_buchi() const
1542  {
1543  return num_ == 1 && is_generalized_co_buchi();
1544  }
1545 
1549  {
1550  set_acceptance(inf(all_sets()));
1551  }
1552 
1556  {
1557  set_acceptance(fin(all_sets()));
1558  }
1559 
1565  {
1566  unsigned s = code_.size();
1567  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1568  && code_[0].mark == all_sets());
1569  }
1570 
1576  {
1577  unsigned s = code_.size();
1578  return (s == 2 &&
1579  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1580  }
1581 
1593  int is_rabin() const;
1594 
1606  int is_streett() const;
1607 
1617  struct SPOT_API rs_pair
1618  {
1619 #ifndef SWIG
1620  rs_pair() = default;
1621  rs_pair(const rs_pair&) = default;
1622 #endif
1623 
1624  rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1625  fin(fin),
1626  inf(inf)
1627  {}
1628  acc_cond::mark_t fin;
1629  acc_cond::mark_t inf;
1630 
1631  bool operator==(rs_pair o) const
1632  {
1633  return fin == o.fin && inf == o.inf;
1634  }
1635  bool operator!=(rs_pair o) const
1636  {
1637  return fin != o.fin || inf != o.inf;
1638  }
1639  bool operator<(rs_pair o) const
1640  {
1641  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1642  }
1643  bool operator<=(rs_pair o) const
1644  {
1645  return !(o < *this);
1646  }
1647  bool operator>(rs_pair o) const
1648  {
1649  return o < *this;
1650  }
1651  bool operator>=(rs_pair o) const
1652  {
1653  return !(*this < o);
1654  }
1655  };
1666  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1667 
1678  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1679 
1689  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1690 
1703  bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1704 
1714  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1715 
1716 
1717  bool is_parity_max_equiv(std::vector<int>& permut, bool even) const;
1718 
1721  bool is_parity() const
1722  {
1723  bool max;
1724  bool odd;
1725  return is_parity(max, odd);
1726  }
1727 
1736  {
1737  return acc_cond(num_, code_.unit_propagation());
1738  }
1739 
1740  // Return (true, m) if there exist some acceptance mark m that
1741  // does not satisfy the acceptance condition. Return (false, 0U)
1742  // otherwise.
1743  std::pair<bool, acc_cond::mark_t> unsat_mark() const
1744  {
1745  return sat_unsat_mark(false);
1746  }
1747  // Return (true, m) if there exist some acceptance mark m that
1748  // does satisfy the acceptance condition. Return (false, 0U)
1749  // otherwise.
1750  std::pair<bool, acc_cond::mark_t> sat_mark() const
1751  {
1752  return sat_unsat_mark(true);
1753  }
1754 
1755  protected:
1756  bool check_fin_acceptance() const;
1757  std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1758 
1759  public:
1768  static acc_code inf(mark_t mark)
1769  {
1770  return acc_code::inf(mark);
1771  }
1772 
1773  static acc_code inf(std::initializer_list<unsigned> vals)
1774  {
1775  return inf(mark_t(vals.begin(), vals.end()));
1776  }
1778 
1795  static acc_code inf_neg(mark_t mark)
1796  {
1797  return acc_code::inf_neg(mark);
1798  }
1799 
1800  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1801  {
1802  return inf_neg(mark_t(vals.begin(), vals.end()));
1803  }
1805 
1813  static acc_code fin(mark_t mark)
1814  {
1815  return acc_code::fin(mark);
1816  }
1817 
1818  static acc_code fin(std::initializer_list<unsigned> vals)
1819  {
1820  return fin(mark_t(vals.begin(), vals.end()));
1821  }
1823 
1840  static acc_code fin_neg(mark_t mark)
1841  {
1842  return acc_code::fin_neg(mark);
1843  }
1844 
1845  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1846  {
1847  return fin_neg(mark_t(vals.begin(), vals.end()));
1848  }
1850 
1855  unsigned add_sets(unsigned num)
1856  {
1857  if (num == 0)
1858  return -1U;
1859  unsigned j = num_;
1860  num += j;
1861  if (num > mark_t::max_accsets())
1862  report_too_many_sets();
1863  // Make sure we do not update if we raised an exception.
1864  num_ = num;
1865  all_ = all_sets_();
1866  return j;
1867  }
1868 
1873  unsigned add_set()
1874  {
1875  return add_sets(1);
1876  }
1877 
1879  mark_t mark(unsigned u) const
1880  {
1881  SPOT_ASSERT(u < num_sets());
1882  return mark_t({u});
1883  }
1884 
1889  mark_t comp(const mark_t& l) const
1890  {
1891  return all_ ^ l;
1892  }
1893 
1896  {
1897  return all_;
1898  }
1899 
1900  acc_cond
1901  apply_permutation(std::vector<unsigned>permut)
1902  {
1903  return acc_cond(apply_permutation_aux(permut));
1904  }
1905 
1906  acc_code
1907  apply_permutation_aux(std::vector<unsigned>permut)
1908  {
1909  auto conj = top_conjuncts();
1910  auto disj = top_disjuncts();
1911 
1912  if (conj.size() > 1)
1913  {
1914  auto transformed = std::vector<acc_code>();
1915  for (auto elem : conj)
1916  transformed.push_back(elem.apply_permutation_aux(permut));
1917  std::sort(transformed.begin(), transformed.end());
1918  auto uniq = std::unique(transformed.begin(), transformed.end());
1919  auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(),
1920  [](acc_code c1, acc_code c2)
1921  {
1922  return c1 & c2;
1923  });
1924  return result;
1925  }
1926  else if (disj.size() > 1)
1927  {
1928  auto transformed = std::vector<acc_code>();
1929  for (auto elem : disj)
1930  transformed.push_back(elem.apply_permutation_aux(permut));
1931  std::sort(transformed.begin(), transformed.end());
1932  auto uniq = std::unique(transformed.begin(), transformed.end());
1933  auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(),
1934  [](acc_code c1, acc_code c2)
1935  {
1936  return c1 | c2;
1937  });
1938  return result;
1939  }
1940  else
1941  {
1942  if (code_.back().sub.op == acc_cond::acc_op::Fin)
1943  return fin(code_[0].mark.apply_permutation(permut));
1944  if (code_.back().sub.op == acc_cond::acc_op::Inf)
1945  return inf(code_[0].mark.apply_permutation(permut));
1946  }
1947  SPOT_ASSERT(false);
1948  return {};
1949  }
1950 
1953  bool accepting(mark_t inf) const
1954  {
1955  return code_.accepting(inf);
1956  }
1957 
1963  bool inf_satisfiable(mark_t inf) const
1964  {
1965  return code_.inf_satisfiable(inf);
1966  }
1967 
1979  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
1980  {
1981  return code_.maybe_accepting(infinitely_often, always_present);
1982  }
1983 
1997  mark_t accepting_sets(mark_t inf) const;
1998 
1999  // Deprecated since Spot 2.8
2000  SPOT_DEPRECATED("Use operator<< instead.")
2001  std::ostream& format(std::ostream& os, mark_t m) const
2002  {
2003  if (!m)
2004  return os;
2005  return os << m;
2006  }
2007 
2008  // Deprecated since Spot 2.8
2009  SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
2010  std::string format(mark_t m) const
2011  {
2012  std::ostringstream os;
2013  if (m)
2014  os << m;
2015  return os.str();
2016  }
2017 
2019  unsigned num_sets() const
2020  {
2021  return num_;
2022  }
2023 
2031  template<class iterator>
2032  mark_t useless(iterator begin, iterator end) const
2033  {
2034  mark_t u = {}; // The set of useless sets
2035  for (unsigned x = 0; x < num_; ++x)
2036  {
2037  // Skip sets that are already known to be useless.
2038  if (u.has(x))
2039  continue;
2040  auto all = comp(u | mark_t({x}));
2041  // Iterate over all mark_t, and keep track of
2042  // set numbers that always appear with x.
2043  for (iterator y = begin; y != end; ++y)
2044  {
2045  const mark_t& v = *y;
2046  if (v.has(x))
2047  {
2048  all &= v;
2049  if (!all)
2050  break;
2051  }
2052  }
2053  u |= all;
2054  }
2055  return u;
2056  }
2057 
2071  acc_cond remove(mark_t rem, bool missing) const
2072  {
2073  return {num_sets(), code_.remove(rem, missing)};
2074  }
2075 
2080  acc_cond strip(mark_t rem, bool missing) const
2081  {
2082  return
2083  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
2084  }
2085 
2088  {
2089  return {num_sets(), code_.force_inf(m)};
2090  }
2091 
2095  {
2096  return {num_sets(), code_.remove(all_sets() - rem, true)};
2097  }
2098 
2110  std::string name(const char* fmt = "alo") const;
2111 
2124  {
2125  return code_.fin_unit();
2126  }
2127 
2132  int fin_one() const
2133  {
2134  return code_.fin_one();
2135  }
2136 
2145  std::vector<acc_cond> top_disjuncts() const;
2146 
2155  std::vector<acc_cond> top_conjuncts() const;
2156 
2157  protected:
2158  mark_t all_sets_() const
2159  {
2160  return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2161  }
2162 
2163  unsigned num_;
2164  mark_t all_;
2165  acc_code code_;
2166  bool uses_fin_acceptance_ = false;
2167 
2168  };
2169 
2170  struct rs_pairs_view {
2171  typedef std::vector<acc_cond::rs_pair> rs_pairs;
2172 
2173  // Creates view of pairs 'p' with restriction only to marks in 'm'
2174  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2175  : pairs_(p), view_marks_(m) {}
2176 
2177  // Creates view of pairs without restriction to marks
2178  explicit rs_pairs_view(const rs_pairs& p)
2180 
2181  acc_cond::mark_t infs() const
2182  {
2183  return do_view([&](const acc_cond::rs_pair& p)
2184  {
2185  return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2186  });
2187  }
2188 
2189  acc_cond::mark_t fins() const
2190  {
2191  return do_view([&](const acc_cond::rs_pair& p)
2192  {
2193  return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2194  });
2195  }
2196 
2197  acc_cond::mark_t fins_alone() const
2198  {
2199  return do_view([&](const acc_cond::rs_pair& p)
2200  {
2201  return !visible(p.inf) && visible(p.fin) ? p.fin
2202  : acc_cond::mark_t({});
2203  });
2204  }
2205 
2206  acc_cond::mark_t infs_alone() const
2207  {
2208  return do_view([&](const acc_cond::rs_pair& p)
2209  {
2210  return !visible(p.fin) && visible(p.inf) ? p.inf
2211  : acc_cond::mark_t({});
2212  });
2213  }
2214 
2215  acc_cond::mark_t paired_with_fin(unsigned mark) const
2216  {
2217  acc_cond::mark_t res = {};
2218  for (const auto& p: pairs_)
2219  if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2220  res |= p.inf;
2221  return res;
2222  }
2223 
2224  const rs_pairs& pairs() const
2225  {
2226  return pairs_;
2227  }
2228 
2229  private:
2230  template<typename filter>
2231  acc_cond::mark_t do_view(const filter& filt) const
2232  {
2233  acc_cond::mark_t res = {};
2234  for (const auto& p: pairs_)
2235  res |= filt(p);
2236  return res;
2237  }
2238 
2239  bool visible(const acc_cond::mark_t& v) const
2240  {
2241  return !!(view_marks_ & v);
2242  }
2243 
2244  const rs_pairs& pairs_;
2245  acc_cond::mark_t view_marks_;
2246  };
2247 
2248 
2249  SPOT_API
2250  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2251 
2253 
2254  namespace internal
2255  {
2256  class SPOT_API mark_iterator
2257  {
2258  public:
2259  typedef unsigned value_type;
2260  typedef const value_type& reference;
2261  typedef const value_type* pointer;
2262  typedef std::ptrdiff_t difference_type;
2263  typedef std::forward_iterator_tag iterator_category;
2264 
2265  mark_iterator() noexcept
2266  : m_({})
2267  {
2268  }
2269 
2270  mark_iterator(acc_cond::mark_t m) noexcept
2271  : m_(m)
2272  {
2273  }
2274 
2275  bool operator==(mark_iterator m) const
2276  {
2277  return m_ == m.m_;
2278  }
2279 
2280  bool operator!=(mark_iterator m) const
2281  {
2282  return m_ != m.m_;
2283  }
2284 
2285  value_type operator*() const
2286  {
2287  SPOT_ASSERT(m_);
2288  return m_.min_set() - 1;
2289  }
2290 
2291  mark_iterator& operator++()
2292  {
2293  m_.clear(this->operator*());
2294  return *this;
2295  }
2296 
2297  mark_iterator operator++(int)
2298  {
2299  mark_iterator it = *this;
2300  ++(*this);
2301  return it;
2302  }
2303  private:
2304  acc_cond::mark_t m_;
2305  };
2306 
2307  class SPOT_API mark_container
2308  {
2309  public:
2311  : m_(m)
2312  {
2313  }
2314 
2315  mark_iterator begin() const
2316  {
2317  return {m_};
2318  }
2319  mark_iterator end() const
2320  {
2321  return {};
2322  }
2323  private:
2325  };
2326  }
2327 
2329  {
2330  return {*this};
2331  }
2332 
2333  inline acc_cond::mark_t
2334  acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut)
2335  {
2336  mark_t result { };
2337  for (auto color : sets())
2338  if (color < permut.size())
2339  result.set(permut[color]);
2340  return result;
2341  }
2342 }
2343 
2344 namespace std
2345 {
2346  template<>
2347  struct hash<spot::acc_cond::mark_t>
2348  {
2349  size_t operator()(spot::acc_cond::mark_t m) const noexcept
2350  {
2351  return m.hash();
2352  }
2353  };
2354 }
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:712
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:146
Definition: automata.hh:26
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:375
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:387
bool is_all() const
Whether the acceptance condition is "all".
Definition: acc.hh:1506
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1895
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2328
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1813
Definition: acc.hh:2256
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:2087
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1512
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:616
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:1963
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition: acc.hh:1530
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1855
acc_op
Operators for acceptance formulas.
Definition: acc.hh:454
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1845
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1879
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:363
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1491
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1617
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:426
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1469
Definition: bitset.hh:37
static acc_code parity_max_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:876
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:630
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1768
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:111
Definition: bitset.hh:405
Definition: acc.hh:2170
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:2094
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:341
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition: acc.hh:1735
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1818
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:156
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1160
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:823
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1564
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1462
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:348
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1840
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:892
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1109
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1403
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1795
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:2071
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:417
static acc_code parity_max_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:880
bool is_none() const
Whether the acceptance condition is "none".
Definition: acc.hh:1521
An acceptance condition.
Definition: acc.hh:60
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:2080
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1446
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1420
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:122
A "node" in an acceptance formulas.
Definition: acc.hh:464
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:1022
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:722
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1555
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:666
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...
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:2132
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:763
static acc_code parity_max(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:872
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1800
(omega-Rational) Or
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1475
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1541
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition: acc.hh:1889
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:644
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:884
Definition: twa.hh:1699
bool is_singleton() const
Whether the mark contains only one bit set.
Definition: acc.hh:393
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:771
unsigned count() const
Number of bits sets.
Definition: acc.hh:354
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:744
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1398
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1575
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition: acc.hh:2123
op
Operator types.
Definition: formula.hh:78
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:1721
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1129
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2019
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1773
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:781
static acc_code parity_min_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:888
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1439
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1117
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:808
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1873
Definition: acc.hh:40
An acceptance formula.
Definition: acc.hh:486
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:656
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition: acc.hh:847
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:2032
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition: acc.hh:1431
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition...
Definition: acc.hh:1953
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1497
Definition: acc.hh:2307
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:1979
(omega-Rational) And
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1548
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:688
An acceptance mark.
Definition: acc.hh:87
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:754
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:698
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:795
bool has_many() const
Whether the mark contains at least two bits set.
Definition: acc.hh:404
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:602

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.8.13