twa.hh 51.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
4
5
6
// Copyright (C) 2009, 2011, 2013-2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003-2005 Laboratoire d'Informatique de 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
{
42
43
44
45
46
47
  struct twa_run;
  typedef std::shared_ptr<twa_run> twa_run_ptr;

  struct twa_word;
  typedef std::shared_ptr<twa_word> twa_word_ptr;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
48
  /// \ingroup twa_essentials
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
85
86
87
88
89
90
  /// \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.
    ///
91
    /// Methods from the tgba or twa_succ_iterator always return a
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
    /// 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
107
108
109
    /// \code s->destroy(); \endcode
    /// instead of
    /// \code delete s; \endcode .
110
111
112
113
114
    virtual ~state()
    {
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
115
  /// \ingroup twa_essentials
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
  /// \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
    {
132
      SPOT_ASSERT(left);
133
134
135
136
      return left->compare(right) < 0;
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
137
  /// \ingroup twa_essentials
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
  /// \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
    {
155
      SPOT_ASSERT(left);
156
157
158
159
      return 0 == left->compare(right);
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
160
  /// \ingroup twa_essentials
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
  /// \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
    {
179
      SPOT_ASSERT(that);
180
181
182
183
      return that->hash();
    }
  };

184
185
186
187
188
  /// \brief Unordered set of abstract states
  ///
  /// Destroying each state if needed is the user's responsibility.
  ///
  /// \see state_unicity_table
189
  typedef std::unordered_set<const state*,
190
                             state_ptr_hash, state_ptr_equal> state_set;
191

192
193
194
195
196
  /// \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,
197
                                       state_ptr_hash, state_ptr_equal>;
198

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
199
  /// \ingroup twa_essentials
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
  /// \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)
218
        s->destroy();
219
220
221
222
223
224
225
226
227
228
229
      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)
230
231
232
233
        {
          s->destroy();
          return nullptr;
        }
234
235
236
237
238
239
      return *p.first;
    }

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

    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
264
  /// \ingroup twa_essentials
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
  /// \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
    {
283
      SPOT_ASSERT(left);
284
285
286
287
      return left->compare(right.get()) < 0;
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
288
  /// \ingroup twa_essentials
289
290
291
292
  /// \brief An Equivalence Relation for \c shared_state
  /// (shared_ptr<const state*>).
  ///
  /// This is meant to be used as a comparison functor for
293
  /// an \c unordered_map whose key are of type \c shared_state.
294
295
296
297
298
299
300
301
302
  ///
  /// 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
303
304
  ///
  /// \see shared_state_set
305
306
307
308
309
310
  struct state_shared_ptr_equal
  {
    bool
    operator()(shared_state left,
               shared_state right) const
    {
311
      SPOT_ASSERT(left);
312
313
314
315
      return 0 == left->compare(right.get());
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
316
  /// \ingroup twa_essentials
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
  /// \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
332
333
  ///
  /// \see shared_state_set
334
335
336
337
338
  struct state_shared_ptr_hash
  {
    size_t
    operator()(shared_state that) const
    {
339
      SPOT_ASSERT(that);
340
341
342
343
      return that->hash();
    }
  };

344
  /// Unordered set of shared states
345
  typedef std::unordered_set<shared_state,
346
347
                             state_shared_ptr_hash,
                             state_shared_ptr_equal> shared_state_set;
348

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
349
  /// \ingroup twa_essentials
350
351
  /// \brief Iterate over the successors of a state.
  ///
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
391
392
393
394
395
396
  /// 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().
397
  class SPOT_API twa_succ_iterator
398
399
400
  {
  public:
    virtual
401
    ~twa_succ_iterator()
402
403
404
405
    {
    }

    /// \name Iteration
406
    ///@{
407
408
409

    /// \brief Position the iterator on the first successor (if any).
    ///
410
411
    /// This method can be called several times in order to make
    /// multiple passes over successors.
412
413
414
415
416
417
    ///
    /// \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.
    ///
418
419
420
421
    /// \return true iff there is at least one successor
    ///
    /// If first() returns false, it is invalid to call next(),
    /// cond(), acc(), or dst().
422
423
424
425
426
427
428
    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.
    ///
429
430
431
432
433
    /// \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().
434
435
436
437
438
439
440
    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.
    ///
441
    /// The typical use case of done() is in a \c for loop such as:
442
443
444
    ///
    ///     for (s->first(); !s->done(); s->next())
    ///       ...
445
446
447
448
449
450
    ///
    /// \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().
451
452
    virtual bool done() const = 0;

453
    ///@}
454
455

    /// \name Inspection
456
    ///@{
457

458
    /// \brief Get the destination state of the current edge.
459
    ///
460
461
462
    /// 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.
463
    ///
464
465
466
    /// 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.
467
    virtual const state* dst() const = 0;
468
    /// \brief Get the condition on the edge leading to this successor.
469
470
    ///
    /// This is a boolean function of atomic propositions.
471
    virtual bdd cond() const = 0;
472
473
    /// \brief Get the acceptance mark of the edge leading to this
    /// successor.
474
    virtual acc_cond::mark_t acc() const = 0;
475

476
    ///@}
477
478
479
480
  };

  namespace internal
  {
481
    /// \brief Helper structure to iterate over the successor of a
482
    /// state using the on-the-fly interface.
483
484
485
    ///
    /// This one emulates an STL-like iterator over the
    /// twa_succ_iterator interface.
486
487
488
    struct SPOT_API succ_iterator
    {
    protected:
489
      twa_succ_iterator* it_;
490
491
    public:

492
      succ_iterator(twa_succ_iterator* it):
493
        it_(it)
494
495
496
497
498
      {
      }

      bool operator==(succ_iterator o) const
      {
499
        return it_ == o.it_;
500
501
502
503
      }

      bool operator!=(succ_iterator o) const
      {
504
        return it_ != o.it_;
505
506
      }

507
      const twa_succ_iterator* operator*() const
508
      {
509
        return it_;
510
511
512
513
      }

      void operator++()
      {
514
515
        if (!it_->next())
          it_ = nullptr;
516
517
      }
    };
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535

#ifndef SWIG
    /// \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.
    class twa_succ_iterable
    {
    protected:
      const twa* aut_;
      twa_succ_iterator* it_;
    public:
      twa_succ_iterable(const twa* aut, twa_succ_iterator* it)
        : aut_(aut), it_(it)
      {
      }

536
      twa_succ_iterable(twa_succ_iterable&& other) noexcept
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
        : aut_(other.aut_), it_(other.it_)
      {
        other.it_ = nullptr;
      }

      ~twa_succ_iterable(); // Defined in this file after twa

      internal::succ_iterator begin()
      {
        return it_->first() ? it_ : nullptr;
      }

      internal::succ_iterator end()
      {
        return nullptr;
      }
    };
#endif // SWIG
555
  }
556

557
  /// \defgroup twa TωA (Transition-based ω-Automata)
558
  ///
559
  /// Spot is centered around the spot::twa type.  This type and its
560
  /// cousins are listed \ref twa_essentials "here".  This is an
561
  /// abstract interface.  Its implementations are either \ref
562
563
564
  /// 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
565
566
  /// "listed separately".

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
567
  /// \addtogroup twa_essentials Essential TωA types
568
  /// \ingroup twa
569

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
570
  /// \ingroup twa_essentials
571
  /// \brief A Transition-based ω-Automaton.
572
  ///
573
574
575
576
  /// 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.
577
  ///
578
579
580
581
582
583
  /// 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.
584
  ///
585
  /// Previous versions of Spot supported a type of automata called
586
  /// TGBA, which are TωA in which the acceptance condition is a set
587
  /// of sets of transitions that must be visited infinitely often.
588
589
  ///
  /// In this version, TGBAs are now represented by TωAs for which
590
  ///
591
592
593
594
595
596
597
  ///     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
598
599
  /// of any given state. A TωA is always assumed to have at least
  /// one state, the initial one.
600
  ///
601
  /// Note that although this is a transition-based automata, we never
602
  /// represent edges in the API.  Information about edges can be
603
604
  /// obtained by querying the iterator over the successors of a
  /// state.
605
606
607
608
  ///
  /// 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.
609
  /// The down-side is that all these methods are virtual, so you
610
611
612
613
614
615
616
617
618
619
620
621
  /// 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.
622
  class SPOT_API twa: public std::enable_shared_from_this<twa>
623
  {
624
  protected:
625
    twa(const bdd_dict_ptr& d);
626
    /// Any iterator returned via release_iter.
627
    mutable twa_succ_iterator* iter_cache_;
628
    /// BDD dictionary used by the automaton.
629
    bdd_dict_ptr dict_;
630
  public:
631

632
    virtual ~twa();
633

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

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

651
#ifndef SWIG
652
653
654
    /// \brief Build an iterable over the successors of \a s.
    ///
    /// This is meant to be used as
655
656
657
658
659
660
661
662
663
664
    ///
    /// \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
    ///
665
    /// \code
666
667
668
669
670
671
672
673
    ///    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);
674
    /// \endcode
675
    internal::twa_succ_iterable
676
677
678
679
    succ(const state* s) const
    {
      return {this, succ_iter(s)};
    }
680
 #endif
681
682
683
684
685

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

694
695
    /// \brief Get the dictionary associated to the automaton.
    ///
696
697
698
699
700
701
702
703
704
705
706
707
708
709
    /// 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.
710
711
    bdd_dict_ptr get_dict() const
    {
712
      return dict_;
713
    }
714

715
716
717
718
719
720
721
722
723
    ///@{
    /// \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.
724
    ///
725
726
    /// \return The BDD variable number assigned for this atomic
    /// proposition.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
727
    int register_ap(formula ap)
728
    {
729
730
      int res = dict_->has_registered_proposition(ap, this);
      if (res < 0)
731
        {
732
          aps_.emplace_back(ap);
733
734
735
          res = dict_->register_proposition(ap, this);
          bddaps_ &= bdd_ithvar(res);
        }
736
737
738
      return res;
    }

739
    int register_ap(std::string ap)
740
    {
741
      return register_ap(formula::ap(ap));
742
    }
743
    ///@}
744

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

    /// \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())
          {
772
            aps_.emplace_back(m[n].f);
773
774
775
776
            bddaps_ &= bdd_ithvar(n);
          }
    }

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

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

790
791
    /// \brief Format the state as a string for printing.
    ///
792
793
794
795
796
    /// 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;
797

798
    /// \brief Project a state on an automaton.
799
800
801
802
803
804
805
806
807
808
809
    ///
    /// 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
810
    ///    destroyed by the caller.
811
    virtual state* project_state(const state* s,
812
                                 const const_twa_ptr& t) const;
813

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

821
822
823
824
    acc_cond& acc()
    {
      return acc_;
    }
825
    ///@}
826

827
    /// \brief Check whether the language of the automaton is empty.
828
829
830
    ///
    /// If you are calling this method on a product of two automata,
    /// consider using intersects() instead.
831
832
    virtual bool is_empty() const;

833
834
    /// \brief Return an accepting run if one exists.
    ///
835
    /// Note that this method currently only works for Fin-less
836
837
838
839
840
841
    /// acceptance.  For acceptance conditions that contain Fin
    /// acceptance, you can either rely on is_empty() and not use any
    /// accepting run, or remove Fin acceptance using remove_fin() and
    /// compute an accepting run on that larger automaton.
    ///
    /// Return nullptr if no accepting run were found.
842
843
844
    ///
    /// If you are calling this method on a product of two automata,
    /// consider using intersecting_run() instead.
845
846
847
848
    virtual twa_run_ptr accepting_run() const;

    /// \brief Return an accepting word if one exists.
    ///
849
    /// Note that this method DOES works with Fin
850
851
852
    /// acceptance.
    ///
    /// Return nullptr if no accepting word were found.
853
854
855
    ///
    /// If you are calling this method on a product of two automata,
    /// consider using intersecting_word() instead.
856
857
    virtual twa_word_ptr accepting_word() const;

858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
    /// \brief Check whether the language of this automaton intersects
    /// that of the \a other automaton.
    virtual bool intersects(const_twa_ptr other) const;

    /// \brief Return an accepting run recognizing a word accepted by
    /// two automata.
    ///
    /// If \a from_other is true, the returned run will be over the
    /// \a other automaton.  Otherwise, the run will be over this
    /// automaton.
    ///
    /// Note that this method currently only works if the automaton
    /// from which the accepting run is extracted uses Fin-less acceptance.
    /// (The other automaton can have any acceptance condition.)
    ///
    /// For acceptance conditions that contain Fin acceptance, you can
    /// either rely on intersects() and not use any accepting run, or
    /// remove Fin acceptance using remove_fin() and compute an
    /// intersecting run on this larger automaton.
    ///
    /// Return nullptr if no accepting run were found.
    virtual twa_run_ptr intersecting_run(const_twa_ptr other,
                                         bool from_other = false) const;


    /// \brief Return a word accepted by two automata.
    ///
    /// Note that this method DOES works with Fin
    /// acceptance.
    ///
    /// Return nullptr if no accepting word were found.
    virtual twa_word_ptr intersecting_word(const_twa_ptr other) const;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
891
  private:
892
893
    acc_cond acc_;

894
895
896
    void set_num_sets_(unsigned num)
    {
      if (num < acc_.num_sets())
897
898
899
900
        {
          acc_.~acc_cond();
          new (&acc_) acc_cond;
        }
901
902
903
      acc_.add_sets(num - acc_.num_sets());
    }

904
  public:
905
    /// Number of acceptance sets used by the automaton.
906
907
908
909
910
    unsigned num_sets() const
    {
      return acc_.num_sets();
    }

911
    /// Acceptance formula used by the automaton.
912
    const acc_cond::acc_code& get_acceptance() const
913
914
915
    {
      return acc_.get_acceptance();
    }
916

917
918
919
920
    /// \brief Set the acceptance condition of the automaton.
    ///
    /// \param num the number of acceptance sets used
    /// \param c the acceptance formula
921
922
    void set_acceptance(unsigned num, const acc_cond::acc_code& c)
    {
923
      set_num_sets_(num);
924
925
926
      acc_.set_acceptance(c);
    }

927
    /// Copy the acceptance condition of another TωA.
928
    void copy_acceptance_of(const const_twa_ptr& a)
929
930
931
932
    {
      acc_ = a->acc();
    }

933
    /// Copy the atomic propositions of another TωA
934
    void copy_ap_of(const const_twa_ptr& a)
935
    {
936
      for (auto f: a->ap())
937
        this->register_ap(f);
938
939
    }

940
941
942
943
944
945
946
947
948
949
950
951
    /// \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.
952
953
954
955
956
957
    void set_generalized_buchi(unsigned num)
    {
      set_num_sets_(num);
      acc_.set_generalized_buchi();
    }

958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
    /// \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
973
974
975
976
977
978
    acc_cond::mark_t set_buchi()
    {
      set_generalized_buchi(1);
      return acc_.mark(0);
    }

979
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
980
    std::vector<formula> aps_;
981
    bdd bddaps_;
982

983
    /// Helper structure used to store property flags.
984
985
    struct bprop
    {
986
987
      trival::repr_t state_based_acc:2;   // State-based acceptance.
      trival::repr_t inherently_weak:2;   // Inherently Weak automaton.
988
989
      trival::repr_t weak:2;               // Weak automaton.
      trival::repr_t terminal:2;               // Terminal automaton.
990
991
992
      trival::repr_t deterministic:2;     // Deterministic automaton.
      trival::repr_t unambiguous:2;       // Unambiguous automaton.
      trival::repr_t stutter_invariant:2; // Stutter invariant language.
993
      trival::repr_t very_weak:2;         // very-weak, or 1-weak
994
      trival::repr_t semi_deterministic:2; // semi-deterministic automaton.
995
      trival::repr_t complete:2;           // Complete automaton.
996
997
998
999
1000
1001
1002
    };
    union
    {
      unsigned props;
      bprop is;
    };

1003
1004
1005
#ifndef SWIG
    // Dynamic properties, are given with a name and a destructor function.
    std::unordered_map<std::string,
1006
1007
                       std::pair<void*,
                                 std::function<void(void*)>>> named_prop_;
1008
#endif
1009
1010
    void* get_named_prop_(std::string s) const;

1011
1012
  public:

1013
#ifndef SWIG
1014
1015
    /// \brief Declare a named property
    ///
1016
    /// Arbitrary objects can be attached to automata.  Those are called
1017
1018
1019
    /// named properties.  They are used for instance to name all the
    /// state of an automaton.
    ///
1020
1021
1022
    /// 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.
1023
1024
1025
    ///
    /// When the automaton is destroyed, the \a destructor function will
    /// be called to destroy the attached object.
1026
1027
1028
    ///
    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
    /// for a list of named properties used by Spot.
1029
    void set_named_prop(std::string s,
1030
                        void* val, std::function<void(void*)> destructor);
1031

1032
1033
    /// \brief Declare a named property
    ///
1034
    /// Arbitrary objects can be attached to automata.  Those are called
1035
1036
1037
    /// named properties.  They are used for instance to name all the
    /// state of an automaton.
    ///
1038
1039
1040
    /// 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.
1041
    ///
1042
1043
    /// When the automaton is destroyed, the attached object will be
    /// destroyed with \c delete.
1044
1045
1046
    ///
    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
    /// for a list of named properties used by Spot.
1047
1048
1049
1050
1051
1052
    template<typename T>
    void set_named_prop(std::string s, T* val)
    {
      set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
    }

1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
    /// \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);

1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
    /// \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.
1077
1078
1079
    ///
    /// See https://spot.lrde.epita.fr/concepts.html#named-properties
    /// for a list of named properties used by Spot.
1080
1081
1082
    template<typename T>
    T* get_named_prop(std::string s) const
    {
1083
1084
1085
      if (void* p = get_named_prop_(s))
        return static_cast<T*>(p);
      else
1086
        return nullptr;
1087
    }
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111

    /// \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;
    }

1112
1113
#endif

1114
1115
1116
1117
    /// \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.
1118
1119
1120
1121
    void release_named_properties()
    {
      // Destroy all named properties.
      for (auto& np: named_prop_)
1122
        np.second.second(np.second.first);
1123
1124
1125
      named_prop_.clear();
    }

1126
1127
1128
1129
1130
1131
    /// \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.
1132
    trival prop_state_acc() const
1133
    {
1134
1135
      if (num_sets() == 0)
        return true;
1136
1137
1138
      return is.state_based_acc;
    }

1139
1140
1141
1142
    /// \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.
1143
    void prop_state_acc(trival val)
1144
    {
1145
      is.state_based_acc = val.val();
1146
1147
    }

1148
1149
1150
1151
    /// \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.
1152
    trival is_sba() const
1153
    {
1154
      return prop_state_acc() && acc().is_buchi();
1155
1156
    }

1157
1158
1159
1160
1161
1162
1163
1164
    /// \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()
1165
    trival prop_inherently_weak() const
1166
1167
1168
1169
    {
      return is.inherently_weak;
    }

1170
1171
1172
    /// \brief Set the "inherently weak" proeprty.
    ///
    /// Setting "inherently weak" to false automatically
1173
    /// disables "terminal", "very weak", and "weak".
1174
1175
1176
    ///
    /// \see prop_weak()
    /// \see prop_terminal()
1177
    void prop_inherently_weak(trival val)
1178
    {
1179
1180
      is.inherently_weak = val.val();
      if (!val)
1181
        is.very_weak = is.terminal = is.weak = val.val();
1182
1183
    }

1184
1185
    /// \brief Whether the automaton is terminal.
    ///
1186
1187
1188
1189
1190
1191
    /// An automaton is terminal if it is weak, its accepting strongly
    /// components are complete, and no accepting edge lead to a
    /// non-accepting SCC.
    ///
    /// This property ensures that a word can be accepted as soon as
    /// on of its prefixes move through an accepting edge.
1192
1193
1194
    ///
    /// \see prop_weak()
    /// \see prop_inherently_weak()
1195
    trival prop_terminal() const
1196
1197
1198
1199
    {
      return is.terminal;
    }

1200
1201
1202
1203
1204
1205
1206
    /// \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()
1207
    void prop_terminal(trival val)
1208
    {
1209
      is.terminal = val.val();
1210
      if (val)
1211
        is.inherently_weak = is.weak = val.val();
1212
1213
    }

1214
1215
1216
1217
1218
1219
1220
    /// \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()
1221
    trival prop_weak() const
1222
1223
1224
1225
    {
      return is.weak;
    }

1226
1227
1228
1229
1230
1231
1232
1233
    /// \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()
1234
    void prop_weak(trival val)
1235
    {
1236
      is.weak = val.val();
1237
      if (val)
1238
        is.inherently_weak = val.val();
1239
      if (!val)
1240
        is.very_weak = is.terminal = val.val();
1241
1242
    }

1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
    /// \brief Whether the automaton is very-weak.
    ///
    /// An automaton is very-weak if it is weak (inside each strongly connected
    /// component, all transitions belong to the same acceptance sets)
    /// and each SCC contains only one state.
    ///
    /// \see prop_terminal()
    /// \see prop_weak()
    trival prop_very_weak() const
    {
      return is.very_weak;
    }

    /// \brief Set the very-weak property.
    ///
    /// Marking an automaton as "very-weak" automatically marks it as
    /// "weak" and "inherently weak".
    ///
    /// \see prop_terminal()
    /// \see prop_weak()
    void prop_very_weak(trival val)
    {
      is.very_weak = val.val();
      if (val)
        is.weak = is.inherently_weak = val.val();
    }


1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
    /// \brief Whether the automaton is complete..
    ///
    /// An automaton is complete if for each state the union of the
    /// labels of its outgoing transitions is always true.
    ///
    /// Note that this method may return trival::maybe() when it is
    /// unknown whether the automaton is complete or not.  If you
    /// need a true/false answer, prefer the is_complete() function.
    ///
    /// \see prop_complete()
    /// \see is_complete()
    trival prop_complete() const
    {
      return is.complete;
    }

    /// \brief Set the complete property.
    ///
    /// \see is_complete()
    void prop_complete(trival val)
    {
      is.complete = val.val();
    }
1294

1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
    /// \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()
1306
    trival prop_deterministic() const
1307
1308
1309
1310
    {
      return is.deterministic;
    }

1311
1312
    /// \brief Set the deterministic property.
    ///
1313
1314
    /// Setting the "deterministic" property automatically sets the
    /// "unambiguous" and "semi-deterministic" properties.
1315
1316
    ///
    /// \see prop_unambiguous()
1317
    /// \see prop_semi_deterministic()
1318
    void prop_deterministic(trival val)
1319
    {
1320
      is.deterministic = val.val();
1321
      if (val)
1322
1323
        // deterministic implies unambiguous and semi-deterministic
        is.unambiguous = is.semi_deterministic = val.val();
1324
1325
    }

1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
    /// \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()
1339
    trival prop_unambiguous() const
1340
1341
1342
1343
    {
      return is.unambiguous;
    }

1344
1345
1346
1347
1348
1349
    /// \brief Sets the unambiguous property
    ///
    /// Marking an automaton as "non unambiguous" automatically
    /// marks it as "non deterministic".
    ///
    /// \see prop_deterministic()
1350
    void prop_unambiguous(trival val)
1351
    {
1352
1353
      is.unambiguous = val.val();
      if (!val)
1354
        is.deterministic = val.val();
1355
1356
    }

1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
    /// \brief Whether the automaton is semi-deterministic
    ///
    /// An automaton is semi-deterministic if the sub-automaton
    /// reachable from any accepting SCC is deterministic.
    ///
    /// Note that this method may return trival::maybe() when it is
    /// unknown whether the automaton is semi-deterministic or not.
    /// If you need a true/false answer, prefer the
    /// is_semi_deterministic() function.
    ///
    /// \see prop_deterministic()
    /// \see is_semi_deterministic()
    trival prop_semi_deterministic() const
    {
      return is.semi_deterministic;
    }

    /// \brief Sets the semi-deterministic property