twasafracomplement.cc 34.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19
20
21
22
23
24

#include <set>
#include <map>
#include <deque>
#include <cassert>
#include <sstream>
25
#include <algorithm>
26
#include <spot/misc/bitvect.hh>
27
#include <bddx.h>
28
29
30
31
32
33
34
35
36
#include <spot/misc/hash.hh>
#include <spot/misc/bddlt.hh>
#include <spot/twa/bdddict.hh>
#include <spot/twa/twa.hh>
#include <spot/misc/hashfunc.hh>
#include <spot/tl/formula.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twa/twasafracomplement.hh>
#include <spot/twaalgos/degen.hh>
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51

namespace spot
{
  namespace
  {
    // forward decl.
    struct safra_tree;
    struct safra_tree_ptr_less_than:
      public std::binary_function<const safra_tree*, const safra_tree*, bool>
    {
      bool
      operator()(const safra_tree* left,
                 const safra_tree* right) const;
    };

52
53
54
    /// \brief Automaton with Safra's tree as states.
    struct safra_tree_automaton
    {
55
      safra_tree_automaton(const const_twa_graph_ptr& sba);
56
57
58
59
60
61
62
63
64
65
66
67
      ~safra_tree_automaton();
      typedef std::map<bdd, const safra_tree*, bdd_less_than> transition_list;
      typedef
      std::map<safra_tree*, transition_list, safra_tree_ptr_less_than>
      automaton_t;
      automaton_t automaton;

      /// \brief The number of acceptance pairs of this Rabin (Streett)
      /// automaton.
      int get_nb_acceptance_pairs() const;
      safra_tree* get_initial_state() const;
      void set_initial_state(safra_tree* s);
68
      const const_twa_graph_ptr& get_sba(void) const
69
70
71
      {
	return a_;
      }
72
73
74
    private:
      mutable int max_nb_pairs_;
      safra_tree* initial_state;
75
      const_twa_graph_ptr a_;
76
    };
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104

    /// \brief A Safra tree, used as state during the determinization
    /// of a Büchi automaton
    ///
    /// It is the key structure of the construction.
    /// Each node of the tree has:
    ///  - A \a name,
    ///  - A subset of states of the original Büchi automaton (\a nodes),
    ///  - A flag that is \a marked to denote vertical merge of nodes,
    ///  - A list of \a children.
    ///
    /// This class implements operations:
    ///  - To compute the successor of this tree,
    ///  - To retrive acceptance condition on this tree.
    /// \see safra_determinisation.
    struct safra_tree
    {
      typedef std::set<const state*, state_ptr_less_than> subset_t;
      typedef std::list<safra_tree*> child_list;
      typedef std::multimap<bdd, const state*, bdd_less_than> tr_cache_t;
      typedef std::map<const state*, tr_cache_t,
                       state_ptr_less_than> cache_t;

      safra_tree();
      safra_tree(const safra_tree& other);
      safra_tree(const subset_t& nodes, safra_tree* p, int n);
      ~safra_tree();

105
      safra_tree& operator=(const safra_tree& other);
106
      int compare(const safra_tree* other) const;
107
      size_t hash() const;
108
109
110
111
112

      void add_node(const state* s);
      int max_name() const;

      // Operations to get successors of a tree.
113
      safra_tree* branch_accepting(const twa_graph& a);
114
115
116
117
118
119
120
      safra_tree* succ_create(const bdd& condition,
                              cache_t& cache_transition);
      safra_tree* normalize_siblings();
      safra_tree* remove_empty();
      safra_tree* mark();

      // To get Rabin/Streett acceptance conditions.
121
122
      void getL(bitvect& bitset) const;
      void getU(bitvect& bitset) const;
123

124
125
      /// \brief Is this node the root of the tree?
      bool is_root() const
126
      {
127
        return parent == nullptr;
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
      }

      bool marked;
      int name;
      subset_t nodes;
      child_list children;
    private:
      void remove_node_from_children(const state* state);
      int get_new_name() const;
      mutable std::deque<int> free_names_; // Some free names.
      safra_tree* parent;
    };

    safra_tree::safra_tree()
      : marked(false), name(0)
    {
144
      parent = nullptr;
145
146
147
148
    }

    /// \brief Copy the tree \a other, and set \c marked to false.
    safra_tree::safra_tree(const safra_tree& other)
149
      : marked(false), name(other.name), nodes(other.nodes)
150
    {
151
      parent = nullptr;
152
      for (auto i: other.children)
153
      {
154
        safra_tree* c = new safra_tree(*i);
155
156
157
158
159
160
161
162
163
164
165
166
167
        c->parent = this;
        children.push_back(c);
      }
    }

