spot  2.11.2
acc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2022 Laboratoire de Recherche et Développement
3 // de l'Epita.
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <functional>
23 #include <sstream>
24 #include <vector>
25 #include <iostream>
26 #include <algorithm>
27 #include <numeric>
28 #include <bddx.h>
29 #include <tuple>
30 #include <spot/misc/_config.h>
31 #include <spot/misc/bitset.hh>
32 #include <spot/misc/trival.hh>
33 
34 namespace spot
35 {
36  namespace internal
37  {
38  class mark_container;
39 
40  template<bool>
41  struct _32acc {};
42  template<>
43  struct _32acc<true>
44  {
45  SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t")
46  typedef unsigned value_t;
47  };
48  }
49 
52 
61  class SPOT_API acc_cond
62  {
63 
64  public:
65  bool
66  has_parity_prefix(acc_cond& new_acc, std::vector<unsigned>& colors) const;
67 
68 #ifndef SWIG
69  private:
70  [[noreturn]] static void report_too_many_sets();
71 #endif
72  public:
73 
88  struct mark_t :
89  public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
90  {
91  private:
92  // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
93  typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
94  _value_t id;
95 
96  mark_t(_value_t id) noexcept
97  : id(id)
98  {
99  }
100 
101  public:
103  mark_t() = default;
104 
105  mark_t
106  apply_permutation(std::vector<unsigned> permut);
107 
108 
109 #ifndef SWIG
111  template<class iterator>
112  mark_t(const iterator& begin, const iterator& end)
113  : mark_t(_value_t::zero())
114  {
115  for (iterator i = begin; i != end; ++i)
116  if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
117  set(*i);
118  else
119  report_too_many_sets();
120  }
121 
123  mark_t(std::initializer_list<unsigned> vals)
124  : mark_t(vals.begin(), vals.end())
125  {
126  }
127 
128  SPOT_DEPRECATED("use brace initialization instead")
129  mark_t(unsigned i)
130  {
131  unsigned j = 0;
132  while (i)
133  {
134  if (i & 1U)
135  this->set(j);
136  ++j;
137  i >>= 1;
138  }
139  }
140 #endif
141 
147  constexpr static unsigned max_accsets()
148  {
149  return SPOT_MAX_ACCSETS;
150  }
151 
157  static mark_t all()
158  {
159  return mark_t(_value_t::mone());
160  }
161 
162  size_t hash() const noexcept
163  {
164  std::hash<decltype(id)> h;
165  return h(id);
166  }
167 
168  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
169  bool operator==(unsigned o) const
170  {
171  SPOT_ASSERT(o == 0U);
172  (void)o;
173  return !id;
174  }
175 
176  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
177  bool operator!=(unsigned o) const
178  {
179  SPOT_ASSERT(o == 0U);
180  (void)o;
181  return !!id;
182  }
183 
184  bool operator==(mark_t o) const
185  {
186  return id == o.id;
187  }
188 
189  bool operator!=(mark_t o) const
190  {
191  return id != o.id;
192  }
193 
194  bool operator<(mark_t o) const
195  {
196  return id < o.id;
197  }
198 
199  bool operator<=(mark_t o) const
200  {
201  return id <= o.id;
202  }
203 
204  bool operator>(mark_t o) const
205  {
206  return id > o.id;
207  }
208 
209  bool operator>=(mark_t o) const
210  {
211  return id >= o.id;
212  }
213 
214  explicit operator bool() const
215  {
216  return !!id;
217  }
218 
219  bool has(unsigned u) const
220  {
221  return !!this->operator&(mark_t({0}) << u);
222  }
223 
224  void set(unsigned u)
225  {
226  id.set(u);
227  }
228 
229  void clear(unsigned u)
230  {
231  id.clear(u);
232  }
233 
234  mark_t& operator&=(mark_t r)
235  {
236  id &= r.id;
237  return *this;
238  }
239 
240  mark_t& operator|=(mark_t r)
241  {
242  id |= r.id;
243  return *this;
244  }
245 
246  mark_t& operator-=(mark_t r)
247  {
248  id &= ~r.id;
249  return *this;
250  }
251 
252  mark_t& operator^=(mark_t r)
253  {
254  id ^= r.id;
255  return *this;
256  }
257 
258  mark_t operator&(mark_t r) const
259  {
260  return id & r.id;
261  }
262 
263  mark_t operator|(mark_t r) const
264  {
265  return id | r.id;
266  }
267 
268  mark_t operator-(mark_t r) const
269  {
270  return id & ~r.id;
271  }
272 
273  mark_t operator~() const
274  {
275  return ~id;
276  }
277 
278  mark_t operator^(mark_t r) const
279  {
280  return id ^ r.id;
281  }
282 
283 #if SPOT_DEBUG || defined(SWIGPYTHON)
284 # define SPOT_WRAP_OP(ins) \
285  try \
286  { \
287  ins; \
288  } \
289  catch (const std::runtime_error& e) \
290  { \
291  report_too_many_sets(); \
292  }
293 #else
294 # define SPOT_WRAP_OP(ins) ins;
295 #endif
296  mark_t operator<<(unsigned i) const
297  {
298  SPOT_WRAP_OP(return id << i);
299  }
300 
301  mark_t& operator<<=(unsigned i)
302  {
303  SPOT_WRAP_OP(id <<= i; return *this);
304  }
305 
306  mark_t operator>>(unsigned i) const
307  {
308  SPOT_WRAP_OP(return id >> i);
309  }
310 
311  mark_t& operator>>=(unsigned i)
312  {
313  SPOT_WRAP_OP(id >>= i; return *this);
314  }
315 #undef SPOT_WRAP_OP
316 
317  mark_t strip(mark_t y) const
318  {
319  // strip every bit of id that is marked in y
320  // 100101110100.strip(
321  // 001011001000)
322  // == 10 1 11 100
323  // == 10111100
324 
325  auto xv = id; // 100101110100
326  auto yv = y.id; // 001011001000
327 
328  while (yv && xv)
329  {
330  // Mask for everything after the last 1 in y
331  auto rm = (~yv) & (yv - 1); // 000000000111
332  // Mask for everything before the last 1 in y
333  auto lm = ~(yv ^ (yv - 1)); // 111111110000
334  xv = ((xv & lm) >> 1) | (xv & rm);
335  yv = (yv & lm) >> 1;
336  }
337  return xv;
338  }
339 
342  bool subset(mark_t m) const
343  {
344  return !((*this) - m);
345  }
346 
349  bool proper_subset(mark_t m) const
350  {
351  return *this != m && this->subset(m);
352  }
353 
355  unsigned count() const
356  {
357  return id.count();
358  }
359 
364  unsigned max_set() const
365  {
366  if (id)
367  return id.highest()+1;
368  else
369  return 0;
370  }
371 
376  unsigned min_set() const
377  {
378  if (id)
379  return id.lowest()+1;
380  else
381  return 0;
382  }
383 
388  mark_t lowest() const
389  {
390  return id & -id;
391  }
392 
394  bool is_singleton() const
395  {
396 #if __GNUC__
397  /* With GCC and Clang, count() is implemented using popcount. */
398  return count() == 1;
399 #else
400  return id && !(id & (id - 1));
401 #endif
402  }
403 
405  bool has_many() const
406  {
407 #if __GNUC__
408  /* With GCC and Clang, count() is implemented using popcount. */
409  return count() > 1;
410 #else
411  return !!(id & (id - 1));
412 #endif
413  }
414 
418  mark_t& remove_some(unsigned n)
419  {
420  while (n--)
421  id &= id - 1;
422  return *this;
423  }
424 
426  template<class iterator>
427  void fill(iterator here) const
428  {
429  auto a = *this;
430  unsigned level = 0;
431  while (a)
432  {
433  if (a.has(0))
434  *here++ = level;
435  ++level;
436  a >>= 1;
437  }
438  }
439 
441  spot::internal::mark_container sets() const;
442 
443  SPOT_API
444  friend std::ostream& operator<<(std::ostream& os, mark_t m);
445 
446  std::string as_string() const
447  {
448  std::ostringstream os;
449  os << *this;
450  return os.str();
451  }
452  };
453 
455  enum class acc_op : unsigned short
456  { Inf, Fin, InfNeg, FinNeg, And, Or };
457 
465  union acc_word
466  {
467  mark_t mark;
468  struct {
469  acc_op op; // Operator
470  unsigned short size; // Size of the subtree (number of acc_word),
471  // not counting this node.
472  } sub;
473  };
474 
487  struct SPOT_API acc_code: public std::vector<acc_word>
488  {
489  acc_code
490  unit_propagation();
491 
492  bool
493  has_parity_prefix(acc_cond& new_cond,
494  std::vector<unsigned>& colors) const;
495 
496  bool
497  is_parity_max_equiv(std::vector<int>& permut,
498  unsigned new_color,
499  bool even) const;
500 
501  bool operator==(const acc_code& other) const
502  {
503  unsigned pos = size();
504  if (other.size() != pos)
505  return false;
506  while (pos > 0)
507  {
508  auto op = (*this)[pos - 1].sub.op;
509  auto sz = (*this)[pos - 1].sub.size;
510  if (other[pos - 1].sub.op != op ||
511  other[pos - 1].sub.size != sz)
512  return false;
513  switch (op)
514  {
515  case acc_cond::acc_op::And:
516  case acc_cond::acc_op::Or:
517  --pos;
518  break;
519  case acc_cond::acc_op::Inf:
520  case acc_cond::acc_op::InfNeg:
521  case acc_cond::acc_op::Fin:
522  case acc_cond::acc_op::FinNeg:
523  pos -= 2;
524  if (other[pos].mark != (*this)[pos].mark)
525  return false;
526  break;
527  }
528  }
529  return true;
530  };
531 
532  bool operator<(const acc_code& other) const
533  {
534  unsigned pos = size();
535  auto osize = other.size();
536  if (pos < osize)
537  return true;
538  if (pos > osize)
539  return false;
540  while (pos > 0)
541  {
542  auto op = (*this)[pos - 1].sub.op;
543  auto oop = other[pos - 1].sub.op;
544  if (op < oop)
545  return true;
546  if (op > oop)
547  return false;
548  auto sz = (*this)[pos - 1].sub.size;
549  auto osz = other[pos - 1].sub.size;
550  if (sz < osz)
551  return true;
552  if (sz > osz)
553  return false;
554  switch (op)
555  {
556  case acc_cond::acc_op::And:
557  case acc_cond::acc_op::Or:
558  --pos;
559  break;
560  case acc_cond::acc_op::Inf:
561  case acc_cond::acc_op::InfNeg:
562  case acc_cond::acc_op::Fin:
563  case acc_cond::acc_op::FinNeg:
564  {
565  pos -= 2;
566  auto m = (*this)[pos].mark;
567  auto om = other[pos].mark;
568  if (m < om)
569  return true;
570  if (m > om)
571  return false;
572  break;
573  }
574  }
575  }
576  return false;
577  }
578 
579  bool operator>(const acc_code& other) const
580  {
581  return other < *this;
582  }
583 
584  bool operator<=(const acc_code& other) const
585  {
586  return !(other < *this);
587  }
588 
589  bool operator>=(const acc_code& other) const
590  {
591  return !(*this < other);
592  }
593 
594  bool operator!=(const acc_code& other) const
595  {
596  return !(*this == other);
597  }
598 
603  bool is_t() const
604  {
605  // We store "t" as an empty condition, or as Inf({}).
606  unsigned s = size();
607  return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
608  && !((*this)[s - 2].mark));
609  }
610 
617  bool is_f() const
618  {
619  // We store "f" as Fin({}).
620  unsigned s = size();
621  return s > 1
622  && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
623  }
624 
631  static acc_code f()
632  {
633  acc_code res;
634  res.resize(2);
635  res[0].mark = {};
636  res[1].sub.op = acc_op::Fin;
637  res[1].sub.size = 1;
638  return res;
639  }
640 
645  static acc_code t()
646  {
647  return {};
648  }
649 
657  static acc_code fin(mark_t m)
658  {
659  acc_code res;
660  res.resize(2);
661  res[0].mark = m;
662  res[1].sub.op = acc_op::Fin;
663  res[1].sub.size = 1;
664  return res;
665  }
666 
667  static acc_code fin(std::initializer_list<unsigned> vals)
668  {
669  return fin(mark_t(vals));
670  }
672 
690  {
691  acc_code res;
692  res.resize(2);
693  res[0].mark = m;
694  res[1].sub.op = acc_op::FinNeg;
695  res[1].sub.size = 1;
696  return res;
697  }
698 
699  static acc_code fin_neg(std::initializer_list<unsigned> vals)
700  {
701  return fin_neg(mark_t(vals));
702  }
704 
713  static acc_code inf(mark_t m)
714  {
715  acc_code res;
716  res.resize(2);
717  res[0].mark = m;
718  res[1].sub.op = acc_op::Inf;
719  res[1].sub.size = 1;
720  return res;
721  }
722 
723  static acc_code inf(std::initializer_list<unsigned> vals)
724  {
725  return inf(mark_t(vals));
726  }
728 
746  {
747  acc_code res;
748  res.resize(2);
749  res[0].mark = m;
750  res[1].sub.op = acc_op::InfNeg;
751  res[1].sub.size = 1;
752  return res;
753  }
754 
755  static acc_code inf_neg(std::initializer_list<unsigned> vals)
756  {
757  return inf_neg(mark_t(vals));
758  }
760 
764  static acc_code buchi()
765  {
766  return inf({0});
767  }
768 
772  static acc_code cobuchi()
773  {
774  return fin({0});
775  }
776 
782  static acc_code generalized_buchi(unsigned n)
783  {
784  if (n == 0)
785  return inf({});
786  acc_cond::mark_t m = mark_t::all();
787  m >>= mark_t::max_accsets() - n;
788  return inf(m);
789  }
790 
796  static acc_code generalized_co_buchi(unsigned n)
797  {
798  if (n == 0)
799  return fin({});
800  acc_cond::mark_t m = mark_t::all();
801  m >>= mark_t::max_accsets() - n;
802  return fin(m);
803  }
804 
809  static acc_code rabin(unsigned n)
810  {
811  acc_cond::acc_code res = f();
812  while (n > 0)
813  {
814  res |= inf({2*n - 1}) & fin({2*n - 2});
815  --n;
816  }
817  return res;
818  }
819 
824  static acc_code streett(unsigned n)
825  {
826  acc_cond::acc_code res = t();
827  while (n > 0)
828  {
829  res &= inf({2*n - 1}) | fin({2*n - 2});
830  --n;
831  }
832  return res;
833  }
834 
847  template<class Iterator>
848  static acc_code generalized_rabin(Iterator begin, Iterator end)
849  {
850  acc_cond::acc_code res = f();
851  unsigned n = 0;
852  for (Iterator i = begin; i != end; ++i)
853  {
854  unsigned f = n++;
855  acc_cond::mark_t m = {};
856  for (unsigned ni = *i; ni > 0; --ni)
857  m.set(n++);
858  auto pair = inf(m) & fin({f});
859  std::swap(pair, res);
860  res |= std::move(pair);
861  }
862  return res;
863  }
864 
872  static acc_code parity(bool is_max, bool is_odd, unsigned sets);
873  static acc_code parity_max(bool is_odd, unsigned sets)
874  {
875  return parity(true, is_odd, sets);
876  }
877  static acc_code parity_max_odd(unsigned sets)
878  {
879  return parity_max(true, sets);
880  }
881  static acc_code parity_max_even(unsigned sets)
882  {
883  return parity_max(false, sets);
884  }
885  static acc_code parity_min(bool is_odd, unsigned sets)
886  {
887  return parity(false, is_odd, sets);
888  }
889  static acc_code parity_min_odd(unsigned sets)
890  {
891  return parity_min(true, sets);
892  }
893  static acc_code parity_min_even(unsigned sets)
894  {
895  return parity_min(false, sets);
896  }
898 
915  static acc_code random(unsigned n, double reuse = 0.0);
916 
919  {
920  if (is_t() || r.is_f())
921  {
922  *this = r;
923  return *this;
924  }
925  if (is_f() || r.is_t())
926  return *this;
927  unsigned s = size() - 1;
928  unsigned rs = r.size() - 1;
929  // We want to group all Inf(x) operators:
930  // Inf(a) & Inf(b) = Inf(a & b)
931  if (((*this)[s].sub.op == acc_op::Inf
932  && r[rs].sub.op == acc_op::Inf)
933  || ((*this)[s].sub.op == acc_op::InfNeg
934  && r[rs].sub.op == acc_op::InfNeg))
935  {
936  (*this)[s - 1].mark |= r[rs - 1].mark;
937  return *this;
938  }
939 
940  // In the more complex scenarios, left and right may both
941  // be conjunctions, and Inf(x) might be a member of each
942  // side. Find it if it exists.
943  // left_inf points to the left Inf mark if any.
944  // right_inf points to the right Inf mark if any.
945  acc_word* left_inf = nullptr;
946  if ((*this)[s].sub.op == acc_op::And)
947  {
948  auto start = &(*this)[s] - (*this)[s].sub.size;
949  auto pos = &(*this)[s] - 1;
950  pop_back();
951  while (pos > start)
952  {
953  if (pos->sub.op == acc_op::Inf)
954  {
955  left_inf = pos - 1;
956  break;
957  }
958  pos -= pos->sub.size + 1;
959  }
960  }
961  else if ((*this)[s].sub.op == acc_op::Inf)
962  {
963  left_inf = &(*this)[s - 1];
964  }
965 
966  const acc_word* right_inf = nullptr;
967  auto right_end = &r.back();
968  if (right_end->sub.op == acc_op::And)
969  {
970  auto start = &r[0];
971  auto pos = --right_end;
972  while (pos > start)
973  {
974  if (pos->sub.op == acc_op::Inf)
975  {
976  right_inf = pos - 1;
977  break;
978  }
979  pos -= pos->sub.size + 1;
980  }
981  }
982  else if (right_end->sub.op == acc_op::Inf)
983  {
984  right_inf = right_end - 1;
985  }
986 
987  acc_cond::mark_t carry = {};
988  if (left_inf && right_inf)
989  {
990  carry = left_inf->mark;
991  auto pos = left_inf - &(*this)[0];
992  erase(begin() + pos, begin() + pos + 2);
993  }
994  auto sz = size();
995  insert(end(), &r[0], right_end + 1);
996  if (carry)
997  (*this)[sz + (right_inf - &r[0])].mark |= carry;
998 
999  acc_word w;
1000  w.sub.op = acc_op::And;
1001  w.sub.size = size();
1002  emplace_back(w);
1003  return *this;
1004  }
1005 
1007  acc_code operator&(const acc_code& r) const
1008  {
1009  acc_code res = *this;
1010  res &= r;
1011  return res;
1012  }
1013 
1016  {
1017  acc_code res = *this;
1018  res &= r;
1019  return res;
1020  }
1021 
1024  {
1025  if (is_t() || r.is_f())
1026  return *this;
1027  if (is_f() || r.is_t())
1028  {
1029  *this = r;
1030  return *this;
1031  }
1032  unsigned s = size() - 1;
1033  unsigned rs = r.size() - 1;
1034  // Fin(a) | Fin(b) = Fin(a | b)
1035  if (((*this)[s].sub.op == acc_op::Fin
1036  && r[rs].sub.op == acc_op::Fin)
1037  || ((*this)[s].sub.op == acc_op::FinNeg
1038  && r[rs].sub.op == acc_op::FinNeg))
1039  {
1040  (*this)[s - 1].mark |= r[rs - 1].mark;
1041  return *this;
1042  }
1043 
1044  // In the more complex scenarios, left and right may both
1045  // be disjunctions, and Fin(x) might be a member of each
1046  // side. Find it if it exists.
1047  // left_inf points to the left Inf mark if any.
1048  // right_inf points to the right Inf mark if any.
1049  acc_word* left_fin = nullptr;
1050  if ((*this)[s].sub.op == acc_op::Or)
1051  {
1052  auto start = &(*this)[s] - (*this)[s].sub.size;
1053  auto pos = &(*this)[s] - 1;
1054  pop_back();
1055  while (pos > start)
1056  {
1057  if (pos->sub.op == acc_op::Fin)
1058  {
1059  left_fin = pos - 1;
1060  break;
1061  }
1062  pos -= pos->sub.size + 1;
1063  }
1064  }
1065  else if ((*this)[s].sub.op == acc_op::Fin)
1066  {
1067  left_fin = &(*this)[s - 1];
1068  }
1069 
1070  const acc_word* right_fin = nullptr;
1071  auto right_end = &r.back();
1072  if (right_end->sub.op == acc_op::Or)
1073  {
1074  auto start = &r[0];
1075  auto pos = --right_end;
1076  while (pos > start)
1077  {
1078  if (pos->sub.op == acc_op::Fin)
1079  {
1080  right_fin = pos - 1;
1081  break;
1082  }
1083  pos -= pos->sub.size + 1;
1084  }
1085  }
1086  else if (right_end->sub.op == acc_op::Fin)
1087  {
1088  right_fin = right_end - 1;
1089  }
1090 
1091  acc_cond::mark_t carry = {};
1092  if (left_fin && right_fin)
1093  {
1094  carry = left_fin->mark;
1095  auto pos = (left_fin - &(*this)[0]);
1096  this->erase(begin() + pos, begin() + pos + 2);
1097  }
1098  auto sz = size();
1099  insert(end(), &r[0], right_end + 1);
1100  if (carry)
1101  (*this)[sz + (right_fin - &r[0])].mark |= carry;
1102  acc_word w;
1103  w.sub.op = acc_op::Or;
1104  w.sub.size = size();
1105  emplace_back(w);
1106  return *this;
1107  }
1108 
1111  {
1112  acc_code res = *this;
1113  res |= r;
1114  return res;
1115  }
1116 
1118  acc_code operator|(const acc_code& r) const
1119  {
1120  acc_code res = *this;
1121  res |= r;
1122  return res;
1123  }
1124 
1130  acc_code& operator<<=(unsigned sets)
1131  {
1132  if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1133  report_too_many_sets();
1134  if (empty())
1135  return *this;
1136  unsigned pos = size();
1137  do
1138  {
1139  switch ((*this)[pos - 1].sub.op)
1140  {
1141  case acc_cond::acc_op::And:
1142  case acc_cond::acc_op::Or:
1143  --pos;
1144  break;
1145  case acc_cond::acc_op::Inf:
1146  case acc_cond::acc_op::InfNeg:
1147  case acc_cond::acc_op::Fin:
1148  case acc_cond::acc_op::FinNeg:
1149  pos -= 2;
1150  (*this)[pos].mark <<= sets;
1151  break;
1152  }
1153  }
1154  while (pos > 0);
1155  return *this;
1156  }
1157 
1161  acc_code operator<<(unsigned sets) const
1162  {
1163  acc_code res = *this;
1164  res <<= sets;
1165  return res;
1166  }
1167 
1174  bool is_dnf() const;
1175 
1182  bool is_cnf() const;
1183 
1194  acc_code to_dnf() const;
1195 
1202  acc_code to_cnf() const;
1203 
1208  bdd to_bdd(const bdd* map) const;
1209 
1218  std::vector<acc_code> top_disjuncts() const;
1219 
1228  std::vector<acc_code> top_conjuncts() const;
1229 
1241 
1253  mark_t fin_unit() const;
1254 
1266  mark_t inf_unit() const;
1267 
1272  int fin_one() const;
1273 
1294  std::pair<int, acc_code> fin_one_extract() const;
1295 
1312  std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
1314 
1327  std::vector<std::vector<int>>
1328  missing(mark_t inf, bool accepting) const;
1329 
1332  bool accepting(mark_t inf) const;
1333 
1339  bool inf_satisfiable(mark_t inf) const;
1340 
1352  trival maybe_accepting(mark_t infinitely_often,
1353  mark_t always_present) const;
1354 
1365  std::vector<unsigned> symmetries() const;
1366 
1380  acc_code remove(acc_cond::mark_t rem, bool missing) const;
1381 
1386  acc_code strip(acc_cond::mark_t rem, bool missing) const;
1389 
1392 
1404  std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
1406 
1414 
1416  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1417 
1422  std::ostream&
1423  to_html(std::ostream& os,
1424  std::function<void(std::ostream&, int)>
1425  set_printer = nullptr) const;
1426 
1431  std::ostream&
1432  to_text(std::ostream& os,
1433  std::function<void(std::ostream&, int)>
1434  set_printer = nullptr) const;
1435 
1440  std::ostream&
1441  to_latex(std::ostream& os,
1442  std::function<void(std::ostream&, int)>
1443  set_printer = nullptr) const;
1444 
1467  acc_code(const char* input);
1468 
1473  {
1474  }
1475 
1477  acc_code(const acc_word* other)
1478  : std::vector<acc_word>(other - other->sub.size, other + 1)
1479  {
1480  }
1481 
1483  SPOT_API
1484  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1485  };
1486 
1494  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1495  : num_(0U), all_({}), code_(code)
1496  {
1497  add_sets(n_sets);
1498  uses_fin_acceptance_ = check_fin_acceptance();
1499  }
1500 
1505  acc_cond(const acc_code& code)
1506  : num_(0U), all_({}), code_(code)
1507  {
1508  add_sets(code.used_sets().max_set());
1509  uses_fin_acceptance_ = check_fin_acceptance();
1510  }
1511 
1513  acc_cond(const acc_cond& o)
1514  : num_(o.num_), all_(o.all_), code_(o.code_),
1515  uses_fin_acceptance_(o.uses_fin_acceptance_)
1516  {
1517  }
1518 
1521  {
1522  num_ = o.num_;
1523  all_ = o.all_;
1524  code_ = o.code_;
1525  uses_fin_acceptance_ = o.uses_fin_acceptance_;
1526  return *this;
1527  }
1528 
1529  ~acc_cond()
1530  {
1531  }
1532 
1536  void set_acceptance(const acc_code& code)
1537  {
1538  code_ = code;
1539  uses_fin_acceptance_ = check_fin_acceptance();
1540  }
1541 
1543  const acc_code& get_acceptance() const
1544  {
1545  return code_;
1546  }
1547 
1550  {
1551  return code_;
1552  }
1553 
1554  bool operator==(const acc_cond& other) const
1555  {
1556  return other.num_sets() == num_ && other.get_acceptance() == code_;
1557  }
1558 
1559  bool operator!=(const acc_cond& other) const
1560  {
1561  return !(*this == other);
1562  }
1563 
1565  bool uses_fin_acceptance() const
1566  {
1567  return uses_fin_acceptance_;
1568  }
1569 
1571  bool is_t() const
1572  {
1573  return code_.is_t();
1574  }
1575 
1580  bool is_all() const
1581  {
1582  return num_ == 0 && is_t();
1583  }
1584 
1586  bool is_f() const
1587  {
1588  return code_.is_f();
1589  }
1590 
1595  bool is_none() const
1596  {
1597  return num_ == 0 && is_f();
1598  }
1599 
1604  bool is_buchi() const
1605  {
1606  unsigned s = code_.size();
1607  return num_ == 1 &&
1608  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1609  }
1610 
1615  bool is_co_buchi() const
1616  {
1617  return num_ == 1 && is_generalized_co_buchi();
1618  }
1619 
1623  {
1624  set_acceptance(inf(all_sets()));
1625  }
1626 
1630  {
1631  set_acceptance(fin(all_sets()));
1632  }
1633 
1639  {
1640  unsigned s = code_.size();
1641  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1642  && code_[0].mark == all_sets());
1643  }
1644 
1650  {
1651  unsigned s = code_.size();
1652  return (s == 2 &&
1653  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1654  }
1655 
1667  int is_rabin() const;
1668 
1680  int is_streett() const;
1681 
1691  struct SPOT_API rs_pair
1692  {
1693 #ifndef SWIG
1694  rs_pair() = default;
1695  rs_pair(const rs_pair&) = default;
1696  rs_pair& operator=(const rs_pair&) = default;
1697 #endif
1698 
1699  rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1700  fin(fin),
1701  inf(inf)
1702  {}
1703  acc_cond::mark_t fin;
1704  acc_cond::mark_t inf;
1705 
1706  bool operator==(rs_pair o) const
1707  {
1708  return fin == o.fin && inf == o.inf;
1709  }
1710  bool operator!=(rs_pair o) const
1711  {
1712  return fin != o.fin || inf != o.inf;
1713  }
1714  bool operator<(rs_pair o) const
1715  {
1716  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1717  }
1718  bool operator<=(rs_pair o) const
1719  {
1720  return !(o < *this);
1721  }
1722  bool operator>(rs_pair o) const
1723  {
1724  return o < *this;
1725  }
1726  bool operator>=(rs_pair o) const
1727  {
1728  return !(*this < o);
1729  }
1730  };
1741  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1742 
1753  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1754 
1764  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1765 
1778  bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1779 
1789  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1790 
1791 
1792  bool is_parity_max_equiv(std::vector<int>& permut, bool even) const;
1793 
1796  bool is_parity() const
1797  {
1798  bool max;
1799  bool odd;
1800  return is_parity(max, odd);
1801  }
1802 
1811  {
1812  return acc_cond(num_, code_.unit_propagation());
1813  }
1814 
1815  // Return (true, m) if there exist some acceptance mark m that
1816  // does not satisfy the acceptance condition. Return (false, 0U)
1817  // otherwise.
1818  std::pair<bool, acc_cond::mark_t> unsat_mark() const
1819  {
1820  return sat_unsat_mark(false);
1821  }
1822  // Return (true, m) if there exist some acceptance mark m that
1823  // does satisfy the acceptance condition. Return (false, 0U)
1824  // otherwise.
1825  std::pair<bool, acc_cond::mark_t> sat_mark() const
1826  {
1827  return sat_unsat_mark(true);
1828  }
1829 
1830  protected:
1831  bool check_fin_acceptance() const;
1832  std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1833 
1834  public:
1843  static acc_code inf(mark_t mark)
1844  {
1845  return acc_code::inf(mark);
1846  }
1847 
1848  static acc_code inf(std::initializer_list<unsigned> vals)
1849  {
1850  return inf(mark_t(vals.begin(), vals.end()));
1851  }
1853 
1870  static acc_code inf_neg(mark_t mark)
1871  {
1872  return acc_code::inf_neg(mark);
1873  }
1874 
1875  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1876  {
1877  return inf_neg(mark_t(vals.begin(), vals.end()));
1878  }
1880 
1888  static acc_code fin(mark_t mark)
1889  {
1890  return acc_code::fin(mark);
1891  }
1892 
1893  static acc_code fin(std::initializer_list<unsigned> vals)
1894  {
1895  return fin(mark_t(vals.begin(), vals.end()));
1896  }
1898 
1915  static acc_code fin_neg(mark_t mark)
1916  {
1917  return acc_code::fin_neg(mark);
1918  }
1919 
1920  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1921  {
1922  return fin_neg(mark_t(vals.begin(), vals.end()));
1923  }
1925 
1930  unsigned add_sets(unsigned num)
1931  {
1932  if (num == 0)
1933  return -1U;
1934  unsigned j = num_;
1935  num += j;
1936  if (num > mark_t::max_accsets())
1937  report_too_many_sets();
1938  // Make sure we do not update if we raised an exception.
1939  num_ = num;
1940  all_ = all_sets_();
1941  return j;
1942  }
1943 
1948  unsigned add_set()
1949  {
1950  return add_sets(1);
1951  }
1952 
1954  mark_t mark(unsigned u) const
1955  {
1956  SPOT_ASSERT(u < num_sets());
1957  return mark_t({u});
1958  }
1959 
1964  mark_t comp(const mark_t& l) const
1965  {
1966  return all_ ^ l;
1967  }
1968 
1971  {
1972  return all_;
1973  }
1974 
1975  acc_cond
1976  apply_permutation(std::vector<unsigned>permut)
1977  {
1978  return acc_cond(apply_permutation_aux(permut));
1979  }
1980 
1981  acc_code
1982  apply_permutation_aux(std::vector<unsigned>permut)
1983  {
1984  auto conj = top_conjuncts();
1985  auto disj = top_disjuncts();
1986 
1987  if (conj.size() > 1)
1988  {
1989  auto transformed = std::vector<acc_code>();
1990  for (auto elem : conj)
1991  transformed.push_back(elem.apply_permutation_aux(permut));
1992  std::sort(transformed.begin(), transformed.end());
1993  auto uniq = std::unique(transformed.begin(), transformed.end());
1994  auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(),
1995  [](acc_code c1, acc_code c2)
1996  {
1997  return c1 & c2;
1998  });
1999  return result;
2000  }
2001  else if (disj.size() > 1)
2002  {
2003  auto transformed = std::vector<acc_code>();
2004  for (auto elem : disj)
2005  transformed.push_back(elem.apply_permutation_aux(permut));
2006  std::sort(transformed.begin(), transformed.end());
2007  auto uniq = std::unique(transformed.begin(), transformed.end());
2008  auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(),
2009  [](acc_code c1, acc_code c2)
2010  {
2011  return c1 | c2;
2012  });
2013  return result;
2014  }
2015  else
2016  {
2017  if (code_.back().sub.op == acc_cond::acc_op::Fin)
2018  return fin(code_[0].mark.apply_permutation(permut));
2019  if (code_.back().sub.op == acc_cond::acc_op::Inf)
2020  return inf(code_[0].mark.apply_permutation(permut));
2021  }
2022  SPOT_ASSERT(false);
2023  return {};
2024  }
2025 
2028  bool accepting(mark_t inf) const
2029  {
2030  return code_.accepting(inf);
2031  }
2032 
2038  bool inf_satisfiable(mark_t inf) const
2039  {
2040  return code_.inf_satisfiable(inf);
2041  }
2042 
2054  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
2055  {
2056  return code_.maybe_accepting(infinitely_often, always_present);
2057  }
2058 
2073 
2074  // Deprecated since Spot 2.8
2075  SPOT_DEPRECATED("Use operator<< instead.")
2076  std::ostream& format(std::ostream& os, mark_t m) const
2077  {
2078  if (!m)
2079  return os;
2080  return os << m;
2081  }
2082 
2083  // Deprecated since Spot 2.8
2084  SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
2085  std::string format(mark_t m) const
2086  {
2087  std::ostringstream os;
2088  if (m)
2089  os << m;
2090  return os.str();
2091  }
2092 
2094  unsigned num_sets() const
2095  {
2096  return num_;
2097  }
2098 
2106  template<class iterator>
2107  mark_t useless(iterator begin, iterator end) const
2108  {
2109  mark_t u = {}; // The set of useless sets
2110  for (unsigned x = 0; x < num_; ++x)
2111  {
2112  // Skip sets that are already known to be useless.
2113  if (u.has(x))
2114  continue;
2115  auto all = comp(u | mark_t({x}));
2116  // Iterate over all mark_t, and keep track of
2117  // set numbers that always appear with x.
2118  for (iterator y = begin; y != end; ++y)
2119  {
2120  const mark_t& v = *y;
2121  if (v.has(x))
2122  {
2123  all &= v;
2124  if (!all)
2125  break;
2126  }
2127  }
2128  u |= all;
2129  }
2130  return u;
2131  }
2132 
2146  acc_cond remove(mark_t rem, bool missing) const
2147  {
2148  return {num_sets(), code_.remove(rem, missing)};
2149  }
2150 
2155  acc_cond strip(mark_t rem, bool missing) const
2156  {
2157  return
2158  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
2159  }
2160 
2163  {
2164  return {num_sets(), code_.force_inf(m)};
2165  }
2166 
2170  {
2171  return {num_sets(), code_.remove(all_sets() - rem, true)};
2172  }
2173 
2185  std::string name(const char* fmt = "alo") const;
2186 
2199  {
2200  return code_.fin_unit();
2201  }
2202 
2215  {
2216  return code_.inf_unit();
2217  }
2218 
2223  int fin_one() const
2224  {
2225  return code_.fin_one();
2226  }
2227 
2248  std::pair<int, acc_cond> fin_one_extract() const
2249  {
2250  auto [f, c] = code_.fin_one_extract();
2251  return {f, {num_sets(), std::move(c)}};
2252  }
2253 
2270  std::tuple<int, acc_cond, acc_cond>
2272  {
2273  auto [f, l, r] = code_.fin_unit_one_split();
2274  return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
2275  }
2276 
2285  std::vector<acc_cond> top_disjuncts() const;
2286 
2295  std::vector<acc_cond> top_conjuncts() const;
2296 
2297  protected:
2298  mark_t all_sets_() const
2299  {
2300  return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
2301  }
2302 
2303  unsigned num_;
2304  mark_t all_;
2305  acc_code code_;
2306  bool uses_fin_acceptance_ = false;
2307 
2308  };
2309 
2310  struct rs_pairs_view {
2311  typedef std::vector<acc_cond::rs_pair> rs_pairs;
2312 
2313  // Creates view of pairs 'p' with restriction only to marks in 'm'
2314  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
2315  : pairs_(p), view_marks_(m) {}
2316 
2317  // Creates view of pairs without restriction to marks
2318  explicit rs_pairs_view(const rs_pairs& p)
2320 
2321  acc_cond::mark_t infs() const
2322  {
2323  return do_view([&](const acc_cond::rs_pair& p)
2324  {
2325  return visible(p.inf) ? p.inf : acc_cond::mark_t({});
2326  });
2327  }
2328 
2329  acc_cond::mark_t fins() const
2330  {
2331  return do_view([&](const acc_cond::rs_pair& p)
2332  {
2333  return visible(p.fin) ? p.fin : acc_cond::mark_t({});
2334  });
2335  }
2336 
2337  acc_cond::mark_t fins_alone() const
2338  {
2339  return do_view([&](const acc_cond::rs_pair& p)
2340  {
2341  return !visible(p.inf) && visible(p.fin) ? p.fin
2342  : acc_cond::mark_t({});
2343  });
2344  }
2345 
2346  acc_cond::mark_t infs_alone() const
2347  {
2348  return do_view([&](const acc_cond::rs_pair& p)
2349  {
2350  return !visible(p.fin) && visible(p.inf) ? p.inf
2351  : acc_cond::mark_t({});
2352  });
2353  }
2354 
2355  acc_cond::mark_t paired_with_fin(unsigned mark) const
2356  {
2357  acc_cond::mark_t res = {};
2358  for (const auto& p: pairs_)
2359  if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2360  res |= p.inf;
2361  return res;
2362  }
2363 
2364  const rs_pairs& pairs() const
2365  {
2366  return pairs_;
2367  }
2368 
2369  private:
2370  template<typename filter>
2371  acc_cond::mark_t do_view(const filter& filt) const
2372  {
2373  acc_cond::mark_t res = {};
2374  for (const auto& p: pairs_)
2375  res |= filt(p);
2376  return res;
2377  }
2378 
2379  bool visible(const acc_cond::mark_t& v) const
2380  {
2381  return !!(view_marks_ & v);
2382  }
2383 
2384  const rs_pairs& pairs_;
2385  acc_cond::mark_t view_marks_;
2386  };
2387 
2388 
2389  SPOT_API
2390  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2391 
2393 
2394  namespace internal
2395  {
2396  class SPOT_API mark_iterator
2397  {
2398  public:
2399  typedef unsigned value_type;
2400  typedef const value_type& reference;
2401  typedef const value_type* pointer;
2402  typedef std::ptrdiff_t difference_type;
2403  typedef std::forward_iterator_tag iterator_category;
2404 
2405  mark_iterator() noexcept
2406  : m_({})
2407  {
2408  }
2409 
2410  mark_iterator(acc_cond::mark_t m) noexcept
2411  : m_(m)
2412  {
2413  }
2414 
2415  bool operator==(mark_iterator m) const
2416  {
2417  return m_ == m.m_;
2418  }
2419 
2420  bool operator!=(mark_iterator m) const
2421  {
2422  return m_ != m.m_;
2423  }
2424 
2425  value_type operator*() const
2426  {
2427  SPOT_ASSERT(m_);
2428  return m_.min_set() - 1;
2429  }
2430 
2431  mark_iterator& operator++()
2432  {
2433  m_.clear(this->operator*());
2434  return *this;
2435  }
2436 
2437  mark_iterator operator++(int)
2438  {
2439  mark_iterator it = *this;
2440  ++(*this);
2441  return it;
2442  }
2443  private:
2444  acc_cond::mark_t m_;
2445  };
2446 
2447  class SPOT_API mark_container
2448  {
2449  public:
2451  : m_(m)
2452  {
2453  }
2454 
2455  mark_iterator begin() const
2456  {
2457  return {m_};
2458  }
2459  mark_iterator end() const
2460  {
2461  return {};
2462  }
2463  private:
2465  };
2466  }
2467 
2469  {
2470  return {*this};
2471  }
2472 
2473  inline acc_cond::mark_t
2474  acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut)
2475  {
2476  mark_t result { };
2477  for (auto color : sets())
2478  if (color < permut.size())
2479  result.set(permut[color]);
2480  return result;
2481  }
2482 }
2483 
2484 namespace std
2485 {
2486  template<>
2487  struct hash<spot::acc_cond::mark_t>
2488  {
2489  size_t operator()(spot::acc_cond::mark_t m) const noexcept
2490  {
2491  return m.hash();
2492  }
2493  };
2494 }
An acceptance condition.
Definition: acc.hh:62
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:2038
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1970
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1915
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1870
acc_cond unit_propagation()
Remove superfluous Fin and Inf by unit propagation.
Definition: acc.hh:1810
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1629
const acc_code & get_acceptance() const
Retrieve the acceptance formula.
Definition: acc.hh:1543
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1888
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1615
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
Definition: acc.hh:2028
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1843
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1638
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1920
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1848
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1948
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:1954
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1622
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:2162
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:2146
std::tuple< int, acc_cond, acc_cond > fin_unit_one_split() const
Split an acceptance condition, trying to select one unit-Fin.
Definition: acc.hh:2271
acc_op
Operators for acceptance formulas.
Definition: acc.hh:456
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1494
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1930
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:1796
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1571
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:1964
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:2248
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1893
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1649
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:2169
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:2054
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:1595
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1536
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:1580
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:2155
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:2223
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:2107
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:2198
acc_code & get_acceptance()
Retrieve the acceptance formula.
Definition: acc.hh:1549
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:1505
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1513
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1520
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1875
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:1604
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
Definition: acc.hh:2214
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1565
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1586
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:2094
std::vector< acc_cond > top_disjuncts() const
Return the top-level disjuncts.
Definition: bitset.hh:39
Definition: acc.hh:2448
Definition: acc.hh:2397
A class implementing Kleene's three-valued logic.
Definition: trival.hh:34
op
Operator types.
Definition: formula.hh:79
@ Or
(omega-Rational) Or
@ U
until
@ And
(omega-Rational) And
SPOT_DEPRECATED("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence rec...
Definition: automata.hh:27
const mc_rvalue operator|(const mc_rvalue &lhs, const mc_rvalue &rhs)
This function helps to find the output value from a set of threads that may have different values.
Definition: mc.hh:131
An acceptance formula.
Definition: acc.hh:488
std::vector< std::pair< acc_cond::mark_t, acc_cond::mark_t > > useless_colors_patterns() const
Find patterns of useless colors.
std::tuple< int, acc_cond::acc_code, acc_cond::acc_code > fin_unit_one_split() const
Split an acceptance condition, trying to select one unit-Fin.
static acc_code parity_max(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:873
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:713
acc_code to_cnf() const
Convert the acceptance formula into disjunctive normal form.
acc_code operator&(acc_code &&r) const
Conjunct the current condition with r.
Definition: acc.hh:1015
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:755
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:1118
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:1110
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:667
bool is_dnf() const
Whether the acceptance formula is in disjunctive normal form.
acc_code operator&(const acc_code &r) const
Conjunct the current condition with r.
Definition: acc.hh:1007
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:723
static acc_code parity_min_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:893
static acc_code parity(bool is_max, bool is_odd, unsigned sets)
Build a parity acceptance condition.
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:617
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:782
static acc_code parity_min_odd(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:889
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1477
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
static acc_code parity_max_even(unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:881
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:631
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition.
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:877
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:603
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1161
static acc_code random(unsigned n, double reuse=0.0)
Build a random acceptance condition.
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:809
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1472
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:772
acc_code complement() const
Complement an acceptance formula.
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:745
bdd to_bdd(const bdd *map) const
Convert the acceptance formula into a BDD.
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:699
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1130
mark_t inf_unit() const
Find a Inf(i) that is a unit clause.
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:824
std::vector< acc_code > top_conjuncts() const
Return the top-level conjuncts.
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:645
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:689
static acc_code parity_min(bool is_odd, unsigned sets)
Build a parity acceptance condition.
Definition: acc.hh:885
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:657
bool inf_satisfiable(mark_t inf) const
Assuming that we will visit at least all sets in inf, is there any chance that we will satisfy the co...
bool is_cnf() const
Whether the acceptance formula is in conjunctive normal form.
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:764
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:796
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:848
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:1023
acc_code & operator&=(const acc_code &r)
Conjunct the current condition in place with r.
Definition: acc.hh:918
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:90
bool is_singleton() const
Whether the mark contains only one bit set.
Definition: acc.hh:394
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:388
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:364
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:418
constexpr static unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:147
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:157
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2468
bool proper_subset(mark_t m) const
Whether the set of bits represented by *this is a proper subset of those represented by m.
Definition: acc.hh:349
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:112
unsigned count() const
Number of bits sets.
Definition: acc.hh:355
mark_t()=default
Initialize an empty mark_t.
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:123
bool has_many() const
Whether the mark contains at least two bits set.
Definition: acc.hh:405
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:376
bool subset(mark_t m) const
Whether the set of bits represented by *this is a subset of those represented by m.
Definition: acc.hh:342
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:427
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1692
Definition: acc.hh:41
Definition: acc.hh:2310
A "node" in an acceptance formulas.
Definition: acc.hh:466

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