spot  2.6
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 
47  class SPOT_API acc_cond
48  {
49 
50 #ifndef SWIG
51  private:
52  [[noreturn]] static void report_too_many_sets();
53 #endif
54  public:
55  struct mark_t :
56  public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
57  {
58  private:
59  // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
60  typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
61  _value_t id;
62 
63  mark_t(_value_t id) noexcept
64  : id(id)
65  {
66  }
67 
68  public:
69  mark_t() = default;
70 
71 #ifndef SWIG
72  template<class iterator>
73  mark_t(const iterator& begin, const iterator& end)
74  : mark_t(_value_t::zero())
75  {
76  for (iterator i = begin; i != end; ++i)
77  set(*i);
78  }
79 
80  mark_t(std::initializer_list<unsigned> vals)
81  : mark_t(vals.begin(), vals.end())
82  {
83  }
84 
85  SPOT_DEPRECATED("use brace initialization instead")
86  mark_t(unsigned i)
87  {
88  unsigned j = 0;
89  while (i)
90  {
91  if (i & 1U)
92  this->set(j);
93  ++j;
94  i >>= 1;
95  }
96  }
97 #endif
98 
104  constexpr static unsigned max_accsets()
105  {
106  return SPOT_MAX_ACCSETS;
107  }
108 
109  static mark_t all()
110  {
111  return mark_t(_value_t::mone());
112  }
113 
114  size_t hash() const noexcept
115  {
116  std::hash<decltype(id)> h;
117  return h(id);
118  }
119 
120  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
121  bool operator==(unsigned o) const
122  {
123  SPOT_ASSERT(o == 0U);
124  (void)o;
125  return !id;
126  }
127 
128  SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
129  bool operator!=(unsigned o) const
130  {
131  SPOT_ASSERT(o == 0U);
132  (void)o;
133  return !!id;
134  }
135 
136  bool operator==(mark_t o) const
137  {
138  return id == o.id;
139  }
140 
141  bool operator!=(mark_t o) const
142  {
143  return id != o.id;
144  }
145 
146  bool operator<(mark_t o) const
147  {
148  return id < o.id;
149  }
150 
151  bool operator<=(mark_t o) const
152  {
153  return id <= o.id;
154  }
155 
156  bool operator>(mark_t o) const
157  {
158  return id > o.id;
159  }
160 
161  bool operator>=(mark_t o) const
162  {
163  return id >= o.id;
164  }
165 
166  explicit operator bool() const
167  {
168  return !!id;
169  }
170 
171  bool has(unsigned u) const
172  {
173  return !!this->operator&(mark_t({0}) << u);
174  }
175 
176  void set(unsigned u)
177  {
178  id.set(u);
179  }
180 
181  void clear(unsigned u)
182  {
183  id.clear(u);
184  }
185 
186  mark_t& operator&=(mark_t r)
187  {
188  id &= r.id;
189  return *this;
190  }
191 
192  mark_t& operator|=(mark_t r)
193  {
194  id |= r.id;
195  return *this;
196  }
197 
198  mark_t& operator-=(mark_t r)
199  {
200  id &= ~r.id;
201  return *this;
202  }
203 
204  mark_t& operator^=(mark_t r)
205  {
206  id ^= r.id;
207  return *this;
208  }
209 
210  mark_t operator&(mark_t r) const
211  {
212  return id & r.id;
213  }
214 
215  mark_t operator|(mark_t r) const
216  {
217  return id | r.id;
218  }
219 
220  mark_t operator-(mark_t r) const
221  {
222  return id & ~r.id;
223  }
224 
225  mark_t operator~() const
226  {
227  return ~id;
228  }
229 
230  mark_t operator^(mark_t r) const
231  {
232  return id ^ r.id;
233  }
234 
235 #if SPOT_DEBUG || defined(SWIGPYTHON)
236 # define SPOT_WRAP_OP(ins) \
237  try \
238  { \
239  ins; \
240  } \
241  catch (const std::runtime_error& e) \
242  { \
243  report_too_many_sets(); \
244  }
245 #else
246 # define SPOT_WRAP_OP(ins) ins;
247 #endif
248  mark_t operator<<(unsigned i) const
249  {
250  SPOT_WRAP_OP(return id << i);
251  }
252 
253  mark_t& operator<<=(unsigned i)
254  {
255  SPOT_WRAP_OP(id <<= i; return *this);
256  }
257 
258  mark_t operator>>(unsigned i) const
259  {
260  SPOT_WRAP_OP(return id >> i);
261  }
262 
263  mark_t& operator>>=(unsigned i)
264  {
265  SPOT_WRAP_OP(id >>= i; return *this);
266  }
267 #undef SPOT_WRAP_OP
268 
269  mark_t strip(mark_t y) const
270  {
271  // strip every bit of id that is marked in y
272  // 100101110100.strip(
273  // 001011001000)
274  // == 10 1 11 100
275  // == 10111100
276 
277  auto xv = id; // 100101110100
278  auto yv = y.id; // 001011001000
279 
280  while (yv && xv)
281  {
282  // Mask for everything after the last 1 in y
283  auto rm = (~yv) & (yv - 1); // 000000000111
284  // Mask for everything before the last 1 in y
285  auto lm = ~(yv ^ (yv - 1)); // 111111110000
286  xv = ((xv & lm) >> 1) | (xv & rm);
287  yv = (yv & lm) >> 1;
288  }
289  return xv;
290  }
291 
292  bool subset(mark_t m) const
293  {
294  return !((*this) - m);
295  }
296 
297  bool proper_subset(mark_t m) const
298  {
299  return *this != m && this->subset(m);
300  }
301 
302  // Number of bits sets.
303  unsigned count() const
304  {
305  return id.count();
306  }
307 
308  // Return the number of the highest set used plus one.
309  // If no set is used, this returns 0,
310  // If the sets {1,3,8} are used, this returns 9.
311  unsigned max_set() const
312  {
313  if (id)
314  return id.highest()+1;
315  else
316  return 0;
317  }
318 
319  // Return the number of the lowest set used plus one.
320  // If no set is used, this returns 0.
321  // If the sets {1,3,8} are used, this returns 2.
322  unsigned min_set() const
323  {
324  if (id)
325  return id.lowest()+1;
326  else
327  return 0;
328  }
329 
330  // Return the lowest acceptance mark
331  mark_t lowest() const
332  {
333  return id & -id;
334  }
335 
336  // Remove n bits that where set
337  mark_t& remove_some(unsigned n)
338  {
339  while (n--)
340  id &= id - 1;
341  return *this;
342  }
343 
344  template<class iterator>
345  void fill(iterator here) const
346  {
347  auto a = *this;
348  unsigned level = 0;
349  while (a)
350  {
351  if (a.has(0))
352  *here++ = level;
353  ++level;
354  a >>= 1;
355  }
356  }
357 
358  // Returns some iterable object that contains the used sets.
359  spot::internal::mark_container sets() const;
360 
361  SPOT_API
362  friend std::ostream& operator<<(std::ostream& os, mark_t m);
363  };
364 
365  // This encodes either an operator or set of acceptance sets.
366  enum class acc_op : unsigned short
367  { Inf, Fin, InfNeg, FinNeg, And, Or };
368  union acc_word
369  {
370  mark_t mark;
371  struct {
372  acc_op op; // Operator
373  unsigned short size; // Size of the subtree (number of acc_word),
374  // not counting this node.
375  } sub;
376  };
377 
378  struct SPOT_API acc_code: public std::vector<acc_word>
379  {
380  bool operator==(const acc_code& other) const
381  {
382  unsigned pos = size();
383  if (other.size() != pos)
384  return false;
385  while (pos > 0)
386  {
387  auto op = (*this)[pos - 1].sub.op;
388  auto sz = (*this)[pos - 1].sub.size;
389  if (other[pos - 1].sub.op != op ||
390  other[pos - 1].sub.size != sz)
391  return false;
392  switch (op)
393  {
394  case acc_cond::acc_op::And:
395  case acc_cond::acc_op::Or:
396  --pos;
397  break;
398  case acc_cond::acc_op::Inf:
399  case acc_cond::acc_op::InfNeg:
400  case acc_cond::acc_op::Fin:
401  case acc_cond::acc_op::FinNeg:
402  pos -= 2;
403  if (other[pos].mark != (*this)[pos].mark)
404  return false;
405  break;
406  }
407  }
408  return true;
409  };
410 
411  bool operator<(const acc_code& other) const
412  {
413  unsigned pos = size();
414  auto osize = other.size();
415  if (pos < osize)
416  return true;
417  if (pos > osize)
418  return false;
419  while (pos > 0)
420  {
421  auto op = (*this)[pos - 1].sub.op;
422  auto oop = other[pos - 1].sub.op;
423  if (op < oop)
424  return true;
425  if (op > oop)
426  return false;
427  auto sz = (*this)[pos - 1].sub.size;
428  auto osz = other[pos - 1].sub.size;
429  if (sz < osz)
430  return true;
431  if (sz > osz)
432  return false;
433  switch (op)
434  {
435  case acc_cond::acc_op::And:
436  case acc_cond::acc_op::Or:
437  --pos;
438  break;
439  case acc_cond::acc_op::Inf:
440  case acc_cond::acc_op::InfNeg:
441  case acc_cond::acc_op::Fin:
442  case acc_cond::acc_op::FinNeg:
443  {
444  pos -= 2;
445  auto m = (*this)[pos].mark;
446  auto om = other[pos].mark;
447  if (m < om)
448  return true;
449  if (m > om)
450  return false;
451  break;
452  }
453  }
454  }
455  return false;
456  }
457 
458  bool operator>(const acc_code& other) const
459  {
460  return other < *this;
461  }
462 
463  bool operator<=(const acc_code& other) const
464  {
465  return !(other < *this);
466  }
467 
468  bool operator>=(const acc_code& other) const
469  {
470  return !(*this < other);
471  }
472 
473  bool operator!=(const acc_code& other) const
474  {
475  return !(*this == other);
476  }
477 
478  bool is_t() const
479  {
480  unsigned s = size();
481  return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
482  && !((*this)[s - 2].mark));
483  }
484 
485  bool is_f() const
486  {
487  unsigned s = size();
488  return s > 1
489  && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
490  }
491 
492  static acc_code f()
493  {
494  acc_code res;
495  res.resize(2);
496  res[0].mark = {};
497  res[1].sub.op = acc_op::Fin;
498  res[1].sub.size = 1;
499  return res;
500  }
501 
502  static acc_code t()
503  {
504  return {};
505  }
506 
507  static acc_code fin(mark_t m)
508  {
509  acc_code res;
510  res.resize(2);
511  res[0].mark = m;
512  res[1].sub.op = acc_op::Fin;
513  res[1].sub.size = 1;
514  return res;
515  }
516 
517  static acc_code fin(std::initializer_list<unsigned> vals)
518  {
519  return fin(mark_t(vals));
520  }
521 
522  static acc_code fin_neg(mark_t m)
523  {
524  acc_code res;
525  res.resize(2);
526  res[0].mark = m;
527  res[1].sub.op = acc_op::FinNeg;
528  res[1].sub.size = 1;
529  return res;
530  }
531 
532  static acc_code fin_neg(std::initializer_list<unsigned> vals)
533  {
534  return fin_neg(mark_t(vals));
535  }
536 
537  static acc_code inf(mark_t m)
538  {
539  acc_code res;
540  res.resize(2);
541  res[0].mark = m;
542  res[1].sub.op = acc_op::Inf;
543  res[1].sub.size = 1;
544  return res;
545  }
546 
547  static acc_code inf(std::initializer_list<unsigned> vals)
548  {
549  return inf(mark_t(vals));
550  }
551 
552  static acc_code inf_neg(mark_t m)
553  {
554  acc_code res;
555  res.resize(2);
556  res[0].mark = m;
557  res[1].sub.op = acc_op::InfNeg;
558  res[1].sub.size = 1;
559  return res;
560  }
561 
562  static acc_code inf_neg(std::initializer_list<unsigned> vals)
563  {
564  return inf_neg(mark_t(vals));
565  }
566 
567  static acc_code buchi()
568  {
569  return inf({0});
570  }
571 
572  static acc_code cobuchi()
573  {
574  return fin({0});
575  }
576 
577  static acc_code generalized_buchi(unsigned n)
578  {
579  if (n == 0)
580  return inf({});
581  acc_cond::mark_t m = mark_t::all();
582  m >>= mark_t::max_accsets() - n;
583  return inf(m);
584  }
585 
586  static acc_code generalized_co_buchi(unsigned n)
587  {
588  if (n == 0)
589  return fin({});
590  acc_cond::mark_t m = mark_t::all();
591  m >>= mark_t::max_accsets() - n;
592  return fin(m);
593  }
594 
595  // n is a number of pairs.
596  static acc_code rabin(unsigned n)
597  {
598  acc_cond::acc_code res = f();
599  while (n > 0)
600  {
601  res |= inf({2*n - 1}) & fin({2*n - 2});
602  --n;
603  }
604  return res;
605  }
606 
607  // n is a number of pairs.
608  static acc_code streett(unsigned n)
609  {
610  acc_cond::acc_code res = t();
611  while (n > 0)
612  {
613  res &= inf({2*n - 1}) | fin({2*n - 2});
614  --n;
615  }
616  return res;
617  }
618 
619  template<class Iterator>
620  static acc_code generalized_rabin(Iterator begin, Iterator end)
621  {
622  acc_cond::acc_code res = f();
623  unsigned n = 0;
624  for (Iterator i = begin; i != end; ++i)
625  {
626  unsigned f = n++;
627  acc_cond::mark_t m = {};
628  for (unsigned ni = *i; ni > 0; --ni)
629  m.set(n++);
630  auto pair = inf(m) & fin({f});
631  std::swap(pair, res);
632  res |= std::move(pair);
633  }
634  return res;
635  }
636 
637  static acc_code parity(bool max, bool odd, unsigned sets);
638 
639  // Number of acceptance sets to use, and probability to reuse
640  // each set another time after it has been used in the
641  // acceptance formula.
642  static acc_code random(unsigned n, double reuse = 0.0);
643 
644  acc_code& operator&=(const acc_code& r)
645  {
646  if (is_t() || r.is_f())
647  {
648  *this = r;
649  return *this;
650  }
651  if (is_f() || r.is_t())
652  return *this;
653  unsigned s = size() - 1;
654  unsigned rs = r.size() - 1;
655  // We want to group all Inf(x) operators:
656  // Inf(a) & Inf(b) = Inf(a & b)
657  if (((*this)[s].sub.op == acc_op::Inf
658  && r[rs].sub.op == acc_op::Inf)
659  || ((*this)[s].sub.op == acc_op::InfNeg
660  && r[rs].sub.op == acc_op::InfNeg))
661  {
662  (*this)[s - 1].mark |= r[rs - 1].mark;
663  return *this;
664  }
665 
666  // In the more complex scenarios, left and right may both
667  // be conjunctions, and Inf(x) might be a member of each
668  // side. Find it if it exists.
669  // left_inf points to the left Inf mark if any.
670  // right_inf points to the right Inf mark if any.
671  acc_word* left_inf = nullptr;
672  if ((*this)[s].sub.op == acc_op::And)
673  {
674  auto start = &(*this)[s] - (*this)[s].sub.size;
675  auto pos = &(*this)[s] - 1;
676  pop_back();
677  while (pos > start)
678  {
679  if (pos->sub.op == acc_op::Inf)
680  {
681  left_inf = pos - 1;
682  break;
683  }
684  pos -= pos->sub.size + 1;
685  }
686  }
687  else if ((*this)[s].sub.op == acc_op::Inf)
688  {
689  left_inf = &(*this)[s - 1];
690  }
691 
692  const acc_word* right_inf = nullptr;
693  auto right_end = &r.back();
694  if (right_end->sub.op == acc_op::And)
695  {
696  auto start = &r[0];
697  auto pos = --right_end;
698  while (pos > start)
699  {
700  if (pos->sub.op == acc_op::Inf)
701  {
702  right_inf = pos - 1;
703  break;
704  }
705  pos -= pos->sub.size + 1;
706  }
707  }
708  else if (right_end->sub.op == acc_op::Inf)
709  {
710  right_inf = right_end - 1;
711  }
712 
713  acc_cond::mark_t carry = {};
714  if (left_inf && right_inf)
715  {
716  carry = left_inf->mark;
717  auto pos = left_inf - &(*this)[0];
718  erase(begin() + pos, begin() + pos + 2);
719  }
720  auto sz = size();
721  insert(end(), &r[0], right_end + 1);
722  if (carry)
723  (*this)[sz + (right_inf - &r[0])].mark |= carry;
724 
725  acc_word w;
726  w.sub.op = acc_op::And;
727  w.sub.size = size();
728  emplace_back(w);
729  return *this;
730  }
731 
732  acc_code operator&(const acc_code& r)
733  {
734  acc_code res = *this;
735  res &= r;
736  return res;
737  }
738 
739  acc_code operator&(acc_code&& r)
740  {
741  acc_code res = *this;
742  res &= r;
743  return res;
744  }
745 
746  acc_code& operator|=(const acc_code& r)
747  {
748  if (is_t() || r.is_f())
749  return *this;
750  if (is_f() || r.is_t())
751  {
752  *this = r;
753  return *this;
754  }
755  unsigned s = size() - 1;
756  unsigned rs = r.size() - 1;
757  // Fin(a) | Fin(b) = Fin(a | b)
758  if (((*this)[s].sub.op == acc_op::Fin
759  && r[rs].sub.op == acc_op::Fin)
760  || ((*this)[s].sub.op == acc_op::FinNeg
761  && r[rs].sub.op == acc_op::FinNeg))
762  {
763  (*this)[s - 1].mark |= r[rs - 1].mark;
764  return *this;
765  }
766 
767  // In the more complex scenarios, left and right may both
768  // be disjunctions, and Fin(x) might be a member of each
769  // side. Find it if it exists.
770  // left_inf points to the left Inf mark if any.
771  // right_inf points to the right Inf mark if any.
772  acc_word* left_fin = nullptr;
773  if ((*this)[s].sub.op == acc_op::Or)
774  {
775  auto start = &(*this)[s] - (*this)[s].sub.size;
776  auto pos = &(*this)[s] - 1;
777  pop_back();
778  while (pos > start)
779  {
780  if (pos->sub.op == acc_op::Fin)
781  {
782  left_fin = pos - 1;
783  break;
784  }
785  pos -= pos->sub.size + 1;
786  }
787  }
788  else if ((*this)[s].sub.op == acc_op::Fin)
789  {
790  left_fin = &(*this)[s - 1];
791  }
792 
793  const acc_word* right_fin = nullptr;
794  auto right_end = &r.back();
795  if (right_end->sub.op == acc_op::Or)
796  {
797  auto start = &r[0];
798  auto pos = --right_end;
799  while (pos > start)
800  {
801  if (pos->sub.op == acc_op::Fin)
802  {
803  right_fin = pos - 1;
804  break;
805  }
806  pos -= pos->sub.size + 1;
807  }
808  }
809  else if (right_end->sub.op == acc_op::Fin)
810  {
811  right_fin = right_end - 1;
812  }
813 
814  acc_cond::mark_t carry = {};
815  if (left_fin && right_fin)
816  {
817  carry = left_fin->mark;
818  auto pos = (left_fin - &(*this)[0]);
819  this->erase(begin() + pos, begin() + pos + 2);
820  }
821  auto sz = size();
822  insert(end(), &r[0], right_end + 1);
823  if (carry)
824  (*this)[sz + (right_fin - &r[0])].mark |= carry;
825  acc_word w;
826  w.sub.op = acc_op::Or;
827  w.sub.size = size();
828  emplace_back(w);
829  return *this;
830  }
831 
832  acc_code operator|(acc_code&& r)
833  {
834  acc_code res = *this;
835  res |= r;
836  return res;
837  }
838 
839  acc_code operator|(const acc_code& r)
840  {
841  acc_code res = *this;
842  res |= r;
843  return res;
844  }
845 
846  acc_code& operator<<=(unsigned sets)
847  {
848  if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
849  report_too_many_sets();
850  if (empty())
851  return *this;
852  unsigned pos = size();
853  do
854  {
855  switch ((*this)[pos - 1].sub.op)
856  {
857  case acc_cond::acc_op::And:
858  case acc_cond::acc_op::Or:
859  --pos;
860  break;
861  case acc_cond::acc_op::Inf:
862  case acc_cond::acc_op::InfNeg:
863  case acc_cond::acc_op::Fin:
864  case acc_cond::acc_op::FinNeg:
865  pos -= 2;
866  (*this)[pos].mark <<= sets;
867  break;
868  }
869  }
870  while (pos > 0);
871  return *this;
872  }
873 
874  acc_code operator<<(unsigned sets) const
875  {
876  acc_code res = *this;
877  res <<= sets;
878  return res;
879  }
880 
881  bool is_dnf() const;
882  bool is_cnf() const;
883 
884  acc_code to_dnf() const;
885  acc_code to_cnf() const;
886 
887  acc_code complement() const;
888 
889  // Return a list of acceptance marks needed to close a cycle
890  // that already visit INF infinitely often, so that the cycle is
891  // accepting (ACCEPTING=true) or rejecting (ACCEPTING=false).
892  // Positive values describe positive set.
893  // A negative value x means the set -x-1 must be absent.
894  std::vector<std::vector<int>>
895  missing(mark_t inf, bool accepting) const;
896 
897  bool accepting(mark_t inf) const;
898 
899  bool inf_satisfiable(mark_t inf) const;
900 
901  trival maybe_accepting(mark_t infinitely_often,
902  mark_t always_present) const;
903 
904 
905  // Remove all the acceptance sets in rem.
906  //
907  // If MISSING is set, the acceptance sets are assumed to be
908  // missing from the automaton, and the acceptance is updated to
909  // reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will
910  // become Fin(3) if we remove 2 because it is missing from this
911  // automaton, because there is no way to fulfill Inf(1)&Inf(2)
912  // in this case. So essentially MISSING causes Inf(rem) to
913  // become f, and Fin(rem) to become t.
914  //
915  // If MISSING is unset, Inf(rem) become t while Fin(rem) become
916  // f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
917  // Inf(1)|Fin(3).
918  acc_code remove(acc_cond::mark_t rem, bool missing) const;
919  // Same as remove, but also shift numbers
920  acc_code strip(acc_cond::mark_t rem, bool missing) const;
921 
922  // Return the set of sets appearing in the condition.
923  acc_cond::mark_t used_sets() const;
924 
925  // Return the sets used as Inf or Fin in the acceptance condition
926  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
927 
928  // Print the acceptance as HTML. The set_printer function can
929  // be used to implement customized output for set numbers.
930  std::ostream&
931  to_html(std::ostream& os,
932  std::function<void(std::ostream&, int)>
933  set_printer = nullptr) const;
934 
935  // Print the acceptance as text. The set_printer function can
936  // be used to implement customized output for set numbers.
937  std::ostream&
938  to_text(std::ostream& os,
939  std::function<void(std::ostream&, int)>
940  set_printer = nullptr) const;
941 
942  // Print the acceptance as Latex. The set_printer function can
943  // be used to implement customized output for set numbers.
944  std::ostream&
945  to_latex(std::ostream& os,
946  std::function<void(std::ostream&, int)>
947  set_printer = nullptr) const;
948 
971  acc_code(const char* input);
972 
977  {
978  }
979 
980  // Calls to_text
981  SPOT_API
982  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
983  };
984 
985  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
986  : num_(0U), all_({}), code_(code)
987  {
988  add_sets(n_sets);
989  uses_fin_acceptance_ = check_fin_acceptance();
990  }
991 
992  acc_cond(const acc_code& code)
993  : num_(0U), all_({}), code_(code)
994  {
995  add_sets(code.used_sets().max_set());
996  uses_fin_acceptance_ = check_fin_acceptance();
997  }
998 
999  acc_cond(const acc_cond& o)
1000  : num_(o.num_), all_(o.all_), code_(o.code_),
1001  uses_fin_acceptance_(o.uses_fin_acceptance_)
1002  {
1003  }
1004 
1005  acc_cond& operator=(const acc_cond& o)
1006  {
1007  num_ = o.num_;
1008  all_ = o.all_;
1009  code_ = o.code_;
1010  uses_fin_acceptance_ = o.uses_fin_acceptance_;
1011  return *this;
1012  }
1013 
1014  ~acc_cond()
1015  {
1016  }
1017 
1018  void set_acceptance(const acc_code& code)
1019  {
1020  code_ = code;
1021  uses_fin_acceptance_ = check_fin_acceptance();
1022  }
1023 
1024  const acc_code& get_acceptance() const
1025  {
1026  return code_;
1027  }
1028 
1029  acc_code& get_acceptance()
1030  {
1031  return code_;
1032  }
1033 
1034  bool operator==(const acc_cond& other) const
1035  {
1036  return other.num_sets() == num_ && other.get_acceptance() == code_;
1037  }
1038 
1039  bool operator!=(const acc_cond& other) const
1040  {
1041  return !(*this == other);
1042  }
1043 
1044  bool uses_fin_acceptance() const
1045  {
1046  return uses_fin_acceptance_;
1047  }
1048 
1049  bool is_t() const
1050  {
1051  return code_.is_t();
1052  }
1053 
1054  bool is_all() const
1055  {
1056  return num_ == 0 && is_t();
1057  }
1058 
1059  bool is_f() const
1060  {
1061  return code_.is_f();
1062  }
1063 
1064  bool is_none() const
1065  {
1066  return num_ == 0 && is_f();
1067  }
1068 
1069  bool is_buchi() const
1070  {
1071  unsigned s = code_.size();
1072  return num_ == 1 &&
1073  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1074  }
1075 
1076  bool is_co_buchi() const
1077  {
1078  return num_ == 1 && is_generalized_co_buchi();
1079  }
1080 
1081  void set_generalized_buchi()
1082  {
1083  set_acceptance(inf(all_sets()));
1084  }
1085 
1086  void set_generalized_co_buchi()
1087  {
1088  set_acceptance(fin(all_sets()));
1089  }
1090 
1091  bool is_generalized_buchi() const
1092  {
1093  unsigned s = code_.size();
1094  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1095  && code_[0].mark == all_sets());
1096  }
1097 
1098  bool is_generalized_co_buchi() const
1099  {
1100  unsigned s = code_.size();
1101  return (s == 2 &&
1102  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1103  }
1104 
1105  // Returns a number of pairs (>=0) if Rabin, or -1 else.
1106  int is_rabin() const;
1107  // Returns a number of pairs (>=0) if Streett, or -1 else.
1108  int is_streett() const;
1109 
1119  struct SPOT_API rs_pair
1120  {
1121  rs_pair() = default;
1122  rs_pair(const rs_pair&) = default;
1123 
1125  fin(fin),
1126  inf(inf)
1127  {}
1128  acc_cond::mark_t fin;
1129  acc_cond::mark_t inf;
1130 
1131  bool operator==(rs_pair o) const
1132  {
1133  return fin == o.fin && inf == o.inf;
1134  }
1135  bool operator!=(rs_pair o) const
1136  {
1137  return fin != o.fin || inf != o.inf;
1138  }
1139  bool operator<(rs_pair o) const
1140  {
1141  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1142  }
1143  bool operator<=(rs_pair o) const
1144  {
1145  return !(o < *this);
1146  }
1147  bool operator>(rs_pair o) const
1148  {
1149  return o < *this;
1150  }
1151  bool operator>=(rs_pair o) const
1152  {
1153  return !(*this < o);
1154  }
1155  };
1166  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1167 
1178  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1179 
1180  // Return the number of Inf in each pair.
1181  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1182 
1183  // Return the number of Inf in each pair.
1184  bool is_generalized_streett(std::vector<unsigned>& pairs) const;
1185 
1186  // If EQUIV is false, this return true iff the acceptance
1187  // condition is a parity condition written in the canonical way
1188  // given in the HOA specifications. If EQUIV is true, then we
1189  // check whether the condition is logically equivalent to some
1190  // parity acceptance condition.
1191  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1192  bool is_parity() const
1193  {
1194  bool max;
1195  bool odd;
1196  return is_parity(max, odd);
1197  }
1198 
1199  // Return (true, m) if there exist some acceptance mark m that
1200  // does not satisfy the acceptance condition. Return (false, 0U)
1201  // otherwise.
1202  std::pair<bool, acc_cond::mark_t> unsat_mark() const
1203  {
1204  return sat_unsat_mark(false);
1205  }
1206  // Return (true, m) if there exist some acceptance mark m that
1207  // does satisfy the acceptance condition. Return (false, 0U)
1208  // otherwise.
1209  std::pair<bool, acc_cond::mark_t> sat_mark() const
1210  {
1211  return sat_unsat_mark(true);
1212  }
1213 
1214  protected:
1215  bool check_fin_acceptance() const;
1216  std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
1217 
1218  public:
1219  static acc_code inf(mark_t mark)
1220  {
1221  return acc_code::inf(mark);
1222  }
1223 
1224  static acc_code inf(std::initializer_list<unsigned> vals)
1225  {
1226  return inf(mark_t(vals.begin(), vals.end()));
1227  }
1228 
1229  static acc_code inf_neg(mark_t mark)
1230  {
1231  return acc_code::inf_neg(mark);
1232  }
1233 
1234  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1235  {
1236  return inf_neg(mark_t(vals.begin(), vals.end()));
1237  }
1238 
1239  static acc_code fin(mark_t mark)
1240  {
1241  return acc_code::fin(mark);
1242  }
1243 
1244  static acc_code fin(std::initializer_list<unsigned> vals)
1245  {
1246  return fin(mark_t(vals.begin(), vals.end()));
1247  }
1248 
1249  static acc_code fin_neg(mark_t mark)
1250  {
1251  return acc_code::fin_neg(mark);
1252  }
1253 
1254  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1255  {
1256  return fin_neg(mark_t(vals.begin(), vals.end()));
1257  }
1258 
1259  unsigned add_sets(unsigned num)
1260  {
1261  if (num == 0)
1262  return -1U;
1263  unsigned j = num_;
1264  num += j;
1265  if (num > mark_t::max_accsets())
1266  report_too_many_sets();
1267  // Make sure we do not update if we raised an exception.
1268  num_ = num;
1269  all_ = all_sets_();
1270  return j;
1271  }
1272 
1273  unsigned add_set()
1274  {
1275  return add_sets(1);
1276  }
1277 
1278  mark_t mark(unsigned u) const
1279  {
1280  SPOT_ASSERT(u < num_sets());
1281  return mark_t({0}) << u;
1282  }
1283 
1284  mark_t comp(const mark_t& l) const
1285  {
1286  return all_ ^ l;
1287  }
1288 
1289  mark_t all_sets() const
1290  {
1291  return all_;
1292  }
1293 
1294  bool accepting(mark_t inf) const
1295  {
1296  return code_.accepting(inf);
1297  }
1298 
1299  bool inf_satisfiable(mark_t inf) const
1300  {
1301  return code_.inf_satisfiable(inf);
1302  }
1303 
1304  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
1305  {
1306  return code_.maybe_accepting(infinitely_often, always_present);
1307  }
1308 
1309  mark_t accepting_sets(mark_t inf) const;
1310 
1311  std::ostream& format(std::ostream& os, mark_t m) const
1312  {
1313  auto a = m;
1314  if (!a)
1315  return os;
1316  return os << m;
1317  }
1318 
1319  std::string format(mark_t m) const
1320  {
1321  std::ostringstream os;
1322  format(os, m);
1323  return os.str();
1324  }
1325 
1326  unsigned num_sets() const
1327  {
1328  return num_;
1329  }
1330 
1331  template<class iterator>
1332  mark_t useless(iterator begin, iterator end) const
1333  {
1334  mark_t u = {}; // The set of useless marks
1335  const mark_t one = {0};
1336  for (unsigned x = 0; x < num_; ++x)
1337  {
1338  // Skip marks that are already known to be useless.
1339  if (u & (one << x))
1340  continue;
1341  auto all = all_ ^ (u | (one << x));
1342  for (iterator y = begin; y != end; ++y)
1343  {
1344  const mark_t& v = *y;
1345  if (!!(v & (one << x)))
1346  {
1347  all &= v;
1348  if (!all)
1349  break;
1350  }
1351  }
1352  u |= all;
1353  }
1354  return u;
1355  }
1356 
1357  // Remove all the acceptance sets in rem.
1358  //
1359  // If MISSING is set, the acceptance sets are assumed to be
1360  // missing from the automaton, and the acceptance is updated to
1361  // reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will
1362  // become Fin(3) if we remove 2 because it is missing from this
1363  // automaton, because there is no way to fulfill Inf(1)&Inf(2)
1364  // in this case. So essentially MISSING causes Inf(rem) to
1365  // become f, and Fin(rem) to become t.
1366  //
1367  // If MISSING is unset, Inf(rem) become t while Fin(rem) become
1368  // f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
1369  // Inf(1)|Fin(3).
1370  acc_cond remove(mark_t rem, bool missing) const
1371  {
1372  return {num_sets(), code_.remove(rem, missing)};
1373  }
1374 
1375  // Same as remove, but also shift the set numbers
1376  acc_cond strip(mark_t rem, bool missing) const
1377  {
1378  return
1379  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
1380  }
1381 
1382  // Restrict an acceptance condition to a subset of set numbers
1383  // that are occurring at some point.
1384  acc_cond restrict_to(mark_t rem) const
1385  {
1386  return {num_sets(), code_.remove(all_sets() - rem, true)};
1387  }
1388 
1400  std::string name(const char* fmt = "alo") const;
1401 
1402  protected:
1403  mark_t all_sets_() const
1404  {
1405  return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
1406  }
1407 
1408  unsigned num_;
1409  mark_t all_;
1410  acc_code code_;
1411  bool uses_fin_acceptance_ = false;
1412 
1413  };
1414 
1415  struct rs_pairs_view {
1416  typedef std::vector<acc_cond::rs_pair> rs_pairs;
1417 
1418  // Creates view of pairs 'p' with restriction only to marks in 'm'
1419  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
1420  : pairs_(p), view_marks_(m) {}
1421 
1422  // Creates view of pairs without restriction to marks
1423  explicit rs_pairs_view(const rs_pairs& p)
1424  : rs_pairs_view(p, acc_cond::mark_t::all()) {}
1425 
1426  acc_cond::mark_t infs() const
1427  {
1428  return do_view([&](const acc_cond::rs_pair& p)
1429  {
1430  return visible(p.inf) ? p.inf : acc_cond::mark_t({});
1431  });
1432  }
1433 
1434  acc_cond::mark_t fins() const
1435  {
1436  return do_view([&](const acc_cond::rs_pair& p)
1437  {
1438  return visible(p.fin) ? p.fin : acc_cond::mark_t({});
1439  });
1440  }
1441 
1442  acc_cond::mark_t fins_alone() const
1443  {
1444  return do_view([&](const acc_cond::rs_pair& p)
1445  {
1446  return !visible(p.inf) && visible(p.fin) ? p.fin
1447  : acc_cond::mark_t({});
1448  });
1449  }
1450 
1451  acc_cond::mark_t infs_alone() const
1452  {
1453  return do_view([&](const acc_cond::rs_pair& p)
1454  {
1455  return !visible(p.fin) && visible(p.inf) ? p.inf
1456  : acc_cond::mark_t({});
1457  });
1458  }
1459 
1460  acc_cond::mark_t paired_with_fin(unsigned mark) const
1461  {
1462  acc_cond::mark_t res = {};
1463  for (const auto& p: pairs_)
1464  if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
1465  res |= p.inf;
1466  return res;
1467  }
1468 
1469  const rs_pairs& pairs() const
1470  {
1471  return pairs_;
1472  }
1473 
1474  private:
1475  template<typename filter>
1476  acc_cond::mark_t do_view(const filter& filt) const
1477  {
1478  acc_cond::mark_t res = {};
1479  for (const auto& p: pairs_)
1480  res |= filt(p);
1481  return res;
1482  }
1483 
1484  bool visible(const acc_cond::mark_t& v) const
1485  {
1486  return !!(view_marks_ & v);
1487  }
1488 
1489  const rs_pairs& pairs_;
1490  acc_cond::mark_t view_marks_;
1491  };
1492 
1493 
1494  SPOT_API
1495  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
1496 
1497  namespace internal
1498  {
1499  class SPOT_API mark_iterator
1500  {
1501  public:
1502  typedef unsigned value_type;
1503  typedef const value_type& reference;
1504  typedef const value_type* pointer;
1505  typedef std::ptrdiff_t difference_type;
1506  typedef std::forward_iterator_tag iterator_category;
1507 
1508  mark_iterator() noexcept
1509  : m_({})
1510  {
1511  }
1512 
1513  mark_iterator(acc_cond::mark_t m) noexcept
1514  : m_(m)
1515  {
1516  }
1517 
1518  bool operator==(mark_iterator m) const
1519  {
1520  return m_ == m.m_;
1521  }
1522 
1523  bool operator!=(mark_iterator m) const
1524  {
1525  return m_ != m.m_;
1526  }
1527 
1528  value_type operator*() const
1529  {
1530  SPOT_ASSERT(m_);
1531  return m_.min_set() - 1;
1532  }
1533 
1534  mark_iterator& operator++()
1535  {
1536  m_.clear(this->operator*());
1537  return *this;
1538  }
1539 
1540  mark_iterator operator++(int)
1541  {
1542  mark_iterator it = *this;
1543  ++(*this);
1544  return it;
1545  }
1546  private:
1547  acc_cond::mark_t m_;
1548  };
1549 
1550  class SPOT_API mark_container
1551  {
1552  public:
1554  : m_(m)
1555  {
1556  }
1557 
1558  mark_iterator begin() const
1559  {
1560  return {m_};
1561  }
1562  mark_iterator end() const
1563  {
1564  return {};
1565  }
1566  private:
1568  };
1569  }
1570 
1571  inline spot::internal::mark_container acc_cond::mark_t::sets() const
1572  {
1573  return {*this};
1574  }
1575 }
1576 
1577 namespace std
1578 {
1579  template<>
1580  struct hash<spot::acc_cond::mark_t>
1581  {
1582  size_t operator()(spot::acc_cond::mark_t m) const noexcept
1583  {
1584  return m.hash();
1585  }
1586  };
1587 }
static constexpr unsigned max_accsets()
The maximum number of acceptance sets supported by this implementation.
Definition: acc.hh:104
Definition: automata.hh:26
Definition: acc.hh:1499
Rabin/streett pairs used by is_rabin_like and is_streett_like.
Definition: acc.hh:1119
Definition: bitset.hh:37
Definition: bitset.hh:405
Definition: acc.hh:1415
Definition: acc.hh:47
Definition: acc.hh:368
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
(omega-Rational) Or
Definition: twa.hh:1692
acc_code()
Build an empty acceptance condition.
Definition: acc.hh:976
op
Operator types.
Definition: formula.hh:65
Definition: acc.hh:38
Definition: acc.hh:378
Definition: acc.hh:1550
(omega-Rational) And
Definition: acc.hh:55

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