spot  2.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
acc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
3 // Développement 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 <unordered_map>
24 #include <sstream>
25 #include <vector>
26 #include <spot/tl/defaultenv.hh>
27 #include <iostream>
28 
29 namespace spot
30 {
31  class SPOT_API acc_cond
32  {
33  public:
34  struct mark_t
35  {
36  typedef unsigned value_t;
37  value_t id;
38 
39  mark_t() = default;
40 
41  mark_t(value_t id) noexcept
42  : id(id)
43  {
44  }
45 
46  template<class iterator>
47  mark_t(const iterator& begin, const iterator& end) noexcept
48  {
49  id = 0U;
50  for (iterator i = begin; i != end; ++i)
51  set(*i);
52  }
53 
54  mark_t(std::initializer_list<unsigned> vals) noexcept
55  : mark_t(vals.begin(), vals.end())
56  {
57  }
58 
59  bool operator==(unsigned o) const
60  {
61  SPOT_ASSERT(o == 0U);
62  return id == o;
63  }
64 
65  bool operator!=(unsigned o) const
66  {
67  SPOT_ASSERT(o == 0U);
68  return id != o;
69  }
70 
71  bool operator==(mark_t o) const
72  {
73  return id == o.id;
74  }
75 
76  bool operator!=(mark_t o) const
77  {
78  return id != o.id;
79  }
80 
81  bool operator<(mark_t o) const
82  {
83  return id < o.id;
84  }
85 
86  bool operator<=(mark_t o) const
87  {
88  return id <= o.id;
89  }
90 
91  bool operator>(mark_t o) const
92  {
93  return id > o.id;
94  }
95 
96  bool operator>=(mark_t o) const
97  {
98  return id >= o.id;
99  }
100 
101  operator bool() const
102  {
103  return id != 0;
104  }
105 
106  bool has(unsigned u) const
107  {
108  return id & (1U << u);
109  }
110 
111  void set(unsigned u)
112  {
113  id |= (1U << u);
114  }
115 
116  void clear(unsigned u)
117  {
118  id &= ~(1U << u);
119  }
120 
121  mark_t& operator&=(mark_t r)
122  {
123  id &= r.id;
124  return *this;
125  }
126 
127  mark_t& operator|=(mark_t r)
128  {
129  id |= r.id;
130  return *this;
131  }
132 
133  mark_t& operator-=(mark_t r)
134  {
135  id &= ~r.id;
136  return *this;
137  }
138 
139  mark_t& operator^=(mark_t r)
140  {
141  id ^= r.id;
142  return *this;
143  }
144 
145  mark_t operator&(mark_t r) const
146  {
147  return id & r.id;
148  }
149 
150  mark_t operator|(mark_t r) const
151  {
152  return id | r.id;
153  }
154 
155  mark_t operator-(mark_t r) const
156  {
157  return id & ~r.id;
158  }
159 
160  mark_t operator~() const
161  {
162  return ~id;
163  }
164 
165  mark_t operator^(mark_t r) const
166  {
167  return id ^ r.id;
168  }
169 
170  mark_t operator<<(unsigned i) const
171  {
172  return id << i;
173  }
174 
175  mark_t& operator<<=(unsigned i)
176  {
177  id <<= i;
178  return *this;
179  }
180 
181  mark_t operator>>(unsigned i) const
182  {
183  return id >> i;
184  }
185 
186  mark_t& operator>>=(unsigned i)
187  {
188  id >>= i;
189  return *this;
190  }
191 
192  mark_t strip(mark_t y) const
193  {
194  // strip every bit of id that is marked in y
195  // 100101110100.strip(
196  // 001011001000)
197  // == 10 1 11 100
198  // == 10111100
199 
200  auto xv = id; // 100101110100
201  auto yv = y.id; // 001011001000
202 
203  while (yv && xv)
204  {
205  // Mask for everything after the last 1 in y
206  auto rm = (~yv) & (yv - 1); // 000000000111
207  // Mask for everything before the last 1 in y
208  auto lm = ~(yv ^ (yv - 1)); // 111111110000
209  xv = ((xv & lm) >> 1) | (xv & rm);
210  yv = (yv & lm) >> 1;
211  }
212  return xv;
213  }
214 
215  // Number of bits sets.
216  unsigned count() const
217  {
218 #ifdef __GNUC__
219  return __builtin_popcount(id);
220 #else
221  unsigned c = 0U;
222  auto v = id;
223  while (v)
224  {
225  ++c;
226  v &= v - 1;
227  }
228  return c;
229 #endif
230  }
231 
232  // Return the number of the highest set used plus one.
233  // So if no set is used, this returns 0,
234  // but if the sets {1,3,8} are used, this returns 9.
235  unsigned max_set() const
236  {
237  auto i = id;
238  int res = 0;
239  while (i)
240  {
241  ++res;
242  i >>= 1;
243  }
244  return res;
245  }
246 
247  // Return the lowest acceptance mark
248  mark_t lowest() const
249  {
250  return id & -id;
251  }
252 
253  // Remove n bits that where set
254  mark_t& remove_some(unsigned n)
255  {
256  while (n--)
257  id &= id - 1;
258  return *this;
259  }
260 
261  template<class iterator>
262  void fill(iterator here) const
263  {
264  auto a = id;
265  unsigned level = 0;
266  while (a)
267  {
268  if (a & 1)
269  *here++ = level;
270  ++level;
271  a >>= 1;
272  }
273  }
274 
275  // FIXME: Return some iterable object without building a vector.
276  std::vector<unsigned> sets() const
277  {
278  std::vector<unsigned> res;
279  fill(std::back_inserter(res));
280  return res;
281  }
282 
283  SPOT_API
284  friend std::ostream& operator<<(std::ostream& os, mark_t m);
285  };
286 
287  // This encodes either an operator or set of acceptance sets.
288  enum class acc_op : unsigned short
289  { Inf, Fin, InfNeg, FinNeg, And, Or };
290  union acc_word
291  {
292  mark_t mark;
293  struct {
294  acc_op op; // Operator
295  unsigned short size; // Size of the subtree (number of acc_word),
296  // not counting this node.
297  };
298  };
299 
300  struct SPOT_API acc_code: public std::vector<acc_word>
301  {
302  bool operator==(const acc_code& other) const
303  {
304  unsigned pos = size();
305  if (other.size() != pos)
306  return false;
307  while (pos > 0)
308  {
309  auto op = (*this)[pos - 1].op;
310  auto sz = (*this)[pos - 1].size;
311  if (other[pos - 1].op != op ||
312  other[pos - 1].size != sz)
313  return false;
314  switch (op)
315  {
316  case acc_cond::acc_op::And:
317  case acc_cond::acc_op::Or:
318  --pos;
319  break;
320  case acc_cond::acc_op::Inf:
321  case acc_cond::acc_op::InfNeg:
322  case acc_cond::acc_op::Fin:
323  case acc_cond::acc_op::FinNeg:
324  pos -= 2;
325  if (other[pos].mark != (*this)[pos].mark)
326  return false;
327  break;
328  }
329  }
330  return true;
331  };
332 
333  bool operator<(const acc_code& other) const
334  {
335  unsigned pos = size();
336  auto osize = other.size();
337  if (pos < osize)
338  return true;
339  if (pos > osize)
340  return false;
341  while (pos > 0)
342  {
343  auto op = (*this)[pos - 1].op;
344  auto oop = other[pos - 1].op;
345  if (op < oop)
346  return true;
347  if (op > oop)
348  return false;
349  auto sz = (*this)[pos - 1].size;
350  auto osz = other[pos - 1].size;
351  if (sz < osz)
352  return true;
353  if (sz > osz)
354  return false;
355  switch (op)
356  {
357  case acc_cond::acc_op::And:
358  case acc_cond::acc_op::Or:
359  --pos;
360  break;
361  case acc_cond::acc_op::Inf:
362  case acc_cond::acc_op::InfNeg:
363  case acc_cond::acc_op::Fin:
364  case acc_cond::acc_op::FinNeg:
365  pos -= 2;
366  auto m = (*this)[pos].mark;
367  auto om = other[pos].mark;
368  if (m < om)
369  return true;
370  if (m > om)
371  return false;
372  break;
373  }
374  }
375  return false;
376  }
377 
378  bool operator>(const acc_code& other) const
379  {
380  return other < *this;
381  }
382 
383  bool operator<=(const acc_code& other) const
384  {
385  return !(other < *this);
386  }
387 
388  bool operator>=(const acc_code& other) const
389  {
390  return !(*this < other);
391  }
392 
393  bool operator!=(const acc_code& other) const
394  {
395  return !(*this == other);
396  }
397 
398  bool is_t() const
399  {
400  unsigned s = size();
401  return s == 0
402  || ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U);
403  }
404 
405  bool is_f() const
406  {
407  unsigned s = size();
408  return s > 1
409  && (*this)[s - 1].op == acc_op::Fin && (*this)[s - 2].mark == 0U;
410  }
411 
412  static acc_code f()
413  {
414  acc_code res;
415  res.resize(2);
416  res[0].mark = 0U;
417  res[1].op = acc_op::Fin;
418  res[1].size = 1;
419  return res;
420  }
421 
422  static acc_code t()
423  {
424  return {};
425  }
426 
427  static acc_code fin(mark_t m)
428  {
429  acc_code res;
430  res.resize(2);
431  res[0].mark = m;
432  res[1].op = acc_op::Fin;
433  res[1].size = 1;
434  return res;
435  }
436 
437  static acc_code fin(std::initializer_list<unsigned> vals)
438  {
439  return fin(mark_t(vals));
440  }
441 
442  static acc_code fin_neg(mark_t m)
443  {
444  acc_code res;
445  res.resize(2);
446  res[0].mark = m;
447  res[1].op = acc_op::FinNeg;
448  res[1].size = 1;
449  return res;
450  }
451 
452  static acc_code fin_neg(std::initializer_list<unsigned> vals)
453  {
454  return fin_neg(mark_t(vals));
455  }
456 
457  static acc_code inf(mark_t m)
458  {
459  acc_code res;
460  res.resize(2);
461  res[0].mark = m;
462  res[1].op = acc_op::Inf;
463  res[1].size = 1;
464  return res;
465  }
466 
467  static acc_code inf(std::initializer_list<unsigned> vals)
468  {
469  return inf(mark_t(vals));
470  }
471 
472  static acc_code inf_neg(mark_t m)
473  {
474  acc_code res;
475  res.resize(2);
476  res[0].mark = m;
477  res[1].op = acc_op::InfNeg;
478  res[1].size = 1;
479  return res;
480  }
481 
482  static acc_code inf_neg(std::initializer_list<unsigned> vals)
483  {
484  return inf_neg(mark_t(vals));
485  }
486 
487  static acc_code buchi()
488  {
489  return inf({0});
490  }
491 
492  static acc_code cobuchi()
493  {
494  return fin({0});
495  }
496 
497  static acc_code generalized_buchi(unsigned n)
498  {
499  acc_cond::mark_t m = (1U << n) - 1;
500  if (n == 8 * sizeof(mark_t::value_t))
501  m = mark_t(-1U);
502  return inf(m);
503  }
504 
505  static acc_code generalized_co_buchi(unsigned n)
506  {
507  acc_cond::mark_t m = (1U << n) - 1;
508  if (n == 8 * sizeof(mark_t::value_t))
509  m = mark_t(-1U);
510  return fin(m);
511  }
512 
513  // n is a number of pairs.
514  static acc_code rabin(unsigned n)
515  {
516  acc_cond::acc_code res = f();
517  while (n > 0)
518  {
519  res |= inf({2*n - 1}) & fin({2*n - 2});
520  --n;
521  }
522  return res;
523  }
524 
525  // n is a number of pairs.
526  static acc_code streett(unsigned n)
527  {
528  acc_cond::acc_code res = t();
529  while (n > 0)
530  {
531  res &= inf({2*n - 1}) | fin({2*n - 2});
532  --n;
533  }
534  return res;
535  }
536 
537  template<class Iterator>
538  static acc_code generalized_rabin(Iterator begin, Iterator end)
539  {
540  acc_cond::acc_code res = f();
541  unsigned n = 0;
542  for (Iterator i = begin; i != end; ++i)
543  {
544  acc_cond::acc_code pair = fin({n++});
545  acc_cond::mark_t m = 0U;
546  for (unsigned ni = *i; ni > 0; --ni)
547  m.set(n++);
548  pair &= inf(m);
549  std::swap(pair, res);
550  res |= std::move(pair);
551  }
552  return res;
553  }
554 
555  static acc_code parity(bool max, bool odd, unsigned sets);
556 
557  // Number of acceptance sets to use, and probability to reuse
558  // each set another time after it has been used in the
559  // acceptance formula.
560  static acc_code random(unsigned n, double reuse = 0.0);
561 
562  acc_code& operator&=(acc_code&& r)
563  {
564  if (is_t() || r.is_f())
565  {
566  *this = std::move(r);
567  return *this;
568  }
569  if (is_f() || r.is_t())
570  return *this;
571  unsigned s = size() - 1;
572  unsigned rs = r.size() - 1;
573  // We want to group all Inf(x) operators:
574  // Inf(a) & Inf(b) = Inf(a & b)
575  if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf)
576  || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg))
577  {
578  (*this)[s - 1].mark |= r[rs - 1].mark;
579  return *this;
580  }
581 
582  // In the more complex scenarios, left and right may both
583  // be conjunctions, and Inf(x) might be a member of each
584  // side. Find it if it exists.
585  // left_inf points to the left Inf mark if any.
586  // right_inf points to the right Inf mark if any.
587  acc_word* left_inf = nullptr;
588  if ((*this)[s].op == acc_op::And)
589  {
590  auto start = &(*this)[s] - (*this)[s].size;
591  auto pos = &(*this)[s] - 1;
592  pop_back();
593  while (pos > start)
594  {
595  if (pos->op == acc_op::Inf)
596  {
597  left_inf = pos - 1;
598  break;
599  }
600  pos -= pos->size + 1;
601  }
602  }
603  else if ((*this)[s].op == acc_op::Inf)
604  {
605  left_inf = &(*this)[s - 1];
606  }
607 
608  acc_word* right_inf = nullptr;
609  auto right_end = &r.back();
610  if (right_end->op == acc_op::And)
611  {
612  auto start = &r[0];
613  auto pos = --right_end;
614  while (pos > start)
615  {
616  if (pos->op == acc_op::Inf)
617  {
618  right_inf = pos - 1;
619  break;
620  }
621  pos -= pos->size + 1;
622  }
623  }
624  else if (right_end->op == acc_op::Inf)
625  {
626  right_inf = right_end - 1;
627  }
628 
629  if (left_inf && right_inf)
630  {
631  left_inf->mark |= right_inf->mark;
632  insert(this->end(), &r[0], right_inf);
633  insert(this->end(), right_inf + 2, right_end + 1);
634  }
635  else if (right_inf)
636  {
637  // Always insert Inf() at the very first entry.
638  insert(this->begin(), right_inf, right_inf + 2);
639  insert(this->end(), &r[0], right_inf);
640  insert(this->end(), right_inf + 2, right_end + 1);
641  }
642  else
643  {
644  insert(this->end(), &r[0], right_end + 1);
645  }
646 
647  acc_word w;
648  w.op = acc_op::And;
649  w.size = size();
650  emplace_back(w);
651  return *this;
652  }
653 
654  acc_code& operator&=(const acc_code& r)
655  {
656  if (is_t() || r.is_f())
657  {
658  *this = r;
659  return *this;
660  }
661  if (is_f() || r.is_t())
662  return *this;
663  unsigned s = size() - 1;
664  unsigned rs = r.size() - 1;
665  // Inf(a) & Inf(b) = Inf(a & b)
666  if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf)
667  || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg))
668  {
669  (*this)[s - 1].mark |= r[rs - 1].mark;
670  return *this;
671  }
672 
673  // In the more complex scenarios, left and right may both
674  // be conjunctions, and Inf(x) might be a member of each
675  // side. Find it if it exists.
676  // left_inf points to the left Inf mark if any.
677  // right_inf points to the right Inf mark if any.
678  acc_word* left_inf = nullptr;
679  if ((*this)[s].op == acc_op::And)
680  {
681  auto start = &(*this)[s] - (*this)[s].size;
682  auto pos = &(*this)[s] - 1;
683  pop_back();
684  while (pos > start)
685  {
686  if (pos->op == acc_op::Inf)
687  {
688  left_inf = pos - 1;
689  break;
690  }
691  pos -= pos->size + 1;
692  }
693  }
694  else if ((*this)[s].op == acc_op::Inf)
695  {
696  left_inf = &(*this)[s - 1];
697  }
698 
699  const acc_word* right_inf = nullptr;
700  auto right_end = &r.back();
701  if (right_end->op == acc_op::And)
702  {
703  auto start = &r[0];
704  auto pos = --right_end;
705  while (pos > start)
706  {
707  if (pos->op == acc_op::Inf)
708  {
709  right_inf = pos - 1;
710  break;
711  }
712  pos -= pos->size + 1;
713  }
714  }
715  else if (right_end->op == acc_op::Inf)
716  {
717  right_inf = right_end - 1;
718  }
719 
720  if (left_inf && right_inf)
721  {
722  left_inf->mark |= right_inf->mark;
723  insert(this->end(), &r[0], right_inf);
724  insert(this->end(), right_inf + 2, right_end + 1);
725  }
726  else if (right_inf)
727  {
728  // Always insert Inf() at the very first entry.
729  insert(this->begin(), right_inf, right_inf + 2);
730  insert(this->end(), &r[0], right_inf);
731  insert(this->end(), right_inf + 2, right_end + 1);
732  }
733  else
734  {
735  insert(this->end(), &r[0], right_end + 1);
736  }
737 
738  acc_word w;
739  w.op = acc_op::And;
740  w.size = size();
741  emplace_back(w);
742  return *this;
743  }
744 
745  acc_code operator&(acc_code&& r)
746  {
747  acc_code res = *this;
748  res &= r;
749  return res;
750  }
751 
752  acc_code operator&(const acc_code& r)
753  {
754  acc_code res = *this;
755  res &= r;
756  return res;
757  }
758 
759  acc_code& operator|=(acc_code&& r)
760  {
761  if (is_t() || r.is_f())
762  return *this;
763  if (is_f() || r.is_t())
764  {
765  *this = std::move(r);
766  return *this;
767  }
768  unsigned s = size() - 1;
769  unsigned rs = r.size() - 1;
770  // Fin(a) | Fin(b) = Fin(a | b)
771  if (((*this)[s].op == acc_op::Fin && r[rs].op == acc_op::Fin)
772  || ((*this)[s].op == acc_op::FinNeg && r[rs].op == acc_op::FinNeg))
773  {
774  (*this)[s - 1].mark |= r[rs - 1].mark;
775  return *this;
776  }
777  if ((*this)[s].op == acc_op::Or)
778  pop_back();
779  if (r.back().op == acc_op::Or)
780  r.pop_back();
781  insert(this->end(), r.begin(), r.end());
782  acc_word w;
783  w.op = acc_op::Or;
784  w.size = size();
785  emplace_back(w);
786  return *this;
787  }
788 
789  acc_code& operator|=(const acc_code& r)
790  {
791  return *this |= acc_code(r);
792  }
793 
794  acc_code operator|(acc_code&& r)
795  {
796  acc_code res = *this;
797  res |= r;
798  return res;
799  }
800 
801  acc_code operator|(const acc_code& r)
802  {
803  acc_code res = *this;
804  res |= r;
805  return res;
806  }
807 
808  acc_code& operator<<=(unsigned sets)
809  {
810  if (empty())
811  return *this;
812  unsigned pos = size();
813  do
814  {
815  switch ((*this)[pos - 1].op)
816  {
817  case acc_cond::acc_op::And:
818  case acc_cond::acc_op::Or:
819  --pos;
820  break;
821  case acc_cond::acc_op::Inf:
822  case acc_cond::acc_op::InfNeg:
823  case acc_cond::acc_op::Fin:
824  case acc_cond::acc_op::FinNeg:
825  pos -= 2;
826  (*this)[pos].mark.id <<= sets;
827  break;
828  }
829  }
830  while (pos > 0);
831  return *this;
832  }
833 
834  acc_code operator<<(unsigned sets) const
835  {
836  acc_code res = *this;
837  res <<= sets;
838  return res;
839  }
840 
841  bool is_dnf() const;
842  bool is_cnf() const;
843 
844  acc_code to_dnf() const;
845  acc_code to_cnf() const;
846 
847  acc_code complement() const;
848 
849  // Return a list of acceptance marks needed to close a cycle
850  // that already visit INF infinitely often, so that the cycle is
851  // accepting (ACCEPTING=true) or rejecting (ACCEPTING=false).
852  // Positive values describe positive set.
853  // A negative value x means the set -x-1 must be absent.
854  std::vector<std::vector<int>>
855  missing(mark_t inf, bool accepting) const;
856 
857  bool accepting(mark_t inf) const;
858 
859  bool inf_satisfiable(mark_t inf) const;
860 
861  // Remove all the acceptance sets in rem.
862  //
863  // If MISSING is set, the acceptance sets are assumed to be
864  // missing from the automaton, and the acceptance is updated to
865  // reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will
866  // become Fin(3) if we remove 2 because it is missing from this
867  // automaton, because there is no way to fulfill Inf(1)&Inf(2)
868  // in this case. So essentially MISSING causes Inf(rem) to
869  // become f, and Fin(rem) to become t.
870  //
871  // If MISSING is unset, Inf(rem) become t while Fin(rem) become
872  // f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
873  // Inf(1)|Fin(3).
874  acc_code strip(acc_cond::mark_t rem, bool missing) const;
875 
876  // Return the set of sets appearing in the condition.
877  acc_cond::mark_t used_sets() const;
878 
879  // Return the sets used as Inf or Fin in the acceptance condition
880  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
881 
882  // Print the acceptance as HTML. The set_printer function can
883  // be used to implement customized output for set numbers.
884  std::ostream&
885  to_html(std::ostream& os,
886  std::function<void(std::ostream&, int)>
887  set_printer = nullptr) const;
888 
889  // Print the acceptance as text. The set_printer function can
890  // be used to implement customized output for set numbers.
891  std::ostream&
892  to_text(std::ostream& os,
893  std::function<void(std::ostream&, int)>
894  set_printer = nullptr) const;
895 
896 
919  acc_code(const char* input);
920 
925  {
926  }
927 
928  // Calls to_text
929  SPOT_API
930  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
931  };
932 
933  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
934  : num_(0U), all_(0U), code_(code)
935  {
936  add_sets(n_sets);
937  uses_fin_acceptance_ = check_fin_acceptance();
938  }
939 
940  acc_cond(const acc_code& code)
941  : num_(0U), all_(0U), code_(code)
942  {
943  add_sets(code.used_sets().max_set());
944  uses_fin_acceptance_ = check_fin_acceptance();
945  }
946 
947  acc_cond(const acc_cond& o)
948  : num_(o.num_), all_(o.all_), code_(o.code_),
949  uses_fin_acceptance_(o.uses_fin_acceptance_)
950  {
951  }
952 
953  acc_cond& operator=(const acc_cond& o)
954  {
955  num_ = o.num_;
956  all_ = o.all_;
957  code_ = o.code_;
958  uses_fin_acceptance_ = o.uses_fin_acceptance_;
959  return *this;
960  }
961 
962  ~acc_cond()
963  {
964  }
965 
966  void set_acceptance(const acc_code& code)
967  {
968  code_ = code;
969  uses_fin_acceptance_ = check_fin_acceptance();
970  }
971 
972  const acc_code& get_acceptance() const
973  {
974  return code_;
975  }
976 
977  acc_code& get_acceptance()
978  {
979  return code_;
980  }
981 
982  bool uses_fin_acceptance() const
983  {
984  return uses_fin_acceptance_;
985  }
986 
987  bool is_t() const
988  {
989  return code_.is_t();
990  }
991 
992  bool is_all() const
993  {
994  return num_ == 0 && is_t();
995  }
996 
997  bool is_f() const
998  {
999  return code_.is_f();
1000  }
1001 
1002  bool is_none() const
1003  {
1004  return num_ == 0 && is_f();
1005  }
1006 
1007  bool is_buchi() const
1008  {
1009  unsigned s = code_.size();
1010  return num_ == 1 &&
1011  s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets();
1012  }
1013 
1014  bool is_co_buchi() const
1015  {
1016  return num_ == 1 && is_generalized_co_buchi();
1017  }
1018 
1019  void set_generalized_buchi()
1020  {
1021  set_acceptance(inf(all_sets()));
1022  }
1023 
1024  bool is_generalized_buchi() const
1025  {
1026  unsigned s = code_.size();
1027  return (s == 0 && num_ == 0) ||
1028  (s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets());
1029  }
1030 
1031  bool is_generalized_co_buchi() const
1032  {
1033  unsigned s = code_.size();
1034  return (s == 2 &&
1035  code_[1].op == acc_op::Fin && code_[0].mark == all_sets());
1036  }
1037 
1038  // Returns a number of pairs (>=0) if Rabin, or -1 else.
1039  int is_rabin() const;
1040  // Returns a number of pairs (>=0) if Streett, or -1 else.
1041  int is_streett() const;
1042 
1043  // Return the number of Inf in each pair.
1044  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1045 
1046  // If EQUIV is false, this return true iff the acceptance
1047  // condition is a parity condition written in the canonical way
1048  // given in the HOA specifications. If EQUIV is true, then we
1049  // check whether the condition is logically equivalent to some
1050  // parity acceptance condition.
1051  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1052  bool is_parity() const
1053  {
1054  bool max;
1055  bool min;
1056  return is_parity(max, min);
1057  }
1058 
1059  // Return (true, m) if there exist some acceptance mark m that
1060  // does not satisfy the acceptance condition. Return (false, 0U)
1061  // otherwise.
1062  std::pair<bool, acc_cond::mark_t> unsat_mark() const;
1063 
1064  protected:
1065  bool check_fin_acceptance() const;
1066 
1067  public:
1068  static acc_code inf(mark_t mark)
1069  {
1070  return acc_code::inf(mark);
1071  }
1072 
1073  static acc_code inf(std::initializer_list<unsigned> vals)
1074  {
1075  return inf(mark_t(vals.begin(), vals.end()));
1076  }
1077 
1078  static acc_code inf_neg(mark_t mark)
1079  {
1080  return acc_code::inf_neg(mark);
1081  }
1082 
1083  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1084  {
1085  return inf_neg(mark_t(vals.begin(), vals.end()));
1086  }
1087 
1088  static acc_code fin(mark_t mark)
1089  {
1090  return acc_code::fin(mark);
1091  }
1092 
1093  static acc_code fin(std::initializer_list<unsigned> vals)
1094  {
1095  return fin(mark_t(vals.begin(), vals.end()));
1096  }
1097 
1098  static acc_code fin_neg(mark_t mark)
1099  {
1100  return acc_code::fin_neg(mark);
1101  }
1102 
1103  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1104  {
1105  return fin_neg(mark_t(vals.begin(), vals.end()));
1106  }
1107 
1108  unsigned add_sets(unsigned num)
1109  {
1110  if (num == 0)
1111  return -1U;
1112  unsigned j = num_;
1113  num_ += num;
1114  if (num_ > 8 * sizeof(mark_t::id))
1115  throw std::runtime_error("Too many acceptance sets used.");
1116  all_ = all_sets_();
1117  return j;
1118  }
1119 
1120  unsigned add_set()
1121  {
1122  return add_sets(1);
1123  }
1124 
1125  mark_t mark(unsigned u) const
1126  {
1127  SPOT_ASSERT(u < num_sets());
1128  return 1U << u;
1129  }
1130 
1131  mark_t comp(mark_t l) const
1132  {
1133  return all_ ^ l.id;
1134  }
1135 
1136  mark_t all_sets() const
1137  {
1138  return all_;
1139  }
1140 
1141  bool accepting(mark_t inf) const
1142  {
1143  return code_.accepting(inf);
1144  }
1145 
1146  bool inf_satisfiable(mark_t inf) const
1147  {
1148  return code_.inf_satisfiable(inf);
1149  }
1150 
1151  mark_t accepting_sets(mark_t inf) const;
1152 
1153  std::ostream& format(std::ostream& os, mark_t m) const
1154  {
1155  auto a = m;
1156  if (a == 0U)
1157  return os;
1158  return os << m;
1159  }
1160 
1161  std::string format(mark_t m) const
1162  {
1163  std::ostringstream os;
1164  format(os, m);
1165  return os.str();
1166  }
1167 
1168  unsigned num_sets() const
1169  {
1170  return num_;
1171  }
1172 
1173  template<class iterator>
1174  mark_t useless(iterator begin, iterator end) const
1175  {
1176  mark_t::value_t u = 0U; // The set of useless marks.
1177  for (unsigned x = 0; x < num_; ++x)
1178  {
1179  // Skip marks that are already known to be useless.
1180  if (u & (1 << x))
1181  continue;
1182  unsigned all = all_ ^ (u | (1 << x));
1183  for (iterator y = begin; y != end; ++y)
1184  {
1185  auto v = y->id;
1186  if (v & (1 << x))
1187  {
1188  all &= v;
1189  if (!all)
1190  break;
1191  }
1192  }
1193  u |= all;
1194  }
1195  return u;
1196  }
1197 
1198  protected:
1199  mark_t::value_t all_sets_() const
1200  {
1201  if (num_ == 0)
1202  return 0;
1203  return -1U >> (8 * sizeof(mark_t::value_t) - num_);
1204  }
1205 
1206  unsigned num_;
1207  mark_t::value_t all_;
1208  acc_code code_;
1209  bool uses_fin_acceptance_ = false;
1210 
1211  };
1212 
1213  SPOT_API
1214  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
1215 }
1216 
1217 namespace std
1218 {
1219  template<>
1220  struct hash<spot::acc_cond::mark_t>
1221  {
1222  size_t operator()(spot::acc_cond::mark_t m) const
1223  {
1224  std::hash<decltype(m.id)> h;
1225  return h(m.id);
1226  }
1227  };
1228 }
Definition: graph.hh:33
Definition: formula.hh:1671
Definition: acc.hh:31
Definition: acc.hh:290
(omega-Rational) Or
acc_code()
Build an empty acceptance condition.
Definition: acc.hh:924
op
Operator types.
Definition: formula.hh:62
Definition: acc.hh:300
(omega-Rational) And
Definition: acc.hh:34

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Thu Jan 19 2017 11:08:40 for spot by doxygen 1.8.8