spot  2.7
acc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
3 // de l'Epita.
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <functional>
23 #include <sstream>
24 #include <vector>
25 #include <iostream>
26 
27 #include <spot/misc/_config.h>
28 #include <spot/misc/bitset.hh>
29 #include <spot/misc/trival.hh>
30 
31 namespace spot
32 {
33  namespace internal
34  {
35  class mark_container;
36 
37  template<bool>
38  struct _32acc {};
39  template<>
40  struct _32acc<true>
41  {
42  SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t")
43  typedef unsigned value_t;
44  };
45  }
46 
49 
58  class SPOT_API acc_cond
59  {
60 
61 #ifndef SWIG
62  private:
63  [[noreturn]] static void report_too_many_sets();
64 #endif
65  public:
66 
81  struct mark_t :
82  public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
83  {
84  private:
85  // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
86  typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
87  _value_t id;
88 
89  mark_t(_value_t id) noexcept
90  : id(id)
91  {
92  }
93 
94  public:
96  mark_t() = default;
97 
98 #ifndef SWIG
99  template<class iterator>
101  mark_t(const iterator& begin, const iterator& end)
102  : mark_t(_value_t::zero())
103  {
104  for (iterator i = begin; i != end; ++i)
105  set(*i);
106  }
107 
109  mark_t(std::initializer_list<unsigned> vals)
110  : mark_t(vals.begin(), vals.end())
111  {
112  }
113 
114  SPOT_DEPRECATED("use brace initialization instead")
115  mark_t(unsigned i)
116  {
117  unsigned j = 0;
118  while (i)
119  {
120  if (i & 1U)
121  this->set(j);
122  ++j;
123  i >>= 1;
124  }
125  }
126 #endif
127 
133  constexpr static unsigned max_accsets()
134  {
135  return SPOT_MAX_ACCSETS;
136  }
137 
143  static mark_t all()
144  {
145  return mark_t(_value_t::mone());
146  }
147 
148  size_t hash() const noexcept
149  {
150  std::hash<decltype(id)> h;
151  return h(id);
152  }
153 
154  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
155  bool operator==(unsigned o) const
156  {
157  SPOT_ASSERT(o == 0U);
158  (void)o;
159  return !id;
160  }
161 
162  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
163  bool operator!=(unsigned o) const
164  {
165  SPOT_ASSERT(o == 0U);
166  (void)o;
167  return !!id;
168  }
169 
170  bool operator==(mark_t o) const
171  {
172  return id == o.id;
173  }
174 
175  bool operator!=(mark_t o) const
176  {
177  return id != o.id;
178  }
179 
180  bool operator<(mark_t o) const
181  {
182  return id < o.id;
183  }
184 
185  bool operator<=(mark_t o) const
186  {
187  return id <= o.id;
188  }
189 
190  bool operator>(mark_t o) const
191  {
192  return id > o.id;
193  }
194 
195  bool operator>=(mark_t o) const
196  {
197  return id >= o.id;
198  }
199 
200  explicit operator bool() const
201  {
202  return !!id;
203  }
204 
205  bool has(unsigned u) const
206  {
207  return !!this->operator&(mark_t({0}) << u);
208  }
209 
210  void set(unsigned u)
211  {
212  id.set(u);
213  }
214 
215  void clear(unsigned u)
216  {
217  id.clear(u);
218  }
219 
220  mark_t& operator&=(mark_t r)
221  {
222  id &= r.id;
223  return *this;
224  }
225 
226  mark_t& operator|=(mark_t r)
227  {
228  id |= r.id;
229  return *this;
230  }
231 
232  mark_t& operator-=(mark_t r)
233  {
234  id &= ~r.id;
235  return *this;
236  }
237 
238  mark_t& operator^=(mark_t r)
239  {
240  id ^= r.id;
241  return *this;
242  }
243 
244  mark_t operator&(mark_t r) const
245  {
246  return id & r.id;
247  }
248 
249  mark_t operator|(mark_t r) const
250  {
251  return id | r.id;
252  }
253 
254  mark_t operator-(mark_t r) const
255  {
256  return id & ~r.id;
257  }
258 
259  mark_t operator~() const
260  {
261  return ~id;
262  }
263 
264  mark_t operator^(mark_t r) const
265  {
266  return id ^ r.id;
267  }
268 
269 #if SPOT_DEBUG || defined(SWIGPYTHON)
270 # define SPOT_WRAP_OP(ins) \
271  try \
272  { \
273  ins; \
274  } \
275  catch (const std::runtime_error& e) \
276  { \
277  report_too_many_sets(); \
278  }
279 #else
280 # define SPOT_WRAP_OP(ins) ins;
281 #endif
282  mark_t operator<<(unsigned i) const
283  {
284  SPOT_WRAP_OP(return id << i);
285  }
286 
287  mark_t& operator<<=(unsigned i)
288  {
289  SPOT_WRAP_OP(id <<= i; return *this);
290  }
291 
292  mark_t operator>>(unsigned i) const
293  {
294  SPOT_WRAP_OP(return id >> i);
295  }
296 
297  mark_t& operator>>=(unsigned i)
298  {
299  SPOT_WRAP_OP(id >>= i; return *this);
300  }
301 #undef SPOT_WRAP_OP
302 
303  mark_t strip(mark_t y) const
304  {
305  // strip every bit of id that is marked in y
306  // 100101110100.strip(
307  // 001011001000)
308  // == 10 1 11 100
309  // == 10111100
310 
311  auto xv = id; // 100101110100
312  auto yv = y.id; // 001011001000
313 
314  while (yv && xv)
315  {
316  // Mask for everything after the last 1 in y
317  auto rm = (~yv) & (yv - 1); // 000000000111
318  // Mask for everything before the last 1 in y
319  auto lm = ~(yv ^ (yv - 1)); // 111111110000
320  xv = ((xv & lm) >> 1) | (xv & rm);
321  yv = (yv & lm) >> 1;
322  }
323  return xv;
324  }
325 
328  bool subset(mark_t m) const
329  {
330  return !((*this) - m);
331  }
332 
335  bool proper_subset(mark_t m) const
336  {
337  return *this != m && this->subset(m);
338  }
339 
341  unsigned count() const
342  {
343  return id.count();
344  }
345 
350  unsigned max_set() const
351  {
352  if (id)
353  return id.highest()+1;
354  else
355  return 0;
356  }
357 
362  unsigned min_set() const
363  {
364  if (id)
365  return id.lowest()+1;
366  else
367  return 0;
368  }
369 
374  mark_t lowest() const
375  {
376  return id & -id;
377  }
378 
382  mark_t& remove_some(unsigned n)
383  {
384  while (n--)
385  id &= id - 1;
386  return *this;
387  }
388 
390  template<class iterator>
391  void fill(iterator here) const
392  {
393  auto a = *this;
394  unsigned level = 0;
395  while (a)
396  {
397  if (a.has(0))
398  *here++ = level;
399  ++level;
400  a >>= 1;
401  }
402  }
403 
405  spot::internal::mark_container sets() const;
406 
407  SPOT_API
408  friend std::ostream& operator<<(std::ostream& os, mark_t m);
409  };
410 
412  enum class acc_op : unsigned short
413  { Inf, Fin, InfNeg, FinNeg, And, Or };
414 
422  union acc_word
423  {
424  mark_t mark;
425  struct {
426  acc_op op; // Operator
427  unsigned short size; // Size of the subtree (number of acc_word),
428  // not counting this node.
429  } sub;
430  };
431 
444  struct SPOT_API acc_code: public std::vector<acc_word>
445  {
446  bool operator==(const acc_code& other) const
447  {
448  unsigned pos = size();
449  if (other.size() != pos)
450  return false;
451  while (pos > 0)
452  {
453  auto op = (*this)[pos - 1].sub.op;
454  auto sz = (*this)[pos - 1].sub.size;
455  if (other[pos - 1].sub.op != op ||
456  other[pos - 1].sub.size != sz)
457  return false;
458  switch (op)
459  {
460  case acc_cond::acc_op::And:
461  case acc_cond::acc_op::Or:
462  --pos;
463  break;
464  case acc_cond::acc_op::Inf:
465  case acc_cond::acc_op::InfNeg:
466  case acc_cond::acc_op::Fin:
467  case acc_cond::acc_op::FinNeg:
468  pos -= 2;
469  if (other[pos].mark != (*this)[pos].mark)
470  return false;
471  break;
472  }
473  }
474  return true;
475  };
476 
477  bool operator<(const acc_code& other) const
478  {
479  unsigned pos = size();
480  auto osize = other.size();
481  if (pos < osize)
482  return true;
483  if (pos > osize)
484  return false;
485  while (pos > 0)
486  {
487  auto op = (*this)[pos - 1].sub.op;
488  auto oop = other[pos - 1].sub.op;
489  if (op < oop)
490  return true;
491  if (op > oop)
492  return false;
493  auto sz = (*this)[pos - 1].sub.size;
494  auto osz = other[pos - 1].sub.size;
495  if (sz < osz)
496  return true;
497  if (sz > osz)
498  return false;
499  switch (op)
500  {
501  case acc_cond::acc_op::And:
502  case acc_cond::acc_op::Or:
503  --pos;
504  break;
505  case acc_cond::acc_op::Inf:
506  case acc_cond::acc_op::InfNeg:
507  case acc_cond::acc_op::Fin:
508  case acc_cond::acc_op::FinNeg:
509  {
510  pos -= 2;
511  auto m = (*this)[pos].mark;
512  auto om = other[pos].mark;
513  if (m < om)
514  return true;
515  if (m > om)
516  return false;
517  break;
518  }
519  }
520  }
521  return false;
522  }
523 
524  bool operator>(const acc_code& other) const
525  {
526  return other < *this;
527  }
528 
529  bool operator<=(const acc_code& other) const
530  {
531  return !(other < *this);
532  }
533 
534  bool operator>=(const acc_code& other) const
535  {
536  return !(*this < other);
537  }
538 
539  bool operator!=(const acc_code& other) const
540  {
541  return !(*this == other);
542  }
543 
548  bool is_t() const
549  {
550  // We store "t" as an empty condition, or as Inf({}).
551  unsigned s = size();
552  return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
553  && !((*this)[s - 2].mark));
554  }
555 
562  bool is_f() const
563  {
564  // We store "f" as Fin({}).
565  unsigned s = size();
566  return s > 1
567  && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
568  }
569 
576  static acc_code f()
577  {
578  acc_code res;
579  res.resize(2);
580  res[0].mark = {};
581  res[1].sub.op = acc_op::Fin;
582  res[1].sub.size = 1;
583  return res;
584  }
585 
590  static acc_code t()
591  {
592  return {};
593  }
594 
602  static acc_code fin(mark_t m)
603  {
604  acc_code res;
605  res.resize(2);
606  res[0].mark = m;
607  res[1].sub.op = acc_op::Fin;
608  res[1].sub.size = 1;
609  return res;
610  }
611 
612  static acc_code fin(std::initializer_list<unsigned> vals)
613  {
614  return fin(mark_t(vals));
615  }
617 
635  {
636  acc_code res;
637  res.resize(2);
638  res[0].mark = m;
639  res[1].sub.op = acc_op::FinNeg;
640  res[1].sub.size = 1;
641  return res;
642  }
643 
644  static acc_code fin_neg(std::initializer_list<unsigned> vals)
645  {
646  return fin_neg(mark_t(vals));
647  }
649 
658  static acc_code inf(mark_t m)
659  {
660  acc_code res;
661  res.resize(2);
662  res[0].mark = m;
663  res[1].sub.op = acc_op::Inf;
664  res[1].sub.size = 1;
665  return res;
666  }
667 
668  static acc_code inf(std::initializer_list<unsigned> vals)
669  {
670  return inf(mark_t(vals));
671  }
673 
691  {
692  acc_code res;
693  res.resize(2);
694  res[0].mark = m;
695  res[1].sub.op = acc_op::InfNeg;
696  res[1].sub.size = 1;
697  return res;
698  }
699 
700  static acc_code inf_neg(std::initializer_list<unsigned> vals)
701  {
702  return inf_neg(mark_t(vals));
703  }
705 
709  static acc_code buchi()
710  {
711  return inf({0});
712  }
713 
717  static acc_code cobuchi()
718  {
719  return fin({0});
720  }
721 
727  static acc_code generalized_buchi(unsigned n)
728  {
729  if (n == 0)
730  return inf({});
731  acc_cond::mark_t m = mark_t::all();
732  m >>= mark_t::max_accsets() - n;
733  return inf(m);
734  }
735 
741  static acc_code generalized_co_buchi(unsigned n)
742  {
743  if (n == 0)
744  return fin({});
745  acc_cond::mark_t m = mark_t::all();
746  m >>= mark_t::max_accsets() - n;
747  return fin(m);
748  }
749 
754  static acc_code rabin(unsigned n)
755  {
756  acc_cond::acc_code res = f();
757  while (n > 0)
758  {
759  res |= inf({2*n - 1}) & fin({2*n - 2});
760  --n;
761  }
762  return res;
763  }
764 
769  static acc_code streett(unsigned n)
770  {
771  acc_cond::acc_code res = t();
772  while (n > 0)
773  {
774  res &= inf({2*n - 1}) | fin({2*n - 2});
775  --n;
776  }
777  return res;
778  }
779 
792  template<class Iterator>
793  static acc_code generalized_rabin(Iterator begin, Iterator end)
794  {
795  acc_cond::acc_code res = f();
796  unsigned n = 0;
797  for (Iterator i = begin; i != end; ++i)
798  {
799  unsigned f = n++;
800  acc_cond::mark_t m = {};
801  for (unsigned ni = *i; ni > 0; --ni)
802  m.set(n++);
803  auto pair = inf(m) & fin({f});
804  std::swap(pair, res);
805  res |= std::move(pair);
806  }
807  return res;
808  }
809 
816  static acc_code parity(bool max, bool odd, unsigned sets);
817 
834  static acc_code random(unsigned n, double reuse = 0.0);
835 
837  acc_code& operator&=(const acc_code& r)
838  {
839  if (is_t() || r.is_f())
840  {
841  *this = r;
842  return *this;
843  }
844  if (is_f() || r.is_t())
845  return *this;
846  unsigned s = size() - 1;
847  unsigned rs = r.size() - 1;
848  // We want to group all Inf(x) operators:
849  // Inf(a) & Inf(b) = Inf(a & b)
850  if (((*this)[s].sub.op == acc_op::Inf
851  && r[rs].sub.op == acc_op::Inf)
852  || ((*this)[s].sub.op == acc_op::InfNeg
853  && r[rs].sub.op == acc_op::InfNeg))
854  {
855  (*this)[s - 1].mark |= r[rs - 1].mark;
856  return *this;
857  }
858 
859  // In the more complex scenarios, left and right may both
860  // be conjunctions, and Inf(x) might be a member of each
861  // side. Find it if it exists.
862  // left_inf points to the left Inf mark if any.
863  // right_inf points to the right Inf mark if any.
864  acc_word* left_inf = nullptr;
865  if ((*this)[s].sub.op == acc_op::And)
866  {
867  auto start = &(*this)[s] - (*this)[s].sub.size;
868  auto pos = &(*this)[s] - 1;
869  pop_back();
870  while (pos > start)
871  {
872  if (pos->sub.op == acc_op::Inf)
873  {
874  left_inf = pos - 1;
875  break;
876  }
877  pos -= pos->sub.size + 1;
878  }
879  }
880  else if ((*this)[s].sub.op == acc_op::Inf)
881  {
882  left_inf = &(*this)[s - 1];
883  }
884 
885  const acc_word* right_inf = nullptr;
886  auto right_end = &r.back();
887  if (right_end->sub.op == acc_op::And)
888  {
889  auto start = &r[0];
890  auto pos = --right_end;
891  while (pos > start)
892  {
893  if (pos->sub.op == acc_op::Inf)
894  {
895  right_inf = pos - 1;
896  break;
897  }
898  pos -= pos->sub.size + 1;
899  }
900  }
901  else if (right_end->sub.op == acc_op::Inf)
902  {
903  right_inf = right_end - 1;
904  }
905 
906  acc_cond::mark_t carry = {};
907  if (left_inf && right_inf)
908  {
909  carry = left_inf->mark;
910  auto pos = left_inf - &(*this)[0];
911  erase(begin() + pos, begin() + pos + 2);
912  }
913  auto sz = size();
914  insert(end(), &r[0], right_end + 1);
915  if (carry)
916  (*this)[sz + (right_inf - &r[0])].mark |= carry;
917 
918  acc_word w;
919  w.sub.op = acc_op::And;
920  w.sub.size = size();
921  emplace_back(w);
922  return *this;
923  }
924 
926  acc_code operator&(const acc_code& r) const
927  {
928  acc_code res = *this;
929  res &= r;
930  return res;
931  }
932 
934  acc_code operator&(acc_code&& r) const
935  {
936  acc_code res = *this;
937  res &= r;
938  return res;
939  }
940 
943  {
944  if (is_t() || r.is_f())
945  return *this;
946  if (is_f() || r.is_t())
947  {
948  *this = r;
949  return *this;
950  }
951  unsigned s = size() - 1;
952  unsigned rs = r.size() - 1;
953  // Fin(a) | Fin(b) = Fin(a | b)
954  if (((*this)[s].sub.op == acc_op::Fin
955  && r[rs].sub.op == acc_op::Fin)
956  || ((*this)[s].sub.op == acc_op::FinNeg
957  && r[rs].sub.op == acc_op::FinNeg))
958  {
959  (*this)[s - 1].mark |= r[rs - 1].mark;
960  return *this;
961  }
962 
963  // In the more complex scenarios, left and right may both
964  // be disjunctions, and Fin(x) might be a member of each
965  // side. Find it if it exists.
966  // left_inf points to the left Inf mark if any.
967  // right_inf points to the right Inf mark if any.
968  acc_word* left_fin = nullptr;
969  if ((*this)[s].sub.op == acc_op::Or)
970  {
971  auto start = &(*this)[s] - (*this)[s].sub.size;
972  auto pos = &(*this)[s] - 1;
973  pop_back();
974  while (pos > start)
975  {
976  if (pos->sub.op == acc_op::Fin)
977  {
978  left_fin = pos - 1;
979  break;
980  }
981  pos -= pos->sub.size + 1;
982  }
983  }
984  else if ((*this)[s].sub.op == acc_op::Fin)
985  {
986  left_fin = &(*this)[s - 1];
987  }
988 
989  const acc_word* right_fin = nullptr;
990  auto right_end = &r.back();
991  if (right_end->sub.op == acc_op::Or)
992  {
993  auto start = &r[0];
994  auto pos = --right_end;
995  while (pos > start)
996  {
997  if (pos->sub.op == acc_op::Fin)
998  {
999  right_fin = pos - 1;
1000  break;
1001  }
1002  pos -= pos->sub.size + 1;
1003  }
1004  }
1005  else if (right_end->sub.op == acc_op::Fin)
1006  {
1007  right_fin = right_end - 1;
1008  }
1009 
1010  acc_cond::mark_t carry = {};
1011  if (left_fin && right_fin)
1012  {
1013  carry = left_fin->mark;
1014  auto pos = (left_fin - &(*this)[0]);
1015  this->erase(begin() + pos, begin() + pos + 2);
1016  }
1017  auto sz = size();
1018  insert(end(), &r[0], right_end + 1);
1019  if (carry)
1020  (*this)[sz + (right_fin - &r[0])].mark |= carry;
1021  acc_word w;
1022  w.sub.op = acc_op::Or;
1023  w.sub.size = size();
1024  emplace_back(w);
1025  return *this;
1026  }
1027 
1030  {
1031  acc_code res = *this;
1032  res |= r;
1033  return res;
1034  }
1035 
1037  acc_code operator|(const acc_code& r) const
1038  {
1039  acc_code res = *this;
1040  res |= r;
1041  return res;
1042  }
1043 
1049  acc_code& operator<<=(unsigned sets)
1050  {
1051  if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
1052  report_too_many_sets();
1053  if (empty())
1054  return *this;
1055  unsigned pos = size();
1056  do
1057  {
1058  switch ((*this)[pos - 1].sub.op)
1059  {
1060  case acc_cond::acc_op::And:
1061  case acc_cond::acc_op::Or:
1062  --pos;
1063  break;
1064  case acc_cond::acc_op::Inf:
1065  case acc_cond::acc_op::InfNeg:
1066  case acc_cond::acc_op::Fin:
1067  case acc_cond::acc_op::FinNeg:
1068  pos -= 2;
1069  (*this)[pos].mark <<= sets;
1070  break;
1071  }
1072  }
1073  while (pos > 0);
1074  return *this;
1075  }
1076 
1080  acc_code operator<<(unsigned sets) const
1081  {
1082  acc_code res = *this;
1083  res <<= sets;
1084  return res;
1085  }
1086 
1093  bool is_dnf() const;
1094 
1101  bool is_cnf() const;
1102 
1113  acc_code to_dnf() const;
1114 
1121  acc_code to_cnf() const;
1122 
1133  acc_code complement() const;
1134 
1146  mark_t fin_unit() const;
1147 
1152  int fin_one() const;
1153 
1166  std::vector<std::vector<int>>
1167  missing(mark_t inf, bool accepting) const;
1168 
1171  bool accepting(mark_t inf) const;
1172 
1178  bool inf_satisfiable(mark_t inf) const;
1179 
1191  trival maybe_accepting(mark_t infinitely_often,
1192  mark_t always_present) const;
1193 
1204  std::vector<unsigned> symmetries() const;
1205 
1219  acc_code remove(acc_cond::mark_t rem, bool missing) const;
1220 
1225  acc_code strip(acc_cond::mark_t rem, bool missing) const;
1227  acc_code force_inf(mark_t m) const;
1228 
1230  acc_cond::mark_t used_sets() const;
1231 
1233  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
1234 
1239  std::ostream&
1240  to_html(std::ostream& os,
1241  std::function<void(std::ostream&, int)>
1242  set_printer = nullptr) const;
1243 
1248  std::ostream&
1249  to_text(std::ostream& os,
1250  std::function<void(std::ostream&, int)>
1251  set_printer = nullptr) const;
1252 
1257  std::ostream&
1258  to_latex(std::ostream& os,
1259  std::function<void(std::ostream&, int)>
1260  set_printer = nullptr) const;
1261 
1284  acc_code(const char* input);
1285 
1290  {
1291  }
1292 
1294  acc_code(const acc_word* other)
1295  : std::vector<acc_word>(other - other->sub.size, other + 1)
1296  {
1297  }
1298 
1300  SPOT_API
1301  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
1302  };
1303 
1311  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
1312  : num_(0U), all_({}), code_(code)
1313  {
1314  add_sets(n_sets);
1315  uses_fin_acceptance_ = check_fin_acceptance();
1316  }
1317 
1322  acc_cond(const acc_code& code)
1323  : num_(0U), all_({}), code_(code)
1324  {
1325  add_sets(code.used_sets().max_set());
1326  uses_fin_acceptance_ = check_fin_acceptance();
1327  }
1328 
1330  acc_cond(const acc_cond& o)
1331  : num_(o.num_), all_(o.all_), code_(o.code_),
1332  uses_fin_acceptance_(o.uses_fin_acceptance_)
1333  {
1334  }
1335 
1338  {
1339  num_ = o.num_;
1340  all_ = o.all_;
1341  code_ = o.code_;
1342  uses_fin_acceptance_ = o.uses_fin_acceptance_;
1343  return *this;
1344  }
1345 
1346  ~acc_cond()
1347  {
1348  }
1349 
1353  void set_acceptance(const acc_code& code)
1354  {
1355  code_ = code;
1356  uses_fin_acceptance_ = check_fin_acceptance();
1357  }
1358 
1360  const acc_code& get_acceptance() const
1361  {
1362  return code_;
1363  }
1364 
1367  {
1368  return code_;
1369  }
1370 
1371  bool operator==(const acc_cond& other) const
1372  {
1373  return other.num_sets() == num_ && other.get_acceptance() == code_;
1374  }
1375 
1376  bool operator!=(const acc_cond& other) const
1377  {
1378  return !(*this == other);
1379  }
1380 
1382  bool uses_fin_acceptance() const
1383  {
1384  return uses_fin_acceptance_;
1385  }
1386 
1388  bool is_t() const
1389  {
1390  return code_.is_t();
1391  }
1392 
1397  bool is_all() const
1398  {
1399  return num_ == 0 && is_t();
1400  }
1401 
1403  bool is_f() const
1404  {
1405  return code_.is_f();
1406  }
1407 
1412  bool is_none() const
1413  {
1414  return num_ == 0 && is_f();
1415  }
1416 
1421  bool is_buchi() const
1422  {
1423  unsigned s = code_.size();
1424  return num_ == 1 &&
1425  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1426  }
1427 
1432  bool is_co_buchi() const
1433  {
1434  return num_ == 1 && is_generalized_co_buchi();
1435  }
1436 
1440  {
1441  set_acceptance(inf(all_sets()));
1442  }
1443 
1447  {
1448  set_acceptance(fin(all_sets()));
1449  }
1450 
1456  {
1457  unsigned s = code_.size();
1458  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1459  && code_[0].mark == all_sets());
1460  }
1461 
1467  {
1468  unsigned s = code_.size();
1469  return (s == 2 &&
1470  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1471  }
1472 
1484  int is_rabin() const;
1485 
1497  int is_streett() const;
1498 
1508  struct SPOT_API rs_pair
1509  {
1510 #ifndef SWIG
1511  rs_pair() = default;
1512  rs_pair(const rs_pair&) = default;
1513 #endif
1514 
1515  rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
1516  fin(fin),
1517  inf(inf)
1518  {}
1519  acc_cond::mark_t fin;
1520  acc_cond::mark_t inf;
1521 
1522  bool operator==(rs_pair o) const
1523  {
1524  return fin == o.fin && inf == o.inf;
1525  }
1526  bool operator!=(rs_pair o) const
1527  {
1528  return fin != o.fin || inf != o.inf;
1529  }
1530  bool operator<(rs_pair o) const
1531  {
1532  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1533  }
1534  bool operator<=(rs_pair o) const
1535  {
1536  return !(o < *this);
1537  }
1538  bool operator>(rs_pair o) const
1539  {
1540  return o < *this;
1541  }
1542  bool operator>=(rs_pair o) const
1543  {
1544  return !(*this < o);
1545  }
1546  };
1557  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1558 
1569  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1570 
1580  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1581 
1594  bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1595 
1605  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1606 
1609  bool is_parity() const
1610  {
1611  bool max;
1612  bool odd;
1613  return is_parity(max, odd);
1614  }
1615 
1616  // Return (true, m) if there exist some acceptance mark m that
1617  // does not satisfy the acceptance condition. Return (false, 0U)
1618  // otherwise.
1619  std::pair<bool, acc_cond::mark_t> unsat_mark() const
1620  {
1621  return sat_unsat_mark(false);
1622  }
1623  // Return (true, m) if there exist some acceptance mark m that
1624  // does satisfy the acceptance condition. Return (false, 0U)
1625  // otherwise.
1626  std::pair<bool, acc_cond::mark_t> sat_mark() const
1627  {
1628  return sat_unsat_mark(true);
1629  }
1630 
1631  protected:
1632  bool check_fin_acceptance() const;
1633  std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1634 
1635  public:
1644  static acc_code inf(mark_t mark)
1645  {
1646  return acc_code::inf(mark);
1647  }
1648 
1649  static acc_code inf(std::initializer_list<unsigned> vals)
1650  {
1651  return inf(mark_t(vals.begin(), vals.end()));
1652  }
1654 
1671  static acc_code inf_neg(mark_t mark)
1672  {
1673  return acc_code::inf_neg(mark);
1674  }
1675 
1676  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1677  {
1678  return inf_neg(mark_t(vals.begin(), vals.end()));
1679  }
1681 
1689  static acc_code fin(mark_t mark)
1690  {
1691  return acc_code::fin(mark);
1692  }
1693 
1694  static acc_code fin(std::initializer_list<unsigned> vals)
1695  {
1696  return fin(mark_t(vals.begin(), vals.end()));
1697  }
1699 
1716  static acc_code fin_neg(mark_t mark)
1717  {
1718  return acc_code::fin_neg(mark);
1719  }
1720 
1721  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1722  {
1723  return fin_neg(mark_t(vals.begin(), vals.end()));
1724  }
1726 
1731  unsigned add_sets(unsigned num)
1732  {
1733  if (num == 0)
1734  return -1U;
1735  unsigned j = num_;
1736  num += j;
1737  if (num > mark_t::max_accsets())
1738  report_too_many_sets();
1739  // Make sure we do not update if we raised an exception.
1740  num_ = num;
1741  all_ = all_sets_();
1742  return j;
1743  }
1744 
1749  unsigned add_set()
1750  {
1751  return add_sets(1);
1752  }
1753 
1755  mark_t mark(unsigned u) const
1756  {
1757  SPOT_ASSERT(u < num_sets());
1758  return mark_t({u});
1759  }
1760 
1765  mark_t comp(const mark_t& l) const
1766  {
1767  return all_ ^ l;
1768  }
1769 
1772  {
1773  return all_;
1774  }
1775 
1778  bool accepting(mark_t inf) const
1779  {
1780  return code_.accepting(inf);
1781  }
1782 
1788  bool inf_satisfiable(mark_t inf) const
1789  {
1790  return code_.inf_satisfiable(inf);
1791  }
1792 
1804  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
1805  {
1806  return code_.maybe_accepting(infinitely_often, always_present);
1807  }
1808 
1822  mark_t accepting_sets(mark_t inf) const;
1823 
1824  // FIXME: deprecate?
1825  std::ostream& format(std::ostream& os, mark_t m) const
1826  {
1827  auto a = m; // ???
1828  if (!a)
1829  return os;
1830  return os << m;
1831  }
1832 
1833  // FIXME: deprecate?
1834  std::string format(mark_t m) const
1835  {
1836  std::ostringstream os;
1837  format(os, m);
1838  return os.str();
1839  }
1840 
1842  unsigned num_sets() const
1843  {
1844  return num_;
1845  }
1846 
1854  template<class iterator>
1855  mark_t useless(iterator begin, iterator end) const
1856  {
1857  mark_t u = {}; // The set of useless sets
1858  for (unsigned x = 0; x < num_; ++x)
1859  {
1860  // Skip sets that are already known to be useless.
1861  if (u.has(x))
1862  continue;
1863  auto all = comp(u | mark_t({x}));
1864  // Iterate over all mark_t, and keep track of
1865  // set numbers that always appear with x.
1866  for (iterator y = begin; y != end; ++y)
1867  {
1868  const mark_t& v = *y;
1869  if (v.has(x))
1870  {
1871  all &= v;
1872  if (!all)
1873  break;
1874  }
1875  }
1876  u |= all;
1877  }
1878  return u;
1879  }
1880 
1894  acc_cond remove(mark_t rem, bool missing) const
1895  {
1896  return {num_sets(), code_.remove(rem, missing)};
1897  }
1898 
1903  acc_cond strip(mark_t rem, bool missing) const
1904  {
1905  return
1906  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
1907  }
1908 
1911  {
1912  return {num_sets(), code_.force_inf(m)};
1913  }
1914 
1918  {
1919  return {num_sets(), code_.remove(all_sets() - rem, true)};
1920  }
1921 
1933  std::string name(const char* fmt = "alo") const;
1934 
1947  {
1948  return code_.fin_unit();
1949  }
1950 
1955  int fin_one() const
1956  {
1957  return code_.fin_one();
1958  }
1959 
1960  protected:
1961  mark_t all_sets_() const
1962  {
1963  return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
1964  }
1965 
1966  unsigned num_;
1967  mark_t all_;
1968  acc_code code_;
1969  bool uses_fin_acceptance_ = false;
1970 
1971  };
1972 
1973  struct rs_pairs_view {
1974  typedef std::vector<acc_cond::rs_pair> rs_pairs;
1975 
1976  // Creates view of pairs 'p' with restriction only to marks in 'm'
1977  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
1978  : pairs_(p), view_marks_(m) {}
1979 
1980  // Creates view of pairs without restriction to marks
1981  explicit rs_pairs_view(const rs_pairs& p)
1983 
1984  acc_cond::mark_t infs() const
1985  {
1986  return do_view([&](const acc_cond::rs_pair& p)
1987  {
1988  return visible(p.inf) ? p.inf : acc_cond::mark_t({});
1989  });
1990  }
1991 
1992  acc_cond::mark_t fins() const
1993  {
1994  return do_view([&](const acc_cond::rs_pair& p)
1995  {
1996  return visible(p.fin) ? p.fin : acc_cond::mark_t({});
1997  });
1998  }
1999 
2000  acc_cond::mark_t fins_alone() const
2001  {
2002  return do_view([&](const acc_cond::rs_pair& p)
2003  {
2004  return !visible(p.inf) && visible(p.fin) ? p.fin
2005  : acc_cond::mark_t({});
2006  });
2007  }
2008 
2009  acc_cond::mark_t infs_alone() const
2010  {
2011  return do_view([&](const acc_cond::rs_pair& p)
2012  {
2013  return !visible(p.fin) && visible(p.inf) ? p.inf
2014  : acc_cond::mark_t({});
2015  });
2016  }
2017 
2018  acc_cond::mark_t paired_with_fin(unsigned mark) const
2019  {
2020  acc_cond::mark_t res = {};
2021  for (const auto& p: pairs_)
2022  if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
2023  res |= p.inf;
2024  return res;
2025  }
2026 
2027  const rs_pairs& pairs() const
2028  {
2029  return pairs_;
2030  }
2031 
2032  private:
2033  template<typename filter>
2034  acc_cond::mark_t do_view(const filter& filt) const
2035  {
2036  acc_cond::mark_t res = {};
2037  for (const auto& p: pairs_)
2038  res |= filt(p);
2039  return res;
2040  }
2041 
2042  bool visible(const acc_cond::mark_t& v) const
2043  {
2044  return !!(view_marks_ & v);
2045  }
2046 
2047  const rs_pairs& pairs_;
2048  acc_cond::mark_t view_marks_;
2049  };
2050 
2051 
2052  SPOT_API
2053  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
2054 
2056 
2057  namespace internal
2058  {
2059  class SPOT_API mark_iterator
2060  {
2061  public:
2062  typedef unsigned value_type;
2063  typedef const value_type& reference;
2064  typedef const value_type* pointer;
2065  typedef std::ptrdiff_t difference_type;
2066  typedef std::forward_iterator_tag iterator_category;
2067 
2068  mark_iterator() noexcept
2069  : m_({})
2070  {
2071  }
2072 
2073  mark_iterator(acc_cond::mark_t m) noexcept
2074  : m_(m)
2075  {
2076  }
2077 
2078  bool operator==(mark_iterator m) const
2079  {
2080  return m_ == m.m_;
2081  }
2082 
2083  bool operator!=(mark_iterator m) const
2084  {
2085  return m_ != m.m_;
2086  }
2087 
2088  value_type operator*() const
2089  {
2090  SPOT_ASSERT(m_);
2091  return m_.min_set() - 1;
2092  }
2093 
2094  mark_iterator& operator++()
2095  {
2096  m_.clear(this->operator*());
2097  return *this;
2098  }
2099 
2100  mark_iterator operator++(int)
2101  {
2102  mark_iterator it = *this;
2103  ++(*this);
2104  return it;
2105  }
2106  private:
2107  acc_cond::mark_t m_;
2108  };
2109 
2110  class SPOT_API mark_container
2111  {
2112  public:
2114  : m_(m)
2115  {
2116  }
2117 
2118  mark_iterator begin() const
2119  {
2120  return {m_};
2121  }
2122  mark_iterator end() const
2123  {
2124  return {};
2125  }
2126  private:
2128  };
2129  }
2130 
2132  {
2133  return {*this};
2134  }
2135 }
2136 
2137 namespace std
2138 {
2139  template<>
2140  struct hash<spot::acc_cond::mark_t>
2141  {
2142  size_t operator()(spot::acc_cond::mark_t m) const noexcept
2143  {
2144  return m.hash();
2145  }
2146  };
2147 }
static acc_code inf(mark_t m)
Construct a generalized Büchi acceptance.
Definition: acc.hh:658
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:133
Definition: automata.hh:26
unsigned min_set() const
The number of the lowest set used plus one.
Definition: acc.hh:362
mark_t lowest() const
A mark_t where all bits have been removed except the lowest one.
Definition: acc.hh:374
bool is_all() const
Whether the acceptance condition is "all".
Definition: acc.hh:1397
mark_t all_sets() const
Construct a mark_t with all declared sets.
Definition: acc.hh:1771
spot::internal::mark_container sets() const
Returns some iterable object that contains the used sets.
Definition: acc.hh:2131
static acc_code fin(mark_t mark)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1689
Definition: acc.hh:2059
acc_cond force_inf(mark_t m) const
For all x in m, replaces Fin(x) by false.
Definition: acc.hh:1910
bool is_f() const
Whether the acceptance formula is "f" (false)
Definition: acc.hh:1403
bool is_f() const
Is this the "false" acceptance condition?
Definition: acc.hh:562
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:1788
bool is_buchi() const
Whether the acceptance condition is "Büchi".
Definition: acc.hh:1421
unsigned add_sets(unsigned num)
Add more sets to the acceptance condition.
Definition: acc.hh:1731
acc_op
Operators for acceptance formulas.
Definition: acc.hh:412
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1721
mark_t mark(unsigned u) const
Build a mark_t with a single set.
Definition: acc.hh:1755
unsigned max_set() const
The number of the highest set used plus one.
Definition: acc.hh:350
bool uses_fin_acceptance() const
Whether the acceptance condition uses Fin terms.
Definition: acc.hh:1382
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1508
void fill(iterator here) const
Fill a container with the indices of the bits that are set.
Definition: acc.hh:391
const acc_code & get_acceptance() const
Retrieve teh acceptance formula.
Definition: acc.hh:1360
Definition: bitset.hh:37
static acc_code f()
Construct the "false" acceptance condition.
Definition: acc.hh:576
static acc_code inf(mark_t mark)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1644
mark_t(const iterator &begin, const iterator &end)
Create a mark_t from a range of set numbers.
Definition: acc.hh:101
Definition: bitset.hh:405
Definition: acc.hh:1973
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:1917
bool subset(mark_t m) const
Whether the set of bits represented by *this is a subset of those represented by m.
Definition: acc.hh:328
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:1694
static mark_t all()
A mark_t with all bits set to one.
Definition: acc.hh:143
acc_code operator<<(unsigned sets) const
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1080
static acc_code streett(unsigned n)
Build a Streett condition with n pairs.
Definition: acc.hh:769
bool is_generalized_buchi() const
Whether the acceptance condition is "generalized-Büchi".
Definition: acc.hh:1455
void set_acceptance(const acc_code &code)
Change the acceptance formula.
Definition: acc.hh:1353
bool proper_subset(mark_t m) const
Whether the set of bits represented by *this is a proper subset of those represented by m...
Definition: acc.hh:335
static acc_code fin_neg(mark_t mark)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:1716
acc_code operator|(acc_code &&r) const
Disjunct the current condition with r.
Definition: acc.hh:1029
acc_code(const acc_word *other)
Copy a part of another acceptance formula.
Definition: acc.hh:1294
static acc_code inf_neg(mark_t mark)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1671
acc_cond remove(mark_t rem, bool missing) const
Remove all the acceptance sets in rem.
Definition: acc.hh:1894
mark_t & remove_some(unsigned n)
Remove n bits that where set.
Definition: acc.hh:382
bool is_none() const
Whether the acceptance condition is "none".
Definition: acc.hh:1412
An acceptance condition.
Definition: acc.hh:58
acc_cond strip(mark_t rem, bool missing) const
Remove acceptance sets, and shift set numbers.
Definition: acc.hh:1903
acc_cond & operator=(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1337
acc_cond(unsigned n_sets=0, const acc_code &code={})
Build an acceptance condition.
Definition: acc.hh:1311
mark_t(std::initializer_list< unsigned > vals)
Create a mark_t from a list of set numbers.
Definition: acc.hh:109
A "node" in an acceptance formulas.
Definition: acc.hh:422
acc_code & operator|=(const acc_code &r)
Disjunct the current condition in place with r.
Definition: acc.hh:942
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:668
void set_generalized_co_buchi()
Change the acceptance condition to generalized-co-Büchi, over all declared sets.
Definition: acc.hh:1446
static acc_code fin(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:612
int fin_one() const
Return one acceptance set i that appear as Fin(i) in the condition.
Definition: acc.hh:1955
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
static acc_code buchi()
Build a Büchi acceptance condition.
Definition: acc.hh:709
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:1676
(omega-Rational) Or
acc_code & get_acceptance()
Retrieve teh acceptance formula.
Definition: acc.hh:1366
bool is_co_buchi() const
Whether the acceptance condition is "co-Büchi".
Definition: acc.hh:1432
mark_t comp(const mark_t &l) const
Complement a mark_t.
Definition: acc.hh:1765
static acc_code t()
Construct the "true" acceptance condition.
Definition: acc.hh:590
Definition: twa.hh:1697
static acc_code cobuchi()
Build a co-Büchi acceptance condition.
Definition: acc.hh:717
unsigned count() const
Number of bits sets.
Definition: acc.hh:341
static acc_code inf_neg(mark_t m)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:690
acc_code()
Build an empty acceptance formula.
Definition: acc.hh:1289
bool is_generalized_co_buchi() const
Whether the acceptance condition is "generalized-co-Büchi".
Definition: acc.hh:1466
mark_t fin_unit() const
Find a Fin(i) that is a unit clause.
Definition: acc.hh:1946
op
Operator types.
Definition: formula.hh:64
bool is_parity() const
check is the acceptance condition matches one of the four type of parity acceptance defined in the HO...
Definition: acc.hh:1609
acc_code & operator<<=(unsigned sets)
Apply a left shift to all mark_t that appear in the condition.
Definition: acc.hh:1049
unsigned num_sets() const
The number of sets used in the acceptance condition.
Definition: acc.hh:1842
static acc_code inf(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance.
Definition: acc.hh:1649
static acc_code generalized_buchi(unsigned n)
Build a generalized-Büchi acceptance condition with n sets.
Definition: acc.hh:727
acc_cond(const acc_cond &o)
Copy an acceptance condition.
Definition: acc.hh:1330
acc_code operator|(const acc_code &r) const
Disjunct the current condition with r.
Definition: acc.hh:1037
static acc_code rabin(unsigned n)
Build a Rabin condition with n pairs.
Definition: acc.hh:754
unsigned add_set()
Add a single set to the acceptance condition.
Definition: acc.hh:1749
Definition: acc.hh:38
An acceptance formulas.
Definition: acc.hh:444
static acc_code fin(mark_t m)
Construct a generalized co-Büchi acceptance.
Definition: acc.hh:602
static acc_code generalized_rabin(Iterator begin, Iterator end)
Build a generalized Rabin condition.
Definition: acc.hh:793
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:1855
acc_cond(const acc_code &code)
Build an acceptance condition.
Definition: acc.hh:1322
bool accepting(mark_t inf) const
Check whether visiting exactly all sets inf infinitely often satisfies the acceptance condition...
Definition: acc.hh:1778
bool is_t() const
Whether the acceptance formula is "t" (true)
Definition: acc.hh:1388
Definition: acc.hh:2110
trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
Check potential acceptance of an SCC.
Definition: acc.hh:1804
(omega-Rational) And
void set_generalized_buchi()
Change the acceptance condition to generalized-Büchi, over all declared sets.
Definition: acc.hh:1439
static acc_code fin_neg(mark_t m)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:634
An acceptance mark.
Definition: acc.hh:81
static acc_code inf_neg(std::initializer_list< unsigned > vals)
Construct a generalized Büchi acceptance for complemented sets.
Definition: acc.hh:700
static acc_code fin_neg(std::initializer_list< unsigned > vals)
Construct a generalized co-Büchi acceptance for complemented sets.
Definition: acc.hh:644
static acc_code generalized_co_buchi(unsigned n)
Build a generalized-co-Büchi acceptance condition with n sets.
Definition: acc.hh:741
bool is_t() const
Is this the "true" acceptance condition?
Definition: acc.hh:548

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