spot  2.8.3
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  if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
106  set(*i);
107  else
108  report_too_many_sets();
109  }
110 
112  mark_t(std::initializer_list<unsigned> vals)
113  : mark_t(vals.begin(), vals.end())
114  {
115  }
116 
117  SPOT_DEPRECATED("use brace initialization instead")
118  mark_t(unsigned i)
119  {
120  unsigned j = 0;
121  while (i)
122  {
123  if (i & 1U)
124  this->set(j);
125  ++j;
126  i >>= 1;
127  }
128  }
129 #endif
130 
136  constexpr static unsigned max_accsets()
137  {
138  return SPOT_MAX_ACCSETS;
139  }
140 
146  static mark_t all()
147  {
148  return mark_t(_value_t::mone());
149  }
150 
151  size_t hash() const noexcept
152  {
153  std::hash<decltype(id)> h;
154  return h(id);
155  }
156 
157  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
158  bool operator==(unsigned o) const
159  {
160  SPOT_ASSERT(o == 0U);
161  (void)o;
162  return !id;
163  }
164 
165  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
166  bool operator!=(unsigned o) const
167  {
168  SPOT_ASSERT(o == 0U);
169  (void)o;
170  return !!id;
171  }
172 
173  bool operator==(mark_t o) const
174  {
175  return id == o.id;
176  }
177 
178  bool operator!=(mark_t o) const
179  {
180  return id != o.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  explicit operator bool() const
204  {
205  return !!id;
206  }
207 
208  bool has(unsigned u) const
209  {
210  return !!this->operator&(mark_t({0}) << u);
211  }
212 
213  void set(unsigned u)
214  {
215  id.set(u);
216  }
217 
218  void clear(unsigned u)
219  {
220  id.clear(u);
221  }
222 
223  mark_t& operator&=(mark_t r)
224  {
225  id &= r.id;
226  return *this;
227  }
228 
229  mark_t& operator|=(mark_t r)
230  {
231  id |= r.id;
232  return *this;
233  }
234 
235  mark_t& operator-=(mark_t r)
236  {
237  id &= ~r.id;
238  return *this;
239  }
240 
241  mark_t& operator^=(mark_t r)
242  {
243  id ^= r.id;
244  return *this;
245  }
246 
247  mark_t operator&(mark_t r) const
248  {
249  return id & r.id;
250  }
251 
252  mark_t operator|(mark_t r) const
253  {
254  return id | r.id;
255  }
256 
257  mark_t operator-(mark_t r) const
258  {
259  return id & ~r.id;
260  }
261 
262  mark_t operator~() const
263  {
264  return ~id;
265  }
266 
267  mark_t operator^(mark_t r) const
268  {
269  return id ^ r.id;
270  }
271 
272 #if SPOT_DEBUG || defined(SWIGPYTHON)
273 # define SPOT_WRAP_OP(ins) \
274  try \
275  { \
276  ins; \
277  } \
278  catch (const std::runtime_error& e) \
279  { \
280  report_too_many_sets(); \
281  }
282 #else
283 # define SPOT_WRAP_OP(ins) ins;
284 #endif
285  mark_t operator<<(unsigned i) const
286  {
287  SPOT_WRAP_OP(return id << i);
288  }
289 
290  mark_t& operator<<=(unsigned i)
291  {
292  SPOT_WRAP_OP(id <<= i; return *this);
293  }
294 
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 #undef SPOT_WRAP_OP
305 
306  mark_t strip(mark_t y) const
307  {
308  // strip every bit of id that is marked in y
309  // 100101110100.strip(
310  // 001011001000)
311  // == 10 1 11 100
312  // == 10111100
313 
314  auto xv = id; // 100101110100
315  auto yv = y.id; // 001011001000
316 
317  while (yv && xv)
318  {
319  // Mask for everything after the last 1 in y
320  auto rm = (~yv) & (yv - 1); // 000000000111
321  // Mask for everything before the last 1 in y
322  auto lm = ~(yv ^ (yv - 1)); // 111111110000
323  xv = ((xv & lm) >> 1) | (xv & rm);
324  yv = (yv & lm) >> 1;
325  }
326  return xv;
327  }
328 
331  bool subset(mark_t m) const
332  {
333  return !((*this) - m);
334  }
335 
338  bool proper_subset(mark_t m) const
339  {
340  return *this != m && this->subset(m);
341  }
342 
344  unsigned count() const
345  {
346  return id.count();
347  }
348 
353  unsigned max_set() const
354  {
355  if (id)
356  return id.highest()+1;
357  else
358  return 0;
359  }
360 
365  unsigned min_set() const
366  {
367  if (id)
368  return id.lowest()+1;
369  else
370  return 0;
371  }
372 
377  mark_t lowest() const
378  {
379  return id & -id;
380  }
381 
385  mark_t& remove_some(unsigned n)
386  {
387  while (n--)
388  id &= id - 1;
389  return *this;
390  }
391 
393  template<class iterator>
394  void fill(iterator here) const
395  {
396  auto a = *this;
397  unsigned level = 0;
398  while (a)
399  {
400  if (a.has(0))
401  *here++ = level;
402  ++level;
403  a >>= 1;
404  }
405  }
406 
408  spot::internal::mark_container sets() const;
409 
410  SPOT_API
411  friend std::ostream& operator<<(std::ostream& os, mark_t m);
412 
413  std::string as_string() const
414  {
415  std::ostringstream os;
416  os << *this;
417  return os.str();
418  }
419  };
420 
422  enum class acc_op : unsigned short
423  { Inf, Fin, InfNeg, FinNeg, And, Or };
424 
432  union acc_word
433  {
434  mark_t mark;
435  struct {
436  acc_op op; // Operator
437  unsigned short size; // Size of the subtree (number of acc_word),
438  // not counting this node.
439  } sub;
440  };
441 
454  struct SPOT_API acc_code: public std::vector<acc_word>
455  {
456  bool operator==(const acc_code& other) const
457  {
458  unsigned pos = size();
459  if (other.size() != pos)
460  return false;
461  while (pos > 0)
462  {
463  auto op = (*this)[pos - 1].sub.op;
464  auto sz = (*this)[pos - 1].sub.size;
465  if (other[pos - 1].sub.op != op ||
466  other[pos - 1].sub.size != sz)
467  return false;
468  switch (op)
469  {
470  case acc_cond::acc_op::And:
471  case acc_cond::acc_op::Or:
472  --pos;
473  break;
474  case acc_cond::acc_op::Inf:
475  case acc_cond::acc_op::InfNeg:
476  case acc_cond::acc_op::Fin:
477  case acc_cond::acc_op::FinNeg:
478  pos -= 2;
479  if (other[pos].mark != (*this)[pos].mark)
480  return false;
481  break;
482  }
483  }
484  return true;
485  };
486 
487  bool operator<(const acc_code& other) const
488  {
489  unsigned pos = size();
490  auto osize = other.size();
491  if (pos < osize)
492  return true;
493  if (pos > osize)
494  return false;
495  while (pos > 0)
496  {
497  auto op = (*this)[pos - 1].sub.op;
498  auto oop = other[pos - 1].sub.op;
499  if (op < oop)
500  return true;
501  if (op > oop)
502  return false;
503  auto sz = (*this)[pos - 1].sub.size;
504  auto osz = other[pos - 1].sub.size;
505  if (sz < osz)
506  return true;
507  if (sz > osz)
508  return false;
509  switch (op)
510  {
511  case acc_cond::acc_op::And:
512  case acc_cond::acc_op::Or:
513  --pos;
514  break;
515  case acc_cond::acc_op::Inf:
516  case acc_cond::acc_op::InfNeg:
517  case acc_cond::acc_op::Fin:
518  case acc_cond::acc_op::FinNeg:
519  {
520  pos -= 2;
521  auto m = (*this)[pos].mark;
522  auto om = other[pos].mark;
523  if (m < om)
524  return true;
525  if (m > om)
526  return false;
527  break;
528  }
529  }
530  }
531  return false;
532  }
533 
534  bool operator>(const acc_code& other) const
535  {
536  return other < *this;
537  }
538 
539  bool operator<=(const acc_code& other) const
540  {
541  return !(other < *this);
542  }
543 
544  bool operator>=(const acc_code& other) const
545  {
546  return !(*this < other);
547  }
548 
549  bool operator!=(const acc_code& other) const
550  {
551  return !(*this == other);
552  }
553 
558  bool is_t() const
559  {
560  // We store "t" as an empty condition, or as Inf({}).
561  unsigned s = size();
562  return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
563  && !((*this)[s - 2].mark));
564  }
565 
572  bool is_f() const
573  {
574  // We store "f" as Fin({}).
575  unsigned s = size();
576  return s > 1
577  && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
578  }
579 
586  static acc_code f()
587  {
588  acc_code res;
589  res.resize(2);
590  res[0].mark = {};
591  res[1].sub.op = acc_op::Fin;
592  res[1].sub.size = 1;
593  return res;
594  }
595 
600  static acc_code t()
601  {
602  return {};
603  }
604 
612  static acc_code fin(mark_t m)
613  {
614  acc_code res;
615  res.resize(2);
616  res[0].mark = m;
617  res[1].sub.op = acc_op::Fin;
618  res[1].sub.size = 1;
619  return res;
620  }
621 
622  static acc_code fin(std::initializer_list<unsigned> vals)
623  {
624  return fin(mark_t(vals));
625  }
627 
645  {
646  acc_code res;
647  res.resize(2);
648  res[0].mark = m;
649  res[1].sub.op = acc_op::FinNeg;
650  res[1].sub.size = 1;
651  return res;
652  }
653 
654  static acc_code fin_neg(std::initializer_list<unsigned> vals)
655  {
656  return fin_neg(mark_t(vals));
657  }
659 
668  static acc_code inf(mark_t m)
669  {
670  acc_code res;
671  res.resize(2);
672  res[0].mark = m;
673  res[1].sub.op = acc_op::Inf;
674  res[1].sub.size = 1;
675  return res;
676  }
677 
678  static acc_code inf(std::initializer_list<unsigned> vals)
679  {
680  return inf(mark_t(vals));
681  }
683 
701  {
702  acc_code res;
703  res.resize(2);
704  res[0].mark = m;
705  res[1].sub.op = acc_op::InfNeg;
706  res[1].sub.size = 1;
707  return res;
708  }
709 
710  static acc_code inf_neg(std::initializer_list<unsigned> vals)
711  {
712  return inf_neg(mark_t(vals));
713  }
715 
719  static acc_code buchi()
720  {
721  return inf({0});
722  }
723 
727  static acc_code cobuchi()
728  {
729  return fin({0});
730  }
731 
737  static acc_code generalized_buchi(unsigned n)
738  {
739  if (n == 0)
740  return inf({});
741  acc_cond::mark_t m = mark_t::all();
742  m >>= mark_t::max_accsets() - n;
743  return inf(m);
744  }
745 
751  static acc_code generalized_co_buchi(unsigned n)
752  {
753  if (n == 0)
754  return fin({});
755  acc_cond::mark_t m = mark_t::all();
756  m >>= mark_t::max_accsets() - n;
757  return fin(m);
758  }
759 
764  static acc_code rabin(unsigned n)
765  {
766  acc_cond::acc_code res = f();
767  while (n > 0)
768  {
769  res |= inf({2*n - 1}) & fin({2*n - 2});
770  --n;
771  }
772  return res;
773  }
774 
779  static acc_code streett(unsigned n)
780  {
781  acc_cond::acc_code res = t();
782  while (n > 0)
783  {
784  res &= inf({2*n - 1}) | fin({2*n - 2});
785  --n;
786  }
787  return res;
788  }
789 
802  template<class Iterator>
803  static acc_code generalized_rabin(Iterator begin, Iterator end)
804  {
805  acc_cond::acc_code res = f();
806  unsigned n = 0;
807  for (Iterator i = begin; i != end; ++i)
808  {
809  unsigned f = n++;
810  acc_cond::mark_t m = {};
811  for (unsigned ni = *i; ni > 0; --ni)
812  m.set(n++);
813  auto pair = inf(m) & fin({f});
814  std::swap(pair, res);
815  res |= std::move(pair);
816  }
817  return res;
818  }
819 
826  static acc_code parity(bool max, bool odd, unsigned sets);
827 
844  static acc_code random(unsigned n, double reuse = 0.0);
845 
847  acc_code& operator&=(const acc_code& r)
848  {
849  if (is_t() || r.is_f())
850  {
851  *this = r;
852  return *this;
853  }
854  if (is_f() || r.is_t())
855  return *this;
856  unsigned s = size() - 1;
857  unsigned rs = r.size() - 1;
858  // We want to group all Inf(x) operators:
859  // Inf(a) & Inf(b) = Inf(a & b)
860  if (((*this)[s].sub.op == acc_op::Inf
861  && r[rs].sub.op == acc_op::Inf)
862  || ((*this)[s].sub.op == acc_op::InfNeg
863  && r[rs].sub.op == acc_op::InfNeg))
864  {
865  (*this)[s - 1].mark |= r[rs - 1].mark;
866  return *this;
867  }
868 
869  // In the more complex scenarios, left and right may both
870  // be conjunctions, and Inf(x) might be a member of each
871  // side. Find it if it exists.
872  // left_inf points to the left Inf mark if any.
873  // right_inf points to the right Inf mark if any.
874  acc_word* left_inf = nullptr;
875  if ((*this)[s].sub.op == acc_op::And)
876  {
877  auto start = &(*this)[s] - (*this)[s].sub.size;
878  auto pos = &(*this)[s] - 1;
879  pop_back();
880  while (pos > start)
881  {
882  if (pos->sub.op == acc_op::Inf)
883  {
884  left_inf = pos - 1;
885  break;
886  }
887  pos -= pos->sub.size + 1;
888  }
889  }
890  else if ((*this)[s].sub.op == acc_op::Inf)
891  {
892  left_inf = &(*this)[s - 1];
893  }
894 
895  const acc_word* right_inf = nullptr;
896  auto right_end = &r.back();
897  if (right_end->sub.op == acc_op::And)
898  {
899  auto start = &r[0];
900  auto pos = --right_end;
901  while (pos > start)
902  {
903  if (pos->sub.op == acc_op::Inf)
904  {
905  right_inf = pos - 1;
906  break;
907  }
908  pos -= pos->sub.size + 1;
909  }
910  }
911  else if (right_end->sub.op == acc_op::Inf)
912  {
913  right_inf = right_end - 1;
914  }
915 
916  acc_cond::mark_t carry = {};
917  if (left_inf && right_inf)
918  {
919  carry = left_inf->mark;
920  auto pos = left_inf - &(*this)[0];
921  erase(begin() + pos, begin() + pos + 2);
922  }
923  auto sz = size();
924  insert(end(), &r[0], right_end + 1);
925  if (carry)
926  (*this)[sz + (right_inf - &r[0])].mark |= carry;
927 
928  acc_word w;
929  w.sub.op = acc_op::And;
930  w.sub.size = size();
931  emplace_back(w);
932  return *this;
933  }
934 
936  acc_code operator&(const acc_code& r) const
937  {
938  acc_code res = *this;
939  res &= r;
940  return res;
941  }
942 
944  acc_code operator&(acc_code&& r) const
945  {
946  acc_code res = *this;
947  res &= r;
948  return res;
949  }
950 
953  {
954  if (is_t() || r.is_f())
955  return *this;
956  if (is_f() || r.is_t())
957  {
958  *this = r;
959  return *this;
960  }
961  unsigned s = size() - 1;
962  unsigned rs = r.size() - 1;
963  // Fin(a) | Fin(b) = Fin(a | b)
964  if (((*this)[s].sub.op == acc_op::Fin
965  && r[rs].sub.op == acc_op::Fin)
966  || ((*this)[s].sub.op == acc_op::FinNeg
967  && r[rs].sub.op == acc_op::FinNeg))
968  {
969  (*this)[s - 1].mark |= r[rs - 1].mark;
970  return *this;
971  }
972 
973  // In the more complex scenarios, left and right may both
974  // be disjunctions, and Fin(x) might be a member of each
975  // side. Find it if it exists.
976  // left_inf points to the left Inf mark if any.
977  // right_inf points to the right Inf mark if any.
978  acc_word* left_fin = nullptr;
979  if ((*this)[s].sub.op == acc_op::Or)
980  {
981  auto start = &(*this)[s] - (*this)[s].sub.size;
982  auto pos = &(*this)[s] - 1;
983  pop_back();
984  while (pos > start)
985  {
986  if (pos->sub.op == acc_op::Fin)
987  {
988  left_fin = pos - 1;
989  break;
990  }
991  pos -= pos->sub.size + 1;
992  }
993  }
994  else if ((*this)[s].sub.op == acc_op::Fin)
995  {
996  left_fin = &(*this)[s - 1];
997  }
998 
999  const acc_word* right_fin = nullptr;
1000  auto right_end = &r.back();
1001  if (right_end->sub.op == acc_op::Or)
1002  {
1003  auto start = &r[0];
1004  auto pos = --right_end;
1005  while (pos > start)
1006  {
1007  if (pos->sub.op == acc_op::Fin)
1008  {
1009  right_fin = pos - 1;
1010  break;
1011  }
1012  pos -= pos->sub.size + 1;
1013  }
1014  }
1015  else if (right_end->sub.op == acc_op::Fin)
1016  {
1017  right_fin = right_end - 1;
1018  }
1019 
1020  acc_cond::mark_t carry = {};
1021  if (left_fin && right_fin)
1022  {
1023  carry = left_fin->mark;
1024  auto pos = (left_fin - &(*this)[0]);
1025  this->erase(begin() + pos, begin() + pos + 2);
1026  }
1027  auto sz = size();
1028  insert(end(), &r[0], right_end + 1);
1029  if (carry)
1030  (*this)[sz + (right_fin - &r[0])].mark |= carry;
1031  acc_word w;
1032  w.sub.op = acc_op::Or;
1033  w.sub.size = size();
1034  emplace_back(w);
1035  return *this;
1036  }
1037 
1040  {
1041  acc_code res = *this;
1042  res |= r;
1043  return res;
1044  }
1045 
1047  acc_code operator|(const acc_code& r) const
1048  {
1049  acc_code res = *this;
1050  res |= r;
1051  return res;
1052  }
1053 
1059  acc_code& operator<<=(unsigned sets)
1060  {
1061  if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1062  report_too_many_sets();
1063  if (empty())
1064  return *this;
1065  unsigned pos = size();
1066  do
1067  {
1068  switch ((*this)[pos - 1].sub.op)
1069  {
1070  case acc_cond::acc_op::And:
1071  case acc_cond::acc_op::Or:
1072  --pos;
1073  break;
1074  case acc_cond::acc_op::Inf:
1075  case acc_cond::acc_op::InfNeg:
1076  case acc_cond::acc_op::Fin:
1077  case acc_cond::acc_op::FinNeg:
1078  pos -= 2;
1079  (*this)[pos].mark <<= sets;
1080  break;
1081  }
1082  }
1083  while (pos > 0);
1084  return *this;
1085  }
1086 
1090  acc_code operator<<(unsigned sets) const
1091  {
1092  acc_code res = *this;
1093  res <<= sets;
1094  return res;
1095  }
1096 
1103  bool is_dnf() const;
1104 
1111  bool is_cnf() const;
1112 
1123  acc_code to_dnf() const;
1124 
1131  acc_code to_cnf() const;
1132 
1133 
1142  std::vector<acc_code> top_disjuncts() const;
1143 
1152  std::vector<acc_code> top_conjuncts() const;
1153 
1164  acc_code complement() const;
1165 
1177  mark_t fin_unit() const;
1178 
1183  int fin_one() const;
1184 
1197  std::vector<std::vector<int>>
1198  missing(mark_t inf, bool accepting) const;
1199 
1202  bool accepting(mark_t inf) const;
1203 
1209  bool inf_satisfiable(mark_t inf) const;
1210 
1222  trival maybe_accepting(mark_t infinitely_often,
1223  mark_t always_present) const;
1224 
1235  std::vector<unsigned> symmetries() const;
1236 
1250  acc_code remove(acc_cond::mark_t rem, bool missing) const;
1251 
1256  acc_code strip(acc_cond::mark_t rem, bool missing) const;
1258  acc_code force_inf(mark_t m) const;
1259 
1261  acc_cond::mark_t used_sets() const;
1262 
1264  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1265 
1270  std::ostream&
1271  to_html(std::ostream& os,
1272  std::function<void(std::ostream&, int)>
1273  set_printer = nullptr) const;
1274 
1279  std::ostream&
1280  to_text(std::ostream& os,
1281  std::function<void(std::ostream&, int)>
1282  set_printer = nullptr) const;
1283 
1288  std::ostream&
1289  to_latex(std::ostream& os,
1290  std::function<void(std::ostream&, int)>
1291  set_printer = nullptr) const;
1292 
1315  acc_code(const char* input);
1316 
1321  {
1322  }
1323 
1325  acc_code(const acc_word* other)
1326  : std::vector<acc_word>(other - other->sub.size, other + 1)
1327  {
1328  }
1329 
1331  SPOT_API
1332  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1333  };
1334 
1342  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1343  : num_(0U), all_({}), code_(code)
1344  {
1345  add_sets(n_sets);
1346  uses_fin_acceptance_ = check_fin_acceptance();
1347  }
1348 
1353  acc_cond(const acc_code& code)
1354  : num_(0U), all_({}), code_(code)
1355  {
1356  add_sets(code.used_sets().max_set());
1357  uses_fin_acceptance_ = check_fin_acceptance();
1358  }
1359 
1361  acc_cond(const acc_cond& o)
1362  : num_(o.num_), all_(o.all_), code_(o.code_),
1363  uses_fin_acceptance_(o.uses_fin_acceptance_)
1364  {
1365  }
1366 
1369  {
1370  num_ = o.num_;
1371  all_ = o.all_;
1372  code_ = o.code_;
1373  uses_fin_acceptance_ = o.uses_fin_acceptance_;
1374  return *this;
1375  }
1376 
1377  ~acc_cond()
1378  {
1379  }
1380 
1384  void set_acceptance(const acc_code& code)
1385  {
1386  code_ = code;
1387  uses_fin_acceptance_ = check_fin_acceptance();
1388  }
1389 
1391  const acc_code& get_acceptance() const
1392  {
1393  return code_;
1394  }
1395 
1398  {
1399  return code_;
1400  }
1401 
1402  bool operator==(const acc_cond& other) const
1403  {
1404  return other.num_sets() == num_ && other.get_acceptance() == code_;
1405  }
1406 
1407  bool operator!=(const acc_cond& other) const
1408  {
1409  return !(*this == other);
1410  }
1411 
1413  bool uses_fin_acceptance() const
1414  {
1415  return uses_fin_acceptance_;
1416  }
1417 
1419  bool is_t() const
1420  {
1421  return code_.is_t();
1422  }
1423 
1428  bool is_all() const
1429  {
1430  return num_ == 0 && is_t();
1431  }
1432 
1434  bool is_f() const
1435  {
1436  return code_.is_f();
1437  }
1438 
1443  bool is_none() const
1444  {
1445  return num_ == 0 && is_f();
1446  }
1447 
1452  bool is_buchi() const
1453  {
1454  unsigned s = code_.size();
1455  return num_ == 1 &&
1456  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1457  }
1458 
1463  bool is_co_buchi() const
1464  {
1465  return num_ == 1 && is_generalized_co_buchi();
1466  }
1467 
1471  {
1472  set_acceptance(inf(all_sets()));
1473  }
1474 
1478  {
1479  set_acceptance(fin(all_sets()));
1480  }
1481 
1487  {
1488  unsigned s = code_.size();
1489  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1490  && code_[0].mark == all_sets());
1491  }
1492 
1498  {
1499  unsigned s = code_.size();
1500  return (s == 2 &&
1501  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1502  }
1503 
1515  int is_rabin() const;
1516 
1528  int is_streett() const;
1529 
1539  struct SPOT_API rs_pair
1540  {
1541 #ifndef SWIG
1542  rs_pair() = default;
1543  rs_pair(const rs_pair&) = default;
1544 #endif
1545 
1546  rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1547  fin(fin),
1548  inf(inf)
1549  {}
1550  acc_cond::mark_t fin;
1551  acc_cond::mark_t inf;
1552 
1553  bool operator==(rs_pair o) const
1554  {
1555  return fin == o.fin && inf == o.inf;
1556  }
1557  bool operator!=(rs_pair o) const
1558  {
1559  return fin != o.fin || inf != o.inf;
1560  }
1561  bool operator<(rs_pair o) const
1562  {
1563  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1564  }
1565  bool operator<=(rs_pair o) const
1566  {
1567  return !(o < *this);
1568  }
1569  bool operator>(rs_pair o) const
1570  {
1571  return o < *this;
1572  }
1573  bool operator>=(rs_pair o) const
1574  {
1575  return !(*this < o);
1576  }
1577  };
1588  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1589 
1600  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1601 
1611  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1612 
1625  bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1626 
1636  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1637 
1640  bool is_parity() const
1641  {
1642  bool max;
1643  bool odd;
1644  return is_parity(max, odd);
1645  }
1646 
1647  // Return (true, m) if there exist some acceptance mark m that
1648  // does not satisfy the acceptance condition. Return (false, 0U)
1649  // otherwise.
1650  std::pair<bool, acc_cond::mark_t> unsat_mark() const
1651  {
1652  return sat_unsat_mark(false);
1653  }
1654  // Return (true, m) if there exist some acceptance mark m that
1655  // does satisfy the acceptance condition. Return (false, 0U)
1656  // otherwise.
1657  std::pair<bool, acc_cond::mark_t> sat_mark() const
1658  {
1659  return sat_unsat_mark(true);
1660  }
1661 
1662  protected:
1663  bool check_fin_acceptance() const;
1664  std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1665 
1666  public:
1675  static acc_code inf(mark_t mark)
1676  {
1677  return acc_code::inf(mark);
1678  }
1679 
1680  static acc_code inf(std::initializer_list<unsigned> vals)
1681  {
1682  return inf(mark_t(vals.begin(), vals.end()));
1683  }
1685 
1702  static acc_code inf_neg(mark_t mark)
1703  {
1704  return acc_code::inf_neg(mark);
1705  }
1706 
1707  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1708  {
1709  return inf_neg(mark_t(vals.begin(), vals.end()));
1710  }
1712 
1720  static acc_code fin(mark_t mark)
1721  {
1722  return acc_code::fin(mark);
1723  }
1724 
1725  static acc_code fin(std::initializer_list<unsigned> vals)
1726  {
1727  return fin(mark_t(vals.begin(), vals.end()));
1728  }
1730 
1747  static acc_code fin_neg(mark_t mark)
1748  {
1749  return acc_code::fin_neg(mark);
1750  }
1751 
1752  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1753  {
1754  return fin_neg(mark_t(vals.begin(), vals.end()));
1755  }
1757 
1762  unsigned add_sets(unsigned num)
1763  {
1764  if (num == 0)
1765  return -1U;
1766  unsigned j = num_;
1767  num += j;
1768  if (num > mark_t::max_accsets())
1769  report_too_many_sets();
1770  // Make sure we do not update if we raised an exception.
1771  num_ = num;
1772  all_ = all_sets_();
1773  return j;
1774  }
1775 
1780  unsigned add_set()
1781  {
1782  return add_sets(1);
1783  }
1784 
1786  mark_t mark(unsigned u) const
1787  {
1788  SPOT_ASSERT(u < num_sets());
1789  return mark_t({u});
1790  }
1791 
1796  mark_t comp(const mark_t& l) const
1797  {
1798  return all_ ^ l;
1799  }
1800 
1803  {
1804  return all_;
1805  }
1806 
1809  bool accepting(mark_t inf) const
1810  {
1811  return code_.accepting(inf);
1812  }
1813 
1819  bool inf_satisfiable(mark_t inf) const
1820  {
1821  return code_.inf_satisfiable(inf);
1822  }
1823 
1835  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
1836  {
1837  return code_.maybe_accepting(infinitely_often, always_present);
1838  }
1839 
1853  mark_t accepting_sets(mark_t inf) const;
1854 
1855  // Deprecated since Spot 2.8
1856  SPOT_DEPRECATED("Use operator<< instead.")
1857  std::ostream& format(std::ostream& os, mark_t m) const
1858  {
1859  if (!m)
1860  return os;
1861  return os << m;
1862  }
1863 
1864  // Deprecated since Spot 2.8
1865  SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
1866  std::string format(mark_t m) const
1867  {
1868  std::ostringstream os;
1869  if (m)
1870  os << m;
1871  return os.str();
1872  }
1873 
1875  unsigned num_sets() const
1876  {
1877  return num_;
1878  }
1879 
1887  template<class iterator>
1888  mark_t useless(iterator begin, iterator end) const
1889  {
1890  mark_t u = {}; // The set of useless sets
1891  for (unsigned x = 0; x < num_; ++x)
1892  {
1893  // Skip sets that are already known to be useless.
1894  if (u.has(x))
1895  continue;
1896  auto all = comp(u | mark_t({x}));
1897  // Iterate over all mark_t, and keep track of
1898  // set numbers that always appear with x.
1899  for (iterator y = begin; y != end; ++y)
1900  {
1901  const mark_t& v = *y;
1902  if (v.has(x))
1903  {
1904  all &= v;
1905  if (!all)
1906  break;
1907  }
1908  }
1909  u |= all;
1910  }
1911  return u;
1912  }
1913 
1927  acc_cond remove(mark_t rem, bool missing) const
1928  {
1929  return {num_sets(), code_.remove(rem, missing)};
1930  }
1931 
1936  acc_cond strip(mark_t rem, bool missing) const
1937  {
1938  return
1939  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
1940  }
1941 
1944  {
1945  return {num_sets(), code_.force_inf(m)};
1946  }
1947 
1951  {
1952  return {num_sets(), code_.remove(all_sets() - rem, true)};
1953  }
1954 
1966  std::string name(const char* fmt = "alo") const;
1967 
1980  {
1981  return code_.fin_unit();
1982  }
1983 
1988  int fin_one() const
1989  {
1990  return code_.fin_one();
1991  }
1992 
2001  std::vector<acc_cond> top_disjuncts() const;
2002 
2011  std::vector<acc_cond> top_conjuncts() const;
2012 
2013  protected:
2014  mark_t all_sets_() const
2015  {
2016  return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2017  }
2018 
2019  unsigned num_;
2020  mark_t all_;
2021  acc_code code_;
2022  bool uses_fin_acceptance_ = false;
2023 
2024  };
2025 
2026  struct rs_pairs_view {
2027  typedef std::vector<acc_cond::rs_pair> rs_pairs;
2028 
2029  // Creates view of pairs 'p' with restriction only to marks in 'm'
2030  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2031  : pairs_(p), view_marks_(m) {}
2032 
2033  // Creates view of pairs without restriction to marks
2034  explicit rs_pairs_view(const rs_pairs& p)
2036 
2037  acc_cond::mark_t infs() const
2038  {
2039  return do_view([&](const acc_cond::rs_pair& p)
2040  {
2041  return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2042  });
2043  }
2044 
2045  acc_cond::mark_t fins() const
2046  {
2047  return do_view([&](const acc_cond::rs_pair& p)
2048  {
2049  return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2050  });
2051  }
2052 
2053  acc_cond::mark_t fins_alone() const
2054  {
2055  return do_view([&](const acc_cond::rs_pair& p)
2056  {
2057  return !visible(p.inf) && visible(p.fin) ? p.fin
2058  : acc_cond::mark_t({});
2059  });
2060  }
2061 
2062  acc_cond::mark_t infs_alone() const
2063  {
2064  return do_view([&](const acc_cond::rs_pair& p)
2065  {
2066  return !visible(p.fin) && visible(p.inf) ? p.inf
2067  : acc_cond::mark_t({});
2068  });
2069  }
2070 
2071  acc_cond::mark_t paired_with_fin(unsigned mark) const
2072  {
2073  acc_cond::mark_t res = {};
2074  for (const auto& p: pairs_)
2075  if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2076  res |= p.inf;
2077  return res;
2078  }
2079 
2080  const rs_pairs& pairs() const
2081  {
2082  return pairs_;
2083  }
2084 
2085  private:
2086  template<typename filter>
2087  acc_cond::mark_t do_view(const filter& filt) const
2088  {
2089  acc_cond::mark_t res = {};
2090  for (const auto& p: pairs_)
2091  res |= filt(p);
2092  return res;
2093  }
2094 
2095  bool visible(const acc_cond::mark_t& v) const
2096  {
2097  return !!(view_marks_ & v);
2098  }
2099 
2100  const rs_pairs& pairs_;
2101  acc_cond::mark_t view_marks_;
2102  };
2103 
2104 
2105  SPOT_API
2106  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2107 
2109 
2110  namespace internal
2111  {
2112  class SPOT_API mark_iterator
2113  {
2114  public:
2115  typedef unsigned value_type;
2116  typedef const value_type& reference;
2117  typedef const value_type* pointer;
2118  typedef std::ptrdiff_t difference_type;
2119  typedef std::forward_iterator_tag iterator_category;
2120 
2121  mark_iterator() noexcept
2122  : m_({})
2123  {
2124  }
2125 
2126  mark_iterator(acc_cond::mark_t m) noexcept
2127  : m_(m)
2128  {
2129  }
2130 
2131  bool operator==(mark_iterator m) const
2132  {
2133  return m_ == m.m_;
2134  }
2135 
2136  bool operator!=(mark_iterator m) const
2137  {
2138  return m_ != m.m_;
2139  }
2140 
2141  value_type operator*() const
2142  {
2143  SPOT_ASSERT(m_);
2144  return m_.min_set() - 1;
2145  }
2146 
2147  mark_iterator& operator++()
2148  {
2149  m_.clear(this->operator*());
2150  return *this;
2151  }
2152 
2153  mark_iterator operator++(int)
2154  {
2155  mark_iterator it = *this;
2156  ++(*this);
2157  return it;
2158  }
2159  private:
2160  acc_cond::mark_t m_;
2161  };
2162 
2163  class SPOT_API mark_container
2164  {
2165  public:
2167  : m_(m)
2168  {
2169  }
2170 
2171  mark_iterator begin() const
2172  {
2173  return {m_};
2174  }
2175  mark_iterator end() const
2176  {
2177  return {};
2178  }
2179  private:
2181  };
2182  }
2183 
2185  {
2186  return {*this};
2187  }
2188 }
2189 
2190 namespace std
2191 {
2192  template<>
2193  struct hash<spot::acc_cond::mark_t>
2194  {
2195  size_t operator()(spot::acc_cond::mark_t m) const noexcept
2196  {
2197  return m.hash();
2198  }
2199  };
2200 }
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:668
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:136
Definition: automata.hh:26
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:365
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:377
bool is_all() const
Whether the acceptance condition is "all".
Definition: acc.hh:1428
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1802
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2184
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1720
Definition: acc.hh:2112
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:1943
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1434
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:572
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:1819
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition: acc.hh:1452
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1762
acc_op
Operators for acceptance formulas.
Definition: acc.hh:422
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1752
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1786
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:353
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1413
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1539
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:394
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1391
Definition: bitset.hh:37
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:586
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1675
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:2026
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:1950
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:331
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1725
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:146
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1090
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:779
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1486
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1384
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:338
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1747
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1039
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1325
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1702
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:1927
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:385
bool is_none() const
Whether the acceptance condition is "none".
Definition: acc.hh:1443
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:1936
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1368
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1342
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:112
A "node" in an acceptance formulas.
Definition: acc.hh:432
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:952
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:678
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1477
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:622
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:1988
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:719
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1707
(omega-Rational) Or
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1397
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1463
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition: acc.hh:1796
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:600
Definition: twa.hh:1721
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:727
unsigned count() const
Number of bits sets.
Definition: acc.hh:344
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:700
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1320
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1497
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition: acc.hh:1979
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:1640
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1059
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:1875
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1680
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:737
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1361
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1047
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:764
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1780
Definition: acc.hh:38
An acceptance formula.
Definition: acc.hh:454
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:612
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition: acc.hh:803
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:1888
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition: acc.hh:1353
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition...
Definition: acc.hh:1809
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1419
Definition: acc.hh:2163
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:1835
(omega-Rational) And
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1470
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:644
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:710
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:654
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:751
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:558

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