    safra_tree::safra_tree(const subset_t& nodes, safra_tree* p, int n)
      : marked(false), name(n), nodes(nodes)
    {
      parent = p;
    }

    safra_tree::~safra_tree()
    {
168
169
170
171
      for (auto c: children)
        delete c;
      for (auto n: nodes)
        n->destroy();
172
173
174
175
    }

    /// \brief Compare two safra trees.
    ///
176
    /// \param other the tree to compare too.
177
178
179
180
181
    ///
    /// \return 0 if the trees are the same. Otherwise
    /// a signed value.
    int safra_tree::compare(const safra_tree* other) const
    {
182
183
184
      int res = name - other->name;
      if (res != 0)
	return res;
185

186
187
      if (marked != other->marked)
        return (marked) ? -1 : 1;
188

189
190
191
      res = nodes.size() - other->nodes.size();
      if (res != 0)
	return res;
192

193
194
195
      res = children.size() - other->children.size();
      if (res != 0)
      	return res;
196

197
198
199
200
201
202
203
      // Call compare() only as a last resort, because it takes time.

      subset_t::const_iterator in1 = nodes.begin();
      subset_t::const_iterator in2 = other->nodes.begin();
      for (; in1 != nodes.end(); ++in1, ++in2)
        if ((res = (*in1)->compare(*in2)) != 0)
	  return res;
204
205
206

      child_list::const_iterator ic1 = children.begin();
      child_list::const_iterator ic2 = other->children.begin();
207
208
209
      for (; ic1 != children.end(); ++ic1, ++ic2)
	if ((res = (*ic1)->compare(*ic2)) != 0)
	  return res;
210
211
212
213

      return 0;
    }

214
215
216
217
218
219
220
221
222

    /// \brief Hash a safra tree.
    size_t
    safra_tree::hash() const
    {
      size_t hash = 0;
      hash ^= wang32_hash(name);
      hash ^= wang32_hash(marked);

223
224
225
226
      for (auto n: nodes)
        hash ^= n->hash();
      for (auto c: children)
        hash ^= c->hash();
227
228
229
230

      return hash;
    }

231
232
233
234
235
236
237
238
239
240
241
242
243
244
    void
    safra_tree::add_node(const state* s)
    {
      nodes.insert(s);
    }

    /*---------------------------------.
    | Operations to compute successors |
    `---------------------------------*/

    int
    safra_tree::max_name() const
    {
      int max_name = name;
245
246
      for (auto c: children)
        max_name = std::max(max_name, c->max_name());
247
248
249
      return max_name;
    }

250
    /// \brief Get a unused name in the tree for a new node.
251
252
253
254
255
256
    ///
    /// The root of the tree maintains a list of unused names.
    /// When this list is empty, new names are computed.
    int
    safra_tree::get_new_name() const
    {
257
      if (parent == nullptr)
258
259
260
261
262
263
264
265
266
267
268
      {
        if (free_names_.empty())
        {
          std::set<int> used_names;
          std::deque<const safra_tree*> queue;
          queue.push_back(this);
          while (!queue.empty())
          {
            const safra_tree* current = queue.front();
            queue.pop_front();
            used_names.insert(current->name);
269
270
	    for (auto c: current->children)
              queue.push_back(c);
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
          }

          int l = 0;
          int nb_found = 0;
          std::set<int>::const_iterator i = used_names.begin();
          while (i != used_names.end() && nb_found != 3)
          {
            if (l != *i)
            {
              free_names_.push_back(l);
              ++nb_found;
            }
            else
              ++i;
            ++l;
          }

          while (nb_found++ < 3)
            free_names_.push_back(l++);
        }

        int result = free_names_.front();
        free_names_.pop_front();
        return result;
      }
      else
        return parent->get_new_name();
    }

    /// If the node has an accepting state in its label, a new child
    /// is inserted with the set of all accepting states of \c nodes
    /// as label and an unused name.
    safra_tree*
304
    safra_tree::branch_accepting(const twa_graph& a)
305
    {
306
307
      for (auto c: children)
        c->branch_accepting(a);
308
309

      subset_t subset;
310
311
312
      for (auto n: nodes)
        if (a.state_is_accepting(n))
          subset.insert(n);
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334

      if (!subset.empty())
        children.push_back(new safra_tree(subset, this, get_new_name()));

      return this;
    }

