spot  2.3.3
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
acc.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014, 2015, 2016, 2017 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  } sub;
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].sub.op;
310  auto sz = (*this)[pos - 1].sub.size;
311  if (other[pos - 1].sub.op != op ||
312  other[pos - 1].sub.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].sub.op;
344  auto oop = other[pos - 1].sub.op;
345  if (op < oop)
346  return true;
347  if (op > oop)
348  return false;
349  auto sz = (*this)[pos - 1].sub.size;
350  auto osz = other[pos - 1].sub.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 || ((*this)[s - 1].sub.op == acc_op::Inf
402  && (*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].sub.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].sub.op = acc_op::Fin;
418  res[1].sub.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].sub.op = acc_op::Fin;
433  res[1].sub.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].sub.op = acc_op::FinNeg;
448  res[1].sub.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].sub.op = acc_op::Inf;
463  res[1].sub.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].sub.op = acc_op::InfNeg;
478  res[1].sub.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].sub.op == acc_op::Inf
576  && r[rs].sub.op == acc_op::Inf)
577  || ((*this)[s].sub.op == acc_op::InfNeg
578  && r[rs].sub.op == acc_op::InfNeg))
579  {
580  (*this)[s - 1].mark |= r[rs - 1].mark;
581  return *this;
582  }
583 
584  // In the more complex scenarios, left and right may both
585  // be conjunctions, and Inf(x) might be a member of each
586  // side. Find it if it exists.
587  // left_inf points to the left Inf mark if any.
588  // right_inf points to the right Inf mark if any.
589  acc_word* left_inf = nullptr;
590  if ((*this)[s].sub.op == acc_op::And)
591  {
592  auto start = &(*this)[s] - (*this)[s].sub.size;
593  auto pos = &(*this)[s] - 1;
594  pop_back();
595  while (pos > start)
596  {
597  if (pos->sub.op == acc_op::Inf)
598  {
599  left_inf = pos - 1;
600  break;
601  }
602  pos -= pos->sub.size + 1;
603  }
604  }
605  else if ((*this)[s].sub.op == acc_op::Inf)
606  {
607  left_inf = &(*this)[s - 1];
608  }
609 
610  acc_word* right_inf = nullptr;
611  auto right_end = &r.back();
612  if (right_end->sub.op == acc_op::And)
613  {
614  auto start = &r[0];
615  auto pos = --right_end;
616  while (pos > start)
617  {
618  if (pos->sub.op == acc_op::Inf)
619  {
620  right_inf = pos - 1;
621  break;
622  }
623  pos -= pos->sub.size + 1;
624  }
625  }
626  else if (right_end->sub.op == acc_op::Inf)
627  {
628  right_inf = right_end - 1;
629  }
630 
631  if (left_inf && right_inf)
632  {
633  left_inf->mark |= right_inf->mark;
634  insert(this->end(), &r[0], right_inf);
635  insert(this->end(), right_inf + 2, right_end + 1);
636  }
637  else if (right_inf)
638  {
639  // Always insert Inf() at the very first entry.
640  insert(this->begin(), right_inf, right_inf + 2);
641  insert(this->end(), &r[0], right_inf);
642  insert(this->end(), right_inf + 2, right_end + 1);
643  }
644  else
645  {
646  insert(this->end(), &r[0], right_end + 1);
647  }
648 
649  acc_word w;
650  w.sub.op = acc_op::And;
651  w.sub.size = size();
652  emplace_back(w);
653  return *this;
654  }
655 
656  acc_code& operator&=(const acc_code& r)
657  {
658  if (is_t() || r.is_f())
659  {
660  *this = r;
661  return *this;
662  }
663  if (is_f() || r.is_t())
664  return *this;
665  unsigned s = size() - 1;
666  unsigned rs = r.size() - 1;
667  // Inf(a) & Inf(b) = Inf(a & b)
668  if (((*this)[s].sub.op == acc_op::Inf
669  && r[rs].sub.op == acc_op::Inf)
670  || ((*this)[s].sub.op == acc_op::InfNeg
671  && r[rs].sub.op == acc_op::InfNeg))
672  {
673  (*this)[s - 1].mark |= r[rs - 1].mark;
674  return *this;
675  }
676 
677  // In the more complex scenarios, left and right may both
678  // be conjunctions, and Inf(x) might be a member of each
679  // side. Find it if it exists.
680  // left_inf points to the left Inf mark if any.
681  // right_inf points to the right Inf mark if any.
682  acc_word* left_inf = nullptr;
683  if ((*this)[s].sub.op == acc_op::And)
684  {
685  auto start = &(*this)[s] - (*this)[s].sub.size;
686  auto pos = &(*this)[s] - 1;
687  pop_back();
688  while (pos > start)
689  {
690  if (pos->sub.op == acc_op::Inf)
691  {
692  left_inf = pos - 1;
693  break;
694  }
695  pos -= pos->sub.size + 1;
696  }
697  }
698  else if ((*this)[s].sub.op == acc_op::Inf)
699  {
700  left_inf = &(*this)[s - 1];
701  }
702 
703  const acc_word* right_inf = nullptr;
704  auto right_end = &r.back();
705  if (right_end->sub.op == acc_op::And)
706  {
707  auto start = &r[0];
708  auto pos = --right_end;
709  while (pos > start)
710  {
711  if (pos->sub.op == acc_op::Inf)
712  {
713  right_inf = pos - 1;
714  break;
715  }
716  pos -= pos->sub.size + 1;
717  }
718  }
719  else if (right_end->sub.op == acc_op::Inf)
720  {
721  right_inf = right_end - 1;
722  }
723 
724  if (left_inf && right_inf)
725  {
726  left_inf->mark |= right_inf->mark;
727  insert(this->end(), &r[0], right_inf);
728  insert(this->end(), right_inf + 2, right_end + 1);
729  }
730  else if (right_inf)
731  {
732  // Always insert Inf() at the very first entry.
733  insert(this->begin(), right_inf, right_inf + 2);
734  insert(this->end(), &r[0], right_inf);
735  insert(this->end(), right_inf + 2, right_end + 1);
736  }
737  else
738  {
739  insert(this->end(), &r[0], right_end + 1);
740  }
741 
742  acc_word w;
743  w.sub.op = acc_op::And;
744  w.sub.size = size();
745  emplace_back(w);
746  return *this;
747  }
748 
749  acc_code operator&(acc_code&& r)
750  {
751  acc_code res = *this;
752  res &= r;
753  return res;
754  }
755 
756  acc_code operator&(const acc_code& r)
757  {
758  acc_code res = *this;
759  res &= r;
760  return res;
761  }
762 
763  acc_code& operator|=(acc_code&& r)
764  {
765  if (is_t() || r.is_f())
766  return *this;
767  if (is_f() || r.is_t())
768  {
769  *this = std::move(r);
770  return *this;
771  }
772  unsigned s = size() - 1;
773  unsigned rs = r.size() - 1;
774  // Fin(a) | Fin(b) = Fin(a | b)
775  if (((*this)[s].sub.op == acc_op::Fin
776  && r[rs].sub.op == acc_op::Fin)
777  || ((*this)[s].sub.op == acc_op::FinNeg
778  && r[rs].sub.op == acc_op::FinNeg))
779  {
780  (*this)[s - 1].mark |= r[rs - 1].mark;
781  return *this;
782  }
783  if ((*this)[s].sub.op == acc_op::Or)
784  pop_back();
785  if (r.back().sub.op == acc_op::Or)
786  r.pop_back();
787  insert(this->end(), r.begin(), r.end());
788  acc_word w;
789  w.sub.op = acc_op::Or;
790  w.sub.size = size();
791  emplace_back(w);
792  return *this;
793  }
794 
795  acc_code& operator|=(const acc_code& r)
796  {
797  return *this |= acc_code(r);
798  }
799 
800  acc_code operator|(acc_code&& r)
801  {
802  acc_code res = *this;
803  res |= r;
804  return res;
805  }
806 
807  acc_code operator|(const acc_code& r)
808  {
809  acc_code res = *this;
810  res |= r;
811  return res;
812  }
813 
814  acc_code& operator<<=(unsigned sets)
815  {
816  if (empty())
817  return *this;
818  unsigned pos = size();
819  do
820  {
821  switch ((*this)[pos - 1].sub.op)
822  {
823  case acc_cond::acc_op::And:
824  case acc_cond::acc_op::Or:
825  --pos;
826  break;
827  case acc_cond::acc_op::Inf:
828  case acc_cond::acc_op::InfNeg:
829  case acc_cond::acc_op::Fin:
830  case acc_cond::acc_op::FinNeg:
831  pos -= 2;
832  (*this)[pos].mark.id <<= sets;
833  break;
834  }
835  }
836  while (pos > 0);
837  return *this;
838  }
839 
840  acc_code operator<<(unsigned sets) const
841  {
842  acc_code res = *this;
843  res <<= sets;
844  return res;
845  }
846 
847  bool is_dnf() const;
848  bool is_cnf() const;
849 
850  acc_code to_dnf() const;
851  acc_code to_cnf() const;
852 
853  acc_code complement() const;
854 
855  // Return a list of acceptance marks needed to close a cycle
856  // that already visit INF infinitely often, so that the cycle is
857  // accepting (ACCEPTING=true) or rejecting (ACCEPTING=false).
858  // Positive values describe positive set.
859  // A negative value x means the set -x-1 must be absent.
860  std::vector<std::vector<int>>
861  missing(mark_t inf, bool accepting) const;
862 
863  bool accepting(mark_t inf) const;
864 
865  bool inf_satisfiable(mark_t inf) const;
866 
867  // Remove all the acceptance sets in rem.
868  //
869  // If MISSING is set, the acceptance sets are assumed to be
870  // missing from the automaton, and the acceptance is updated to
871  // reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will
872  // become Fin(3) if we remove 2 because it is missing from this
873  // automaton, because there is no way to fulfill Inf(1)&Inf(2)
874  // in this case. So essentially MISSING causes Inf(rem) to
875  // become f, and Fin(rem) to become t.
876  //
877  // If MISSING is unset, Inf(rem) become t while Fin(rem) become
878  // f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
879  // Inf(1)|Fin(3).
880  acc_code strip(acc_cond::mark_t rem, bool missing) const;
881 
882  // Return the set of sets appearing in the condition.
883  acc_cond::mark_t used_sets() const;
884 
885  // Return the sets used as Inf or Fin in the acceptance condition
886  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
887 
888  // Print the acceptance as HTML. The set_printer function can
889  // be used to implement customized output for set numbers.
890  std::ostream&
891  to_html(std::ostream& os,
892  std::function<void(std::ostream&, int)>
893  set_printer = nullptr) const;
894 
895  // Print the acceptance as text. The set_printer function can
896  // be used to implement customized output for set numbers.
897  std::ostream&
898  to_text(std::ostream& os,
899  std::function<void(std::ostream&, int)>
900  set_printer = nullptr) const;
901 
902 
925  acc_code(const char* input);
926 
931  {
932  }
933 
934  // Calls to_text
935  SPOT_API
936  friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
937  };
938 
939  acc_cond(unsigned n_sets = 0, const acc_code& code = {})
940  : num_(0U), all_(0U), code_(code)
941  {
942  add_sets(n_sets);
943  uses_fin_acceptance_ = check_fin_acceptance();
944  }
945 
946  acc_cond(const acc_code& code)
947  : num_(0U), all_(0U), code_(code)
948  {
949  add_sets(code.used_sets().max_set());
950  uses_fin_acceptance_ = check_fin_acceptance();
951  }
952 
953  acc_cond(const acc_cond& o)
954  : num_(o.num_), all_(o.all_), code_(o.code_),
955  uses_fin_acceptance_(o.uses_fin_acceptance_)
956  {
957  }
958 
959  acc_cond& operator=(const acc_cond& o)
960  {
961  num_ = o.num_;
962  all_ = o.all_;
963  code_ = o.code_;
964  uses_fin_acceptance_ = o.uses_fin_acceptance_;
965  return *this;
966  }
967 
968  ~acc_cond()
969  {
970  }
971 
972  void set_acceptance(const acc_code& code)
973  {
974  code_ = code;
975  uses_fin_acceptance_ = check_fin_acceptance();
976  }
977 
978  const acc_code& get_acceptance() const
979  {
980  return code_;
981  }
982 
983  acc_code& get_acceptance()
984  {
985  return code_;
986  }
987 
988  bool uses_fin_acceptance() const
989  {
990  return uses_fin_acceptance_;
991  }
992 
993  bool is_t() const
994  {
995  return code_.is_t();
996  }
997 
998  bool is_all() const
999  {
1000  return num_ == 0 && is_t();
1001  }
1002 
1003  bool is_f() const
1004  {
1005  return code_.is_f();
1006  }
1007 
1008  bool is_none() const
1009  {
1010  return num_ == 0 && is_f();
1011  }
1012 
1013  bool is_buchi() const
1014  {
1015  unsigned s = code_.size();
1016  return num_ == 1 &&
1017  s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1018  }
1019 
1020  bool is_co_buchi() const
1021  {
1022  return num_ == 1 && is_generalized_co_buchi();
1023  }
1024 
1025  void set_generalized_buchi()
1026  {
1027  set_acceptance(inf(all_sets()));
1028  }
1029 
1030  bool is_generalized_buchi() const
1031  {
1032  unsigned s = code_.size();
1033  return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
1034  && code_[0].mark == all_sets());
1035  }
1036 
1037  bool is_generalized_co_buchi() const
1038  {
1039  unsigned s = code_.size();
1040  return (s == 2 &&
1041  code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1042  }
1043 
1044  // Returns a number of pairs (>=0) if Rabin, or -1 else.
1045  int is_rabin() const;
1046  // Returns a number of pairs (>=0) if Streett, or -1 else.
1047  int is_streett() const;
1048 
1049  // Return the number of Inf in each pair.
1050  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1051 
1052  // If EQUIV is false, this return true iff the acceptance
1053  // condition is a parity condition written in the canonical way
1054  // given in the HOA specifications. If EQUIV is true, then we
1055  // check whether the condition is logically equivalent to some
1056  // parity acceptance condition.
1057  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1058  bool is_parity() const
1059  {
1060  bool max;
1061  bool min;
1062  return is_parity(max, min);
1063  }
1064 
1065  // Return (true, m) if there exist some acceptance mark m that
1066  // does not satisfy the acceptance condition. Return (false, 0U)
1067  // otherwise.
1068  std::pair<bool, acc_cond::mark_t> unsat_mark() const;
1069 
1070  protected:
1071  bool check_fin_acceptance() const;
1072 
1073  public:
1074  static acc_code inf(mark_t mark)
1075  {
1076  return acc_code::inf(mark);
1077  }
1078 
1079  static acc_code inf(std::initializer_list<unsigned> vals)
1080  {
1081  return inf(mark_t(vals.begin(), vals.end()));
1082  }
1083 
1084  static acc_code inf_neg(mark_t mark)
1085  {
1086  return acc_code::inf_neg(mark);
1087  }
1088 
1089  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1090  {
1091  return inf_neg(mark_t(vals.begin(), vals.end()));
1092  }
1093 
1094  static acc_code fin(mark_t mark)
1095  {
1096  return acc_code::fin(mark);
1097  }
1098 
1099  static acc_code fin(std::initializer_list<unsigned> vals)
1100  {
1101  return fin(mark_t(vals.begin(), vals.end()));
1102  }
1103 
1104  static acc_code fin_neg(mark_t mark)
1105  {
1106  return acc_code::fin_neg(mark);
1107  }
1108 
1109  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1110  {
1111  return fin_neg(mark_t(vals.begin(), vals.end()));
1112  }
1113 
1114  unsigned add_sets(unsigned num)
1115  {
1116  if (num == 0)
1117  return -1U;
1118  unsigned j = num_;
1119  num_ += num;
1120  if (num_ > 8 * sizeof(mark_t::id))
1121  throw std::runtime_error("Too many acceptance sets used.");
1122  all_ = all_sets_();
1123  return j;
1124  }
1125 
1126  unsigned add_set()
1127  {
1128  return add_sets(1);
1129  }
1130 
1131  mark_t mark(unsigned u) const
1132  {
1133  SPOT_ASSERT(u < num_sets());
1134  return 1U << u;
1135  }
1136 
1137  mark_t comp(mark_t l) const
1138  {
1139  return all_ ^ l.id;
1140  }
1141 
1142  mark_t all_sets() const
1143  {
1144  return all_;
1145  }
1146 
1147  bool accepting(mark_t inf) const
1148  {
1149  return code_.accepting(inf);
1150  }
1151 
1152  bool inf_satisfiable(mark_t inf) const
1153  {
1154  return code_.inf_satisfiable(inf);
1155  }
1156 
1157  mark_t accepting_sets(mark_t inf) const;
1158 
1159  std::ostream& format(std::ostream& os, mark_t m) const
1160  {
1161  auto a = m;
1162  if (a == 0U)
1163  return os;
1164  return os << m;
1165  }
1166 
1167  std::string format(mark_t m) const
1168  {
1169  std::ostringstream os;
1170  format(os, m);
1171  return os.str();
1172  }
1173 
1174  unsigned num_sets() const
1175  {
1176  return num_;
1177  }
1178 
1179  template<class iterator>
1180  mark_t useless(iterator begin, iterator end) const
1181  {
1182  mark_t::value_t u = 0U; // The set of useless marks.
1183  for (unsigned x = 0; x < num_; ++x)
1184  {
1185  // Skip marks that are already known to be useless.
1186  if (u & (1 << x))
1187  continue;
1188  unsigned all = all_ ^ (u | (1 << x));
1189  for (iterator y = begin; y != end; ++y)
1190  {
1191  auto v = y->id;
1192  if (v & (1 << x))
1193  {
1194  all &= v;
1195  if (!all)
1196  break;
1197  }
1198  }
1199  u |= all;
1200  }
1201  return u;
1202  }
1203 
1204  protected:
1205  mark_t::value_t all_sets_() const
1206  {
1207  if (num_ == 0)
1208  return 0;
1209  return -1U >> (8 * sizeof(mark_t::value_t) - num_);
1210  }
1211 
1212  unsigned num_;
1213  mark_t::value_t all_;
1214  acc_code code_;
1215  bool uses_fin_acceptance_ = false;
1216 
1217  };
1218 
1219  SPOT_API
1220  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
1221 }
1222 
1223 namespace std
1224 {
1225  template<>
1226  struct hash<spot::acc_cond::mark_t>
1227  {
1228  size_t operator()(spot::acc_cond::mark_t m) const
1229  {
1230  std::hash<decltype(m.id)> h;
1231  return h(m.id);
1232  }
1233  };
1234 }
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:930
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 Tue Apr 11 2017 13:40:03 for spot by doxygen 1.8.8