spot  2.10.6
acc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2021 Laboratoire de Recherche et Développement
3 // de l'Epita.
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <functional>
23 #include <sstream>
24 #include <vector>
25 #include <iostream>
26 #include <algorithm>
27 #include <numeric>
28 #include <bddx.h>
29 #include <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
110  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 
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 
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 
1207  bdd to_bdd(const bdd* map) const;
1208 
1217  std::vector<acc_code> top_disjuncts() const;
1218 
1227  std::vector<acc_code> top_conjuncts() const;
1228 
1240 
1252  mark_t fin_unit() const;
1253 
1265  mark_t inf_unit() const;
1266 
1271  int fin_one() const;
1272 
1290  std::pair<int, acc_code> fin_one_extract() const;
1291 
1304  std::vector<std::vector<int>>
1305  missing(mark_t inf, bool accepting) const;
1306 
1309  bool accepting(mark_t inf) const;
1310 
1316  bool inf_satisfiable(mark_t inf) const;
1317 
1329  trival maybe_accepting(mark_t infinitely_often,
1330  mark_t always_present) const;
1331 
1342  std::vector<unsigned> symmetries() const;
1343 
1357  acc_code remove(acc_cond::mark_t rem, bool missing) const;
1358 
1363  acc_code strip(acc_cond::mark_t rem, bool missing) const;
1366 
1369 
1381  std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
1383 
1391 
1393  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1394 
1399  std::ostream&
1400  to_html(std::ostream& os,
1401  std::function<void(std::ostream&, int)>
1402  set_printer = nullptr) const;
1403 
1408  std::ostream&
1409  to_text(std::ostream& os,
1410  std::function<void(std::ostream&, int)>
1411  set_printer = nullptr) const;
1412 
1417  std::ostream&
1418  to_latex(std::ostream& os,
1419  std::function<void(std::ostream&, int)>
1420  set_printer = nullptr) const;
1421 
1444  acc_code(const char* input);
1445 
1450  {
1451  }
1452 
1454  acc_code(const acc_word* other)
1455  : std::vector<acc_word>(other - other->sub.size, other + 1)
1456  {
1457  }
1458 
1460  SPOT_API
1461  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1462  };
1463 
1471  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1472  : num_(0U), all_({}), code_(code)
1473  {
1474  add_sets(n_sets);
1475  uses_fin_acceptance_ = check_fin_acceptance();
1476  }
1477 
1482  acc_cond(const acc_code& code)
1483  : num_(0U), all_({}), code_(code)
1484  {
1485  add_sets(code.used_sets().max_set());
1486  uses_fin_acceptance_ = check_fin_acceptance();
1487  }
1488 
1490  acc_cond(const acc_cond& o)
1491  : num_(o.num_), all_(o.all_), code_(o.code_),
1492  uses_fin_acceptance_(o.uses_fin_acceptance_)
1493  {
1494  }
1495 
1498  {
1499  num_ = o.num_;
1500  all_ = o.all_;
1501  code_ = o.code_;
1502  uses_fin_acceptance_ = o.uses_fin_acceptance_;
1503  return *this;
1504  }
1505 
1506  ~acc_cond()
1507  {
1508  }
1509 
1513  void set_acceptance(const acc_code& code)
1514  {
1515  code_ = code;
1516  uses_fin_acceptance_ = check_fin_acceptance();
1517  }
1518 
1520  const acc_code& get_acceptance() const
1521  {
1522  return code_;
1523  }
1524 
1527  {
1528  return code_;
1529  }
1530 
1531  bool operator==(const acc_cond& other) const
1532  {
1533  return other.num_sets() == num_ && other.get_acceptance() == code_;
1534  }
1535 
1536  bool operator!=(const acc_cond& other) const
1537  {
1538  return !(*this == other);
1539  }
1540 
1542  bool uses_fin_acceptance() const
1543  {
1544  return uses_fin_acceptance_;
1545  }
1546 
1548  bool is_t() const
1549  {
1550  return code_.is_t();
1551  }
1552 
1557  bool is_all() const
1558  {
1559  return num_ == 0 && is_t();
1560  }
1561 
1563  bool is_f() const
1564  {
1565  return code_.is_f();
1566  }
1567 
1572  bool is_none() const
1573  {
1574  return num_ == 0 && is_f();
1575  }
1576 
1581  bool is_buchi() const
1582  {
1583  unsigned s = code_.size();
1584  return num_ == 1 &&
1585  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1586  }
1587 
1592  bool is_co_buchi() const
1593  {
1594  return num_ == 1 && is_generalized_co_buchi();
1595  }
1596 
1600  {
1601  set_acceptance(inf(all_sets()));
1602  }
1603 
1607  {
1608  set_acceptance(fin(all_sets()));
1609  }
1610 
1616  {
1617  unsigned s = code_.size();
1618  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1619  && code_[0].mark == all_sets());
1620  }
1621 
1627  {
1628  unsigned s = code_.size();
1629  return (s == 2 &&
1630  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1631  }
1632 
1644  int is_rabin() const;
1645 
1657  int is_streett() const;
1658 
1668  struct SPOT_API rs_pair
1669  {
1670 #ifndef SWIG
1671  rs_pair() = default;
1672  rs_pair(const rs_pair&) = default;
1673  rs_pair& operator=(const rs_pair&) = default;
1674 #endif
1675 
1676  rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1677  fin(fin),
1678  inf(inf)
1679  {}
1680  acc_cond::mark_t fin;
1681  acc_cond::mark_t inf;
1682 
1683  bool operator==(rs_pair o) const
1684  {
1685  return fin == o.fin && inf == o.inf;
1686  }
1687  bool operator!=(rs_pair o) const
1688  {
1689  return fin != o.fin || inf != o.inf;
1690  }
1691  bool operator<(rs_pair o) const
1692  {
1693  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1694  }
1695  bool operator<=(rs_pair o) const
1696  {
1697  return !(o < *this);
1698  }
1699  bool operator>(rs_pair o) const
1700  {
1701  return o < *this;
1702  }
1703  bool operator>=(rs_pair o) const
1704  {
1705  return !(*this < o);
1706  }
1707  };
1718  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1719 
1730  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1731 
1741  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1742 
1755  bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1756 
1766  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1767 
1768 
1769  bool is_parity_max_equiv(std::vector<int>& permut, bool even) const;
1770 
1773  bool is_parity() const
1774  {
1775  bool max;
1776  bool odd;
1777  return is_parity(max, odd);
1778  }
1779 
1788  {
1789  return acc_cond(num_, code_.unit_propagation());
1790  }
1791 
1792  // Return (true, m) if there exist some acceptance mark m that
1793  // does not satisfy the acceptance condition. Return (false, 0U)
1794  // otherwise.
1795  std::pair<bool, acc_cond::mark_t> unsat_mark() const
1796  {
1797  return sat_unsat_mark(false);
1798  }
1799  // Return (true, m) if there exist some acceptance mark m that
1800  // does satisfy the acceptance condition. Return (false, 0U)
1801  // otherwise.
1802  std::pair<bool, acc_cond::mark_t> sat_mark() const
1803  {
1804  return sat_unsat_mark(true);
1805  }
1806 
1807  protected:
1808  bool check_fin_acceptance() const;
1809  std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1810 
1811  public:
1820  static acc_code inf(mark_t mark)
1821  {
1822  return acc_code::inf(mark);
1823  }
1824 
1825  static acc_code inf(std::initializer_list<unsigned> vals)
1826  {
1827  return inf(mark_t(vals.begin(), vals.end()));
1828  }
1830 
1847  static acc_code inf_neg(mark_t mark)
1848  {
1849  return acc_code::inf_neg(mark);
1850  }
1851 
1852  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1853  {
1854  return inf_neg(mark_t(vals.begin(), vals.end()));
1855  }
1857 
1865  static acc_code fin(mark_t mark)
1866  {
1867  return acc_code::fin(mark);
1868  }
1869 
1870  static acc_code fin(std::initializer_list<unsigned> vals)
1871  {
1872  return fin(mark_t(vals.begin(), vals.end()));
1873  }
1875 
1892  static acc_code fin_neg(mark_t mark)
1893  {
1894  return acc_code::fin_neg(mark);
1895  }
1896 
1897  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1898  {
1899  return fin_neg(mark_t(vals.begin(), vals.end()));
1900  }
1902 
1907  unsigned add_sets(unsigned num)
1908  {
1909  if (num == 0)
1910  return -1U;
1911  unsigned j = num_;
1912  num += j;
1913  if (num > mark_t::max_accsets())
1914  report_too_many_sets();
1915  // Make sure we do not update if we raised an exception.
1916  num_ = num;
1917  all_ = all_sets_();
1918  return j;
1919  }
1920 
1925  unsigned add_set()
1926  {
1927  return add_sets(1);
1928  }
1929 
1931  mark_t mark(unsigned u) const
1932  {
1933  SPOT_ASSERT(u < num_sets());
1934  return mark_t({u});
1935  }
1936 
1941  mark_t comp(const mark_t& l) const
1942  {
1943  return all_ ^ l;
1944  }
1945 
1948  {
1949  return all_;
1950  }
1951 
1952  acc_cond
1953  apply_permutation(std::vector<unsigned>permut)
1954  {
1955  return acc_cond(apply_permutation_aux(permut));
1956  }
1957 
1958  acc_code
1959  apply_permutation_aux(std::vector<unsigned>permut)
1960  {
1961  auto conj = top_conjuncts();
1962  auto disj = top_disjuncts();
1963 
1964  if (conj.size() > 1)
1965  {
1966  auto transformed = std::vector<acc_code>();
1967  for (auto elem : conj)
1968  transformed.push_back(elem.apply_permutation_aux(permut));
1969  std::sort(transformed.begin(), transformed.end());
1970  auto uniq = std::unique(transformed.begin(), transformed.end());
1971  auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(),
1972  [](acc_code c1, acc_code c2)
1973  {
1974  return c1 & c2;
1975  });
1976  return result;
1977  }
1978  else if (disj.size() > 1)
1979  {
1980  auto transformed = std::vector<acc_code>();
1981  for (auto elem : disj)
1982  transformed.push_back(elem.apply_permutation_aux(permut));
1983  std::sort(transformed.begin(), transformed.end());
1984  auto uniq = std::unique(transformed.begin(), transformed.end());
1985  auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(),
1986  [](acc_code c1, acc_code c2)
1987  {
1988  return c1 | c2;
1989  });
1990  return result;
1991  }
1992  else
1993  {
1994  if (code_.back().sub.op == acc_cond::acc_op::Fin)
1995  return fin(code_[0].mark.apply_permutation(permut));
1996  if (code_.back().sub.op == acc_cond::acc_op::Inf)
1997  return inf(code_[0].mark.apply_permutation(permut));
1998  }
1999  SPOT_ASSERT(false);
2000  return {};
2001  }
2002 
2005  bool accepting(mark_t inf) const
2006  {
2007  return code_.accepting(inf);
2008  }
2009 
2015  bool inf_satisfiable(mark_t inf) const
2016  {
2017  return code_.inf_satisfiable(inf);
2018  }
2019 
2031  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
2032  {
2033  return code_.maybe_accepting(infinitely_often, always_present);
2034  }
2035 
2050 
2051  // Deprecated since Spot 2.8
2052  SPOT_DEPRECATED("Use operator<< instead.")
2053  std::ostream& format(std::ostream& os, mark_t m) const
2054  {
2055  if (!m)
2056  return os;
2057  return os << m;
2058  }
2059 
2060  // Deprecated since Spot 2.8
2061  SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
2062  std::string format(mark_t m) const
2063  {
2064  std::ostringstream os;
2065  if (m)
2066  os << m;
2067  return os.str();
2068  }
2069 
2071  unsigned num_sets() const
2072  {
2073  return num_;
2074  }
2075 
2083  template<class iterator>
2084  mark_t useless(iterator begin, iterator end) const
2085  {
2086  mark_t u = {}; // The set of useless sets
2087  for (unsigned x = 0; x < num_; ++x)
2088  {
2089  // Skip sets that are already known to be useless.
2090  if (u.has(x))
2091  continue;
2092  auto all = comp(u | mark_t({x}));
2093  // Iterate over all mark_t, and keep track of
2094  // set numbers that always appear with x.
2095  for (iterator y = begin; y != end; ++y)
2096  {
2097  const mark_t& v = *y;
2098  if (v.has(x))
2099  {
2100  all &= v;
2101  if (!all)
2102  break;
2103  }
2104  }
2105  u |= all;
2106  }
2107  return u;
2108  }
2109 
2123  acc_cond remove(mark_t rem, bool missing) const
2124  {
2125  return {num_sets(), code_.remove(rem, missing)};
2126  }
2127 
2132  acc_cond strip(mark_t rem, bool missing) const
2133  {
2134  return
2135  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
2136  }
2137 
2140  {
2141  return {num_sets(), code_.force_inf(m)};
2142  }
2143 
2147  {
2148  return {num_sets(), code_.remove(all_sets() - rem, true)};
2149  }
2150 
2162  std::string name(const char* fmt = "alo") const;
2163 
2176  {
2177  return code_.fin_unit();
2178  }
2179 
2192  {
2193  return code_.inf_unit();
2194  }
2195 
2200  int fin_one() const
2201  {
2202  return code_.fin_one();
2203  }
2204 
2222  std::pair<int, acc_cond> fin_one_extract() const
2223  {
2224  auto [f, c] = code_.fin_one_extract();
2225  return {f, {num_sets(), std::move(c)}};
2226  }
2227 
2236  std::vector<acc_cond> top_disjuncts() const;
2237 
2246  std::vector<acc_cond> top_conjuncts() const;
2247 
2248  protected:
2249  mark_t all_sets_() const
2250  {
2251  return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2252  }
2253 
2254  unsigned num_;
2255  mark_t all_;
2256  acc_code code_;
2257  bool uses_fin_acceptance_ = false;
2258 
2259  };
2260 
2261  struct rs_pairs_view {
2262  typedef std::vector<acc_cond::rs_pair> rs_pairs;
2263 
2264  // Creates view of pairs 'p' with restriction only to marks in 'm'
2265  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2266  : pairs_(p), view_marks_(m) {}
2267 
2268  // Creates view of pairs without restriction to marks
2269  explicit rs_pairs_view(const rs_pairs& p)
2271 
2272  acc_cond::mark_t infs() const
2273  {
2274  return do_view([&](const acc_cond::rs_pair& p)
2275  {
2276  return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2277  });
2278  }
2279 
2280  acc_cond::mark_t fins() const
2281  {
2282  return do_view([&](const acc_cond::rs_pair& p)
2283  {
2284  return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2285  });
2286  }
2287 
2288  acc_cond::mark_t fins_alone() const
2289  {
2290  return do_view([&](const acc_cond::rs_pair& p)
2291  {
2292  return !visible(p.inf) && visible(p.fin) ? p.fin
2293  : acc_cond::mark_t({});
2294  });
2295  }
2296 
2297  acc_cond::mark_t infs_alone() const
2298  {
2299  return do_view([&](const acc_cond::rs_pair& p)
2300  {
2301  return !visible(p.fin) && visible(p.inf) ? p.inf
2302  : acc_cond::mark_t({});
2303  });
2304  }
2305 
2306  acc_cond::mark_t paired_with_fin(unsigned mark) const
2307  {
2308  acc_cond::mark_t res = {};
2309  for (const auto& p: pairs_)
2310  if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2311  res |= p.inf;
2312  return res;
2313  }
2314 
2315  const rs_pairs& pairs() const
2316  {
2317  return pairs_;
2318  }
2319 
2320  private:
2321  template<typename filter>
2322  acc_cond::mark_t do_view(const filter& filt) const
2323  {
2324  acc_cond::mark_t res = {};
2325  for (const auto& p: pairs_)
2326  res |= filt(p);
2327  return res;
2328  }
2329 
2330  bool visible(const acc_cond::mark_t& v) const
2331  {
2332  return !!(view_marks_ & v);
2333  }
2334 
2335  const rs_pairs& pairs_;
2336  acc_cond::mark_t view_marks_;
2337  };
2338 
2339 
2340  SPOT_API
2341  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2342 
2344 
2345  namespace internal
2346  {
2347  class SPOT_API mark_iterator
2348  {
2349  public:
2350  typedef unsigned value_type;
2351  typedef const value_type& reference;
2352  typedef const value_type* pointer;
2353  typedef std::ptrdiff_t difference_type;
2354  typedef std::forward_iterator_tag iterator_category;
2355 
2356  mark_iterator() noexcept
2357  : m_({})
2358  {
2359  }
2360 
2361  mark_iterator(acc_cond::mark_t m) noexcept
2362  : m_(m)
2363  {
2364  }
2365 
2366  bool operator==(mark_iterator m) const
2367  {
2368  return m_ == m.m_;
2369  }
2370 
2371  bool operator!=(mark_iterator m) const
2372  {
2373  return m_ != m.m_;
2374  }
2375 
2376  value_type operator*() const
2377  {
2378  SPOT_ASSERT(m_);
2379  return m_.min_set() - 1;
2380  }
2381 
2382  mark_iterator& operator++()
2383  {
2384  m_.clear(this->operator*());
2385  return *this;
2386  }
2387 
2388  mark_iterator operator++(int)
2389  {
2390  mark_iterator it = *this;
2391  ++(*this);
2392  return it;
2393  }
2394  private:
2395  acc_cond::mark_t m_;
2396  };
2397 
2398  class SPOT_API mark_container
2399  {
2400  public:
2402  : m_(m)
2403  {
2404  }
2405 
2406  mark_iterator begin() const
2407  {
2408  return {m_};
2409  }
2410  mark_iterator end() const
2411  {
2412  return {};
2413  }
2414  private:
2416  };
2417  }
2418 
2420  {
2421  return {*this};
2422  }
2423 
2424  inline acc_cond::mark_t
2425  acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut)
2426  {
2427  mark_t result { };
2428  for (auto color : sets())
2429  if (color < permut.size())
2430  result.set(permut[color]);
2431  return result;
2432  }
2433 }
2434 
2435 namespace std
2436 {
2437  template<>
2438  struct hash<spot::acc_cond::mark_t>
2439  {
2440  size_t operator()(spot::acc_cond::mark_t m) const noexcept
2441  {
2442  return m.hash();
2443  }
2444  };
2445 }
An acceptance condition.
Definition: acc.hh:61
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:2015
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1947
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1892
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1847
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition: acc.hh:1787
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1606
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1520
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1865
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1592
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
Definition: acc.hh:2005
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1820
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1615
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1897
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1825
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1925
bool is_parity(bool &max, bool &odd, bool equiv=false) const
check is the acceptance condition matches one of the four type of parity acceptance defined in the HO...
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1931
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1599
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:2139
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:2123
acc_op
Operators for acceptance formulas.
Definition: acc.hh:455
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1471
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1907
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:1773
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1548
bool is_generalized_rabin(std::vector< unsigned > &pairs) const
Is the acceptance condition generalized-Rabin?
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition: acc.hh:1941
std::vector< acc_cond > top_conjuncts() const
Return the top-level conjuncts.
std::pair< int, acc_cond > fin_one_extract() const
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it.
Definition: acc.hh:2222
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1870
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1626
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:2146
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:2031
std::string name(const char *fmt="alo") const
Return the name of this acceptance condition, in the specified format.
bool is_none() const
Whether the acceptance condition is "none".
Definition: acc.hh:1572
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1513
int is_rabin() const
Check if the acceptance condition matches the Rabin acceptance of the HOA format.
bool is_rabin_like(std::vector< rs_pair > &pairs) const
Test whether an acceptance condition is Rabin-like and returns each Rabin pair in an std::vector<rs_p...
mark_t accepting_sets(mark_t inf) const
Return an accepting subset of inf.
bool is_all() const
Whether the acceptance condition is "all".
Definition: acc.hh:1557
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:2132
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:2200
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:2084
int is_streett() const
Check if the acceptance condition matches the Streett acceptance of the HOA format.
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition: acc.hh:2175
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1526
bool is_generalized_streett(std::vector< unsigned > &pairs) const
Is the acceptance condition generalized-Streett?
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition: acc.hh:1482
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1490
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1497
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1852
bool is_streett_like(std::vector< rs_pair > &pairs) const
Test whether an acceptance condition is Streett-like and returns each Streett pair in an std::vector<...
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition: acc.hh:1581
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
Definition: acc.hh:2191
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1542
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1563
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2071
std::vector< acc_cond > top_disjuncts() const
Return the top-level disjuncts.
Definition: bitset.hh:39
Definition: acc.hh:2399
Definition: acc.hh:2348
A class implementing Kleene's three-valued logic.
Definition: trival.hh:34
op
Operator types.
Definition: formula.hh:79
@ Or
(omega-Rational) Or
@ U
until
@ And
(omega-Rational) And
SPOT_DEPRECATED("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence rec...
Definition: automata.hh:27
const mc_rvalue operator|(const mc_rvalue &lhs, const mc_rvalue &rhs)
This function helps to find the output value from a set of threads that may have different values.
Definition: mc.hh:131
An acceptance formula.
Definition: acc.hh:487
std::vector< std::pair< acc_cond::mark_t, acc_cond::mark_t > > useless_colors_patterns() const
Find patterns of useless colors.
static acc_code parity_max(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:872
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:712
acc_code to_cnf() const
Convert the acceptance formula into disjunctive normal form.
acc_code operator&(acc_code &&r) const
Conjunct the current condition with r.
Definition: acc.hh:1014
acc_code force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
std::ostream & to_html(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as HTML.
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:754
std::vector< acc_code > top_disjuncts() const
Return the top-level disjuncts.
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1117
std::vector< std::vector< int > > missing(mark_t inf, bool accepting) const
Help closing accepting or rejecting cycle.
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1109
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:666
bool is_dnf() const
Whether the acceptance formula is in disjunctive normal form.
acc_code operator&(const acc_code &r) const
Conjunct the current condition with r.
Definition: acc.hh:1006
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:722
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:892
static acc_code parity(bool is_max, bool is_odd, unsigned sets)
Build a parity acceptance condition.
std::pair< acc_cond::mark_t, acc_cond::mark_t > used_inf_fin_sets() const
Return the sets used as Inf or Fin in the acceptance condition.
mark_t used_once_sets() const
Return the sets that appears only once in the acceptance.
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:616
std::ostream & to_text(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as text.
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_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1454
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
static acc_code parity_max_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:880
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:630
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
friend std::ostream & operator<<(std::ostream &os, const acc_code &code)
prints the acceptance formula as text
static acc_code parity_max_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:876
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:602
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 random(unsigned n, double reuse=0.0)
Build a random acceptance condition.
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:808
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1449
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:771
acc_code complement() const
Complement an acceptance formula.
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:744
bdd to_bdd(const bdd *map) const
Convert the acceptance formula into a BDD.
int fin_one() const
Return one acceptance set i that appears as Fin(i) in the condition.
acc_cond::mark_t used_sets() const
Return the set of sets appearing in the condition.
acc_code strip(acc_cond::mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
acc_code(const char *input)
Construct an acc_code from a string.
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:698
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1129
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:823
std::vector< acc_code > top_conjuncts() const
Return the top-level conjuncts.
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:644
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:688
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:884
std::pair< int, acc_code > fin_one_extract() const
Return one acceptance set i that appears as Fin(i) in the condition, and all disjuncts containing it.
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:656
bool inf_satisfiable(mark_t inf) const
Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the co...
bool is_cnf() const
Whether the acceptance formula is in conjunctive normal form.
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:763
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:795
std::vector< unsigned > symmetries() const
compute the symmetry class of the acceptance sets.
acc_code remove(acc_cond::mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
acc_code to_dnf() const
Convert the acceptance formula into disjunctive normal form.
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition: acc.hh:847
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:1022
acc_code & operator&=(const acc_code &r)
Conjunct the current condition in place with r.
Definition: acc.hh:917
std::ostream & to_latex(std::ostream &os, std::function< void(std::ostream &, int)> set_printer=nullptr) const
Print the acceptance formula as LaTeX.
An acceptance mark.
Definition: acc.hh:89
bool is_singleton() const
Whether the mark contains only one bit set.
Definition: acc.hh:393
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:387
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:363
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:417
constexpr static unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:146
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:156
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2419
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
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:111
unsigned count() const
Number of bits sets.
Definition: acc.hh:354
mark_t()=default
Initialize an empty mark_t.
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:122
bool has_many() const
Whether the mark contains at least two bits set.
Definition: acc.hh:404
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:375
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
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:426
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1669
Definition: acc.hh:40
Definition: acc.hh:2261
A "node" in an acceptance formulas.
Definition: acc.hh:465

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