    /// \brief A powerset construction.
    ///
    /// The successors of each state in \c nodes with \a condition
    /// as atomic property remplace the current \c nodes set.
    ///
    /// @param cache_transition is a map of the form: state -> bdd -> state.
    ///        Only states present in \c nodes are keys of the map.
    /// @param condition is an atomic property. We are looking for successors
    ///        of this atomic property.
    safra_tree*
    safra_tree::succ_create(const bdd& condition,
                            cache_t& cache_transition)
    {
      subset_t new_subset;

335
      for (auto n: nodes)
336
      {
337
	cache_t::const_iterator it = cache_transition.find(n);
338
        if (it == cache_transition.end())
339
340
          continue;

341
        const tr_cache_t& transitions = it->second;
342
        for (auto t: transitions)
343
        {
344
          if ((t.first & condition) != bddfalse)
345
          {
346
            if (new_subset.find(t.second) == new_subset.end())
347
            {
348
              const state* s = t.second->clone();
349
350
351
352
353
              new_subset.insert(s);
            }
          }
        }
      }
354
      std::swap(nodes, new_subset);
355

356
357
      for (auto c: children)
        c->succ_create(condition, cache_transition);
358
359
360
361
362
363
364
365
366
367
368
369

      return this;
    }

    /// \brief Horizontal Merge
    ///
    /// If many children share the same state in their labels, we must keep
    /// only one occurrence (in the older node).
    safra_tree*
    safra_tree::normalize_siblings()
    {
      std::set<const state*, state_ptr_less_than> node_set;
370
      for (auto c: children)
371
      {
372
373
        subset_t::iterator node_it = c->nodes.begin();
        while (node_it != c->nodes.end())
374
        {
375
376
	  if (!node_set.insert(*node_it).second)
	  {
377
            const state* s = *node_it;
378
379
            c->remove_node_from_children(*node_it);
            c->nodes.erase(node_it++);
380
            s->destroy();
381
          }
382
383
384
385
	  else
	  {
	    ++node_it;
	  }
386
387
        }

388
        c->normalize_siblings();
389
390
391
392
393
394
395
396
397
      }

      return this;
    }

    /// \brief Remove recursively all the occurrences of \c state in the label.
    void
    safra_tree::remove_node_from_children(const state* state)
    {
398
      for (auto c: children)
399
      {
400
401
        subset_t::iterator it = c->nodes.find(state);
        if (it != c->nodes.end())
402
403
        {
          const spot::state* s = *it;
404
	  c->nodes.erase(it);
405
          s->destroy();
406
        }
407
        c->remove_node_from_children(state);
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
      }
    }

    /// \brief Remove empty nodes
    ///
    /// If a child of the node has an empty label, we remove this child.
    safra_tree*
    safra_tree::remove_empty()
    {
      child_list::iterator child_it = children.begin();
      while (child_it != children.end())
      {
        if ((*child_it)->nodes.empty())
        {
          safra_tree* to_delete = *child_it;
          child_it = children.erase(child_it);
          delete to_delete;
        }
        else
        {
          (*child_it)->remove_empty();
          ++child_it;
        }
      }

      return this;
    }

    /// \brief Vertical merge
    ///
    /// If a parent has the same states as its childen in its label,
    /// All the children a deleted and the node is marked. This mean
    /// an accepting infinite run is found.
    safra_tree*
    safra_tree::mark()
    {
      std::set<const state*, state_ptr_less_than> node_set;
445
      for (auto c: children)
446
      {
447
448
        node_set.insert(c->nodes.begin(), c->nodes.end());
        c->mark();
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
      }

      char same = node_set.size() == nodes.size();

      if (same)
      {
        subset_t::const_iterator i = node_set.begin();
        subset_t::const_iterator j = nodes.begin();

        while (i != node_set.end() && j != nodes.end())
        {
          if ((*i)->compare(*j) != 0)
          {
            same = 0;
            break;
          }
          ++i;
          ++j;
        }
      }

      if (same)
      {
        marked = true;
473
474
        for (auto c: children)
          delete c;
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
        children = child_list();
      }

      return this;
    }

    /*-----------------------.
    | Acceptances conditions |
    `-----------------------*/

    /// Returns in which sets L (the semantic differs according to Rabin or
    /// Streett) the state-tree is included.
    ///
    /// \param bitset a bitset of size \c this->get_nb_acceptance_pairs()
    /// filled with FALSE bits.
490
    /// On return bitset[i] will be set if this state-tree is included in L_i.
491
    void
492
    safra_tree::getL(bitvect& bitset) const
493
494
495
    {
      assert(bitset.size() > static_cast<unsigned>(name));
      if (marked && !nodes.empty())
496
        bitset.set(name);
497
498
      for (auto c: children)
        c->getL(bitset);
499
500
501
502
503
504
505
    }

    /// Returns in which sets U (the semantic differs according to Rabin or
    /// Streett) the state-tree is included.
    ///
    /// \param bitset a bitset of size \c this->get_nb_acceptance_pairs()
    /// filled with TRUE bits.
506
    /// On return bitset[i] will be set if this state-tree is included in U_i.
507
    void
508
    safra_tree::getU(bitvect& bitset) const
509
510
511
    {
      assert(bitset.size() > static_cast<unsigned>(name));
      if (!nodes.empty())
512
        bitset.clear(name);
513
514
      for (auto c: children)
        c->getU(bitset);
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
    }

