spot  2.4
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 <spot/misc/trival.hh>
28 #include <iostream>
29 
30 namespace spot
31 {
32  namespace internal
33  {
34  class mark_container;
35  }
36  class SPOT_API acc_cond
37  {
38  public:
39  struct mark_t
40  {
41  typedef unsigned value_t;
42  value_t id;
43 
44  mark_t() = default;
45 
46  mark_t(value_t id) noexcept
47  : id(id)
48  {
49  }
50 
51  template<class iterator>
52  mark_t(const iterator& begin, const iterator& end) noexcept
53  {
54  id = 0U;
55  for (iterator i = begin; i != end; ++i)
56  set(*i);
57  }
58 
59  mark_t(std::initializer_list<unsigned> vals) noexcept
60  : mark_t(vals.begin(), vals.end())
61  {
62  }
63 
64  bool operator==(unsigned o) const
65  {
66  SPOT_ASSERT(o == 0U);
67  return id == o;
68  }
69 
70  bool operator!=(unsigned o) const
71  {
72  SPOT_ASSERT(o == 0U);
73  return id != o;
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  bool operator>=(mark_t o) const
102  {
103  return id >= o.id;
104  }
105 
106  explicit operator bool() const
107  {
108  return id != 0;
109  }
110 
111  bool has(unsigned u) const
112  {
113  return id & (1U << u);
114  }
115 
116  void set(unsigned u)
117  {
118  id |= (1U << u);
119  }
120 
121  void clear(unsigned u)
122  {
123  id &= ~(1U << u);
124  }
125 
126  mark_t& operator&=(mark_t r)
127  {
128  id &= r.id;
129  return *this;
130  }
131 
132  mark_t& operator|=(mark_t r)
133  {
134  id |= r.id;
135  return *this;
136  }
137 
138  mark_t& operator-=(mark_t r)
139  {
140  id &= ~r.id;
141  return *this;
142  }
143 
144  mark_t& operator^=(mark_t r)
145  {
146  id ^= r.id;
147  return *this;
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-(mark_t r) const
161  {
162  return id & ~r.id;
163  }
164 
165  mark_t operator~() const
166  {
167  return ~id;
168  }
169 
170  mark_t operator^(mark_t r) const
171  {
172  return id ^ r.id;
173  }
174 
175  mark_t operator<<(unsigned i) const
176  {
177  return id << i;
178  }
179 
180  mark_t& operator<<=(unsigned i)
181  {
182  id <<= i;
183  return *this;
184  }
185 
186  mark_t operator>>(unsigned i) const
187  {
188  return id >> i;
189  }
190 
191  mark_t& operator>>=(unsigned i)
192  {
193  id >>= i;
194  return *this;
195  }
196 
197  mark_t strip(mark_t y) const
198  {
199  // strip every bit of id that is marked in y
200  // 100101110100.strip(
201  // 001011001000)
202  // == 10 1 11 100
203  // == 10111100
204 
205  auto xv = id; // 100101110100
206  auto yv = y.id; // 001011001000
207 
208  while (yv && xv)
209  {
210  // Mask for everything after the last 1 in y
211  auto rm = (~yv) & (yv - 1); // 000000000111
212  // Mask for everything before the last 1 in y
213  auto lm = ~(yv ^ (yv - 1)); // 111111110000
214  xv = ((xv & lm) >> 1) | (xv & rm);
215  yv = (yv & lm) >> 1;
216  }
217  return xv;
218  }
219 
220  bool subset(mark_t m) const
221  {
222  return this->strip(m) == 0U;
223  }
224 
225  bool proper_subset(mark_t m) const
226  {
227  return *this != m && this->subset(m);
228  }
229 
230  // Number of bits sets.
231  unsigned count() const
232  {
233 #ifdef __GNUC__
234  return __builtin_popcount(id);
235 #else
236  unsigned c = 0U;
237  auto v = id;
238  while (v)
239  {
240  ++c;
241  v &= v - 1;
242  }
243  return c;
244 #endif
245  }
246 
247  // Return the number of the highest set used plus one.
248  // If no set is used, this returns 0,
249  // If the sets {1,3,8} are used, this returns 9.
250  unsigned max_set() const
251  {
252 #ifdef __GNUC__
253  return (id == 0) ? 0 : (sizeof(unsigned) * 8 - __builtin_clz(id));
254 #else
255  auto i = id;
256  int res = 0;
257  while (i)
258  {
259  ++res;
260  i >>= 1;
261  }
262  return res;
263 #endif
264  }
265 
266  // Return the number of the lowest set used plus one.
267  // If no set is used, this returns 0.
268  // If the sets {1,3,8} are used, this returns 2.
269  unsigned min_set() const
270  {
271  if (id == 0)
272  return 0;
273 #ifdef __GNUC__
274  return __builtin_ctz(id) + 1;
275 #else
276  auto i = id;
277  int res = 1;
278  while ((i & 1) == 0)
279  {
280  ++res;
281  i >>= 1;
282  }
283  return res;
284 #endif
285  }
286 
287  // Return the lowest acceptance mark
288  mark_t lowest() const
289  {
290  return id & -id;
291  }
292 
293  // Remove n bits that where set
294  mark_t& remove_some(unsigned n)
295  {
296  while (n--)
297  id &= id - 1;
298  return *this;
299  }
300 
301  template<class iterator>
302  void fill(iterator here) const
303  {
304  auto a = id;
305  unsigned level = 0;
306  while (a)
307  {
308  if (a & 1)
309  *here++ = level;
310  ++level;
311  a >>= 1;
312  }
313  }
314 
315  // Returns some iterable object that contains the used sets.
316  spot::internal::mark_container sets() const;
317 
318  SPOT_API
319  friend std::ostream& operator<<(std::ostream& os, mark_t m);
320  };
321 
322  // This encodes either an operator or set of acceptance sets.
323  enum class acc_op : unsigned short
324  { Inf, Fin, InfNeg, FinNeg, And, Or };
325  union acc_word
326  {
327  mark_t mark;
328  struct {
329  acc_op op; // Operator
330  unsigned short size; // Size of the subtree (number of acc_word),
331  // not counting this node.
332  } sub;
333  };
334 
335  struct SPOT_API acc_code: public std::vector<acc_word>
336  {
337  bool operator==(const acc_code& other) const
338  {
339  unsigned pos = size();
340  if (other.size() != pos)
341  return false;
342  while (pos > 0)
343  {
344  auto op = (*this)[pos - 1].sub.op;
345  auto sz = (*this)[pos - 1].sub.size;
346  if (other[pos - 1].sub.op != op ||
347  other[pos - 1].sub.size != sz)
348  return false;
349  switch (op)
350  {
351  case acc_cond::acc_op::And:
352  case acc_cond::acc_op::Or:
353  --pos;
354  break;
355  case acc_cond::acc_op::Inf:
356  case acc_cond::acc_op::InfNeg:
357  case acc_cond::acc_op::Fin:
358  case acc_cond::acc_op::FinNeg:
359  pos -= 2;
360  if (other[pos].mark != (*this)[pos].mark)
361  return false;
362  break;
363  }
364  }
365  return true;
366  };
367 
368  bool operator<(const acc_code& other) const
369  {
370  unsigned pos = size();
371  auto osize = other.size();
372  if (pos < osize)
373  return true;
374  if (pos > osize)
375  return false;
376  while (pos > 0)
377  {
378  auto op = (*this)[pos - 1].sub.op;
379  auto oop = other[pos - 1].sub.op;
380  if (op < oop)
381  return true;
382  if (op > oop)
383  return false;
384  auto sz = (*this)[pos - 1].sub.size;
385  auto osz = other[pos - 1].sub.size;
386  if (sz < osz)
387  return true;
388  if (sz > osz)
389  return false;
390  switch (op)
391  {
392  case acc_cond::acc_op::And:
393  case acc_cond::acc_op::Or:
394  --pos;
395  break;
396  case acc_cond::acc_op::Inf:
397  case acc_cond::acc_op::InfNeg:
398  case acc_cond::acc_op::Fin:
399  case acc_cond::acc_op::FinNeg:
400  {
401  pos -= 2;
402  auto m = (*this)[pos].mark;
403  auto om = other[pos].mark;
404  if (m < om)
405  return true;
406  if (m > om)
407  return false;
408  break;
409  }
410  }
411  }
412  return false;
413  }
414 
415  bool operator>(const acc_code& other) const
416  {
417  return other < *this;
418  }
419 
420  bool operator<=(const acc_code& other) const
421  {
422  return !(other < *this);
423  }
424 
425  bool operator>=(const acc_code& other) const
426  {
427  return !(*this < other);
428  }
429 
430  bool operator!=(const acc_code& other) const
431  {
432  return !(*this == other);
433  }
434 
435  bool is_t() const
436  {
437  unsigned s = size();
438  return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
439  && (*this)[s - 2].mark == 0U);
440  }
441 
442  bool is_f() const
443  {
444  unsigned s = size();
445  return s > 1
446  && (*this)[s - 1].sub.op == acc_op::Fin && (*this)[s - 2].mark == 0U;
447  }
448 
449  static acc_code f()
450  {
451  acc_code res;
452  res.resize(2);
453  res[0].mark = 0U;
454  res[1].sub.op = acc_op::Fin;
455  res[1].sub.size = 1;
456  return res;
457  }
458 
459  static acc_code t()
460  {
461  return {};
462  }
463 
464  static acc_code fin(mark_t m)
465  {
466  acc_code res;
467  res.resize(2);
468  res[0].mark = m;
469  res[1].sub.op = acc_op::Fin;
470  res[1].sub.size = 1;
471  return res;
472  }
473 
474  static acc_code fin(std::initializer_list<unsigned> vals)
475  {
476  return fin(mark_t(vals));
477  }
478 
479  static acc_code fin_neg(mark_t m)
480  {
481  acc_code res;
482  res.resize(2);
483  res[0].mark = m;
484  res[1].sub.op = acc_op::FinNeg;
485  res[1].sub.size = 1;
486  return res;
487  }
488 
489  static acc_code fin_neg(std::initializer_list<unsigned> vals)
490  {
491  return fin_neg(mark_t(vals));
492  }
493 
494  static acc_code inf(mark_t m)
495  {
496  acc_code res;
497  res.resize(2);
498  res[0].mark = m;
499  res[1].sub.op = acc_op::Inf;
500  res[1].sub.size = 1;
501  return res;
502  }
503 
504  static acc_code inf(std::initializer_list<unsigned> vals)
505  {
506  return inf(mark_t(vals));
507  }
508 
509  static acc_code inf_neg(mark_t m)
510  {
511  acc_code res;
512  res.resize(2);
513  res[0].mark = m;
514  res[1].sub.op = acc_op::InfNeg;
515  res[1].sub.size = 1;
516  return res;
517  }
518 
519  static acc_code inf_neg(std::initializer_list<unsigned> vals)
520  {
521  return inf_neg(mark_t(vals));
522  }
523 
524  static acc_code buchi()
525  {
526  return inf({0});
527  }
528 
529  static acc_code cobuchi()
530  {
531  return fin({0});
532  }
533 
534  static acc_code generalized_buchi(unsigned n)
535  {
536  acc_cond::mark_t m = (1U << n) - 1;
537  if (n == 8 * sizeof(mark_t::value_t))
538  m = mark_t(-1U);
539  return inf(m);
540  }
541 
542  static acc_code generalized_co_buchi(unsigned n)
543  {
544  acc_cond::mark_t m = (1U << n) - 1;
545  if (n == 8 * sizeof(mark_t::value_t))
546  m = mark_t(-1U);
547  return fin(m);
548  }
549 
550  // n is a number of pairs.
551  static acc_code rabin(unsigned n)
552  {
553  acc_cond::acc_code res = f();
554  while (n > 0)
555  {
556  res |= inf({2*n - 1}) & fin({2*n - 2});
557  --n;
558  }
559  return res;
560  }
561 
562  // n is a number of pairs.
563  static acc_code streett(unsigned n)
564  {
565  acc_cond::acc_code res = t();
566  while (n > 0)
567  {
568  res &= inf({2*n - 1}) | fin({2*n - 2});
569  --n;
570  }
571  return res;
572  }
573 
574  template<class Iterator>
575  static acc_code generalized_rabin(Iterator begin, Iterator end)
576  {
577  acc_cond::acc_code res = f();
578  unsigned n = 0;
579  for (Iterator i = begin; i != end; ++i)
580  {
581  unsigned f = n++;
582  acc_cond::mark_t m = 0U;
583  for (unsigned ni = *i; ni > 0; --ni)
584  m.set(n++);
585  auto pair = inf(m) & fin({f});
586  std::swap(pair, res);
587  res |= std::move(pair);
588  }
589  return res;
590  }
591 
592  static acc_code parity(bool max, bool odd, unsigned sets);
593 
594  // Number of acceptance sets to use, and probability to reuse
595  // each set another time after it has been used in the
596  // acceptance formula.
597  static acc_code random(unsigned n, double reuse = 0.0);
598 
599  acc_code& operator&=(const acc_code& r)
600  {
601  if (is_t() || r.is_f())
602  {
603  *this = r;
604  return *this;
605  }
606  if (is_f() || r.is_t())
607  return *this;
608  unsigned s = size() - 1;
609  unsigned rs = r.size() - 1;
610  // We want to group all Inf(x) operators:
611  // Inf(a) & Inf(b) = Inf(a & b)
612  if (((*this)[s].sub.op == acc_op::Inf
613  && r[rs].sub.op == acc_op::Inf)
614  || ((*this)[s].sub.op == acc_op::InfNeg
615  && r[rs].sub.op == acc_op::InfNeg))
616  {
617  (*this)[s - 1].mark |= r[rs - 1].mark;
618  return *this;
619  }
620 
621  // In the more complex scenarios, left and right may both
622  // be conjunctions, and Inf(x) might be a member of each
623  // side. Find it if it exists.
624  // left_inf points to the left Inf mark if any.
625  // right_inf points to the right Inf mark if any.
626  acc_word* left_inf = nullptr;
627  if ((*this)[s].sub.op == acc_op::And)
628  {
629  auto start = &(*this)[s] - (*this)[s].sub.size;
630  auto pos = &(*this)[s] - 1;
631  pop_back();
632  while (pos > start)
633  {
634  if (pos->sub.op == acc_op::Inf)
635  {
636  left_inf = pos - 1;
637  break;
638  }
639  pos -= pos->sub.size + 1;
640  }
641  }
642  else if ((*this)[s].sub.op == acc_op::Inf)
643  {
644  left_inf = &(*this)[s - 1];
645  }
646 
647  const acc_word* right_inf = nullptr;
648  auto right_end = &r.back();
649  if (right_end->sub.op == acc_op::And)
650  {
651  auto start = &r[0];
652  auto pos = --right_end;
653  while (pos > start)
654  {
655  if (pos->sub.op == acc_op::Inf)
656  {
657  right_inf = pos - 1;
658  break;
659  }
660  pos -= pos->sub.size + 1;
661  }
662  }
663  else if (right_end->sub.op == acc_op::Inf)
664  {
665  right_inf = right_end - 1;
666  }
667 
668  acc_cond::mark_t carry = 0U;
669  if (left_inf && right_inf)
670  {
671  carry = left_inf->mark;
672  auto pos = left_inf - &(*this)[0];
673  erase(begin() + pos, begin() + pos + 2);
674  }
675  auto sz = size();
676  insert(end(), &r[0], right_end + 1);
677  if (carry)
678  (*this)[sz + (right_inf - &r[0])].mark |= carry;
679 
680  acc_word w;
681  w.sub.op = acc_op::And;
682  w.sub.size = size();
683  emplace_back(w);
684  return *this;
685  }
686 
687  acc_code operator&(const acc_code& r)
688  {
689  acc_code res = *this;
690  res &= r;
691  return res;
692  }
693 
694  acc_code operator&(acc_code&& r)
695  {
696  acc_code res = *this;
697  res &= r;
698  return res;
699  }
700 
701  acc_code& operator|=(const acc_code& r)
702  {
703  if (is_t() || r.is_f())
704  return *this;
705  if (is_f() || r.is_t())
706  {
707  *this = r;
708  return *this;
709  }
710  unsigned s = size() - 1;
711  unsigned rs = r.size() - 1;
712  // Fin(a) | Fin(b) = Fin(a | b)
713  if (((*this)[s].sub.op == acc_op::Fin
714  && r[rs].sub.op == acc_op::Fin)
715  || ((*this)[s].sub.op == acc_op::FinNeg
716  && r[rs].sub.op == acc_op::FinNeg))
717  {
718  (*this)[s - 1].mark |= r[rs - 1].mark;
719  return *this;
720  }
721 
722  // In the more complex scenarios, left and right may both
723  // be disjunctions, and Fin(x) might be a member of each
724  // side. Find it if it exists.
725  // left_inf points to the left Inf mark if any.
726  // right_inf points to the right Inf mark if any.
727  acc_word* left_fin = nullptr;
728  if ((*this)[s].sub.op == acc_op::Or)
729  {
730  auto start = &(*this)[s] - (*this)[s].sub.size;
731  auto pos = &(*this)[s] - 1;
732  pop_back();
733  while (pos > start)
734  {
735  if (pos->sub.op == acc_op::Fin)
736  {
737  left_fin = pos - 1;
738  break;
739  }
740  pos -= pos->sub.size + 1;
741  }
742  }
743  else if ((*this)[s].sub.op == acc_op::Fin)
744  {
745  left_fin = &(*this)[s - 1];
746  }
747 
748  const acc_word* right_fin = nullptr;
749  auto right_end = &r.back();
750  if (right_end->sub.op == acc_op::Or)
751  {
752  auto start = &r[0];
753  auto pos = --right_end;
754  while (pos > start)
755  {
756  if (pos->sub.op == acc_op::Fin)
757  {
758  right_fin = pos - 1;
759  break;
760  }
761  pos -= pos->sub.size + 1;
762  }
763  }
764  else if (right_end->sub.op == acc_op::Fin)
765  {
766  right_fin = right_end - 1;
767  }
768 
769  acc_cond::mark_t carry = 0U;
770  if (left_fin && right_fin)
771  {
772  carry = left_fin->mark;
773  auto pos = (left_fin - &(*this)[0]);
774  this->erase(begin() + pos, begin() + pos + 2);
775  }
776  auto sz = size();
777  insert(end(), &r[0], right_end + 1);
778  if (carry)
779  (*this)[sz + (right_fin - &r[0])].mark |= carry;
780  acc_word w;
781  w.sub.op = acc_op::Or;
782  w.sub.size = size();
783  emplace_back(w);
784  return *this;
785  }
786 
787  acc_code operator|(acc_code&& r)
788  {
789  acc_code res = *this;
790  res |= r;
791  return res;
792  }
793 
794  acc_code operator|(const acc_code& r)
795  {
796  acc_code res = *this;
797  res |= r;
798  return res;
799  }
800 
801  acc_code& operator<<=(unsigned sets)
802  {
803  if (empty())
804  return *this;
805  unsigned pos = size();
806  do
807  {
808  switch ((*this)[pos - 1].sub.op)
809  {
810  case acc_cond::acc_op::And:
811  case acc_cond::acc_op::Or:
812  --pos;
813  break;
814  case acc_cond::acc_op::Inf:
815  case acc_cond::acc_op::InfNeg:
816  case acc_cond::acc_op::Fin:
817  case acc_cond::acc_op::FinNeg:
818  pos -= 2;
819  (*this)[pos].mark.id <<= sets;
820  break;
821  }
822  }
823  while (pos > 0);
824  return *this;
825  }
826 
827  acc_code operator<<(unsigned sets) const
828  {
829  acc_code res = *this;
830  res <<= sets;
831  return res;
832  }
833 
834  bool is_dnf() const;
835  bool is_cnf() const;
836 
837  acc_code to_dnf() const;
838  acc_code to_cnf() const;
839 
840  acc_code complement() const;
841 
842  // Return a list of acceptance marks needed to close a cycle
843  // that already visit INF infinitely often, so that the cycle is
844  // accepting (ACCEPTING=true) or rejecting (ACCEPTING=false).
845  // Positive values describe positive set.
846  // A negative value x means the set -x-1 must be absent.
847  std::vector<std::vector<int>>
848  missing(mark_t inf, bool accepting) const;
849 
850  bool accepting(mark_t inf) const;
851 
852  bool inf_satisfiable(mark_t inf) const;
853 
854  trival maybe_accepting(mark_t infinitely_often,
855  mark_t always_present) const;
856 
857 
858  // Remove all the acceptance sets in rem.
859  //
860  // If MISSING is set, the acceptance sets are assumed to be
861  // missing from the automaton, and the acceptance is updated to
862  // reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will
863  // become Fin(3) if we remove 2 because it is missing from this
864  // automaton, because there is no way to fulfill Inf(1)&Inf(2)
865  // in this case. So essentially MISSING causes Inf(rem) to
866  // become f, and Fin(rem) to become t.
867  //
868  // If MISSING is unset, Inf(rem) become t while Fin(rem) become
869  // f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
870  // Inf(1)|Fin(3).
871  acc_code remove(acc_cond::mark_t rem, bool missing) const;
872  // Same as remove, but also shift numbers
873  acc_code strip(acc_cond::mark_t rem, bool missing) const;
874 
875  // Return the set of sets appearing in the condition.
876  acc_cond::mark_t used_sets() const;
877 
878  // Return the sets used as Inf or Fin in the acceptance condition
879  std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
880 
881  // Print the acceptance as HTML. The set_printer function can
882  // be used to implement customized output for set numbers.
883  std::ostream&
884  to_html(std::ostream& os,
885  std::function<void(std::ostream&, int)>
886  set_printer = nullptr) const;
887 
888  // Print the acceptance as text. The set_printer function can
889  // be used to implement customized output for set numbers.
890  std::ostream&
891  to_text(std::ostream& os,
892  std::function<void(std::ostream&, int)>
893  set_printer = nullptr) const;
894 
895  // Print the acceptance as Latex. The set_printer function can
896  // be used to implement customized output for set numbers.
897  std::ostream&
898  to_latex(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  struct SPOT_API rs_pair
1050  {
1051  rs_pair() = default;
1052  rs_pair(const rs_pair&) = default;
1053 
1055  fin(fin),
1056  inf(inf)
1057  {}
1058  acc_cond::mark_t fin;
1059  acc_cond::mark_t inf;
1060 
1061  bool operator==(rs_pair o) const
1062  {
1063  return fin == o.fin && inf == o.inf;
1064  }
1065  bool operator!=(rs_pair o) const
1066  {
1067  return fin != o.fin || inf != o.inf;
1068  }
1069  bool operator<(rs_pair o) const
1070  {
1071  return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
1072  }
1073  bool operator<=(rs_pair o) const
1074  {
1075  return !(o < *this);
1076  }
1077  bool operator>(rs_pair o) const
1078  {
1079  return o < *this;
1080  }
1081  bool operator>=(rs_pair o) const
1082  {
1083  return !(*this < o);
1084  }
1085  };
1096  bool is_streett_like(std::vector<rs_pair>& pairs) const;
1097 
1108  bool is_rabin_like(std::vector<rs_pair>& pairs) const;
1109 
1110  // Return the number of Inf in each pair.
1111  bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
1112 
1113  // If EQUIV is false, this return true iff the acceptance
1114  // condition is a parity condition written in the canonical way
1115  // given in the HOA specifications. If EQUIV is true, then we
1116  // check whether the condition is logically equivalent to some
1117  // parity acceptance condition.
1118  bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1119  bool is_parity() const
1120  {
1121  bool max;
1122  bool odd;
1123  return is_parity(max, odd);
1124  }
1125 
1126  // Return (true, m) if there exist some acceptance mark m that
1127  // does not satisfy the acceptance condition. Return (false, 0U)
1128  // otherwise.
1129  std::pair<bool, acc_cond::mark_t> unsat_mark() const;
1130 
1131  protected:
1132  bool check_fin_acceptance() const;
1133 
1134  public:
1135  static acc_code inf(mark_t mark)
1136  {
1137  return acc_code::inf(mark);
1138  }
1139 
1140  static acc_code inf(std::initializer_list<unsigned> vals)
1141  {
1142  return inf(mark_t(vals.begin(), vals.end()));
1143  }
1144 
1145  static acc_code inf_neg(mark_t mark)
1146  {
1147  return acc_code::inf_neg(mark);
1148  }
1149 
1150  static acc_code inf_neg(std::initializer_list<unsigned> vals)
1151  {
1152  return inf_neg(mark_t(vals.begin(), vals.end()));
1153  }
1154 
1155  static acc_code fin(mark_t mark)
1156  {
1157  return acc_code::fin(mark);
1158  }
1159 
1160  static acc_code fin(std::initializer_list<unsigned> vals)
1161  {
1162  return fin(mark_t(vals.begin(), vals.end()));
1163  }
1164 
1165  static acc_code fin_neg(mark_t mark)
1166  {
1167  return acc_code::fin_neg(mark);
1168  }
1169 
1170  static acc_code fin_neg(std::initializer_list<unsigned> vals)
1171  {
1172  return fin_neg(mark_t(vals.begin(), vals.end()));
1173  }
1174 
1175  unsigned add_sets(unsigned num)
1176  {
1177  if (num == 0)
1178  return -1U;
1179  unsigned j = num_;
1180  num_ += num;
1181  if (num_ > 8 * sizeof(mark_t::id))
1182  throw std::runtime_error("Too many acceptance sets used.");
1183  all_ = all_sets_();
1184  return j;
1185  }
1186 
1187  unsigned add_set()
1188  {
1189  return add_sets(1);
1190  }
1191 
1192  mark_t mark(unsigned u) const
1193  {
1194  SPOT_ASSERT(u < num_sets());
1195  return 1U << u;
1196  }
1197 
1198  mark_t comp(mark_t l) const
1199  {
1200  return all_ ^ l.id;
1201  }
1202 
1203  mark_t all_sets() const
1204  {
1205  return all_;
1206  }
1207 
1208  bool accepting(mark_t inf) const
1209  {
1210  return code_.accepting(inf);
1211  }
1212 
1213  bool inf_satisfiable(mark_t inf) const
1214  {
1215  return code_.inf_satisfiable(inf);
1216  }
1217 
1218  trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
1219  {
1220  return code_.maybe_accepting(infinitely_often, always_present);
1221  }
1222 
1223  mark_t accepting_sets(mark_t inf) const;
1224 
1225  std::ostream& format(std::ostream& os, mark_t m) const
1226  {
1227  auto a = m;
1228  if (a == 0U)
1229  return os;
1230  return os << m;
1231  }
1232 
1233  std::string format(mark_t m) const
1234  {
1235  std::ostringstream os;
1236  format(os, m);
1237  return os.str();
1238  }
1239 
1240  unsigned num_sets() const
1241  {
1242  return num_;
1243  }
1244 
1245  template<class iterator>
1246  mark_t useless(iterator begin, iterator end) const
1247  {
1248  mark_t::value_t u = 0U; // The set of useless marks.
1249  for (unsigned x = 0; x < num_; ++x)
1250  {
1251  // Skip marks that are already known to be useless.
1252  if (u & (1 << x))
1253  continue;
1254  unsigned all = all_ ^ (u | (1 << x));
1255  for (iterator y = begin; y != end; ++y)
1256  {
1257  auto v = y->id;
1258  if (v & (1 << x))
1259  {
1260  all &= v;
1261  if (!all)
1262  break;
1263  }
1264  }
1265  u |= all;
1266  }
1267  return u;
1268  }
1269 
1270  // Remove all the acceptance sets in rem.
1271  //
1272  // If MISSING is set, the acceptance sets are assumed to be
1273  // missing from the automaton, and the acceptance is updated to
1274  // reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will
1275  // become Fin(3) if we remove 2 because it is missing from this
1276  // automaton, because there is no way to fulfill Inf(1)&Inf(2)
1277  // in this case. So essentially MISSING causes Inf(rem) to
1278  // become f, and Fin(rem) to become t.
1279  //
1280  // If MISSING is unset, Inf(rem) become t while Fin(rem) become
1281  // f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
1282  // Inf(1)|Fin(3).
1283  acc_cond remove(mark_t rem, bool missing) const
1284  {
1285  return {num_sets(), code_.remove(rem, missing)};
1286  }
1287 
1288  // Same as remove, but also shift the set numbers
1289  acc_cond strip(mark_t rem, bool missing) const
1290  {
1291  return
1292  { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
1293  }
1294 
1295  // Restrict an acceptance condition to a subset of set numbers
1296  // that are occurring at some point.
1297  acc_cond restrict_to(mark_t rem) const
1298  {
1299  return {num_sets(), code_.remove(all_sets() - rem, true)};
1300  }
1301 
1302  protected:
1303  mark_t::value_t all_sets_() const
1304  {
1305  if (num_ == 0)
1306  return 0;
1307  return -1U >> (8 * sizeof(mark_t::value_t) - num_);
1308  }
1309 
1310  unsigned num_;
1311  mark_t::value_t all_;
1312  acc_code code_;
1313  bool uses_fin_acceptance_ = false;
1314 
1315  };
1316 
1317  struct rs_pairs_view {
1318  typedef std::vector<acc_cond::rs_pair> rs_pairs;
1319 
1320  // Creates view of pairs 'p' with restriction only to marks in 'm'
1321  explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
1322  : pairs_(p), view_marks_(m) {}
1323 
1324  // Creates view of pairs without restriction to marks
1325  explicit rs_pairs_view(const rs_pairs& p)
1326  : rs_pairs_view(p, std::numeric_limits<unsigned>::max()) {}
1327 
1328  acc_cond::mark_t infs() const
1329  {
1330  return do_view([&](const acc_cond::rs_pair& p)
1331  {
1332  return visible(p.inf) ? p.inf : 0U;
1333  });
1334  }
1335 
1336  acc_cond::mark_t fins() const
1337  {
1338  return do_view([&](const acc_cond::rs_pair& p)
1339  {
1340  return visible(p.fin) ? p.fin : 0U;
1341  });
1342  }
1343 
1344  acc_cond::mark_t fins_alone() const
1345  {
1346  return do_view([&](const acc_cond::rs_pair& p)
1347  {
1348  return !visible(p.inf) && visible(p.fin) ? p.fin : 0U;
1349  });
1350  }
1351 
1352  acc_cond::mark_t infs_alone() const
1353  {
1354  return do_view([&](const acc_cond::rs_pair& p)
1355  {
1356  return !visible(p.fin) && visible(p.inf) ? p.inf : 0U;
1357  });
1358  }
1359 
1360  acc_cond::mark_t paired_with(unsigned mark) const
1361  {
1362  acc_cond::mark_t res = 0U;
1363  for (const auto& p: pairs_)
1364  {
1365  if (visible(p.fin) && visible(p.inf))
1366  {
1367  if (p.fin.has(mark))
1368  res |= p.inf;
1369  if (p.inf.has(mark))
1370  res |= p.fin;
1371  }
1372  }
1373  return res;
1374  }
1375 
1376  const rs_pairs& pairs() const
1377  {
1378  return pairs_;
1379  }
1380 
1381  private:
1382  template<typename filter>
1383  acc_cond::mark_t do_view(const filter& filt) const
1384  {
1385  acc_cond::mark_t res = 0U;
1386  for (const auto& p: pairs_)
1387  res |= filt(p);
1388  return res;
1389  }
1390 
1391  bool visible(const acc_cond::mark_t& v) const
1392  {
1393  return (view_marks_ & v) != 0;
1394  }
1395 
1396  const rs_pairs& pairs_;
1397  acc_cond::mark_t view_marks_;
1398  };
1399 
1400 
1401  SPOT_API
1402  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
1403 
1404  namespace internal
1405  {
1406  class SPOT_API mark_iterator
1407  {
1408  public:
1409  typedef unsigned value_type;
1410  typedef const value_type& reference;
1411  typedef const value_type* pointer;
1412  typedef std::ptrdiff_t difference_type;
1413  typedef std::forward_iterator_tag iterator_category;
1414 
1415  mark_iterator() noexcept
1416  : m_(0U)
1417  {
1418  }
1419 
1420  mark_iterator(acc_cond::mark_t m) noexcept
1421  : m_(m)
1422  {
1423  }
1424 
1425  bool operator==(mark_iterator m) const
1426  {
1427  return m_ == m.m_;
1428  }
1429 
1430  bool operator!=(mark_iterator m) const
1431  {
1432  return m_ != m.m_;
1433  }
1434 
1435  value_type operator*() const
1436  {
1437  SPOT_ASSERT(m_);
1438  return m_.min_set() - 1;
1439  }
1440 
1441  mark_iterator operator++()
1442  {
1443  m_.id &= m_.id - 1;
1444  return *this;
1445  }
1446 
1447  mark_iterator operator++(int)
1448  {
1449  mark_iterator it = *this;
1450  ++(*this);
1451  return it;
1452  }
1453  private:
1454  acc_cond::mark_t m_;
1455  };
1456 
1457  class SPOT_API mark_container
1458  {
1459  public:
1461  : m_(m)
1462  {
1463  }
1464 
1465  mark_iterator begin() const
1466  {
1467  return {m_};
1468  }
1469  mark_iterator end() const
1470  {
1471  return {};
1472  }
1473  private:
1475  };
1476  }
1477 
1478  inline spot::internal::mark_container acc_cond::mark_t::sets() const
1479  {
1480  return {*this};
1481  }
1482 }
1483 
1484 namespace std
1485 {
1486  template<>
1487  struct hash<spot::acc_cond::mark_t>
1488  {
1489  size_t operator()(spot::acc_cond::mark_t m) const
1490  {
1491  std::hash<decltype(m.id)> h;
1492  return h(m.id);
1493  }
1494  };
1495 }
Definition: automata.hh:26
Definition: acc.hh:1406
Definition: acc.hh:1049
Definition: formula.hh:1678
Definition: acc.hh:1317
Definition: acc.hh:36
Definition: acc.hh:325
A class implementing Kleene&#39;s three-valued logic.
Definition: trival.hh:33
(omega-Rational) Or
Definition: twa.hh:1629
acc_code()
Build an empty acceptance condition.
Definition: acc.hh:930
op
Operator types.
Definition: formula.hh:62
Definition: acc.hh:335
Definition: acc.hh:1457
(omega-Rational) And
Definition: acc.hh:39

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Wed Sep 6 2017 05:14:05 for spot by doxygen 1.8.13