acc.hh 37 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
3
// Développement de l'Epita.
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

20
#pragma once
21

22
23
24
25
#include <functional>
#include <unordered_map>
#include <sstream>
#include <vector>
26
#include <spot/tl/defaultenv.hh>
27
#include <spot/misc/trival.hh>
28
#include <iostream>
29
30
31

namespace spot
{
32
33
34
35
  namespace internal
  {
    class mark_container;
  }
36
  class SPOT_API acc_cond
37
38
39
40
41
42
43
44
45
  {
  public:
    struct mark_t
    {
      typedef unsigned value_t;
      value_t id;

      mark_t() = default;

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
55
56
        id = 0U;
        for (iterator i = begin; i != end; ++i)
          set(*i);
57
58
      }

59
      mark_t(std::initializer_list<unsigned> vals) noexcept
60
        : mark_t(vals.begin(), vals.end())
61
62
63
      {
      }

64
65
      bool operator==(unsigned o) const
      {
66
        SPOT_ASSERT(o == 0U);
67
        return id == o;
68
69
70
71
      }

      bool operator!=(unsigned o) const
      {
72
        SPOT_ASSERT(o == 0U);
73
        return id != o;
74
75
76
77
      }

      bool operator==(mark_t o) const
      {
78
        return id == o.id;
79
80
81
82
      }

      bool operator!=(mark_t o) const
      {
83
        return id != o.id;
84
85
86
87
      }

      bool operator<(mark_t o) const
      {
88
        return id < o.id;
89
90
91
92
      }

      bool operator<=(mark_t o) const
      {
93
        return id <= o.id;
94
95
96
97
      }

      bool operator>(mark_t o) const
      {
98
        return id > o.id;
99
100
101
102
      }

      bool operator>=(mark_t o) const
      {
103
        return id >= o.id;
104
105
      }

106
      explicit operator bool() const
107
      {
108
        return id != 0;
109
110
111
112
      }

      bool has(unsigned u) const
      {
113
        return id & (1U << u);
114
115
116
117
      }

      void set(unsigned u)
      {
118
        id |= (1U << u);
119
120
      }

121
122
      void clear(unsigned u)
      {
123
        id &= ~(1U << u);
124
125
      }

126
127
      mark_t& operator&=(mark_t r)
      {
128
129
        id &= r.id;
        return *this;
130
131
132
133
      }

      mark_t& operator|=(mark_t r)
      {
134
135
        id |= r.id;
        return *this;
136
137
138
139
      }

      mark_t& operator-=(mark_t r)
      {
140
141
        id &= ~r.id;
        return *this;
142
143
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
144
145
      mark_t& operator^=(mark_t r)
      {
146
147
        id ^= r.id;
        return *this;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
148
149
      }

150
151
      mark_t operator&(mark_t r) const
      {
152
        return id & r.id;
153
154
155
156
      }

      mark_t operator|(mark_t r) const
      {
157
        return id | r.id;
158
159
160
161
      }

      mark_t operator-(mark_t r) const
      {
162
        return id & ~r.id;
163
164
      }

165
166
      mark_t operator~() const
      {
167
        return ~id;
168
169
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
170
171
      mark_t operator^(mark_t r) const
      {
172
        return id ^ r.id;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
173
174
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
175
      mark_t operator<<(unsigned i) const
176
      {
177
        return id << i;
178
179
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
180
      mark_t& operator<<=(unsigned i)
181
      {
182
183
        id <<= i;
        return *this;
184
185
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
186
      mark_t operator>>(unsigned i) const
187
      {
188
        return id >> i;
189
190
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
191
      mark_t& operator>>=(unsigned i)
192
      {
193
194
        id >>= i;
        return *this;
195
196
      }

197
198
      mark_t strip(mark_t y) const
      {
199
200
201
202
203
        // strip every bit of id that is marked in y
        //       100101110100.strip(
        //       001011001000)
        //   ==  10 1  11 100
        //   ==      10111100
204

205
206
        auto xv = id;                // 100101110100
        auto yv = y.id;                // 001011001000
207

208
209
210
211
212
213
214
215
216
217
        while (yv && xv)
          {
            // Mask for everything after the last 1 in y
            auto rm = (~yv) & (yv - 1);        // 000000000111
            // Mask for everything before the last 1 in y
            auto lm = ~(yv ^ (yv - 1));        // 111111110000
            xv = ((xv & lm) >> 1) | (xv & rm);
            yv = (yv & lm) >> 1;
          }
        return xv;
218
219
      }

220
221
222
223
224
225
226
227
228
229
      bool subset(mark_t m) const
      {
        return this->strip(m) == 0U;
      }

      bool proper_subset(mark_t m) const
      {
        return *this != m && this->subset(m);
      }

230
231
232
233
      // Number of bits sets.
      unsigned count() const
      {
#ifdef __GNUC__
234
        return __builtin_popcount(id);
235
#else
236
237
238
239
240
241
242
243
        unsigned c = 0U;
        auto v = id;
        while (v)
          {
            ++c;
            v &= v - 1;
          }
        return c;
244
245
246
#endif
      }

247
      // Return the number of the highest set used plus one.
248
249
      // If no set is used, this returns 0,
      // If the sets {1,3,8} are used, this returns 9.
250
251
      unsigned max_set() const
      {
252
253
254
#ifdef __GNUC__
        return (id == 0) ? 0 : (sizeof(unsigned) * 8 - __builtin_clz(id));
#else
255
256
257
258
259
260
261
262
        auto i = id;
        int res = 0;
        while (i)
          {
            ++res;
            i >>= 1;
          }
        return res;
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
#endif
      }

      // Return the number of the lowest set used plus one.
      // If no set is used, this returns 0.
      // If the sets {1,3,8} are used, this returns 2.
      unsigned min_set() const
      {
        if (id == 0)
          return 0;
#ifdef __GNUC__
        return __builtin_ctz(id) + 1;
#else
        auto i = id;
        int res = 1;
        while ((i & 1) == 0)
          {
            ++res;
            i >>= 1;
          }
        return res;
#endif
285
286
      }

287
288
289
      // Return the lowest acceptance mark
      mark_t lowest() const
      {
290
        return id & -id;
291
292
      }

293
294
295
      // Remove n bits that where set
      mark_t& remove_some(unsigned n)
      {
296
297
298
        while (n--)
          id &= id - 1;
        return *this;
299
300
      }

301
302
      template<class iterator>
      void fill(iterator here) const
303
      {
304
305
306
307
308
309
310
311
312
        auto a = id;
        unsigned level = 0;
        while (a)
          {
            if (a & 1)
              *here++ = level;
            ++level;
            a >>= 1;
          }
313
314
      }

315
316
      // Returns some iterable object that contains the used sets.
      spot::internal::mark_container sets() const;
317
318
319
320
321
322

      SPOT_API
      friend std::ostream& operator<<(std::ostream& os, mark_t m);
    };

    // This encodes either an operator or set of acceptance sets.
323
    enum class acc_op : unsigned short
324
325
326
327
328
    { Inf, Fin, InfNeg, FinNeg, And, Or };
    union acc_word
    {
      mark_t mark;
      struct {
329
330
331
        acc_op op;             // Operator
        unsigned short size; // Size of the subtree (number of acc_word),
                             // 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
340
341
342
343
        unsigned pos = size();
        if (other.size() != pos)
          return false;
        while (pos > 0)
          {
344
345
346
347
            auto op = (*this)[pos - 1].sub.op;
            auto sz = (*this)[pos - 1].sub.size;
            if (other[pos - 1].sub.op != op ||
                other[pos - 1].sub.size != sz)
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
              return false;
            switch (op)
              {
              case acc_cond::acc_op::And:
              case acc_cond::acc_op::Or:
                --pos;
                break;
              case acc_cond::acc_op::Inf:
              case acc_cond::acc_op::InfNeg:
              case acc_cond::acc_op::Fin:
              case acc_cond::acc_op::FinNeg:
                pos -= 2;
                if (other[pos].mark != (*this)[pos].mark)
                  return false;
                break;
              }
          }
        return true;
366
367
      };

368
369
      bool operator<(const acc_code& other) const
      {
370
371
372
373
374
375
376
377
        unsigned pos = size();
        auto osize = other.size();
        if (pos < osize)
          return true;
        if (pos > osize)
          return false;
        while (pos > 0)
          {
378
379
            auto op = (*this)[pos - 1].sub.op;
            auto oop = other[pos - 1].sub.op;
380
381
382
383
            if (op < oop)
              return true;
            if (op > oop)
              return false;
384
385
            auto sz = (*this)[pos - 1].sub.size;
            auto osz = other[pos - 1].sub.size;
386
387
388
389
390
391
392
393
394
395
396
397
398
399
            if (sz < osz)
              return true;
            if (sz > osz)
              return false;
            switch (op)
              {
              case acc_cond::acc_op::And:
              case acc_cond::acc_op::Or:
                --pos;
                break;
              case acc_cond::acc_op::Inf:
              case acc_cond::acc_op::InfNeg:
              case acc_cond::acc_op::Fin:
              case acc_cond::acc_op::FinNeg:
400
401
402
403
404
405
406
407
408
409
                {
                  pos -= 2;
                  auto m = (*this)[pos].mark;
                  auto om = other[pos].mark;
                  if (m < om)
                    return true;
                  if (m > om)
                    return false;
                  break;
                }
410
411
412
              }
          }
        return false;
413
414
415
416
      }

      bool operator>(const acc_code& other) const
      {
417
        return other < *this;
418
419
420
421
      }

      bool operator<=(const acc_code& other) const
      {
422
        return !(other < *this);
423
424
425
426
      }

      bool operator>=(const acc_code& other) const
      {
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
439
        return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
                          && (*this)[s - 2].mark == 0U);
440
441
      }

442
      bool is_f() const
443
      {
444
445
        unsigned s = size();
        return s > 1
446
          && (*this)[s - 1].sub.op == acc_op::Fin && (*this)[s - 2].mark == 0U;
447
448
      }

449
450
      static acc_code f()
      {
451
452
453
        acc_code res;
        res.resize(2);
        res[0].mark = 0U;
454
455
        res[1].sub.op = acc_op::Fin;
        res[1].sub.size = 1;
456
        return res;
457
458
459
460
      }

      static acc_code t()
      {
461
        return {};
462
463
464
465
      }

      static acc_code fin(mark_t m)
      {
466
467
468
        acc_code res;
        res.resize(2);
        res[0].mark = m;
469
470
        res[1].sub.op = acc_op::Fin;
        res[1].sub.size = 1;
471
        return res;
472
473
      }

474
475
      static acc_code fin(std::initializer_list<unsigned> vals)
      {
476
        return fin(mark_t(vals));
477
478
      }

479
480
      static acc_code fin_neg(mark_t m)
      {
481
482
483
        acc_code res;
        res.resize(2);
        res[0].mark = m;
484
485
        res[1].sub.op = acc_op::FinNeg;
        res[1].sub.size = 1;
486
        return res;
487
488
      }

489
490
      static acc_code fin_neg(std::initializer_list<unsigned> vals)
      {
491
        return fin_neg(mark_t(vals));
492
493
      }

494
495
      static acc_code inf(mark_t m)
      {
496
497
498
        acc_code res;
        res.resize(2);
        res[0].mark = m;
499
500
        res[1].sub.op = acc_op::Inf;
        res[1].sub.size = 1;
501
        return res;
502
503
      }

504
505
      static acc_code inf(std::initializer_list<unsigned> vals)
      {
506
        return inf(mark_t(vals));
507
508
      }

509
510
      static acc_code inf_neg(mark_t m)
      {
511
512
513
        acc_code res;
        res.resize(2);
        res[0].mark = m;
514
515
        res[1].sub.op = acc_op::InfNeg;
        res[1].sub.size = 1;
516
        return res;
517
518
      }

519
520
      static acc_code inf_neg(std::initializer_list<unsigned> vals)
      {
521
        return inf_neg(mark_t(vals));
522
523
      }

524
525
      static acc_code buchi()
      {
526
        return inf({0});
527
528
529
530
      }

      static acc_code cobuchi()
      {
531
        return fin({0});
532
533
534
535
      }

      static acc_code generalized_buchi(unsigned n)
      {
536
537
538
539
        acc_cond::mark_t m = (1U << n) - 1;
        if (n == 8 * sizeof(mark_t::value_t))
          m = mark_t(-1U);
        return inf(m);
540
541
542
543
      }

      static acc_code generalized_co_buchi(unsigned n)
      {
544
545
546
547
        acc_cond::mark_t m = (1U << n) - 1;
        if (n == 8 * sizeof(mark_t::value_t))
          m = mark_t(-1U);
        return fin(m);
548
549
550
551
552
      }

      // n is a number of pairs.
      static acc_code rabin(unsigned n)
      {
553
554
555
556
557
558
559
        acc_cond::acc_code res = f();
        while (n > 0)
          {
            res |= inf({2*n - 1}) & fin({2*n - 2});
            --n;
          }
        return res;
560
561
562
563
564
      }

       // n is a number of pairs.
      static acc_code streett(unsigned n)
      {
565
566
567
568
569
570
571
        acc_cond::acc_code res = t();
        while (n > 0)
          {
            res &= inf({2*n - 1}) | fin({2*n - 2});
            --n;
          }
        return res;
572
573
      }

574
575
      template<class Iterator>
      static acc_code generalized_rabin(Iterator begin, Iterator end)
576
      {
577
578
579
580
        acc_cond::acc_code res = f();
        unsigned n = 0;
        for (Iterator i = begin; i != end; ++i)
          {
581
            unsigned f = n++;
582
583
584
            acc_cond::mark_t m = 0U;
            for (unsigned ni = *i; ni > 0; --ni)
              m.set(n++);
585
            auto pair = inf(m) & fin({f});
586
587
588
589
            std::swap(pair, res);
            res |= std::move(pair);
          }
        return res;
590
591
      }

592
593
      static acc_code parity(bool max, bool odd, unsigned sets);

594
595
596
597
598
      // Number of acceptance sets to use, and probability to reuse
      // each set another time after it has been used in the
      // acceptance formula.
      static acc_code random(unsigned n, double reuse = 0.0);

599
      acc_code& operator&=(const acc_code& r)
600
      {
601
602
        if (is_t() || r.is_f())
          {
603
            *this = r;
604
605
606
607
608
609
610
611
            return *this;
          }
        if (is_f() || r.is_t())
          return *this;
        unsigned s = size() - 1;
        unsigned rs = r.size() - 1;
        // We want to group all Inf(x) operators:
        //   Inf(a) & Inf(b) = Inf(a & b)
612
613
614
615
        if (((*this)[s].sub.op == acc_op::Inf
             && r[rs].sub.op == acc_op::Inf)
            || ((*this)[s].sub.op == acc_op::InfNeg
                && r[rs].sub.op == acc_op::InfNeg))
616
617
618
619
620
621
622
623
624
625
626
          {
            (*this)[s - 1].mark |= r[rs - 1].mark;
            return *this;
          }

        // In the more complex scenarios, left and right may both
        // be conjunctions, and Inf(x) might be a member of each
        // side.  Find it if it exists.
        // left_inf points to the left Inf mark if any.
        // right_inf points to the right Inf mark if any.
        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
631
632
633
            auto pos = &(*this)[s] - 1;
            pop_back();
            while (pos > start)
              {
634
                if (pos->sub.op == acc_op::Inf)
635
636
637
638
                  {
                    left_inf = pos - 1;
                    break;
                  }
639
                pos -= pos->sub.size + 1;
640
641
              }
          }
642
        else if ((*this)[s].sub.op == acc_op::Inf)
643
644
645
646
          {
            left_inf = &(*this)[s - 1];
          }

647
        const acc_word* right_inf = nullptr;
648
        auto right_end = &r.back();
649
        if (right_end->sub.op == acc_op::And)
650
651
652
653
654
          {
            auto start = &r[0];
            auto pos = --right_end;
            while (pos > start)
            {
655
              if (pos->sub.op == acc_op::Inf)
656
657
658
659
                {
                  right_inf = pos - 1;
                  break;
                }
660
              pos -= pos->sub.size + 1;
661
662
            }
          }
663
        else if (right_end->sub.op == acc_op::Inf)
664
665
666
667
          {
            right_inf = right_end - 1;
          }

668
        acc_cond::mark_t carry = 0U;
669
670
        if (left_inf && right_inf)
          {
671
672
673
            carry = left_inf->mark;
            auto pos = left_inf - &(*this)[0];
            erase(begin() + pos, begin() + pos + 2);
674
          }
675
676
677
678
        auto sz = size();
        insert(end(), &r[0], right_end + 1);
        if (carry)
          (*this)[sz + (right_inf - &r[0])].mark |= carry;
679
680

        acc_word w;
681
682
        w.sub.op = acc_op::And;
        w.sub.size = size();
683
        emplace_back(w);
684
        return *this;
685
686
      }

687
688
      acc_code operator&(const acc_code& r)
      {
689
690
691
        acc_code res = *this;
        res &= r;
        return res;
692
693
694
695
696
697
698
699
700
701
      }

      acc_code operator&(acc_code&& r)
      {
        acc_code res = *this;
        res &= r;
        return res;
      }

      acc_code& operator|=(const acc_code& r)
702
      {
703
        if (is_t() || r.is_f())
704
705
          return *this;
        if (is_f() || r.is_t())
706
707
708
709
710
711
          {
            *this = r;
            return *this;
          }
        unsigned s = size() - 1;
        unsigned rs = r.size() - 1;
712
713
714
715
716
        // Fin(a) | Fin(b) = Fin(a | b)
        if (((*this)[s].sub.op == acc_op::Fin
             && r[rs].sub.op == acc_op::Fin)
            || ((*this)[s].sub.op == acc_op::FinNeg
                && r[rs].sub.op == acc_op::FinNeg))
717
718
719
720
721
722
          {
            (*this)[s - 1].mark |= r[rs - 1].mark;
            return *this;
          }

        // In the more complex scenarios, left and right may both
723
        // be disjunctions, and Fin(x) might be a member of each
724
725
726
        // side.  Find it if it exists.
        // left_inf points to the left Inf mark if any.
        // right_inf points to the right Inf mark if any.
727
728
        acc_word* left_fin = nullptr;
        if ((*this)[s].sub.op == acc_op::Or)
729
          {
730
            auto start = &(*this)[s] - (*this)[s].sub.size;
731
732
733
734
            auto pos = &(*this)[s] - 1;
            pop_back();
            while (pos > start)
              {
735
                if (pos->sub.op == acc_op::Fin)
736
                  {
737
                    left_fin = pos - 1;
738
739
                    break;
                  }
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
753
754
755
          {
            auto start = &r[0];
            auto pos = --right_end;
            while (pos > start)
            {
756
              if (pos->sub.op == acc_op::Fin)
757
                {
758
                  right_fin = pos - 1;
759
760
                  break;
                }
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
770
        acc_cond::mark_t carry = 0U;
        if (left_fin && right_fin)
771
          {
772
773
774
            carry = left_fin->mark;
            auto pos = (left_fin - &(*this)[0]);
            this->erase(begin() + pos, begin() + pos + 2);
775
          }
776
777
778
779
        auto sz = size();
        insert(end(), &r[0], right_end + 1);
        if (carry)
          (*this)[sz + (right_fin - &r[0])].mark |= carry;
780
        acc_word w;
781
782
        w.sub.op = acc_op::Or;
        w.sub.size = size();
783
        emplace_back(w);
784
        return *this;
785
786
787
788
      }

      acc_code operator|(acc_code&& r)
      {
789
790
791
        acc_code res = *this;
        res |= r;
        return res;
792
793
      }

794
      acc_code operator|(const acc_code& r)
795
      {
796
797
798
        acc_code res = *this;
        res |= r;
        return res;
799
800
801
      }

      acc_code& operator<<=(unsigned sets)
802
      {
803
804
805
806
807
        if (empty())
          return *this;
        unsigned pos = size();
        do
          {
808
            switch ((*this)[pos - 1].sub.op)
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
              {
              case acc_cond::acc_op::And:
              case acc_cond::acc_op::Or:
                --pos;
                break;
              case acc_cond::acc_op::Inf:
              case acc_cond::acc_op::InfNeg:
              case acc_cond::acc_op::Fin:
              case acc_cond::acc_op::FinNeg:
                pos -= 2;
                (*this)[pos].mark.id <<= sets;
                break;
              }
          }
        while (pos > 0);
        return *this;
825
826
827
828
      }

      acc_code operator<<(unsigned sets) const
      {
829
830
831
        acc_code res = *this;
        res <<= sets;
        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
841
      acc_code complement() const;

842
843
844
845
846
847
      // Return a list of acceptance marks needed to close a cycle
      // that already visit INF infinitely often, so that the cycle is
      // accepting (ACCEPTING=true) or rejecting (ACCEPTING=false).
      // Positive values describe positive set.
      // A negative value x means the set -x-1 must be absent.
      std::vector<std::vector<int>>
848
        missing(mark_t inf, bool accepting) const;
849
850
851
852
853

      bool accepting(mark_t inf) const;

      bool inf_satisfiable(mark_t inf) const;

854
855
856
857
      trival maybe_accepting(mark_t infinitely_often,
                             mark_t always_present) const;


858
859
860
861
862
863
864
865
866
867
868
869
870
      // Remove all the acceptance sets in rem.
      //
      // If MISSING is set, the acceptance sets are assumed to be
      // missing from the automaton, and the acceptance is updated to
      // reflect this.  For instance (Inf(1)&Inf(2))|Fin(3) will
      // become Fin(3) if we remove 2 because it is missing from this
      // automaton, because there is no way to fulfill Inf(1)&Inf(2)
      // in this case.  So essentially MISSING causes Inf(rem) to
      // become f, and Fin(rem) to become t.
      //
      // If MISSING is unset, Inf(rem) become t while Fin(rem) become
      // f.  Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give
      // Inf(1)|Fin(3).
871
872
      acc_code remove(acc_cond::mark_t rem, bool missing) const;
      // Same as remove, but also shift numbers
873
874
875
876
877
      acc_code strip(acc_cond::mark_t rem, bool missing) const;

      // Return the set of sets appearing in the condition.
      acc_cond::mark_t used_sets() const;

878
879
880
881
882
883
884
      // Return the sets used as Inf or Fin in the acceptance condition
      std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;

      // Print the acceptance as HTML.  The set_printer function can
      // be used to implement customized output for set numbers.
      std::ostream&
      to_html(std::ostream& os,
885
886
              std::function<void(std::ostream&, int)>
              set_printer = nullptr) const;
887
888
889
890
891

      // Print the acceptance as text.  The set_printer function can
      // be used to implement customized output for set numbers.
      std::ostream&
      to_text(std::ostream& os,
892
893
              std::function<void(std::ostream&, int)>
              set_printer = nullptr) const;
894

895
896
897
898
899
900
901
      // Print the acceptance as Latex.  The set_printer function can
      // be used to implement customized output for set numbers.
      std::ostream&
      to_latex(std::ostream& os,
               std::function<void(std::ostream&, int)>
               set_printer = nullptr) const;

902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933

      /// \brief Construct an acc_code from a string.
      ///
      /// The string can follow the following grammar:
      ///
      /// <pre>
      ///   acc ::= "t"
      ///         | "f"
      ///         | "Inf" "(" num ")"
      ///         | "Fin" "(" num ")"
      ///         | "(" acc ")"
      ///         | acc "&" acc
      ///         | acc "|" acc
      /// </pre>
      ///
      /// Where num is an integer and "&" has priority over "|".  Note that
      /// "Fin(!x)" and "Inf(!x)" are not supported by this parser.
      ///
      /// Or the string can be the name of an acceptance condition, as
      /// speficied in the HOA format.  (E.g. "Rabin 2", "parity max odd 3",
      /// "generalized-Rabin 4 2 1", etc.).
      ///
      /// A spot::parse_error is thrown on syntax error.
      acc_code(const char* input);

      /// \brief Build an empty acceptance condition.
      ///
      /// This is the same as t().
      acc_code()
      {
      }

934
      // Calls to_text
935
936
      SPOT_API
      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
944
945
946
947
948
949
950
      uses_fin_acceptance_ = check_fin_acceptance();
    }

    acc_cond(const acc_code& code)
      : num_(0U), all_(0U), code_(code)
    {
      add_sets(code.used_sets().max_set());
      uses_fin_acceptance_ = check_fin_acceptance();
951
952
953
    }

    acc_cond(const acc_cond& o)
954
955
      : num_(o.num_), all_(o.all_), code_(o.code_),
        uses_fin_acceptance_(o.uses_fin_acceptance_)
956
957
958
    {
    }

959
960
961
962
963
964
965
966
967
    acc_cond& operator=(const acc_cond& o)
    {
      num_ = o.num_;
      all_ = o.all_;
      code_ = o.code_;
      uses_fin_acceptance_ = o.uses_fin_acceptance_;
      return *this;
    }

968
969
970
971
    ~acc_cond()
    {
    }

972
973
974
975
976
977
    void set_acceptance(const acc_code& code)
    {
      code_ = code;
      uses_fin_acceptance_ = check_fin_acceptance();
    }

978
    const acc_code& get_acceptance() const
979
980
981
982
    {
      return code_;
    }

983
984
985
986
987
    acc_code& get_acceptance()
    {
      return code_;
    }

988
989
990
991
992
    bool uses_fin_acceptance() const
    {
      return uses_fin_acceptance_;
    }

993
    bool is_t() const
994
    {
995
      return code_.is_t();
996
997
    }

998
    bool is_all() const
999
    {
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
      return num_ == 0 && is_t();
    }

    bool is_f() const
    {
      return code_.is_f();
    }

    bool is_none() const
    {
      return num_ == 0 && is_f();
1011
1012
1013
1014
1015
1016
    }

    bool is_buchi() const
    {
      unsigned s = code_.size();
      return num_ == 1 &&
1017
        s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
1018
1019
1020
1021
1022
1023
1024
    }

    bool is_co_buchi() const
    {
      return num_ == 1 && is_generalized_co_buchi();
    }

1025
1026
1027
1028
1029
1030
1031
1032
    void set_generalized_buchi()
    {
      set_acceptance(inf(all_sets()));
    }

    bool is_generalized_buchi() const
    {
      unsigned s = code_.size();
1033
1034
      return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
                                       && code_[0].mark == all_sets());
1035
1036
    }

1037
1038
1039
1040
    bool is_generalized_co_buchi() const
    {
      unsigned s = code_.size();
      return (s == 2 &&
1041
              code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
1042
1043
1044
1045
1046
1047
1048
    }

    // Returns a number of pairs (>=0) if Rabin, or -1 else.
    int is_rabin() const;
    // Returns a number of pairs (>=0) if Streett, or -1 else.
    int is_streett() const;

1049
1050
1051
1052
1053
1054
1055
1056
1057
    /// \brief Rabin/streett pairs used by is_rabin_like and is_streett_like.
    ///
    /// These pairs hold two marks which can each contain one or no set.
    ///
    /// For instance is_streett_like() rewrites  Inf(0)&(Inf(2)|Fin(1))&Fin(3)
    /// as three pairs: [(fin={},inf={0}),(fin={1},inf={2}),(fin={3},inf={})].
    ///
    /// Empty marks should be interpreted in a way that makes them
    /// false in Streett, and true in Rabin.
1058
1059
1060
    struct SPOT_API rs_pair
    {
      rs_pair() = default;
1061
      rs_pair(const rs_pair&) = default;
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099

      rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf):
        fin(fin),
        inf(inf)
        {}
      acc_cond::mark_t fin;
      acc_cond::mark_t inf;

      bool operator==(rs_pair o) const
      {
        return fin == o.fin && inf == o.inf;
      }
      bool operator!=(rs_pair o) const
      {
        return fin != o.fin || inf != o.inf;
      }
      bool operator<(rs_pair o) const
      {
        return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
      }
      bool operator<=(rs_pair o) const
      {
        return !(o < *this);
      }
      bool operator>(rs_pair o) const
      {
        return o < *this;
      }
      bool operator>=(rs_pair o) const
      {
        return !(*this < o);
      }
    };
    /// \brief Test whether an acceptance condition is Streett-like
    ///  and returns each Streett pair in an std::vector<rs_pair>.
    ///
    /// An acceptance condition is Streett-like if it can be transformed into
    /// a Streett acceptance with little modification to its automaton.
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
1100
    /// A Streett-like acceptance condition follows one of those rules:
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
    /// -It is a conjunction of disjunctive clauses containing at most one
    ///  Inf and at most one Fin.
    /// -It is true (with 0 pair)
    /// -It is false (1 pair [0U, 0U])
    bool is_streett_like(std::vector<rs_pair>& pairs) const;

    /// \brief Test whether an acceptance condition is Rabin-like
    ///  and returns each Rabin pair in an std::vector<rs_pair>.
    ///
    /// An acceptance condition is Rabin-like if it can be transformed into
    /// a Rabin acceptance with little modification to its automaton.
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
1112
    /// A Rabin-like acceptance condition follows one of those rules:
1113
1114
1115
1116
1117
1118
    /// -It is a disjunction of conjunctive clauses containing at most one
    ///  Inf and at most one Fin.
    /// -It is true (1 pair [0U, 0U])
    /// -It is false (0 pairs)
    bool is_rabin_like(std::vector<rs_pair>& pairs) const;

1119
1120
1121
    // Return the number of Inf in each pair.
    bool is_generalized_rabin(std::vector<unsigned>& pairs) const;

1122
1123
1124
1125
1126
1127
    // If EQUIV is false, this return true iff the acceptance
    // condition is a parity condition written in the canonical way
    // given in the HOA specifications.  If EQUIV is true, then we
    // check whether the condition is logically equivalent to some
    // parity acceptance condition.
    bool is_parity(bool& max, bool& odd, bool equiv = false) const;
1128
1129
1130
    bool is_parity() const
    {
      bool max;
Maximilien Colange's avatar
Typos    
Maximilien Colange committed
1131
1132
      bool odd;
      return is_parity(max, odd);
1133
    }
1134

1135
1136
1137
1138
1139
    // Return (true, m) if there exist some acceptance mark m that
    // does not satisfy the acceptance condition.  Return (false, 0U)
    // otherwise.
    std::pair<bool, acc_cond::mark_t> unsat_mark() const;

1140
1141
1142
  protected:
    bool check_fin_acceptance() const;

1143
  public:
1144
    static acc_code inf(mark_t mark)
1145
    {
1146
      return acc_code::inf(mark);
1147
1148
    }

1149
    static acc_code inf(std::initializer_list<unsigned> vals)
1150
    {
1151
      return inf(mark_t(vals.begin(), vals.end()));
1152
1153
    }

1154
    static acc_code inf_neg(mark_t mark)
1155
    {
1156
      return acc_code::inf_neg(mark);
1157
1158
    }

1159
    static acc_code inf_neg(std::initializer_list<unsigned> vals)
1160
    {
1161
      return inf_neg(mark_t(vals.begin(), vals.end()));
1162
1163
    }

1164
    static acc_code fin(mark_t mark)