    bool
    safra_tree_ptr_less_than::operator()(const safra_tree* left,
                                         const safra_tree* right) const
    {
      assert(left);
      return left->compare(right) < 0;
    }

    struct safra_tree_ptr_equal:
      public std::unary_function<const safra_tree*, bool>
    {
      safra_tree_ptr_equal(const safra_tree* left)
        : left_(left) {}

      bool
      operator()(const safra_tree* right) const
      {
        return left_->compare(right) == 0;
      }
    private:
      const safra_tree* left_;
    };

    /// \brief Algorithm to determinize Büchi automaton.
    ///
    /// Determinization of a Büchi automaton into a Rabin automaton
    /// using the Safra's construction.
    ///
    /// This construction is presented in:
    /// @PhDThesis{      safra.89.phd,
    ///     author     = {Shmuel Safra},
    ///     title      = {Complexity of Automata on Infinite Objects},
    ///     school     = {The Weizmann Institute of Science},
    ///     year       = {1989},
    ///     address    = {Rehovot, Israel},
    ///     month      = mar
    /// }
    ///
    class safra_determinisation
    {
    public:
558
      static safra_tree_automaton*
559
      create_safra_automaton(const const_twa_graph_ptr& a);
560
561
562
    private:
      typedef std::set<int> atomic_list_t;
      typedef std::set<bdd, bdd_less_than> conjunction_list_t;
563
      static void retrieve_atomics(const safra_tree* node,
564
				   twa_graph_ptr sba_aut,
565
566
567
568
569
570
571
572
573
                                   safra_tree::cache_t& cache,
                                   atomic_list_t& atomic_list);
      static void set_atomic_list(atomic_list_t& list, bdd condition);
      static conjunction_list_t
      get_conj_list(const atomic_list_t& atomics);
    };

    /// \brief The body of Safra's construction.
    safra_tree_automaton*
574
    safra_determinisation::create_safra_automaton
575
    (const const_twa_graph_ptr& a)
576
577
    {
      // initialization.
578
      auto sba_aut = degeneralize(a);
579

580
      safra_tree_automaton* st = new safra_tree_automaton(sba_aut);
581
582
583

      std::deque<safra_tree*> queue;
      safra_tree* q0 = new safra_tree();
584
      q0->add_node(sba_aut->get_init_state());
585
586
587
588
589
590
591
592
593
594
595
596
      queue.push_back(q0);
      st->set_initial_state(q0);

      // main loop
      while (!queue.empty())
      {
        safra_tree* current = queue.front();
        // safra_tree* node = new safra_tree(*current);

        // Get conjunction list and save successors.
        safra_tree::cache_t cache;
        atomic_list_t atomic_list;
597
        retrieve_atomics(current, sba_aut, cache, atomic_list);
598
599
600
601
        conjunction_list_t conjunction = get_conj_list(atomic_list);

        // Create successors of the Safra's tree.
        safra_tree_automaton::transition_list transitions;
602
        for (auto i: conjunction)
603
604
        {
          safra_tree* successor = new safra_tree(*current);
605
          successor->branch_accepting(*sba_aut); // Step 2
606
          successor->succ_create(i, cache); // Step 3
607
608
609
610
611
612
613
614
          successor->normalize_siblings(); // Step 4
          successor->remove_empty(); // Step 5
          successor->mark(); // Step 6

          bool delete_this_successor = true;
          safra_tree_ptr_equal comparator(successor);
          if (st->automaton.find(successor) != st->automaton.end())
          {
615
            transitions[i] = st->automaton.find(successor)->first;
616
617
618
619
620
621
622
          }
          else
          {
            std::deque<safra_tree*>::iterator item_in_queue =
              std::find_if(queue.begin(), queue.end(), comparator);
            if (item_in_queue != queue.end())
            {
623
              transitions[i] = *item_in_queue;
624
625
626
627
            }
            else
            {
              delete_this_successor = false;
628
              transitions[i] = successor;
629
630
631
632
633
634
635
636
637
638
639
640
              queue.push_back(successor);
            }
          }
          if (delete_this_successor)
            delete successor;
        }

        if (st->automaton.find(current) == st->automaton.end())
          st->automaton[current] = transitions;

        queue.pop_front();

641
642
643
        for (auto i: cache)
          for (auto j: i.second)
            j.second->destroy();
644
645
646
        // delete node;
      }

647
      // delete sba_aut;
648
649
650
651
652
653
654
      return st;
    }

