twa.hh 43.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2011, 2013, 2014, 2015, 2016 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
5
6
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
#pragma once
24

25
#include <cstddef>
26
27
28
#include <spot/twa/fwd.hh>
#include <spot/twa/acc.hh>
#include <spot/twa/bdddict.hh>
29
30
#include <cassert>
#include <memory>
31
32
#include <unordered_map>
#include <functional>
33
#include <array>
34
#include <vector>
35
36
37
#include <spot/misc/casts.hh>
#include <spot/misc/hash.hh>
#include <spot/tl/formula.hh>
38
#include <spot/misc/trival.hh>
39
40
41

namespace spot
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
42
  /// \ingroup twa_essentials
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
  /// \brief Abstract class for states.
  class SPOT_API state
  {
  public:
    /// \brief Compares two states (that come from the same automaton).
    ///
    /// This method returns an integer less than, equal to, or greater
    /// than zero if \a this is found, respectively, to be less than, equal
    /// to, or greater than \a other according to some implicit total order.
    ///
    /// This method should not be called to compare states from
    /// different automata.
    ///
    /// \sa spot::state_ptr_less_than
    virtual int compare(const state* other) const = 0;

    /// \brief Hash a state.
    ///
    /// This method returns an integer that can be used as a
    /// hash value for this state.
    ///
    /// Note that the hash value is guaranteed to be unique for all
    /// equal states (in compare()'s sense) for only has long has one
    /// of these states exists.  So it's OK to use a spot::state as a
    /// key in a \c hash_map because the mere use of the state as a
    /// key in the hash will ensure the state continues to exist.
    ///
    /// However if you create the state, get its hash key, delete the
    /// state, recreate the same state, and get its hash key, you may
    /// obtain two different hash keys if the same state were not
    /// already used elsewhere.  In practice this weird situation can
    /// occur only when the state is BDD-encoded, because BDD numbers
    /// (used to build the hash value) can be reused for other
    /// formulas.  That probably doesn't matter, since the hash value
    /// is meant to be used in a \c hash_map, but it had to be noted.
    virtual size_t hash() const = 0;

    /// Duplicate a state.
    virtual state* clone() const = 0;

    /// \brief Release a state.
    ///
85
    /// Methods from the tgba or twa_succ_iterator always return a
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
    /// new state that you should deallocate with this function.
    /// Before Spot 0.7, you had to "delete" your state directly.
    /// Starting with Spot 0.7, you should update your code to use
    /// this function instead. destroy() usually call delete, except
    /// in subclasses that destroy() to allow better memory management
    /// (e.g., no memory allocation for explicit automata).
    virtual void destroy() const
    {
      delete this;
    }

  protected:
    /// \brief Destructor.
    ///
    /// Note that client code should call
101
102
103
    /// \code s->destroy(); \endcode
    /// instead of
    /// \code delete s; \endcode .
104
105
106
107
108
    virtual ~state()
    {
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
  /// \ingroup twa_essentials
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
  /// \brief Strict Weak Ordering for \c state*.
  ///
  /// This is meant to be used as a comparison functor for
  /// STL \c map whose key are of type \c state*.
  ///
  /// For instance here is how one could declare
  /// a map of \c state*.
  /// \code
  ///   // Remember how many times each state has been visited.
  ///   std::map<spot::state*, int, spot::state_ptr_less_than> seen;
  /// \endcode
  struct state_ptr_less_than
  {
    bool
    operator()(const state* left, const state* right) const
    {
      assert(left);
      return left->compare(right) < 0;
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
131
  /// \ingroup twa_essentials
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
  /// \brief An Equivalence Relation for \c state*.
  ///
  /// This is meant to be used as a comparison functor for
  /// an \c unordered_map whose key are of type \c state*.
  ///
  /// For instance here is how one could declare
  /// a map of \c state*.
  /// \code
  ///   // Remember how many times each state has been visited.
  ///   std::unordered_map<spot::state*, int, spot::state_ptr_hash,
  ///                                    spot::state_ptr_equal> seen;
  /// \endcode
  struct state_ptr_equal
  {
    bool
    operator()(const state* left, const state* right) const
    {
      assert(left);
      return 0 == left->compare(right);
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
154
  /// \ingroup twa_essentials
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
  /// \ingroup hash_funcs
  /// \brief Hash Function for \c state*.
  ///
  /// This is meant to be used as a hash functor for
  /// an \c unordered_map whose key are of type \c state*.
  ///
  /// For instance here is how one could declare
  /// a map of \c state*.
  /// \code
  ///   // Remember how many times each state has been visited.
  ///   std::unordered_map<spot::state*, int, spot::state_ptr_hash,
  ///                                    spot::state_ptr_equal> seen;
  /// \endcode
  struct state_ptr_hash
  {
    size_t
    operator()(const state* that) const
    {
      assert(that);
      return that->hash();
    }
  };

178
179
180
181
182
  /// \brief Unordered set of abstract states
  ///
  /// Destroying each state if needed is the user's responsibility.
  ///
  /// \see state_unicity_table
183
  typedef std::unordered_set<const state*,
184
                             state_ptr_hash, state_ptr_equal> state_set;
185

186
187
188
189
190
  /// \brief Unordered map of abstract states
  ///
  /// Destroying each state if needed is the user's responsibility.
  template<class val>
  using state_map = std::unordered_map<const state*, val,
191
                                       state_ptr_hash, state_ptr_equal>;
192

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
193
  /// \ingroup twa_essentials
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
  /// \brief Render state pointers unique via a hash table.
  class SPOT_API state_unicity_table
  {
    state_set m;
  public:

    /// \brief Canonicalize state pointer.
    ///
    /// If this is the first time a state is seen, this return the
    /// state pointer as-is, otherwise it frees the state and returns
    /// a point to the previously seen copy.
    ///
    /// States are owned by the table and will be freed on
    /// destruction.
    const state* operator()(const state* s)
    {
      auto p = m.insert(s);
      if (!p.second)
212
        s->destroy();
213
214
215
216
217
218
219
220
221
222
223
      return *p.first;
    }

    /// \brief Canonicalize state pointer.
    ///
    /// Same as operator(), except that a nullptr
    /// is returned if the state is not new.
    const state* is_new(const state* s)
    {
      auto p = m.insert(s);
      if (!p.second)
224
225
226
227
        {
          s->destroy();
          return nullptr;
        }
228
229
230
231
232
233
      return *p.first;
    }

    ~state_unicity_table()
    {
      for (state_set::iterator i = m.begin(); i != m.end();)
234
235
236
237
238
239
        {
          // Advance the iterator before destroying its key.  This
          // avoid issues with old g++ implementations.
          state_set::iterator old = i++;
          (*old)->destroy();
        }
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
    }

    size_t
    size()
    {
      return m.size();
    }
  };



  // Functions related to shared_ptr.
  //////////////////////////////////////////////////

  typedef std::shared_ptr<const state> shared_state;

  inline void shared_state_deleter(state* s) { s->destroy(); }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
258
  /// \ingroup twa_essentials
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
  /// \brief Strict Weak Ordering for \c shared_state
  /// (shared_ptr<const state*>).
  ///
  /// This is meant to be used as a comparison functor for
  /// STL \c map whose key are of type \c shared_state.
  ///
  /// For instance here is how one could declare
  /// a map of \c shared_state.
  /// \code
  ///   // Remember how many times each state has been visited.
  ///   std::map<shared_state, int, spot::state_shared_ptr_less_than> seen;
  /// \endcode
  struct state_shared_ptr_less_than
  {
    bool
    operator()(shared_state left,
               shared_state right) const
    {
      assert(left);
      return left->compare(right.get()) < 0;
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
282
  /// \ingroup twa_essentials
283
284
285
286
  /// \brief An Equivalence Relation for \c shared_state
  /// (shared_ptr<const state*>).
  ///
  /// This is meant to be used as a comparison functor for
287
  /// an \c unordered_map whose key are of type \c shared_state.
288
289
290
291
292
293
294
295
296
  ///
  /// For instance here is how one could declare
  /// a map of \c shared_state
  /// \code
  ///   // Remember how many times each state has been visited.
  ///   std::unordered_map<shared_state, int,
  ///                      state_shared_ptr_hash,
  ///                      state_shared_ptr_equal> seen;
  /// \endcode
297
298
  ///
  /// \see shared_state_set
299
300
301
302
303
304
305
306
307
308
309
  struct state_shared_ptr_equal
  {
    bool
    operator()(shared_state left,
               shared_state right) const
    {
      assert(left);
      return 0 == left->compare(right.get());
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
310
  /// \ingroup twa_essentials
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
  /// \ingroup hash_funcs
  /// \brief Hash Function for \c shared_state (shared_ptr<const state*>).
  ///
  /// This is meant to be used as a hash functor for
  /// an \c unordered_map whose key are of type
  /// \c shared_state.
  ///
  /// For instance here is how one could declare
  /// a map of \c shared_state.
  /// \code
  ///   // Remember how many times each state has been visited.
  ///   std::unordered_map<shared_state, int,
  ///                      state_shared_ptr_hash,
  ///                      state_shared_ptr_equal> seen;
  /// \endcode
326
327
  ///
  /// \see shared_state_set
328
329
330
331
332
333
334
335
336
337
  struct state_shared_ptr_hash
  {
    size_t
    operator()(shared_state that) const
    {
      assert(that);
      return that->hash();
    }
  };

338
  /// Unordered set of shared states
339
  typedef std::unordered_set<shared_state,
340
341
                             state_shared_ptr_hash,
                             state_shared_ptr_equal> shared_state_set;
342

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
343
  /// \ingroup twa_essentials
344
345
  /// \brief Iterate over the successors of a state.
  ///
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
  /// This class provides the basic functionality required to iterate
  /// over the set of edges leaving a given state.  Instance of
  /// twa_succ_iterator should normally not be created directly.
  /// Instead, they are created by passing a "source" state to
  /// twa::succ_iter(), which will create the instance of
  /// twa_succ_iterator to iterate over the successors of that state.
  ///
  /// This twa_succ_iterator class offers two types of services,
  /// offered by two groups of methods.  The methods first(), next(),
  /// and done() allow iteration over the set of outgoing edges.
  /// The methods cond(), acc(), dst(), allow inspecting the current
  /// edge.
  ///
  /// The twa_succ_iterator is usually subclassed so that iteration
  /// methods and accessor methods can be implemented differently in
  /// different automata.  In particular, this interface allows
  /// computing the set of successor on the fly if needed.
  ///
  /// The iterator can be used to iterate over all successors in a
  /// loop as follows:
  ///
  /// \code
  ///     for (i->first(); !i->done(); i->next())
  ///       {
  ///         // use i->cond(), i->acc(), i->dst()
  ///       }
  /// \endcode
  ///
  /// If there are n successors, there will be 1 call to first(), n
  /// calls to next() and n+1 calls to done(), so a total of 2(n+1)
  /// calls to virtual methods just to handle the iteration.  For this
  /// reason, we usually favor the following more efficient way of
  /// performing the same loop:
  ///
  /// \code
  ///     if (i->first())
  ///       do
  ///         {
  ///           // use i->cond(), i->acc(), i->dst()
  ///         }
  ///       while(i->next());
  /// \endcode
  ///
  /// This loops uses the return value of first() and next() to save
  /// n+1 calls to done().
391
  class SPOT_API twa_succ_iterator
392
393
394
  {
  public:
    virtual
395
    ~twa_succ_iterator()
396
397
398
399
    {
    }

    /// \name Iteration
400
    ///@{
401
402
403

    /// \brief Position the iterator on the first successor (if any).
    ///
404
405
    /// This method can be called several times in order to make
    /// multiple passes over successors.
406
407
408
409
410
411
    ///
    /// \warning One should always call \c done() (or better: check
    /// the return value of first()) to ensure there is a successor,
    /// even after \c first().  A common trap is to assume that there
    /// is at least one successor: this is wrong.
    ///
412
413
414
415
    /// \return true iff there is at least one successor
    ///
    /// If first() returns false, it is invalid to call next(),
    /// cond(), acc(), or dst().
416
417
418
419
420
421
422
    virtual bool first() = 0;

    /// \brief Jump to the next successor (if any).
    ///
    /// \warning Again, one should always call \c done() (or better:
    /// check the return value of next()) ensure there is a successor.
    ///
423
424
425
426
427
    /// \return true if the iterator moved to a new successor, false
    /// if the iterator could not move to a new successor.
    ///
    /// If next() returns false, it is invalid to call next() again,
    /// or to call cond(), acc() or dst().
428
429
430
431
432
433
434
    virtual bool next() = 0;

    /// \brief Check whether the iteration is finished.
    ///
    /// This function should be called after any call to \c first()
    /// or \c next() and before any enquiry about the current state.
    ///
435
    /// The typical use case of done() is in a \c for loop such as:
436
437
438
    ///
    ///     for (s->first(); !s->done(); s->next())
    ///       ...
439
440
441
442
443
444
    ///
    /// \return false iff the iterator is pointing to a successor.
    ///
    /// It is incorrect to call done() if first() hasn't been called
    /// before.  If done() returns true, it is invalid to call
    /// next(), cond(), acc(), or dst().
445
446
    virtual bool done() const = 0;

447
    ///@}
448
449

    /// \name Inspection
450
    ///@{
451

452
    /// \brief Get the destination state of the current edge.
453
    ///
454
455
456
    /// Each call to dst() (even several times on the same edge)
    /// creates a new state that has to be destroyed (see
    /// state::destroy()).  by the caller after it is no longer used.
457
    ///
458
459
460
    /// Note that the same state may occur at different points in the
    /// iteration, as different outgoing edges (usually with different
    /// labels or acceptance membership) may go to the same state.
461
    virtual const state* dst() const = 0;
462
    /// \brief Get the condition on the edge leading to this successor.
463
464
    ///
    /// This is a boolean function of atomic propositions.
465
    virtual bdd cond() const = 0;
466
467
    /// \brief Get the acceptance mark of the edge leading to this
    /// successor.
468
    virtual acc_cond::mark_t acc() const = 0;
469

470
    ///@}
471
472
473
474
  };

  namespace internal
  {
475
    /// \brief Helper structure to iterate over the successor of a
476
    /// state using the on-the-fly interface.
477
478
479
    ///
    /// This one emulates an STL-like iterator over the
    /// twa_succ_iterator interface.
480
481
482
    struct SPOT_API succ_iterator
    {
    protected:
483
      twa_succ_iterator* it_;
484
485
    public:

486
      succ_iterator(twa_succ_iterator* it):
487
        it_(it)
488
489
490
491
492
      {
      }

      bool operator==(succ_iterator o) const
      {
493
        return it_ == o.it_;
494
495
496
497
      }

      bool operator!=(succ_iterator o) const
      {
498
        return it_ != o.it_;
499
500
      }

501
      const twa_succ_iterator* operator*() const
502
      {
503
        return it_;
504
505
506
507
      }

      void operator++()
      {
508
509
        if (!it_->next())
          it_ = nullptr;
510
511
512
      }
    };
  }
513

514
  /// \defgroup twa TωA (Transition-based ω-Automata)
515
  ///
516
  /// Spot is centered around the spot::twa type.  This type and its
517
  /// cousins are listed \ref twa_essentials "here".  This is an
518
  /// abstract interface.  Its implementations are either \ref
519
520
521
  /// twa_representation "concrete representations", or \ref
  /// twa_on_the_fly_algorithms "on-the-fly algorithms".  Other
  /// algorithms that work on spot::twa are \ref twa_algorithms
522
523
  /// "listed separately".

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
524
  /// \addtogroup twa_essentials Essential TωA types
525
  /// \ingroup twa
526

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
527
  /// \ingroup twa_essentials
528
  /// \brief A Transition-based ω-Automaton.
529
  ///
530
531
532
533
  /// The acronym TωA stands for Transition-based ω-automaton.
  /// We may write it as TwA or twa, but never as TWA as the
  /// w is just a non-utf8 replacement for ω that should not be
  /// capitalized.
534
  ///
535
536
537
538
539
540
  /// TωAs are transition-based automata, meanings that not-only do
  /// they have labels on edges, but they also have an acceptance
  /// condition defined in term of sets of transitions.  The
  /// acceptance condition can be anything supported by the HOA format
  /// (http://adl.github.io/hoaf/).  The only restriction w.r.t. the
  /// format is that this class does not support alternating automata.
541
  ///
542
  /// Previous versions of Spot supported a type of automata called
543
  /// TGBA, which are TωA in which the acceptance condition is a set
544
  /// of sets of transitions that must be visited infinitely often.
545
546
  ///
  /// In this version, TGBAs are now represented by TωAs for which
547
  ///
548
549
550
551
552
553
554
555
  ///     aut->acc().is_generalized_buchi()
  ///
  /// returns true.
  ///
  /// Browsing a TωA is usually achieved using two methods: \c
  /// get_init_state(), and succ().  The former returns the initial
  /// state while the latter allows iterating over the outgoing edges
  /// of any given state.
556
  ///
557
  /// Note that although this is a transition-based automata, we never
558
  /// represent edges in the API.  Information about edges can be
559
560
  /// obtained by querying the iterator over the successors of a
  /// state.
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
  ///
  /// The interface presented here is what we call the on-the-fly
  /// interface of automata, because the TωA class can be subclassed
  /// to implement an object that computes its successors on-the-fly.
  /// The down-side is that all these methods are virtual, so you you
  /// pay the cost of virtual calls when iterating over automata
  /// constructed on-the-fly.  Also the interface assumes that each
  /// successor state is a new object whose memory management is the
  /// responsibility of the caller, who should then call
  /// state::destroy() to release it.
  ///
  /// If you want to work with a TωA that is explicitly stored as a
  /// graph in memory, use the spot::twa_graph subclass instead.  A
  /// twa_graph object can be used as a spot::twa (using the
  /// on-the-fly interface, even though nothing needs to be
  /// constructed), but it also offers a faster interface that do not
  /// use virtual methods.
578
  class SPOT_API twa: public std::enable_shared_from_this<twa>
579
  {
580
  protected:
581
    twa(const bdd_dict_ptr& d);
582
    /// Any iterator returned via release_iter.
583
    mutable twa_succ_iterator* iter_cache_;
584
    /// BDD dictionary used by the automaton.
585
    bdd_dict_ptr dict_;
586
  public:
587
588

#ifndef SWIG
589
590
591
592
593
    /// \brief Helper class to iterate over the successor of a state
    /// using the on-the-fly interface
    ///
    /// This one emulates an STL-like container with begin()/end()
    /// methods so that it can be iterated using a ranged-for.
594
595
596
    class succ_iterable
    {
    protected:
597
      const twa* aut_;
598
      twa_succ_iterator* it_;
599
    public:
600
      succ_iterable(const twa* aut, twa_succ_iterator* it)
601
        : aut_(aut), it_(it)
602
603
604
605
      {
      }

      succ_iterable(succ_iterable&& other)
606
        : aut_(other.aut_), it_(other.it_)
607
      {
608
        other.it_ = nullptr;
609
610
611
612
      }

      ~succ_iterable()
      {
613
614
        if (it_)
          aut_->release_iter(it_);
615
616
617
618
      }

      internal::succ_iterator begin()
      {
619
        return it_->first() ? it_ : nullptr;
620
621
622
623
      }

      internal::succ_iterator end()
      {
624
        return nullptr;
625
626
627
628
      }
    };
#endif

629
    virtual ~twa();
630

631
632
633
    /// \brief Get the initial state of the automaton.
    ///
    /// The state has been allocated with \c new.  It is the
634
    /// responsability of the caller to \c destroy it when no
635
    /// longer needed.
636
    virtual const state* get_init_state() const = 0;
637

638
    /// \brief Get an iterator over the successors of \a local_state.
639
640
641
642
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
643
644
    ///
    /// \see succ()
645
    virtual twa_succ_iterator*
646
    succ_iter(const state* local_state) const = 0;
647

648
#ifndef SWIG
649
650
651
    /// \brief Build an iterable over the successors of \a s.
    ///
    /// This is meant to be used as
652
653
654
655
656
657
658
659
660
661
    ///
    /// \code
    ///    for (auto i: aut->succ(s))
    ///      {
    ///        // use i->cond(), i->acc(), i->dst()
    ///      }
    /// \endcode
    ///
    /// and the above loop is in fact syntactic sugar for
    ///
662
    /// \code
663
664
665
666
667
668
669
670
    ///    twa_succ_iterator* i = aut->succ_iter(s);
    ///    if (i->first())
    ///      do
    ///        {
    ///          // use i->cond(), i->acc(), i->dst()
    ///        }
    ///      while (i->next());
    ///    aut->release_iter(i);
671
    /// \endcode
672
    succ_iterable
673
674
675
676
    succ(const state* s) const
    {
      return {this, succ_iter(s)};
    }
677
678
679
680
681
682
#endif

    /// \brief Release an iterator after usage.
    ///
    /// This iterator can then be reused by succ_iter() to avoid
    /// memory allocation.
683
    void release_iter(twa_succ_iterator* i) const
684
685
    {
      if (iter_cache_)
686
        delete i;
687
      else
688
        iter_cache_ = i;
689
    }
690

691
692
    /// \brief Get the dictionary associated to the automaton.
    ///
693
694
695
696
697
698
699
700
701
702
703
704
705
706
    /// Automata are labeled by Boolean formulas over atomic
    /// propositions.  These Boolean formula are represented as BDDs.
    /// The dictionary allows to map BDD variables back to atomic
    /// propositions, and vice versa.
    ///
    /// Usually automata that are involved in the same computations
    /// should share their dictionaries so that operations between
    /// BDDs of the two automata work naturally.
    ///
    /// It is however possible to declare automata that use different
    /// sets of atomic propositions with different dictionaries.  That
    /// way a BDD variable associated to some atomic proposition in
    /// one automaton might be reused for another atomic proposition
    /// in the other automaton.
707
708
    bdd_dict_ptr get_dict() const
    {
709
      return dict_;
710
    }
711

712
713
714
715
716
717
718
719
720
    ///@{
    /// \brief Register an atomic proposition designated by \a ap.
    ///
    /// This is the preferred way to declare that an automaton is using
    /// a given atomic proposition.
    ///
    /// This adds the atomic proposition to the list of atomic
    /// proposition of the automaton, and also register it to the
    /// bdd_dict.
721
    ///
722
723
    /// \return The BDD variable number assigned for this atomic
    /// proposition.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
724
    int register_ap(formula ap)
725
    {
726
727
      int res = dict_->has_registered_proposition(ap, this);
      if (res < 0)
728
729
730
731
732
        {
          aps_.push_back(ap);
          res = dict_->register_proposition(ap, this);
          bddaps_ &= bdd_ithvar(res);
        }
733
734
735
      return res;
    }

736
    int register_ap(std::string ap)
737
    {
738
      return register_ap(formula::ap(ap));
739
    }
740
    ///@}
741

742
743
744
745
    /// \brief Unregister an atomic proposition.
    ///
    /// \param num the BDD variable number returned by register_ap().
    void unregister_ap(int num);
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773

    /// \brief Register all atomic propositions that have
    /// already be register by the bdd_dict for this automaton.
    ///
    /// This method may only be called on an automaton with an empty
    /// list of AP.  It will fetch all atomic proposition that have
    /// been set in the bdd_dict for this particular automaton.
    ///
    /// The typical use-case for this function is when the labels of
    /// an automaton are created by functions such as
    /// formula_to_bdd().  This is for instance done in the parser
    /// for never claims or LBTT.
    void register_aps_from_dict()
    {
      if (!aps_.empty())
        throw std::runtime_error("register_ap_from_dict() may not be"
                                 " called on an automaton that has already"
                                 " registered some AP");
      auto& m = get_dict()->bdd_map;
      unsigned s = m.size();
      for (unsigned n = 0; n < s; ++n)
        if (m[n].refs.find(this) != m[n].refs.end())
          {
            aps_.push_back(m[n].f);
            bddaps_ &= bdd_ithvar(n);
          }
    }

774
    /// \brief The vector of atomic propositions registered by this
775
    /// automaton.
776
    const std::vector<formula>& ap() const
777
778
779
780
    {
      return aps_;
    }

781
    /// \brief The set of atomic propositions as a conjunction.
782
    bdd ap_vars() const
783
784
785
786
    {
      return bddaps_;
    }

787
788
    /// \brief Format the state as a string for printing.
    ///
789
790
791
792
793
    /// Formating is the responsability of the automata that owns the
    /// state, so that state objects could be implemented as very
    /// small objects, maybe sharing data with other state objects via
    /// data structure stored in the automaton.
    virtual std::string format_state(const state* s) const = 0;
794

795
    /// \brief Project a state on an automaton.
796
797
798
799
800
801
802
803
804
805
806
    ///
    /// This converts \a s, into that corresponding spot::state for \a
    /// t.  This is useful when you have the state of a product, and
    /// want restrict this state to a specific automata occuring in
    /// the product.
    ///
    /// It goes without saying that \a s and \a t should be compatible
    /// (i.e., \a s is a state of \a t).
    ///
    /// \return 0 if the projection fails (\a s is unrelated to \a t),
    ///    or a new \c state* (the projected state) that must be
807
    ///    destroyed by the caller.
808
    virtual state* project_state(const state* s,
809
                                 const const_twa_ptr& t) const;
810

811
812
    ///@{
    /// \brief The acceptance condition of the automaton.
813
814
815
816
    const acc_cond& acc() const
    {
      return acc_;
    }
817

818
819
820
821
    acc_cond& acc()
    {
      return acc_;
    }
822
    ///@}
823

824
    /// Check whether the language of the automaton is empty.
825
826
    virtual bool is_empty() const;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
827
  private:
828
829
    acc_cond acc_;

830
831
832
    void set_num_sets_(unsigned num)
    {
      if (num < acc_.num_sets())
833
834
835
836
        {
          acc_.~acc_cond();
          new (&acc_) acc_cond;
        }
837
838
839
      acc_.add_sets(num - acc_.num_sets());
    }

840
  public:
841
    /// Number of acceptance sets used by the automaton.
842
843
844
845
846
    unsigned num_sets() const
    {
      return acc_.num_sets();
    }

847
    /// Acceptance formula used by the automaton.
848
    const acc_cond::acc_code& get_acceptance() const
849
850
851
    {
      return acc_.get_acceptance();
    }
852

853
854
855
856
    /// \brief Set the acceptance condition of the automaton.
    ///
    /// \param num the number of acceptance sets used
    /// \param c the acceptance formula
857
858
    void set_acceptance(unsigned num, const acc_cond::acc_code& c)
    {
859
      set_num_sets_(num);
860
861
      acc_.set_acceptance(c);
      if (num == 0)
862
        prop_state_acc(true);
863
864
    }

865
    /// Copy the acceptance condition of another TωA.
866
    void copy_acceptance_of(const const_twa_ptr& a)
867
868
869
870
    {
      acc_ = a->acc();
      unsigned num = acc_.num_sets();
      if (num == 0)
871
        prop_state_acc(true);
872
873
    }

874
    /// Copy the atomic propositions of another TωA
875
    void copy_ap_of(const const_twa_ptr& a)
876
    {
877
      for (auto f: a->ap())
878
        this->register_ap(f);
879
880
    }

881
882
883
884
885
886
887
888
889
890
891
892
    /// \brief Set generalized Büchi acceptance
    ///
    /// \param num the number of acceptance sets to used
    ///
    /// The acceptance formula of the form
    /// \code
    /// Inf(0)&Inf(1)&...&Inf(num-1)
    /// \endcode
    /// is generated.
    ///
    /// In the case where \a num is null, the state-acceptance
    /// property is automatically turned on.
893
894
895
896
897
    void set_generalized_buchi(unsigned num)
    {
      set_num_sets_(num);
      acc_.set_generalized_buchi();
      if (num == 0)
898
        prop_state_acc(true);
899
900
    }

901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
    /// \brief Set Büchi acceptance.
    ///
    /// This declares a single acceptance set, and \c Inf(0)
    /// acceptance.  The returned mark \c {0} can be used to tag
    /// accepting transition.
    ///
    /// Note that this does not make the automaton as using
    /// state-based acceptance.  If you want to create a Büchi
    /// automaton with state-based acceptance, call
    /// \code
    /// prop_state_acc(true)
    /// \endcode
    /// in addition.
    ///
    /// \see prop_state_acc
916
917
918
919
920
921
    acc_cond::mark_t set_buchi()
    {
      set_generalized_buchi(1);
      return acc_.mark(0);
    }

922
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
923
    std::vector<formula> aps_;
924
    bdd bddaps_;
925

926
    /// Helper structure used to store property flags.
927
928
    struct bprop
    {
929
930
      trival::repr_t state_based_acc:2;   // State-based acceptance.
      trival::repr_t inherently_weak:2;   // Inherently Weak automaton.
931
932
      trival::repr_t weak:2;               // Weak automaton.
      trival::repr_t terminal:2;               // Terminal automaton.
933
934
935
      trival::repr_t deterministic:2;     // Deterministic automaton.
      trival::repr_t unambiguous:2;       // Unambiguous automaton.
      trival::repr_t stutter_invariant:2; // Stutter invariant language.
936
937
938
939
940
941
942
    };
    union
    {
      unsigned props;
      bprop is;
    };

943
944
945
#ifndef SWIG
    // Dynamic properties, are given with a name and a destructor function.
    std::unordered_map<std::string,
946
947
                       std::pair<void*,
                                 std::function<void(void*)>>> named_prop_;
948
#endif
949
950
    void* get_named_prop_(std::string s) const;

951
952
  public:

953
#ifndef SWIG
954
955
    /// \brief Declare a named property
    ///
956
    /// Arbitrary objects can be attached to automata.  Those are called
957
958
959
    /// named properties.  They are used for instance to name all the
    /// state of an automaton.
    ///
960
961
962
    /// This function attaches the object \a val to the current
    /// automaton, under the name \a s and destroy any previous
    /// property with the same name.
963
964
965
    ///
    /// When the automaton is destroyed, the \a destructor function will
    /// be called to destroy the attached object.
966
967
968
    ///
    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
    /// for a list of named properties used by Spot.
969
    void set_named_prop(std::string s,
970
                        void* val, std::function<void(void*)> destructor);
971

972
973
    /// \brief Declare a named property
    ///
974
    /// Arbitrary objects can be attached to automata.  Those are called
975
976
977
    /// named properties.  They are used for instance to name all the
    /// state of an automaton.
    ///
978
979
980
    /// This function attaches the object \a val to the current
    /// automaton, under the name \a s and destroy any previous
    /// property with the same name.
981
    ///
982
983
    /// When the automaton is destroyed, the attached object will be
    /// destroyed with \c delete.
984
985
986
    ///
    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
    /// for a list of named properties used by Spot.
987
988
989
990
991
992
    template<typename T>
    void set_named_prop(std::string s, T* val)
    {
      set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
    }

993
994
995
996
997
998
999
1000
1001
1002
1003
1004
    /// \brief Erase a named property
    ///
    /// Arbitrary objects can be attached to automata.  Those are called
    /// named properties.  They are used for instance to name all the
    /// state of an automaton.
    ///
    /// This function removes the property \a s if it exists.
    ///
    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
    /// for a list of named properties used by Spot.
    void set_named_prop(std::string s, std::nullptr_t);

1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
    /// \brief Retrieve a named property
    ///
    /// Because named property can be object of any type, retrieving
    /// the object requires knowing its type.
    ///
    /// \param s the name of the object to retrieve
    /// \tparam T the type of the object to retrieve
    ///
    /// Note that the return is a pointer to \c T, so the type should
    /// not include the pointer.
    ///
    /// Returns a nullptr if no such named property exists.
1017
1018
1019
    ///
    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
    /// for a list of named properties used by Spot.
1020
1021
1022
    template<typename T>
    T* get_named_prop(std::string s) const
    {
1023
1024
1025
      if (void* p = get_named_prop_(s))
        return static_cast<T*>(p);
      else
1026
        return nullptr;
1027
    }
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051

    /// \brief Create or retrieve a named property
    ///
    /// Arbitrary objects can be attached to automata.  Those are called
    /// named properties.  They are used for instance to name all the
    /// state of an automaton.
    ///
    /// This function create a property object of a given type, and
    /// attached it to \a name if not such property exist, or it
    /// returns
    ///
    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
    /// for a list of named properties used by Spot.
    template<typename T>
    T* get_or_set_named_prop(std::string s)
    {
      if (void* p = get_named_prop_(s))
        return static_cast<T*>(p);

      auto tmp = new T;
      set_named_prop(s, tmp);
      return tmp;
    }

1052
1053
#endif

1054
1055
1056
1057
    /// \brief Destroy all named properties.
    ///
    /// This is used by the automaton destructor, but it could be used
    /// by any algorithm that want to get rid of all named properties.
1058
1059
1060
1061
    void release_named_properties()
    {
      // Destroy all named properties.
      for (auto& np: named_prop_)
1062
        np.second.second(np.second.first);
1063
1064
1065
      named_prop_.clear();
    }

1066
1067
1068
1069
1070
1071
    /// \brief Whether the automaton uses state-based acceptance.
    ///
    /// From the point of view of Spot, this means that all
    /// transitions leaving a state belong to the same acceptance
    /// sets.  Then it is equivalent to pretend that the state is in
    /// the acceptance set.
1072
    trival prop_state_acc() const
1073
1074
1075
1076
    {
      return is.state_based_acc;
    }

1077
1078
1079
1080
    /// \brief Set the state-based-acceptance property.
    ///
    /// If this property is set to true, then all transitions leaving
    /// a state must belong to the same acceptance sets.
1081
    void prop_state_acc(trival val)
1082
    {
1083
      is.state_based_acc = val.val();
1084
1085
    }

1086
1087
1088
1089
    /// \brief Whether this is a state-based Büchi automaton.
    ///
    /// An SBA has a Büchi acceptance, and should have its
    /// state-based acceptance property set.
1090
    trival is_sba() const
1091
    {
1092
      return prop_state_acc() && acc().is_buchi();
1093
1094
    }

1095
1096
1097
1098
1099
1100
1101
1102
    /// \brief Whether the automaton is inherently weak.
    ///
    /// An automaton is inherently weak if accepting cycles and
    /// rejecting cycles are never mixed in the same strongly
    /// connected component.
    ///
    /// \see prop_weak()
    /// \see prop_terminal()
1103
    trival prop_inherently_weak() const
1104
1105
1106
1107
    {
      return is.inherently_weak;
    }

1108
1109
1110
1111
1112
1113
1114
    /// \brief Set the "inherently weak" proeprty.
    ///
    /// Setting "inherently weak" to false automatically
    /// disables "terminal" and "weak".
    ///
    /// \see prop_weak()
    /// \see prop_terminal()
1115
    void prop_inherently_weak(trival val)
1116
    {
1117
1118
      is.inherently_weak = val.val();
      if (!val)
1119
        is.terminal = is.weak = val.val();
1120
1121
    }

1122
1123
1124
1125
1126
1127
1128
1129
1130
    /// \brief Whether the automaton is terminal.
    ///
    /// An automaton is terminal if it is weak, no non-accepting cycle
    /// can be reached from an accepting cycle, and the accepting
    /// strongly components are complete (i.e., any suffix is accepted
    /// as soon as we enter an accepting component).
    ///
    /// \see prop_weak()
    /// \see prop_inherently_weak()
1131
    trival prop_terminal() const
1132
1133
1134
1135
    {
      return is.terminal;
    }

1136
1137
1138
1139
1140
1141
1142
    /// \brief Set the terminal property.
    ///
    /// Marking an automaton as "terminal" automatically marks it as
    /// "weak" and "inherently weak".
    ///
    /// \see prop_weak()
    /// \see prop_inherently_weak()
1143
    void prop_terminal(trival val)
1144
    {
1145
      is.terminal = val.val();
1146
      if (val)
1147
        is.inherently_weak = is.weak = val.val();
1148
1149
    }

1150
1151
1152
1153
1154
1155
1156
    /// \brief Whether the automaton is weak.
    ///
    /// An automaton is weak if inside each strongly connected
    /// component, all transitions belong to the same acceptance sets.
    ///
    /// \see prop_terminal()
    /// \see prop_inherently_weak()
1157
    trival prop_weak() const
1158
1159
1160
1161
    {
      return is.weak;
    }

1162
1163
1164
1165
1166
1167
1168
1169
    /// \brief Set the weak property.
    ///
    /// Marking an automaton as "weak" automatically marks it as
    /// "inherently weak".  Marking an automaton as "not weak"
    /// automatically marks are as "not terminal".
    ///
    /// \see prop_terminal()
    /// \see prop_inherently_weak()
1170
    void prop_weak(trival val)
1171
    {
1172
      is.weak = val.val();
1173
      if (val)
1174
        is.inherently_weak = val.val();
1175
      if (!val)
1176
        is.terminal = val.val();
1177
1178
    }

1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
    /// \brief Whether the automaton is deterministic.
    ///
    /// An automaton is deterministic if the conjunction between the
    /// labels of two transitions leaving a state is always false.
    ///
    /// Note that this method may return trival::maybe() when it is
    /// unknown whether the automaton is deterministic or not.  If you
    /// need a true/false answer, prefer the is_deterministic() function.
    ///
    /// \see prop_unambiguous()
    /// \see is_deterministic()
1190
    trival prop_deterministic() const
1191
1192
1193
1194
    {
      return is.deterministic;
    }

1195
1196
1197
1198
1199
1200
    /// \brief Set the deterministic property.
    ///
    /// Setting the "deterministic" property automatically
    /// sets the "unambiguous" property.
    ///
    /// \see prop_unambiguous()
1201
    void prop_deterministic(trival val)
1202
    {
1203
      is.deterministic = val.val();
1204
      if (val)
1205
1206
        // deterministic implies unambiguous
        is.unambiguous = val.val();
1207
1208
    }

1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
    /// \brief Whether the automaton is unambiguous
    ///
    /// An automaton is unambiguous if any accepted word is recognized
    /// by exactly one accepting path in the automaton.  Any word
    /// (accepted or not) may be recognized by several rejecting paths
    /// in the automaton.
    ///
    /// Note that this method may return trival::maybe() when it is
    /// unknown whether the automaton is unambiguous or not.  If you
    /// need a true/false answer, prefer the is_unambiguous() function.
    ///
    /// \see prop_deterministic()
    /// \see is_unambiguous()
1222
    trival prop_unambiguous() const
1223
1224
1225
1226
    {
      return is.unambiguous;
    }

1227
1228
1229
1230
1231
1232
    /// \brief Sets the unambiguous property
    ///
    /// Marking an automaton as "non unambiguous" automatically
    /// marks it as "non deterministic".
    ///
    /// \see prop_deterministic()
1233
    void prop_unambiguous(trival val)
1234
    {
1235
1236
      is.unambiguous = val.val();
      if (!val)
1237
        is.deterministic = val.val();
1238
1239
    }

1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
    /// \brief Whether the automaton is stutter-invariant.
    ///
    /// An automaton is stutter-invariant iff any accepted word
    /// remains accepted after removing a finite number of duplicate
    /// letters, or after duplicating finite number of letters.
    ///
    /// Note that this method may return trival::maybe() when it is
    /// unknown whether the automaton is stutter-invariant or not.  If
    /// you need a true/false answer, prefer one using of the the
    /// is_stutter_invariant() function.
    ///
    /// \see is_stutter_invariant
1252
    trival prop_stutter_invariant() const
1253
    {
1254
1255
1256
      return is.stutter_invariant;
    }

1257
    /// \brief Set the stutter-invariant property
1258
    void prop_stutter_invariant(trival val)
1259
    {
1260
      is.stutter_invariant = val.val();
1261
1262
    }

1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
    /// \brief A structure for selecting a set of automaton properties
    /// to copy.
    ///
    /// When an algorithm copies an automaton before making some
    /// modification on that automaton, it should use a \c prop_set
    /// structure to indicate which properties should be copied from
    /// the original automaton.
    ///
    /// This structure does not list all supported properties, because
    /// properties are copied by groups of related properties.  For
    /// instance if an algorithm breaks the "inherent_weak"
    /// properties, it usually also breaks the "weak" and "terminal"
    /// properties.
    ///
    /// Set the flags to true to copy the value of the original
    /// property, and to false to ignore the original property
    /// (leaving the property of the new automaton to its default
    /// value, which is trival::maybe()).
    ///
    /// This can be used for instance as:
    /// \code
    ///    aut->prop_copy(other_aut, {true, false, false, true});
    /// \endcode
    /// This would copy the "state-based acceptance" and
    /// "stutter invariant" properties from \c other_aut to \c code.
    ///
    /// The reason there is no default value for these flags is that
    /// whenever we add a new property that do not fall into any of
    /// these groups, we will be forced to review all algorithm to
    /// decide if the property should be preserved or not.
    ///
    /// \see make_twa_graph_ptr
    /// \see prop_copy
1296
    struct prop_set
1297
    {
1298
1299
1300
1301
      bool state_based;     ///< preserve state-based acceptnace
      bool inherently_weak; ///< preserve inherently weak, weak, & terminal
      bool deterministic;   ///< preserve deterministic and unambiguous
      bool stutter_inv;     ///< preserve stutter invariance
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317

      /// \brief An all-true \c prop_set
      ///
      /// Use that only in algorithms that copy an automaton without
      /// performing any modification.
      ///
      /// If an algorithm X does modifications, but preserves all the
      /// properties currently implemented, use an explicit
      ///
      /// \code
      ///    {true, true, true, true}
      /// \endcode
      ///
      /// instead of calling \c all().  This way, the day a new
      /// property is added, we will still be forced to review
      /// algorithm X, in case that new property is not preserved.
1318
1319
      static prop_set all()
      {
1320
        return { true, true, true, true };
1321
1322
1323
      }
    };

1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
    /// \brief Copy the properties of another automaton.
    ///
    /// Copy the property speciefied with \a p from \a other to the
    /// current automaton.
    ///
    /// There is no default value for \a p on purpose.  This way any
    /// time we add a new property we have to update every call to
    /// prop_copy().
    ///
    /// \see prop_set
1334
    void prop_copy(const const_twa_ptr& other, prop_set p)
1335
1336
    {
      if (p.state_based)
1337
        prop_state_acc(other->prop_state_acc());
1338
      if (p.inherently_weak)
1339
1340
1341
1342
1343
        {
          prop_terminal(other->prop_terminal());
          prop_weak(other->prop_weak());
          prop_inherently_weak(other->prop_inherently_weak());
        }
1344
      if (p.deterministic)
1345
1346
1347
1348
        {
          prop_deterministic(other->prop_deterministic());
          prop_unambiguous(other->prop_unambiguous());
        }
1349
      if (p.stutter_inv)
1350
        prop_stutter_invariant(other->prop_stutter_invariant());
1351
1352
    }

1353
1354
1355
1356
1357
    /// \brief Keep only a subset of properties of the current
    /// automaton.
    ///
    /// All properties part of a group set to \c false in \a p are reset
    /// to their default value of trival::maybe().
1358
1359
1360
    void prop_keep(prop_set