twasafracomplement.cc 34.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 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
723
      typedef std::unordered_map<const state*, int,
				 state_ptr_hash, state_ptr_equal> stnum_t;
724

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

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

        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
769
                    << "[color=\"red\", arrowhead=\"none\"];"
770
771
772
773
774
775
                    << std::endl;
        }
      }

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

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

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

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

802
803
804
805
	// 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";

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

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

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

      /// \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.
834
      const bitvect& get_U() const
835
      {
836
        return *U;
837
838
839
      }

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

      /// \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:
858
859
      bitvect* U;
      bitvect* L;
860
861
862
863
      const safra_tree* tree;
      bool use_bitset;
    };

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

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

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

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

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

    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)
929
      {
930
        ss << " - I:" << *L;
931
#if TRANSFORM_TO_TBA
932
        ss << " J:" << *U;
933
934
#endif
      }
935
936
937
      return ss.str();
    }

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

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

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

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

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

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

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

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

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

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

  } // anonymous

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

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

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

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

    int max = -1;
1035
1036
    for (auto& p: automaton)
      max = std::max(max, p.first->max_name());
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
    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
  //////////////////////////////////////////

1055
  // tgba_safra_complement
1056
1057
  //////////////////////////

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

1064
#if TRANSFORM_TO_TBA
1065
    the_acceptance_cond_ = acc_.mark(acc_.add_set());
1066
1067
1068
#endif

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

1072
1073
    acceptance_cond_vec_.reserve(nb_acc);
    for (unsigned i = 0; i < nb_acc; ++i)
1074
      acceptance_cond_vec_.push_back(acc_.mark(acc_.add_set()));
1075
#endif
1076
    acc_.set_generalized_buchi();
1077
1078
  }

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

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


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

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

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

1142
    if (!s->get_use_bitset()) // if \delta'(q, a)
1143
      {
1144
        for (auto& p: tr->second)
1145
1146
1147
1148
1149
	  {
	    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);
1150
1151
	    succ_list.emplace(p.first, s1);
	    succ_list.emplace(p.first, s2);
1152
	  }
1153
      }
1154
    else
1155
      {
1156
1157
1158
1159
1160
        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}
1161
1162
1163
        state_complement* st;

#if TRANSFORM_TO_TBA
1164
1165
1166
1167
        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}}
1168

1169
1170
	// \delta'((q, I, J), a) if I'\subseteq J'
        if (newI->is_subset_of(*newJ))
1171
1172
1173
1174
1175
	  {
	    for (auto& p: tr->second)
	      {
		st = new state_complement(e->clone(), e->clone(),
					  p.second, true);
1176
		succ_list.emplace(p.first, st);
1177
1178
1179
	      }
	    condition = the_acceptance_cond_;
	  }
1180
        else  // \delta'((q, I, J), a)
1181
1182
1183
1184
	  {
	    for (auto& p: tr->second)
	      {
		st = new state_complement(newI, newJ, p.second, true);
1185
		succ_list.emplace(p.first, st);
1186
1187
	      }
	  }
1188
1189
	delete newI;
	delete newJ;
1190
#else
1191
1192
1193
1194
1195
	// {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;
1196
        for (auto& p: tr->second)
1197
1198
1199
	  {
	    st = new state_complement(pending->clone(), e->clone(),
				      p.second, true);
1200
	    succ_list.emplace(p.first, st);
1201
	  }
1202
	delete pending;
1203

1204
1205
        for (unsigned i = 0; i < l->size(); ++i)
          if (!S.get(i))
1206
	    condition |= acceptance_cond_vec_[i];
1207
#endif
1208
1209
	delete u;
	delete l;
1210
      }
1211
    delete e;
1212
    return new twa_safra_complement_succ_iterator(succ_list, condition);
1213
1214
1215
  }

  std::string
1216
  tgba_safra_complement::format_state(const state* state) const
1217
1218
  {
    const state_complement* s =
1219
      down_cast<const state_complement*>(state);
1220
1221
1222
1223
1224
    assert(s);
    return s->to_string();
  }

  bdd
1225
  tgba_safra_complement::compute_support_conditions(const state* state) const
1226
  {
1227
    const safra_tree_automaton* a = static_cast<safra_tree_automaton*>(safra_);
1228
    const state_complement* s = down_cast<const state_complement*>(state);
1229