    /// Retrieve all atomics properties that are in successors formulae
    /// of the states in the label of the node.
    void
    safra_determinisation::retrieve_atomics(const safra_tree* node,
655
                                            twa_graph_ptr sba_aut,
656
657
658
                                            safra_tree::cache_t& cache,
                                            atomic_list_t& atomic_list)
    {
659
      for (auto n: node->nodes)
660
661
      {
        safra_tree::tr_cache_t transitions;
662
	for (auto iterator: sba_aut->succ(n))
663
        {
664
          bdd condition = iterator->cond();
665
          typedef std::pair<bdd, const state*> bdd_state;
666
          transitions.insert(bdd_state(condition, iterator->dst()));
667
668
          set_atomic_list(atomic_list, condition);
        }
669
        cache[n] = transitions;
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
      }
    }

    /// Insert in \a list atomic properties of the formula \a c.
    void
    safra_determinisation::set_atomic_list(atomic_list_t& list, bdd c)
    {
      bdd current = bdd_satone(c);
      while (current != bddtrue && current != bddfalse)
      {
        list.insert(bdd_var(current));
        bdd high = bdd_high(current);
        if (high == bddfalse)
          current = bdd_low(current);
        else
          current = high;
      }
    }

    /// From the list of atomic properties \a atomics, create the list
    /// of all the conjunctions of properties.
    safra_determinisation::conjunction_list_t
    safra_determinisation::get_conj_list(const atomic_list_t& atomics)
    {
      conjunction_list_t list;
      unsigned atomics_size = atomics.size();

      assert(atomics_size < 32);
      for (unsigned i = 1; i <= static_cast<unsigned>(1 << atomics_size); ++i)
      {
        bdd result = bddtrue;
        unsigned position = 1;
702
        for (auto a: atomics)
703
704
705
        {
          bdd this_atomic;
          if (position & i)
706
            this_atomic = bdd_ithvar(a);
707
          else
708
709
710
            this_atomic = bdd_nithvar(a);
          result &= this_atomic;
	  position <<= 1;
711
712
713
714
715
716
717
718
719
720
721
        }
        list.insert(result);
      }

      return list;
    }

    // Safra's test part. Dot output.
    //////////////////////////////
    namespace test
    {
722
      typedef state_map<int> stnum_t;
723

724
      void print_safra_tree(const safra_tree* this_node,
725
                            stnum_t& node_names,
726
727
728
729
                            int& current_node,
                            int nb_accepting_conditions)
      {
        std::string conditions;
730
        if (this_node->is_root())
731
        {
732
733
734
735
736
          bitvect* l = make_bitvect(nb_accepting_conditions);
	  bitvect* u = make_bitvect(nb_accepting_conditions);
          u->set_all();
          this_node->getL(*l);
          this_node->getU(*u);
737
          std::stringstream s;
738
          s << "\\nL:" << *l << ", U:" << *u;
739
          conditions = s.str();
740
741
	  delete u;
	  delete l;
742
743
744
        }

        std::cout << "node" << this_node << "[label=\"";
745
        std::cout << this_node->name << '|';
746
        for (auto j: this_node->nodes)
747
        {
748
	  stnum_t::const_iterator it = node_names.find(j);
749
750
	  int name;
          if (it == node_names.end())
751
	    name = node_names[j] = current_node++;
752
753
754
	  else
	    name = it->second;
          std::cout << name << ", ";
755
756
757
        }
        std::cout << conditions;
        if (this_node->marked)
758
          std::cout << "\", style=filled, fillcolor=\"gray";
759
760
761
762
763
764
765
766
767

        std::cout << "\"];" << std::endl;

        safra_tree::child_list::const_iterator i = this_node->children.begin();
        for (; i != this_node->children.end(); ++i)
        {
          print_safra_tree(*i, node_names, current_node,
                           nb_accepting_conditions);
          std::cout << "node" << this_node << " -> node" << *i
768
                    << "[color=\"red\", arrowhead=\"none\"];"
769
770
771
772
773
774
                    << std::endl;
        }
      }

