spot  2.8.1
acc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2019 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 
27 #include <spot/misc/_config.h>
28 #include <spot/misc/bitset.hh>
29 #include <spot/misc/trival.hh>
30 
31 namespace spot
32 {
33  namespace internal
34  {
35  class mark_container;
36 
37  template<bool>
38  struct _32acc {};
39  template<>
40  struct _32acc<true>
41  {
42  SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t")
43  typedef unsigned value_t;
44  };
45  }
46 
49 
58  class SPOT_API acc_cond
59  {
60 
61 #ifndef SWIG
62  private:
63  [[noreturn]] static void report_too_many_sets();
64 #endif
65  public:
66 
81  struct mark_t :
82  public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
83  {
84  private:
85  // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
86  typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
87  _value_t id;
88 
89  mark_t(_value_t id) noexcept
90  : id(id)
91  {
92  }
93 
94  public:
96  mark_t() = default;
97 
98 #ifndef SWIG
99  template<class iterator>
101  mark_t(const iterator& begin, const iterator& end)
102  : mark_t(_value_t::zero())
103  {
104  for (iterator i = begin; i != end; ++i)
105  set(*i);
106  }
107 
109  mark_t(std::initializer_list<unsigned> vals)
110  : mark_t(vals.begin(), vals.end())
111  {
112  }
113 
114  SPOT_DEPRECATED("use brace initialization instead")
115  mark_t(unsigned i)
116  {
117  unsigned j = 0;
118  while (i)
119  {
120  if (i & 1U)
121  this->set(j);
122  ++j;
123  i >>= 1;
124  }
125  }
126 #endif
127 
133  constexpr static unsigned max_accsets()
134  {
135  return SPOT_MAX_ACCSETS;
136  }
137 
143  static mark_t all()
144  {
145  return mark_t(_value_t::mone());
146  }
147 
148  size_t hash() const noexcept
149  {
150  std::hash<decltype(id)> h;
151  return h(id);
152  }
153 
154  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
155  bool operator==(unsigned o) const
156  {
157  SPOT_ASSERT(o == 0U);
158  (void)o;
159  return !id;
160  }
161 
162  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
163  bool operator!=(unsigned o) const
164  {
165  SPOT_ASSERT(o == 0U);
166  (void)o;
167  return !!id;
168  }
169 
170  bool operator==(mark_t o) const
171  {
172  return id == o.id;
173  }
174 
175  bool operator!=(mark_t o) const
176  {
177  return id != o.id;
178  }
179 
180  bool operator<(mark_t o) const
181  {
182  return id < o.id;
183  }
184 
185  bool operator<=(mark_t o) const
186  {
187  return id <= o.id;
188  }
189 
190  bool operator>(mark_t o) const
191  {
192  return id > o.id;
193  }
194 
195  bool operator>=(mark_t o) const
196  {
197  return id >= o.id;
198  }
199 
200  explicit operator bool() const
201  {
202  return !!id;
203  }
204 
205  bool has(unsigned u) const
206  {
207  return !!this->operator&(mark_t({0}) << u);
208  }
209 
210  void set(unsigned u)
211  {
212  id.set(u);
213  }
214 
215  void clear(unsigned u)
216  {
217  id.clear(u);
218  }
219 
220  mark_t& operator&=(mark_t r)
221  {
222  id &= r.id;
223  return *this;
224  }
225 
226  mark_t& operator|=(mark_t r)
227  {
228  id |= r.id;
229  return *this;
230  }
231 
232  mark_t& operator-=(mark_t r)
233  {
234  id &= ~r.id;
235  return *this;
236  }
237 
238  mark_t& operator^=(mark_t r)
239  {
240  id ^= r.id;
241  return *this;
242  }
243 
244  mark_t operator&(mark_t r) const
245  {
246  return id & r.id;
247  }
248 
249  mark_t operator|(mark_t r) const
250  {
251  return id | r.id;
252  }
253 
254  mark_t operator-(mark_t r) const
255  {
256  return id & ~r.id;
257  }
258 
259  mark_t operator~() const
260  {
261  return ~id;
262  }
263 
264  mark_t operator^(mark_t r) const
265  {
266  return id ^ r.id;
267  }
268 
269 #if SPOT_DEBUG || defined(SWIGPYTHON)
270 # define SPOT_WRAP_OP(ins) \
271  try \
272  { \
273  ins; \
274  } \
275  catch (const std::runtime_error& e) \
276  { \
277  report_too_many_sets(); \
278  }
279 #else
280 # define SPOT_WRAP_OP(ins) ins;
281 #endif
282  mark_t operator<<(unsigned i) const
283  {
284  SPOT_WRAP_OP(return id << i);
285  }
286 
287  mark_t& operator<<=(unsigned i)
288  {
289  SPOT_WRAP_OP(id <<= i; return *this);
290  }
291 
292  mark_t operator>>(unsigned i) const
293  {
294  SPOT_WRAP_OP(return id >> i);
295  }
296 
297  mark_t& operator>>=(unsigned i)
298  {
299  SPOT_WRAP_OP(id >>= i; return *this);
300  }
301 #undef SPOT_WRAP_OP
302 
303  mark_t strip(mark_t y) const
304  {
305  // strip every bit of id that is marked in y
306  // 100101110100.strip(
307  // 001011001000)
308  // == 10 1 11 100
309  // == 10111100
310 
311  auto xv = id; // 100101110100
312  auto yv = y.id; // 001011001000
313 
314  while (yv && xv)
315  {
316  // Mask for everything after the last 1 in y
317  auto rm = (~yv) & (yv - 1); // 000000000111
318  // Mask for everything before the last 1 in y
319  auto lm = ~(yv ^ (yv - 1)); // 111111110000
320  xv = ((xv & lm) >> 1) | (xv & rm);
321  yv = (yv & lm) >> 1;
322  }
323  return xv;
324  }
325 
328  bool subset(mark_t m) const
329  {
330  return !((*this) - m);
331  }
332 
335  bool proper_subset(mark_t m) const
336  {
337  return *this != m && this->subset(m);
338  }
339 
341  unsigned count() const
342  {
343  return id.count();
344  }
345 
350  unsigned max_set() const
351  {
352  if (id)
353  return id.highest()+1;
354  else
355  return 0;
356  }
357 
362  unsigned min_set() const
363  {
364  if (id)
365  return id.lowest()+1;
366  else
367  return 0;
368  }
369 
374  mark_t lowest() const
375  {
376  return id & -id;
377  }
378 
382  mark_t& remove_some(unsigned n)
383  {
384  while (n--)
385  id &= id - 1;
386  return *this;
387  }
388 
390  template<class iterator>
391  void fill(iterator here) const
392  {
393  auto a = *this;
394  unsigned level = 0;
395  while (a)
396  {
397  if (a.has(0))
398  *here++ = level;
399  ++level;
400  a >>= 1;
401  }
402  }
403 
405  spot::internal::mark_container sets() const;
406 
407  SPOT_API
408  friend std::ostream& operator<<(std::ostream& os, mark_t m);
409 
410  std::string as_string() const
411  {
412  std::ostringstream os;
413  os << *this;
414  return os.str();
415  }
416  };
417 
419  enum class acc_op : unsigned short
420  { Inf, Fin, InfNeg, FinNeg, And, Or };
421 
429  union acc_word
430  {
431  mark_t mark;
432  struct {
433  acc_op op; // Operator
434  unsigned short size; // Size of the subtree (number of acc_word),
435  // not counting this node.
436  } sub;
437  };
438 
451  struct SPOT_API acc_code: public std::vector<acc_word>
452  {
453  bool operator==(const acc_code& other) const
454  {
455  unsigned pos = size();
456  if (other.size() != pos)
457  return false;
458  while (pos > 0)
459  {
460  auto op = (*this)[pos - 1].sub.op;
461  auto sz = (*this)[pos - 1].sub.size;
462  if (other[pos - 1].sub.op != op ||
463  other[pos - 1].sub.size != sz)
464  return false;
465  switch (op)
466  {
467  case acc_cond::acc_op::And:
468  case acc_cond::acc_op::Or:
469  --pos;
470  break;
471  case acc_cond::acc_op::Inf:
472  case acc_cond::acc_op::InfNeg:
473  case acc_cond::acc_op::Fin:
474  case acc_cond::acc_op::FinNeg:
475  pos -= 2;
476  if (other[pos].mark != (*this)[pos].mark)
477  return false;
478  break;
479  }
480  }
481  return true;
482  };
483 
484  bool operator<(const acc_code& other) const
485  {
486  unsigned pos = size();
487  auto osize = other.size();
488  if (pos < osize)
489  return true;
490  if (pos > osize)
491  return false;
492  while (pos > 0)
493  {
494  auto op = (*this)[pos - 1].sub.op;
495  auto oop = other[pos - 1].sub.op;
496  if (op < oop)
497  return true;
498  if (op > oop)
499  return false;
500  auto sz = (*this)[pos - 1].sub.size;
501  auto osz = other[pos - 1].sub.size;
502  if (sz < osz)
503  return true;
504  if (sz > osz)
505  return false;
506  switch (op)
507  {
508  case acc_cond::acc_op::And:
509  case acc_cond::acc_op::Or:
510  --pos;
511  break;
512  case acc_cond::acc_op::Inf:
513  case acc_cond::acc_op::InfNeg:
514  case acc_cond::acc_op::Fin:
515  case acc_cond::acc_op::FinNeg:
516  {
517  pos -= 2;
518  auto m = (*this)[pos].mark;
519  auto om = other[pos].mark;
520  if (m < om)
521  return true;
522  if (m > om)
523  return false;
524  break;
525  }
526  }
527  }
528  return false;
529  }
530 
531  bool operator>(const acc_code& other) const
532  {
533  return other < *this;
534  }
535 
536  bool operator<=(const acc_code& other) const
537  {
538  return !(other < *this);
539  }
540 
541  bool operator>=(const acc_code& other) const
542  {
543  return !(*this < other);
544  }
545 
546  bool operator!=(const acc_code& other) const
547  {
548  return !(*this == other);
549  }
550 
555  bool is_t() const
556  {
557  // We store "t" as an empty condition, or as Inf({}).
558  unsigned s = size();
559  return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
560  && !((*this)[s - 2].mark));
561  }
562 
569  bool is_f() const
570  {
571  // We store "f" as Fin({}).
572  unsigned s = size();
573  return s > 1
574  && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
575  }
576 
583  static acc_code f()
584  {
585  acc_code res;
586  res.resize(2);
587  res[0].mark = {};
588  res[1].sub.op = acc_op::Fin;
589  res[1].sub.size = 1;
590  return res;
591  }
592 
597  static acc_code t()
598  {
599  return {};
600  }
601 
609  static acc_code fin(mark_t m)
610  {
611  acc_code res;
612  res.resize(2);
613  res[0].mark = m;
614  res[1].sub.op = acc_op::Fin;
615  res[1].sub.size = 1;
616  return res;
617  }
618 
619  static acc_code fin(std::initializer_list<unsigned> vals)
620  {
621  return fin(mark_t(vals));
622  }
624 
642  {
643  acc_code res;
644  res.resize(2);
645  res[0].mark = m;
646  res[1].sub.op = acc_op::FinNeg;
647  res[1].sub.size = 1;
648  return res;
649  }
650 
651  static acc_code fin_neg(std::initializer_list<unsigned> vals)
652  {
653  return fin_neg(mark_t(vals));
654  }
656 
665  static acc_code inf(mark_t m)
666  {
667  acc_code res;
668  res.resize(2);
669  res[0].mark = m;
670  res[1].sub.op = acc_op::Inf;
671  res[1].sub.size = 1;
672  return res;
673  }
674 
675  static acc_code inf(std::initializer_list<unsigned> vals)
676  {
677  return inf(mark_t(vals));
678  }
680 
698  {
699  acc_code res;
700  res.resize(2);
701  res[0].mark = m;
702  res[1].sub.op = acc_op::InfNeg;
703  res[1].sub.size = 1;
704  return res;
705  }
706 
707  static acc_code inf_neg(std::initializer_list<unsigned> vals)
708  {
709  return inf_neg(mark_t(vals));
710  }
712 
716  static acc_code buchi()
717  {
718  return inf({0});
719  }
720 
724  static acc_code cobuchi()
725  {
726  return fin({0});
727  }
728 
734  static acc_code generalized_buchi(unsigned n)
735  {
736  if (n == 0)
737  return inf({});
738  acc_cond::mark_t m = mark_t::all();
739  m >>= mark_t::max_accsets() - n;
740  return inf(m);
741  }
742 
748  static acc_code generalized_co_buchi(unsigned n)
749  {
750  if (n == 0)
751  return fin({});
752  acc_cond::mark_t m = mark_t::all();
753  m >>= mark_t::max_accsets() - n;
754  return fin(m);
755  }
756 
761  static acc_code rabin(unsigned n)
762  {
763  acc_cond::acc_code res = f();
764  while (n > 0)
765  {
766  res |= inf({2*n - 1}) & fin({2*n - 2});
767  --n;
768  }
769  return res;
770  }
771 
776  static acc_code streett(unsigned n)
777  {
778  acc_cond::acc_code res = t();
779  while (n > 0)
780  {
781  res &= inf({2*n - 1}) | fin({2*n - 2});
782  --n;
783  }
784  return res;
785  }
786 
799  template<class Iterator>
800  static acc_code generalized_rabin(Iterator begin, Iterator end)
801  {
802  acc_cond::acc_code res = f();
803  unsigned n = 0;
804  for (Iterator i = begin; i != end; ++i)
805  {
806  unsigned f = n++;
807  acc_cond::mark_t m = {};
808  for (unsigned ni = *i; ni > 0; --ni)
809  m.set(n++);
810  auto pair = inf(m) & fin({f});
811  std::swap(pair, res);
812  res |= std::move(pair);
813  }
814  return res;
815  }
816 
823  static acc_code parity(bool max, bool odd, unsigned sets);
824 
841  static acc_code random(unsigned n, double reuse = 0.0);
842 
844  acc_code& operator&=(const acc_code& r)
845  {
846  if (is_t() || r.is_f())
847  {
848  *this = r;
849  return *this;
850  }
851  if (is_f() || r.is_t())
852  return *this;
853  unsigned s = size() - 1;
854  unsigned rs = r.size() - 1;
855  // We want to group all Inf(x) operators:
856  // Inf(a) & Inf(b) = Inf(a & b)
857  if (((*this)[s].sub.op == acc_op::Inf
858  && r[rs].sub.op == acc_op::Inf)
859  || ((*this)[s].sub.op == acc_op::InfNeg
860  && r[rs].sub.op == acc_op::InfNeg))
861  {
862  (*this)[s - 1].mark |= r[rs - 1].mark;
863  return *this;
864  }
865 
866  // In the more complex scenarios, left and right may both
867  // be conjunctions, and Inf(x) might be a member of each
868  // side. Find it if it exists.
869  // left_inf points to the left Inf mark if any.
870  // right_inf points to the right Inf mark if any.
871  acc_word* left_inf = nullptr;
872  if ((*this)[s].sub.op == acc_op::And)
873  {
874  auto start = &(*this)[s] - (*this)[s].sub.size;
875  auto pos = &(*this)[s] - 1;
876  pop_back();
877  while (pos > start)
878  {
879  if (pos->sub.op == acc_op::Inf)
880  {
881  left_inf = pos - 1;
882  break;
883  }
884  pos -= pos->sub.size + 1;
885  }
886  }
887  else if ((*this)[s].sub.op == acc_op::Inf)
888  {
889  left_inf = &(*this)[s - 1];
890  }
891 
892  const acc_word* right_inf = nullptr;
893  auto right_end = &r.back();
894  if (right_end->sub.op == acc_op::And)
895  {
896  auto start = &r[0];
897  auto pos = --right_end;
898  while (pos > start)
899  {
900  if (pos->sub.op == acc_op::Inf)
901  {
902  right_inf = pos - 1;
903  break;
904  }
905  pos -= pos->sub.size + 1;
906  }
907  }
908  else if (right_end->sub.op == acc_op::Inf)
909  {
910  right_inf = right_end - 1;
911  }
912 
913  acc_cond::mark_t carry = {};
914  if (left_inf && right_inf)
915  {
916  carry = left_inf->mark;
917  auto pos = left_inf - &(*this)[0];
918  erase(begin() + pos, begin() + pos + 2);
919  }
920  auto sz = size();
921  insert(end(), &r[0], right_end + 1);
922  if (carry)
923  (*this)[sz + (right_inf - &r[0])].mark |= carry;
924 
925  acc_word w;
926  w.sub.op = acc_op::And;
927  w.sub.size = size();
928  emplace_back(w);
929  return *this;
930  }
931 
933  acc_code operator&(const acc_code& r) const
934  {
935  acc_code res = *this;
936  res &= r;
937  return res;
938  }
939 
941  acc_code operator&(acc_code&& r) const
942  {
943  acc_code res = *this;
944  res &= r;
945  return res;
946  }
947 
950  {
951  if (is_t() || r.is_f())
952  return *this;
953  if (is_f() || r.is_t())
954  {
955  *this = r;
956  return *this;
957  }
958  unsigned s = size() - 1;
959  unsigned rs = r.size() - 1;
960  // Fin(a) | Fin(b) = Fin(a | b)
961  if (((*this)[s].sub.op == acc_op::Fin
962  && r[rs].sub.op == acc_op::Fin)
963  || ((*this)[s].sub.op == acc_op::FinNeg
964  && r[rs].sub.op == acc_op::FinNeg))
965  {
966  (*this)[s - 1].mark |= r[rs - 1].mark;
967  return *this;
968  }
969 
970  // In the more complex scenarios, left and right may both
971  // be disjunctions, and Fin(x) might be a member of each
972  // side. Find it if it exists.
973  // left_inf points to the left Inf mark if any.
974  // right_inf points to the right Inf mark if any.
975  acc_word* left_fin = nullptr;
976  if ((*this)[s].sub.op == acc_op::Or)
977  {
978  auto start = &(*this)[s] - (*this)[s].sub.size;
979  auto pos = &(*this)[s] - 1;
980  pop_back();
981  while (pos > start)
982  {
983  if (pos->sub.op == acc_op::Fin)
984  {
985  left_fin = pos - 1;
986  break;
987  }
988  pos -= pos->sub.size + 1;
989  }
990  }
991  else if ((*this)[s].sub.op == acc_op::Fin)
992  {
993  left_fin = &(*this)[s - 1];
994  }
995 
996  const acc_word* right_fin = nullptr;
997  auto right_end = &r.back();
998  if (right_end->sub.op == acc_op::Or)
999  {
1000  auto start = &r[0];
1001  auto pos = --right_end;
1002  while (pos > start)
1003  {
1004  if (pos->sub.op == acc_op::Fin)
1005  {
1006  right_fin = pos - 1;
1007  break;
1008  }
1009  pos -= pos->sub.size + 1;
1010  }
1011  }
1012  else if (right_end->sub.op == acc_op::Fin)
1013  {
1014  right_fin = right_end - 1;
1015  }
1016 
1017  acc_cond::mark_t carry = {};
1018  if (left_fin && right_fin)
1019  {
1020  carry = left_fin->mark;
1021  auto pos = (left_fin - &(*this)[0]);
1022  this->erase(begin() + pos, begin() + pos + 2);
1023  }
1024  auto sz = size();
1025  insert(end(), &r[0], right_end + 1);
1026  if (carry)
1027  (*this)[sz + (right_fin - &r[0])].mark |= carry;
1028  acc_word w;
1029  w.sub.op = acc_op::Or;
1030  w.sub.size = size();
1031  emplace_back(w);
1032  return *this;
1033  }
1034 
1037  {
1038  acc_code res = *this;
1039  res |= r;
1040  return res;
1041  }
1042 
1044  acc_code operator|(const acc_code& r) const
1045  {
1046  acc_code res = *this;
1047  res |= r;
1048  return res;
1049  }
1050 
1056  acc_code& operator<<=(unsigned sets)
1057  {
1058  if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1059  report_too_many_sets();
1060  if (empty())
1061  return *this;
1062  unsigned pos = size();
1063  do
1064  {
1065  switch ((*this)[pos - 1].sub.op)
1066  {
1067  case acc_cond::acc_op::And:
1068  case acc_cond::acc_op::Or:
1069  --pos;
1070  break;
1071  case acc_cond::acc_op::Inf:
1072  case acc_cond::acc_op::InfNeg:
1073  case acc_cond::acc_op::Fin:
1074  case acc_cond::acc_op::FinNeg:
1075  pos -= 2;
1076  (*this)[pos].mark <<= sets;
1077  break;
1078  }
1079  }
1080  while (pos > 0);
1081  return *this;
1082  }
1083 
1087  acc_code operator<<(unsigned sets) const
1088  {
1089  acc_code res = *this;
1090  res <<= sets;
1091  return res;
1092  }
1093 
1100  bool is_dnf() const;
1101 
1108  bool is_cnf() const;
1109 
1120  acc_code to_dnf() const;
1121 
1128  acc_code to_cnf() const;
1129 
1130 
1139  std::vector<acc_code> top_disjuncts() const;
1140 
1149  std::vector<acc_code> top_conjuncts() const;
1150 
1161  acc_code complement() const;
1162 
1174  mark_t fin_unit() const;
1175 
1180  int fin_one() const;
1181 
1194  std::vector<std::vector<int>>
1195  missing(mark_t inf, bool accepting) const;
1196 
1199  bool accepting(mark_t inf) const;
1200 
1206  bool inf_satisfiable(mark_t inf) const;
1207 
1219  trival maybe_accepting(mark_t infinitely_often,
1220  mark_t always_present) const;
1221 
1232  std::vector<unsigned> symmetries() const;
1233 
1247  acc_code remove(acc_cond::mark_t rem, bool missing) const;
1248 
1253  acc_code strip(acc_cond::mark_t rem, bool missing) const;
1255  acc_code force_inf(mark_t m) const;
1256 
1258  acc_cond::mark_t used_sets() const;
1259 
1261  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1262 
1267  std::ostream&
1268  to_html(std::ostream& os,
1269  std::function<void(std::ostream&, int)>
1270  set_printer = nullptr) const;
1271 
1276  std::ostream&
1277  to_text(std::ostream& os,
1278  std::function<void(std::ostream&, int)>
1279  set_printer = nullptr) const;
1280 
1285  std::ostream&
1286  to_latex(std::ostream& os,
1287  std::function<void(std::ostream&, int)>
1288  set_printer = nullptr) const;
1289 
1312  acc_code(const char* input);
1313 
1318  {
1319  }
1320 
1322  acc_code(const acc_word* other)
1323  : std::vector<acc_word>(other - other->sub.size, other + 1)
1324  {
1325  }
1326 
1328  SPOT_API
1329  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1330  };
1331 
1339  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1340  : num_(0U), all_({}), code_(code)
1341  {
1342  add_sets(n_sets);
1343  uses_fin_acceptance_ = check_fin_acceptance();
1344  }
1345 
1350  acc_cond(const acc_code& code)
1351  : num_(0U), all_({}), code_(code)
1352  {
1353  add_sets(code.used_sets().max_set());
1354  uses_fin_acceptance_ = check_fin_acceptance();
1355  }
1356 
1358  acc_cond(const acc_cond& o)
1359  : num_(o.num_), all_(o.all_), code_(o.code_),
1360  uses_fin_acceptance_(o.uses_fin_acceptance_)
1361  {
1362  }
1363 
1366  {
1367  num_ = o.num_;
1368  all_ = o.all_;
1369  code_ = o.code_;
1370  uses_fin_acceptance_ = o.uses_fin_acceptance_;
1371  return *this;
1372  }
1373 
1374  ~acc_cond()
1375  {
1376  }
1377 
1381  void set_acceptance(const acc_code& code)
1382  {
1383  code_ = code;
1384  uses_fin_acceptance_ = check_fin_acceptance();
1385  }
1386 
1388  const acc_code& get_acceptance() const
1389  {
1390  return code_;
1391  }
1392 
1395  {
1396  return code_;
1397  }
1398 
1399  bool operator==(const acc_cond& other) const
1400  {
1401  return other.num_sets() == num_ && other.get_acceptance() == code_;
1402  }
1403 
1404  bool operator!=(const acc_cond& other) const
1405  {
1406  return !(*this == other);
1407  }
1408 
1410  bool uses_fin_acceptance() const
1411  {
1412  return uses_fin_acceptance_;
1413  }
1414 
1416  bool is_t() const
1417  {
1418  return code_.is_t();
1419  }
1420 
1425  bool is_all() const
1426  {
1427  return num_ == 0 && is_t();
1428  }
1429 
1431  bool is_f() const
1432  {
1433  return code_.is_f();
1434  }
1435 
1440  bool is_none() const
1441  {
1442  return num_ == 0 && is_f();
1443  }
1444 
1449  bool is_buchi() const
1450  {
1451  unsigned s = code_.size();
1452  return num_ == 1 &&
1453  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1454  }
1455 
1460  bool is_co_buchi() const
1461  {
1462  return num_ == 1 && is_generalized_co_buchi();
1463  }
1464 
1468  {
1469  set_acceptance(inf(all_sets()));
1470  }
1471 
1475  {
1476  set_acceptance(fin(all_sets()));
1477  }
1478 
1484  {
1485  unsigned s = code_.size();
1486  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1487  && code_[0].mark == all_sets());
1488  }
1489 
1495  {
1496  unsigned s = code_.size();
1497  return (s == 2 &&
1498  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1499  }
1500 
1512  int is_rabin() const;
1513 
1525  int is_streett() const;
1526 
1536  struct SPOT_API rs_pair
1537  {
1538 #ifndef SWIG
1539  rs_pair() = default;
1540  rs_pair(const rs_pair&) = default;
1541 #endif
1542 
1543  rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1544  fin(fin),
1545  inf(inf)
1546  {}
1547  acc_cond::mark_t fin;
1548  acc_cond::mark_t inf;
1549 
1550  bool operator==(rs_pair o) const
1551  {
1552  return fin == o.fin && inf == o.inf;
1553  }
1554  bool operator!=(rs_pair o) const
1555  {
1556  return fin != o.fin || inf != o.inf;
1557  }
1558  bool operator<(rs_pair o) const
1559  {
1560  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1561  }
1562  bool operator<=(rs_pair o) const
1563  {
1564  return !(o < *this);
1565  }
1566  bool operator>(rs_pair o) const
1567  {
1568  return o < *this;
1569  }
1570  bool operator>=(rs_pair o) const
1571  {
1572  return !(*this < o);
1573  }
1574  };
1585  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1586 
1597  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1598 
1608  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1609 
1622  bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1623 
1633  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1634 
1637  bool is_parity() const
1638  {
1639  bool max;
1640  bool odd;
1641  return is_parity(max, odd);
1642  }
1643 
1644  // Return (true, m) if there exist some acceptance mark m that
1645  // does not satisfy the acceptance condition. Return (false, 0U)
1646  // otherwise.
1647  std::pair<bool, acc_cond::mark_t> unsat_mark() const
1648  {
1649  return sat_unsat_mark(false);
1650  }
1651  // Return (true, m) if there exist some acceptance mark m that
1652  // does satisfy the acceptance condition. Return (false, 0U)
1653  // otherwise.
1654  std::pair<bool, acc_cond::mark_t> sat_mark() const
1655  {
1656  return sat_unsat_mark(true);
1657  }
1658 
1659  protected:
1660  bool check_fin_acceptance() const;
1661  std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1662 
1663  public:
1672  static acc_code inf(mark_t mark)
1673  {
1674  return acc_code::inf(mark);
1675  }
1676 
1677  static acc_code inf(std::initializer_list<unsigned> vals)
1678  {
1679  return inf(mark_t(vals.begin(), vals.end()));
1680  }
1682 
1699  static acc_code inf_neg(mark_t mark)
1700  {
1701  return acc_code::inf_neg(mark);
1702  }
1703 
1704  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1705  {
1706  return inf_neg(mark_t(vals.begin(), vals.end()));
1707  }
1709 
1717  static acc_code fin(mark_t mark)
1718  {
1719  return acc_code::fin(mark);
1720  }
1721 
1722  static acc_code fin(std::initializer_list<unsigned> vals)
1723  {
1724  return fin(mark_t(vals.begin(), vals.end()));
1725  }
1727 
1744  static acc_code fin_neg(mark_t mark)
1745  {
1746  return acc_code::fin_neg(mark);
1747  }
1748 
1749  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1750  {
1751  return fin_neg(mark_t(vals.begin(), vals.end()));
1752  }
1754 
1759  unsigned add_sets(unsigned num)
1760  {
1761  if (num == 0)
1762  return -1U;
1763  unsigned j = num_;
1764  num += j;
1765  if (num > mark_t::max_accsets())
1766  report_too_many_sets();
1767  // Make sure we do not update if we raised an exception.
1768  num_ = num;
1769  all_ = all_sets_();
1770  return j;
1771  }
1772 
1777  unsigned add_set()
1778  {
1779  return add_sets(1);
1780  }
1781 
1783  mark_t mark(unsigned u) const
1784  {
1785  SPOT_ASSERT(u < num_sets());
1786  return mark_t({u});
1787  }
1788 
1793  mark_t comp(const mark_t& l) const
1794  {
1795  return all_ ^ l;
1796  }
1797 
1800  {
1801  return all_;
1802  }
1803 
1806  bool accepting(mark_t inf) const
1807  {
1808  return code_.accepting(inf);
1809  }
1810 
1816  bool inf_satisfiable(mark_t inf) const
1817  {
1818  return code_.inf_satisfiable(inf);
1819  }
1820 
1832  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
1833  {
1834  return code_.maybe_accepting(infinitely_often, always_present);
1835  }
1836 
1850  mark_t accepting_sets(mark_t inf) const;
1851 
1852  // Deprecated since Spot 2.8
1853  SPOT_DEPRECATED("Use operator<< instead.")
1854  std::ostream& format(std::ostream& os, mark_t m) const
1855  {
1856  if (!m)
1857  return os;
1858  return os << m;
1859  }
1860 
1861  // Deprecated since Spot 2.8
1862  SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
1863  std::string format(mark_t m) const
1864  {
1865  std::ostringstream os;
1866  if (m)
1867  os << m;
1868  return os.str();
1869  }
1870 
1872  unsigned num_sets() const
1873  {
1874  return num_;
1875  }
1876 
1884  template<class iterator>
1885  mark_t useless(iterator begin, iterator end) const
1886  {
1887  mark_t u = {}; // The set of useless sets
1888  for (unsigned x = 0; x < num_; ++x)
1889  {
1890  // Skip sets that are already known to be useless.
1891  if (u.has(x))
1892  continue;
1893  auto all = comp(u | mark_t({x}));
1894  // Iterate over all mark_t, and keep track of
1895  // set numbers that always appear with x.
1896  for (iterator y = begin; y != end; ++y)
1897  {
1898  const mark_t& v = *y;
1899  if (v.has(x))
1900  {
1901  all &= v;
1902  if (!all)
1903  break;
1904  }
1905  }
1906  u |= all;
1907  }
1908  return u;
1909  }
1910 
1924  acc_cond remove(mark_t rem, bool missing) const
1925  {
1926  return {num_sets(), code_.remove(rem, missing)};
1927  }
1928 
1933  acc_cond strip(mark_t rem, bool missing) const
1934  {
1935  return
1936  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
1937  }
1938 
1941  {
1942  return {num_sets(), code_.force_inf(m)};
1943  }
1944 
1948  {
1949  return {num_sets(), code_.remove(all_sets() - rem, true)};
1950  }
1951 
1963  std::string name(const char* fmt = "alo") const;
1964 
1977  {
1978  return code_.fin_unit();
1979  }
1980 
1985  int fin_one() const
1986  {
1987  return code_.fin_one();
1988  }
1989 
1998  std::vector<acc_cond> top_disjuncts() const;
1999 
2008  std::vector<acc_cond> top_conjuncts() const;
2009 
2010  protected:
2011  mark_t all_sets_() const
2012  {
2013  return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2014  }
2015 
2016  unsigned num_;
2017  mark_t all_;
2018  acc_code code_;
2019  bool uses_fin_acceptance_ = false;
2020 
2021  };
2022 
2023  struct rs_pairs_view {
2024  typedef std::vector<acc_cond::rs_pair> rs_pairs;
2025 
2026  // Creates view of pairs 'p' with restriction only to marks in 'm'
2027  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2028  : pairs_(p), view_marks_(m) {}
2029 
2030  // Creates view of pairs without restriction to marks
2031  explicit rs_pairs_view(const rs_pairs& p)
2033 
2034  acc_cond::mark_t infs() const
2035  {
2036  return do_view([&](const acc_cond::rs_pair& p)
2037  {
2038  return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2039  });
2040  }
2041 
2042  acc_cond::mark_t fins() const
2043  {
2044  return do_view([&](const acc_cond::rs_pair& p)
2045  {
2046  return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2047  });
2048  }
2049 
2050  acc_cond::mark_t fins_alone() const
2051  {
2052  return do_view([&](const acc_cond::rs_pair& p)
2053  {
2054  return !visible(p.inf) && visible(p.fin) ? p.fin
2055  : acc_cond::mark_t({});
2056  });
2057  }
2058 
2059  acc_cond::mark_t infs_alone() const
2060  {
2061  return do_view([&](const acc_cond::rs_pair& p)
2062  {
2063  return !visible(p.fin) && visible(p.inf) ? p.inf
2064  : acc_cond::mark_t({});
2065  });
2066  }
2067 
2068  acc_cond::mark_t paired_with_fin(unsigned mark) const
2069  {
2070  acc_cond::mark_t res = {};
2071  for (const auto& p: pairs_)
2072  if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2073  res |= p.inf;
2074  return res;
2075  }
2076 
2077  const rs_pairs& pairs() const
2078  {
2079  return pairs_;
2080  }
2081 
2082  private:
2083  template<typename filter>
2084  acc_cond::mark_t do_view(const filter& filt) const
2085  {
2086  acc_cond::mark_t res = {};
2087  for (const auto& p: pairs_)
2088  res |= filt(p);
2089  return res;
2090  }
2091 
2092  bool visible(const acc_cond::mark_t& v) const
2093  {
2094  return !!(view_marks_ & v);
2095  }
2096 
2097  const rs_pairs& pairs_;
2098  acc_cond::mark_t view_marks_;
2099  };
2100 
2101 
2102  SPOT_API
2103  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2104 
2106 
2107  namespace internal
2108  {
2109  class SPOT_API mark_iterator
2110  {
2111  public:
2112  typedef unsigned value_type;
2113  typedef const value_type& reference;
2114  typedef const value_type* pointer;
2115  typedef std::ptrdiff_t difference_type;
2116  typedef std::forward_iterator_tag iterator_category;
2117 
2118  mark_iterator() noexcept
2119  : m_({})
2120  {
2121  }
2122 
2123  mark_iterator(acc_cond::mark_t m) noexcept
2124  : m_(m)
2125  {
2126  }
2127 
2128  bool operator==(mark_iterator m) const
2129  {
2130  return m_ == m.m_;
2131  }
2132 
2133  bool operator!=(mark_iterator m) const
2134  {
2135  return m_ != m.m_;
2136  }
2137 
2138  value_type operator*() const
2139  {
2140  SPOT_ASSERT(m_);
2141  return m_.min_set() - 1;
2142  }
2143 
2144  mark_iterator& operator++()
2145  {
2146  m_.clear(this->operator*());
2147  return *this;
2148  }
2149 
2150  mark_iterator operator++(int)
2151  {
2152  mark_iterator it = *this;
2153  ++(*this);
2154  return it;
2155  }
2156  private:
2157  acc_cond::mark_t m_;
2158  };
2159 
2160  class SPOT_API mark_container
2161  {
2162  public:
2164  : m_(m)
2165  {
2166  }
2167 
2168  mark_iterator begin() const
2169  {
2170  return {m_};
2171  }
2172  mark_iterator end() const
2173  {
2174  return {};
2175  }
2176  private:
2178  };
2179  }
2180 
2182  {
2183  return {*this};
2184  }
2185 }
2186 
2187 namespace std
2188 {
2189  template<>
2190  struct hash<spot::acc_cond::mark_t>
2191  {
2192  size_t operator()(spot::acc_cond::mark_t m) const noexcept
2193  {
2194  return m.hash();
2195  }
2196  };
2197 }
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:665
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:133
Definition: automata.hh:26
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:362
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:374
bool is_all() const
Whether the acceptance condition is "all".
Definition: acc.hh:1425
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1799
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2181
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1717
Definition: acc.hh:2109
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:1940
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1431
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:569
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:1816
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition: acc.hh:1449
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1759
acc_op
Operators for acceptance formulas.
Definition: acc.hh:419
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1749
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1783
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:350
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1410
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1536
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:391
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1388
Definition: bitset.hh:37
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:583
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1672
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:101
Definition: bitset.hh:405
Definition: acc.hh:2023
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:1947
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:328
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1722
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:143
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1087
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:776
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1483
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1381
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:335
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1744
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1036
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1322
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1699
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:1924
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:382
bool is_none() const
Whether the acceptance condition is "none".
Definition: acc.hh:1440
An acceptance condition.
Definition: acc.hh:58
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:1933
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1365
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1339
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:109
A "node" in an acceptance formulas.
Definition: acc.hh:429
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:949
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:675
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1474
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:619
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:1985
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:716
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1704
(omega-Rational) Or
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1394
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1460
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition: acc.hh:1793
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:597
Definition: twa.hh:1721
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:724
unsigned count() const
Number of bits sets.
Definition: acc.hh:341
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:697
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1317
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1494
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition: acc.hh:1976
op
Operator types.
Definition: formula.hh:64
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:1637
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1056
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:1872
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1677
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:734
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1358
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1044
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:761
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1777
Definition: acc.hh:38
An acceptance formula.
Definition: acc.hh:451
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:609
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition: acc.hh:800
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:1885
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition: acc.hh:1350
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition...
Definition: acc.hh:1806
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1416
Definition: acc.hh:2160
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:1832
(omega-Rational) And
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1467
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:641
An acceptance mark.
Definition: acc.hh:81
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:707
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:651
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:748
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:555

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