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

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