      void print_safra_automaton(safra_tree_automaton* a)
      {
775
        typedef safra_tree_automaton::automaton_t::reverse_iterator
776
          automaton_cit;
777
        stnum_t node_names;
778
779
780
781
782
        int current_node = 0;
        int nb_accepting_conditions = a->get_nb_acceptance_pairs();

        std::cout << "digraph A {" << std::endl;

783
784
	/// GCC 3.3 complains if a const_reverse_iterator is used.
	/// error: no match for 'operator!='
785
786
787
788
        for (automaton_cit i = a->automaton.rbegin();
             i != a->automaton.rend();
             ++i)
        {
789
          std::cout << "subgraph sg" << i->first << '{' << std::endl;
790
791
          print_safra_tree(i->first, node_names, current_node,
                           nb_accepting_conditions);
792
          std::cout << "}\n";
793
794

          // Successors.
795
          for (const auto& j: i->second)
796
            std::cout << "node" << i->first << "->"
797
                      << "node" << j.second <<
798
              " [label=\"" << bddset << j.first << "\"];\n";
799
800
        }

801
802
803
804
	// Output the real name of all states.
	std::cout << "{ rank=sink; legend [shape=none,margin=0,label=<\n"
		  << "<TABLE BORDER='1' CELLBORDER='0' CELLSPACING='0'>\n";

805
806
807
	for (const auto& nn: node_names)
	  std::cout << "<TR><TD>" << nn.second << "</TD><TD>"
		    << a->get_sba()->format_state(nn.first)
808
		    << "</TD></TR>\n";
809
	std::cout << "</TABLE>\n>]}\n}\n";
810
811
812
813
814
815
      }
    } // test

    ////////////////////////////////////////
    // state_complement

816
    /// States used by spot::tgba_safra_complement.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
817
    /// \ingroup twa_representation
818
819
820
    class state_complement : public state
    {
    public:
821
      state_complement(bitvect* U, bitvect* L, const safra_tree* tree,
822
823
                       bool use_bitset = true);
      state_complement(const state_complement& other);
824
      virtual ~state_complement();
825
826
827
828
829
830
831
832

      /// \return the safra tree associated to this state.
      const safra_tree* get_safra() const
      {
        return tree;
      }

      /// \return in which sets U this state is included.
833
      const bitvect& get_U() const
834
      {
835
        return *U;
836
837
838
      }

      /// \return in which sets L this state is included.
839
      const bitvect& get_L() const
840
      {
841
        return *L;
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
      }

      /// \return whether this state track an infinite run.
      bool get_use_bitset() const
      {
        return use_bitset;
      }

      virtual int compare(const state* other) const;
      virtual size_t hash() const;
      virtual state_complement* clone() const;

      std::string to_string() const;
      const state* get_state() const;
    private:
857
858
      bitvect* U;
      bitvect* L;
859
860
861
862
      const safra_tree* tree;
      bool use_bitset;
    };

863
    state_complement::state_complement(bitvect* L, bitvect* U,
864
865
                                       const safra_tree* tree,
                                       bool use_bitset)
866
      : state(), U(U), L(L), tree(tree), use_bitset(use_bitset)
867
868
869
870
    {
    }

    state_complement::state_complement(const state_complement& other)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
871
      : state()
872
    {
873
874
      U = other.U->clone();
      L = other.L->clone();
875
876
877
878
      tree = other.tree;
      use_bitset = other.use_bitset;
    }

879
880
881
882
883
884
    state_complement::~state_complement()
    {
      delete U;
      delete L;
    }

885
886
887
888
889
    int
    state_complement::compare(const state* other) const
    {
      if (other == this)
        return 0;
890
      const state_complement* s = down_cast<const state_complement*>(other);
891
      assert(s);
892
893
#if TRANSFORM_TO_TBA
      // When we transform to TBA instead of TGBA, states depend on the U set.
894
895
      if (*U != *s->U)
        return (*U < *s->U) ? -1 : 1;
896
#endif
897
898
      if (*L != *s->L)
        return (*L < *s->L) ? -1 : 1;
899
900
901
902
903
904
905
906
      if (use_bitset != s->use_bitset)
        return use_bitset - s->use_bitset;
      return tree->compare(s->tree);
    }

    size_t
    state_complement::hash() const
    {
907
908
      size_t hash = tree->hash();
      hash ^= wang32_hash(use_bitset);
909
      hash ^= L->hash();
910
#if TRANSFORM_TO_TBA
911
      hash ^= U->hash();
912
#endif
913
      return hash;
914
915
916
917
918
919
920
921
922
923
924
925
926
927
    }

    state_complement*
    state_complement::clone() const
    {
      return new state_complement(*this);
    }

    std::string
    state_complement::to_string() const
    {
      std::stringstream ss;
      ss << tree;
      if (use_bitset)
928
      {
929
        ss << " - I:" << *L;
930
#if TRANSFORM_TO_TBA
931
        ss << " J:" << *U;
932
933
#endif
      }
934
935
936
      return ss.str();
    }

937
    /// Successor iterators used by spot::tgba_safra_complement.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
938
    /// \ingroup twa_representation
939
    class twa_safra_complement_succ_iterator: public twa_succ_iterator
940
941
942
943
    {
    public:
      typedef std::multimap<bdd, state_complement*, bdd_less_than> succ_list_t;

944
      twa_safra_complement_succ_iterator(const succ_list_t& list,
945
                                          acc_cond::mark_t the_acceptance_cond)
946
947
948
949
950
        : list_(list), the_acceptance_cond_(the_acceptance_cond)
      {
      }

      virtual
951
      ~twa_safra_complement_succ_iterator()
952
      {
953
954
        for (auto& p: list_)
          delete p.second;
955
956
      }

957
958
      virtual bool first();
      virtual bool next();
959
      virtual bool done() const;
960
961
962
      virtual state_complement* dst() const;
      virtual bdd cond() const;
      virtual acc_cond::mark_t acc() const;
963
964
    private:
      succ_list_t list_;
965
      acc_cond::mark_t the_acceptance_cond_;
966
967
968
      succ_list_t::const_iterator it_;
    };

969
    bool
970
    twa_safra_complement_succ_iterator::first()
971
972
    {
      it_ = list_.begin();
973
      return it_ != list_.end();
974
975
    }

976
    bool
977
    twa_safra_complement_succ_iterator::next()
978
979
    {
      ++it_;
980
      return it_ != list_.end();
981
982
983
    }

    bool
984
    twa_safra_complement_succ_iterator::done() const
985
986
987
988
989
    {
      return it_ == list_.end();
    }

    state_complement*
990
    twa_safra_complement_succ_iterator::dst() const
991
992
993
994
995
996
    {
      assert(!done());
      return new state_complement(*(it_->second));
    }

    bdd
997
    twa_safra_complement_succ_iterator::cond() const
998
999
1000
1001
1002
    {
      assert(!done());
      return it_->first;
    }

1003
    acc_cond::mark_t
1004
    twa_safra_complement_succ_iterator::acc() const
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
    {
      assert(!done());
      return the_acceptance_cond_;
    }

  } // anonymous

  // safra_tree_automaton
  ////////////////////////

1015
  safra_tree_automaton::safra_tree_automaton(const const_twa_graph_ptr& a)
1016
    : max_nb_pairs_(-1), initial_state(nullptr), a_(a)
1017
1018
1019
1020
1021
1022
  {
    a->get_dict()->register_all_variables_of(a, this);
  }

  safra_tree_automaton::~safra_tree_automaton()
  {
1023
1024
    for (auto& p: automaton)
      delete p.first;
1025
1026
1027
1028
1029
1030
1031
1032
1033
  }

  int
  safra_tree_automaton::get_nb_acceptance_pairs() const
  {
    if (max_nb_pairs_ != -1)
      return max_nb_pairs_;

    int max = -1;
1034
1035
    for (auto& p: automaton)
      max = std::max(max, p.first->max_name());
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
    return max_nb_pairs_ = max + 1;
  }

  safra_tree*
  safra_tree_automaton::get_initial_state() const
  {
    return initial_state;
  }

  void
  safra_tree_automaton::set_initial_state(safra_tree* s)
  {
    initial_state = s;
  }

  // End of the safra construction
  //////////////////////////////////////////

1054
  // tgba_safra_complement
1055
1056
  //////////////////////////

1057
  tgba_safra_complement::tgba_safra_complement(const const_twa_graph_ptr& a)
1058
    : twa(a->get_dict()), automaton_(a),
1059
      safra_(safra_determinisation::create_safra_automaton(a))
1060
  {
1061
    assert(safra_ || !"safra construction fails");
1062

1063
#if TRANSFORM_TO_TBA
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1064
    the_acceptance_cond_ = set_buchi();
1065
1066
1067
#endif

#if TRANSFORM_TO_TGBA
1068
1069
    unsigned nb_acc =
      static_cast<safra_tree_automaton*>(safra_)->get_nb_acceptance_pairs();
1070

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1071
    set_generalized_buchi(nb_acc);
1072
1073
    acceptance_cond_vec_.reserve(nb_acc);
    for (unsigned i = 0; i < nb_acc; ++i)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1074
      acceptance_cond_vec_.emplace_back(acc_cond::mark_t{i});
1075
#endif
1076
1077
  }

1078
  tgba_safra_complement::~tgba_safra_complement()
1079
1080
  {
    get_dict()->unregister_all_my_variables(safra_);
1081
    delete static_cast<safra_tree_automaton*>(safra_);
1082
1083
1084
  }

  state*
1085
  tgba_safra_complement::get_init_state() const
1086
  {
1087
    safra_tree_automaton* a = static_cast<safra_tree_automaton*>(safra_);
1088
1089
1090
    bitvect* empty = make_bitvect(a->get_nb_acceptance_pairs());
    return new state_complement(empty->clone(), empty,
				a->get_initial_state(), false);
1091
1092
1093
1094
1095
1096
  }


  /// @brief Compute successors of the state @a local_state, and returns an
  /// iterator on the successors collection.
  ///
1097
  /// The old algorithm is a Deterministic Streett to nondeterministic Büchi
1098
1099
1100
  /// transformation, presented by Christof Löding in his Diploma thesis.
  ///
  /// @MastersThesis{	  loding.98,
1101
  ///   author		= {Christof L\"oding},
1102
  ///   title		= {Methods for the Transformation of omega-Automata:
1103
1104
  ///			  Complexity and Connection to Second Order Logic},
  ///   school		= {University of Kiel},
1105
1106
1107
  ///   year		= {1998}
  /// }
  ///
1108
1109
1110
1111
1112
  ///
  /// The new algorithm produce a TGBA instead of a TBA. This algorithm
  /// comes from:
  ///
  /// @InProceedings{   duret.09.atva,
1113
1114
1115
1116
  ///   author        = {Alexandre Duret-Lutz and Denis Poitrenaud and
  ///                    Jean-Michel Couvreur},
  ///   title         = {On-the-fly Emptiness Check of Transition-based
  ///                    {S}treett Automata},
1117
1118
1119
1120
1121
1122
1123
1124
  ///   booktitle     = {Proceedings of the 7th International Symposium on
  ///                   Automated Technology for Verification and Analysis
  ///                   (ATVA'09)},
  ///   year          = {2009},
  ///   editor        = {Zhiming Liu and Anders P. Ravn},
  ///   series        = {Lecture Notes in Computer Science},
  ///   publisher     = {Springer-Verlag}
  /// }
1125
  twa_succ_iterator*
1126
  tgba_safra_complement::succ_iter(const state* state) const
1127
  {
1128
    const safra_tree_automaton* a = static_cast<safra_tree_automaton*>(safra_);
1129
    const state_complement* s = down_cast<const state_complement*>(state);
1130
1131
    assert(s);
    safra_tree_automaton::automaton_t::const_iterator tr =
1132
      a->automaton.find(const_cast<safra_tree*>(s->get_safra()));
1133

1134
1135
    assert(tr != a->automaton.end());

1136
    acc_cond::mark_t condition = 0U;
1137
    twa_safra_complement_succ_iterator::succ_list_t succ_list;
1138
1139
    int nb_acceptance_pairs = a->get_nb_acceptance_pairs();
    bitvect* e = make_bitvect(nb_acceptance_pairs);
1140

1141
    if (!s->get_use_bitset()) // if \delta'(q, a)
1142
      {
1143
        for (auto& p: tr->second)
1144
1145
1146
1147
1148
	  {
	    state_complement* s1 = new state_complement(e->clone(), e->clone(),
							p.second, false);
	    state_complement* s2 = new state_complement(e->clone(), e->clone(),
							p.second, true);
1149
1150
	    succ_list.emplace(p.first, s1);
	    succ_list.emplace(p.first, s2);
1151
	  }
1152
      }
1153
    else
1154
      {
1155
1156
1157
1158
1159
        bitvect* l = make_bitvect(nb_acceptance_pairs);
        bitvect* u = make_bitvect(nb_acceptance_pairs);
        u->set_all();
        s->get_safra()->getL(*l); // {i : q \in L_i}
        s->get_safra()->getU(*u); // {j : q \in U_i}
1160
1161
1162
        state_complement* st;

#if TRANSFORM_TO_TBA
1163
1164
1165
1166
        bitvect* newI = s->get_L().clone();
	*newI |= *l; // {I' = I \cup {i : q \in L_i}}
        bitvect* newJ = s->get_U().clone();
	*newJ |= *u; // {J' = J \cup {j : q \in U_i}}
1167

1168
1169
	// \delta'((q, I, J), a) if I'\subseteq J'
        if (newI->is_subset_of(*newJ))
1170
1171
1172
1173
1174
	  {
	    for (auto& p: tr->second)
	      {
		st = new state_complement(e->clone(), e->clone(),
					  p.second, true);
1175
		succ_list.emplace(p.first, st);
1176
1177
1178
	      }
	    condition = the_acceptance_cond_;
	  }
1179
        else  // \delta'((q, I, J), a)
1180
1181
1182
1183
	  {
	    for (auto& p: tr->second)
	      {
		st = new state_complement(newI, newJ, p.second, true);
1184
		succ_list.emplace(p.first, st);
1185
1186
	      }
	  }
1187
1188
	delete newI;
	delete newJ;
1189
#else
1190
1191
1192
1193
1194
	// {pending = S \cup {i : q \in L_i} \setminus {j : q \in U_j})}
	const bitvect& S = s->get_L();
        bitvect* pending = S.clone();
	*pending |= *l;
	*pending -= *u;
1195
        for (auto& p: tr->second)