twa.hh 37.6 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
26
27
#include <spot/twa/fwd.hh>
#include <spot/twa/acc.hh>
#include <spot/twa/bdddict.hh>
28
29
#include <cassert>
#include <memory>
30
31
#include <unordered_map>
#include <functional>
32
#include <array>
33
#include <vector>
34
35
36
#include <spot/misc/casts.hh>
#include <spot/misc/hash.hh>
#include <spot/tl/formula.hh>
37
#include <spot/misc/trival.hh>
38
39
40

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
108
  /// \ingroup twa_essentials
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
  /// \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
130
  /// \ingroup twa_essentials
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
  /// \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
153
  /// \ingroup twa_essentials
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
  /// \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();
    }
  };

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
192
  /// \ingroup twa_essentials
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
  /// \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)
	s->destroy();
      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)
	{
	  s->destroy();
	  return nullptr;
	}
      return *p.first;
    }

    ~state_unicity_table()
    {
      for (state_set::iterator i = m.begin(); i != m.end();)
	{
	  // Advance the iterator before destroying its key.  This
	  // avoid issues with old g++ implementations.
	  state_set::iterator old = i++;
	  (*old)->destroy();
	}
    }

    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
257
  /// \ingroup twa_essentials
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
  /// \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
281
  /// \ingroup twa_essentials
282
283
284
285
  /// \brief An Equivalence Relation for \c shared_state
  /// (shared_ptr<const state*>).
  ///
  /// This is meant to be used as a comparison functor for
286
  /// an \c unordered_map whose key are of type \c shared_state.
287
288
289
290
291
292
293
294
295
  ///
  /// 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
296
297
  ///
  /// \see shared_state_set
298
299
300
301
302
303
304
305
306
307
308
  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
309
  /// \ingroup twa_essentials
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
  /// \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
325
326
  ///
  /// \see shared_state_set
327
328
329
330
331
332
333
334
335
336
  struct state_shared_ptr_hash
  {
    size_t
    operator()(shared_state that) const
    {
      assert(that);
      return that->hash();
    }
  };

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
342
  /// \ingroup twa_essentials
343
344
345
346
347
348
349
  /// \brief Iterate over the successors of a state.
  ///
  /// This class provides the basic functionalities required to
  /// iterate over the successors of a state, as well as querying
  /// transition labels.  Because transitions are never explicitely
  /// encoded, labels (conditions and acceptance conditions) can only
  /// be queried while iterating over the successors.
350
  class SPOT_API twa_succ_iterator
351
352
353
  {
  public:
    virtual
354
    ~twa_succ_iterator()
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
397
398
399
400
401
402
403
404
405
406
    {
    }

    /// \name Iteration
    //@{

    /// \brief Position the iterator on the first successor (if any).
    ///
    /// This method can be called several times to make multiple
    /// passes over successors.
    ///
    /// \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.
    ///
    /// \return whether there is actually a successor
    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.
    ///
    /// \return whether there is actually a successor
    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.
    ///
    /// The usual way to do this is with a \c for loop.
    ///
    ///     for (s->first(); !s->done(); s->next())
    ///       ...
    virtual bool done() const = 0;

    //@}

    /// \name Inspection
    //@{

    /// \brief Get the state of the current successor.
    ///
    /// Note that the same state may occur at different points
    /// in the iteration.  These actually correspond to the same
    /// destination.  It just means there were several transitions,
    /// with different conditions, leading to the same state.
    ///
    /// The returned state should be destroyed (see state::destroy)
    /// by the caller after it is no longer used.
407
    virtual const state* dst() const = 0;
408
409
410
    /// \brief Get the condition on the transition leading to this successor.
    ///
    /// This is a boolean function of atomic propositions.
411
    virtual bdd cond() const = 0;
412
413
    /// \brief Get the acceptance conditions on the transition leading
    /// to this successor.
414
    virtual acc_cond::mark_t acc() const = 0;
415
416
417
418
419
420

    //@}
  };

  namespace internal
  {
421
422
423
424
425
    /// \brief Helper structure to iterate over the successor of a
    /// state using the on-the-flay interface.
    ///
    /// This one emulates an STL-like iterator over the
    /// twa_succ_iterator interface.
426
427
428
    struct SPOT_API succ_iterator
    {
    protected:
429
      twa_succ_iterator* it_;
430
431
    public:

432
      succ_iterator(twa_succ_iterator* it):
433
434
435
436
437
438
439
440
441
442
443
444
445
446
	it_(it)
      {
      }

      bool operator==(succ_iterator o) const
      {
	return it_ == o.it_;
      }

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

447
      const twa_succ_iterator* operator*() const
448
449
450
451
452
453
454
455
456
457
458
      {
	return it_;
      }

      void operator++()
      {
	if (!it_->next())
	  it_ = nullptr;
      }
    };
  }
459

460
  /// \defgroup twa TωA (Transition-based ω-Automata)
461
  ///
462
  /// Spot is centered around the spot::twa type.  This type and its
463
  /// cousins are listed \ref twa_essentials "here".  This is an
464
  /// abstract interface.  Its implementations are either \ref
465
466
467
  /// 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
468
469
  /// "listed separately".

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
470
  /// \addtogroup twa_essentials Essential TωA types
471
  /// \ingroup twa
472

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
473
  /// \ingroup twa_essentials
474
  /// \brief A Transition-based ω-Automaton.
475
  ///
476
477
478
479
  /// 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.
480
  ///
481
482
483
484
485
486
487
488
  /// TωAs are transition-based automata, meanings that not-only
  /// do they have labels on arcs, 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
  ///
489
  /// Previous versions of Spot supported a type of automata called
490
491
492
493
494
495
  /// TGBA, which are TωA in which the acceptance condition is a set
  /// of sets of transitions that must be intersected infinitely
  /// often.
  ///
  /// In this version, TGBAs are now represented by TωAs for which
  /// <code>aut->acc().is_generalized_buchi())</code> returns true.
496
  ///
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
497
  /// Browsing such automaton can be achieved using two functions:
498
  /// \c get_init_state, and \c succ.  The former returns
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
499
  /// the initial state while the latter lists the
500
501
  /// successor states of any state.
  ///
502
503
504
505
506
  /// Note that although this is a transition-based automata, we never
  /// represent transitions in the API!  Transition data are
  /// obtained by querying the iterator over the successors of a
  /// state.
  class SPOT_API twa: public std::enable_shared_from_this<twa>
507
  {
508
  protected:
509
    twa(const bdd_dict_ptr& d);
510
    /// Any iterator returned via release_iter.
511
    mutable twa_succ_iterator* iter_cache_;
512
    /// BDD dictionary used by the automaton.
513
    bdd_dict_ptr dict_;
514
  public:
515
516

#ifndef SWIG
517
518
519
520
521
    /// \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.
522
523
524
    class succ_iterable
    {
    protected:
525
      const twa* aut_;
526
      twa_succ_iterator* it_;
527
    public:
528
      succ_iterable(const twa* aut, twa_succ_iterator* it)
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
	: aut_(aut), it_(it)
      {
      }

      succ_iterable(succ_iterable&& other)
	: aut_(other.aut_), it_(other.it_)
      {
	other.it_ = nullptr;
      }

      ~succ_iterable()
      {
	if (it_)
	  aut_->release_iter(it_);
      }

      internal::succ_iterator begin()
      {
547
	return it_->first() ? it_ : nullptr;
548
549
550
551
552
553
554
555
556
      }

      internal::succ_iterator end()
      {
	return nullptr;
      }
    };
#endif

557
    virtual ~twa();
558

559
560
561
    /// \brief Get the initial state of the automaton.
    ///
    /// The state has been allocated with \c new.  It is the
562
    /// responsability of the caller to \c destroy it when no
563
    /// longer needed.
564
    virtual const state* get_init_state() const = 0;
565

566
    /// \brief Get an iterator over the successors of \a local_state.
567
568
569
570
    ///
    /// The iterator has been allocated with \c new.  It is the
    /// responsability of the caller to \c delete it when no
    /// longer needed.
571
    virtual twa_succ_iterator*
572
    succ_iter(const state* local_state) const = 0;
573

574
#ifndef SWIG
575
576
577
    /// \brief Build an iterable over the successors of \a s.
    ///
    /// This is meant to be used as
578
579
580
581
582
583
    /// \code
    /// for (auto i: aut->succ(s))
    ///   {
    ///     /* i->dst() */
    ///   }
    /// \endcode
584
    succ_iterable
585
586
587
588
    succ(const state* s) const
    {
      return {this, succ_iter(s)};
    }
589
590
591
592
593
594
#endif

    /// \brief Release an iterator after usage.
    ///
    /// This iterator can then be reused by succ_iter() to avoid
    /// memory allocation.
595
    void release_iter(twa_succ_iterator* i) const
596
597
598
599
600
601
    {
      if (iter_cache_)
	delete i;
      else
	iter_cache_ = i;
    }
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617

    /// \brief Get a formula that must hold whatever successor is taken.
    ///
    /// \return A formula which must be verified for all successors
    ///  of \a state.
    ///
    /// This can be as simple as \c bddtrue, or more completely
    /// the disjunction of the condition of all successors.  This
    /// is used as an hint by \c succ_iter() to reduce the number
    /// of successor to compute in a product.
    ///
    /// Sub classes should implement compute_support_conditions(),
    /// this function is just a wrapper that will cache the
    /// last return value for efficiency.
    bdd support_conditions(const state* state) const;

618
619
    /// \brief Get the dictionary associated to the automaton.
    ///
620
621
    /// Atomic propositions and acceptance conditions are represented
    /// as BDDs.  The dictionary allows to map BDD variables back to
622
    /// formulas, and vice versa.  This is useful when dealing with
623
624
    /// several automata (which may use the same BDD variable for
    /// different formula), or simply when printing.
625
626
    bdd_dict_ptr get_dict() const
    {
627
      return dict_;
628
    }
629

630
631
    /// \brief Register an atomic proposition designated by formula \a ap.
    ///
632
    /// \return The BDD variable number.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
633
    int register_ap(formula ap)
634
    {
635
636
637
638
639
640
641
      int res = dict_->has_registered_proposition(ap, this);
      if (res < 0)
	{
	  aps_.push_back(ap);
	  res = dict_->register_proposition(ap, this);
	  bddaps_ &= bdd_ithvar(res);
	}
642
643
644
645
646
      return res;
    }

    /// \brief Register an atomic proposition designated by string \a ap.
    ///
647
648
    /// \return The BDD variable number.
    int register_ap(std::string name)
649
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
650
      return register_ap(formula::ap(name));
651
652
653
654
    }

    /// \brief Get the vector of atomic propositions used by this
    /// automaton.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
655
    const std::vector<formula>&  ap() const
656
657
658
659
    {
      return aps_;
    }

660
    /// The list of atomic propositions as a conjunction.
661
662
663
664
665
    bdd ap_var() const
    {
      return bddaps_;
    }

666
667
668
    /// \brief Format the state as a string for printing.
    ///
    /// This formating is the responsability of the automata
669
    /// that owns the state.
670
    virtual std::string format_state(const state* state) const = 0;
671

672
673
674
    /// \brief Return a possible annotation for the transition
    /// pointed to by the iterator.
    ///
675
676
677
678
679
    /// You may decide to use annotations when building a tgba class
    /// that represents the state space of a model, for instance to
    /// indicate how the tgba transitions relate to the original model
    /// (e.g. the annotation could be the name of a PetriNet
    /// transition, or the line number of some textual formalism).
680
    ///
681
682
683
    /// Implementing this method is optional; the default annotation
    /// is the empty string.
    ///
684
    /// This method is used for instance in print_dot(),
685
    /// and replay_twa_run().
686
    ///
687
    /// \param t a non-done twa_succ_iterator for this automaton
688
    virtual std::string
689
    transition_annotation(const twa_succ_iterator* t) const;
690

691
    /// \brief Project a state on an automaton.
692
693
694
695
696
697
698
699
700
701
702
    ///
    /// 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
703
    ///    destroyed by the caller.
704
    virtual state* project_state(const state* s,
705
				 const const_twa_ptr& t) const;
706

707

708
709
    /// The acceptance condition of the automaton.
    /// @{
710
711
712
713
    const acc_cond& acc() const
    {
      return acc_;
    }
714

715
716
717
718
    acc_cond& acc()
    {
      return acc_;
    }
719
    /// @}
720

721
    /// Check whether the language of the automaton is empty.
722
723
    virtual bool is_empty() const;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
724
  private:
725
726
    acc_cond acc_;

727
728
729
730
731
732
733
734
735
736
    void set_num_sets_(unsigned num)
    {
      if (num < acc_.num_sets())
	{
	  acc_.~acc_cond();
	  new (&acc_) acc_cond;
	}
      acc_.add_sets(num - acc_.num_sets());
    }

737
  public:
738
    /// Number of acceptance sets used by the automaton.
739
740
741
742
743
    unsigned num_sets() const
    {
      return acc_.num_sets();
    }

744
    /// Acceptance formula used by the automaton.
745
    const acc_cond::acc_code& get_acceptance() const
746
747
748
    {
      return acc_.get_acceptance();
    }
749

750
751
752
753
    /// \brief Set the acceptance condition of the automaton.
    ///
    /// \param num the number of acceptance sets used
    /// \param c the acceptance formula
754
755
    void set_acceptance(unsigned num, const acc_cond::acc_code& c)
    {
756
      set_num_sets_(num);
757
758
      acc_.set_acceptance(c);
      if (num == 0)
759
	prop_state_acc(true);
760
761
    }

762
    /// Copy the acceptance condition of another TωA.
763
    void copy_acceptance_of(const const_twa_ptr& a)
764
765
766
767
    {
      acc_ = a->acc();
      unsigned num = acc_.num_sets();
      if (num == 0)
768
	prop_state_acc(true);
769
770
    }

771
    /// Copy the atomic propositions of another TωA
772
    void copy_ap_of(const const_twa_ptr& a)
773
    {
774
      for (auto f: a->ap())
775
	this->register_ap(f);
776
777
    }

778
779
780
781
782
783
784
785
786
787
788
789
    /// \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.
790
791
792
793
794
    void set_generalized_buchi(unsigned num)
    {
      set_num_sets_(num);
      acc_.set_generalized_buchi();
      if (num == 0)
795
	prop_state_acc(true);
796
797
    }

798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
    /// \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
813
814
815
816
817
818
    acc_cond::mark_t set_buchi()
    {
      set_generalized_buchi(1);
      return acc_.mark(0);
    }

819
  protected:
820
821
822
    /// Do the actual computation of tgba::support_conditions().
    virtual bdd compute_support_conditions(const state* state) const = 0;
    mutable const state* last_support_conditions_input_;
823
824
  private:
    mutable bdd last_support_conditions_output_;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
825
    std::vector<formula> aps_;
826
    bdd bddaps_;
827
828
829

  protected:

830
    /// Helper structure used to store property flags.
831
832
    struct bprop
    {
833
834
835
836
837
838
839
      trival::repr_t state_based_acc:2;   // State-based acceptance.
      trival::repr_t inherently_weak:2;   // Inherently Weak automaton.
      trival::repr_t weak:2;	       // Weak automaton.
      trival::repr_t terminal:2;	       // Terminal automaton.
      trival::repr_t deterministic:2;     // Deterministic automaton.
      trival::repr_t unambiguous:2;       // Unambiguous automaton.
      trival::repr_t stutter_invariant:2; // Stutter invariant language.
840
841
842
843
844
845
846
    };
    union
    {
      unsigned props;
      bprop is;
    };

847
848
849
850
851
852
#ifndef SWIG
    // Dynamic properties, are given with a name and a destructor function.
    std::unordered_map<std::string,
		       std::pair<void*,
				 std::function<void(void*)>>> named_prop_;
#endif
853
854
    void* get_named_prop_(std::string s) const;

855
856
  public:

857
#ifndef SWIG
858
859
860
861
862
863
864
865
866
867
868
    /// \brief Declare a named property
    ///
    /// Arbitrary object 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 attaches the object \a val to the current automaton,
    /// under the name \a s.
    ///
    /// When the automaton is destroyed, the \a destructor function will
    /// be called to destroy the attached object.
869
870
    void set_named_prop(std::string s,
			void* val, std::function<void(void*)> destructor);
871

872
873
874
875
876
877
878
879
880
881
882
    /// \brief Declare a named property
    ///
    /// Arbitrary object 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 attaches the object \a val to the current automaton,
    /// under the name \a s.
    ///
    /// The object will be automatically destroyed when the automaton
    /// is destroyed.
883
884
885
886
887
888
    template<typename T>
    void set_named_prop(std::string s, T* val)
    {
      set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
    }

889
890
891
892
893
894
895
896
897
898
899
900
    /// \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.
901
902
903
904
905
906
907
908
    template<typename T>
    T* get_named_prop(std::string s) const
    {
      void* p = get_named_prop_(s);
      if (!p)
	return nullptr;
      return static_cast<T*>(p);
    }
909
910
#endif

911
912
913
914
    /// \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.
915
916
917
918
919
920
921
922
    void release_named_properties()
    {
      // Destroy all named properties.
      for (auto& np: named_prop_)
	np.second.second(np.second.first);
      named_prop_.clear();
    }

923
924
925
926
927
928
    /// \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.
929
    trival prop_state_acc() const
930
931
932
933
    {
      return is.state_based_acc;
    }

934
935
936
937
    /// \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.
938
    void prop_state_acc(trival val)
939
    {
940
      is.state_based_acc = val.val();
941
942
    }

943
944
945
946
    /// \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.
947
    trival is_sba() const
948
    {
949
      return prop_state_acc() && acc().is_buchi();
950
951
    }

952
953
954
955
956
957
958
959
    /// \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()
960
    trival prop_inherently_weak() const
961
962
963
964
    {
      return is.inherently_weak;
    }

965
966
967
968
969
970
971
    /// \brief Set the "inherently weak" proeprty.
    ///
    /// Setting "inherently weak" to false automatically
    /// disables "terminal" and "weak".
    ///
    /// \see prop_weak()
    /// \see prop_terminal()
972
    void prop_inherently_weak(trival val)
973
    {
974
975
976
      is.inherently_weak = val.val();
      if (!val)
	is.terminal = is.weak = val.val();
977
978
    }

979
980
981
982
983
984
985
986
987
    /// \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()
988
    trival prop_terminal() const
989
990
991
992
    {
      return is.terminal;
    }

993
994
995
996
997
998
999
    /// \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()
1000
    void prop_terminal(trival val)
1001
    {
1002
      is.terminal = val.val();
1003
      if (val)
1004
	is.inherently_weak = is.weak = val.val();
1005
1006
    }

1007
1008
1009
1010
1011
1012
1013
    /// \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()
1014
    trival prop_weak() const
1015
1016
1017
1018
    {
      return is.weak;
    }

1019
1020
1021
1022
1023
1024
1025
1026
    /// \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()
1027
    void prop_weak(trival val)
1028
    {
1029
      is.weak = val.val();
1030
      if (val)
1031
1032
1033
	is.inherently_weak = val.val();
      if (!val)
	is.terminal = val.val();
1034
1035
    }

1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
    /// \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()
1047
    trival prop_deterministic() const
1048
1049
1050
1051
    {
      return is.deterministic;
    }

1052
1053
1054
1055
1056
1057
    /// \brief Set the deterministic property.
    ///
    /// Setting the "deterministic" property automatically
    /// sets the "unambiguous" property.
    ///
    /// \see prop_unambiguous()
1058
    void prop_deterministic(trival val)
1059
    {
1060
      is.deterministic = val.val();
1061
      if (val)
1062
1063
	// deterministic implies unambiguous
	is.unambiguous = val.val();
1064
1065
    }

1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
    /// \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()
1079
    trival prop_unambiguous() const
1080
1081
1082
1083
    {
      return is.unambiguous;
    }

1084
1085
1086
1087
1088
1089
    /// \brief Sets the unambiguous property
    ///
    /// Marking an automaton as "non unambiguous" automatically
    /// marks it as "non deterministic".
    ///
    /// \see prop_deterministic()
1090
    void prop_unambiguous(trival val)
1091
    {
1092
1093
1094
      is.unambiguous = val.val();
      if (!val)
	is.deterministic = val.val();
1095
1096
    }

1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
    /// \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
1109
    trival prop_stutter_invariant() const
1110
    {
1111
1112
1113
      return is.stutter_invariant;
    }

1114
    /// \brief Set the stutter-invariant property
1115
    void prop_stutter_invariant(trival val)
1116
    {
1117
      is.stutter_invariant = val.val();
1118
1119
    }

1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
    /// \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
1153
    struct prop_set
1154
    {
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
      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

      /// \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.
1175
1176
      static prop_set all()
      {
1177
	return { true, true, true, true };
1178
1179
1180
      }
    };

1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
    /// \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
1191
    void prop_copy(const const_twa_ptr& other, prop_set p)
1192
1193
    {
      if (p.state_based)
1194
	prop_state_acc(other->prop_state_acc());
1195
      if (p.inherently_weak)
1196
	{
1197
	  prop_terminal(other->prop_terminal());
1198
1199
1200
	  prop_weak(other->prop_weak());
	  prop_inherently_weak(other->prop_inherently_weak());
	}
1201
      if (p.deterministic)
1202
	{
1203
1204
	  prop_deterministic(other->prop_deterministic());
	  prop_unambiguous(other->prop_unambiguous());
1205
	}
1206
      if (p.stutter_inv)
1207
	prop_stutter_invariant(other->prop_stutter_invariant());
1208
1209
    }

1210
1211
1212
1213
1214
    /// \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().
1215
1216
1217
    void prop_keep(prop_set p)
    {
      if (!p.state_based)
1218
	prop_state_acc(trival::maybe());
1219
      if (!p.inherently_weak)
1220
	{
1221
1222
1223
	  prop_terminal(trival::maybe());
	  prop_weak(trival::maybe());
	  prop_inherently_weak(trival::maybe());
1224
	}
1225
      if (!p.deterministic)
1226
	{
1227
1228
	  prop_deterministic(trival::maybe());
	  prop_unambiguous(trival::maybe());
1229
	}
1230
      if (!p.stutter_inv)
1231
	prop_stutter_invariant(trival::maybe());
1232
1233
    }

1234
  };
1235

1236
  /// \addtogroup twa_representation TωA representations
1237
  /// \ingroup twa
1238

1239
  /// \addtogroup twa_algorithms TωA algorithms
1240
  /// \ingroup twa
1241

1242
  /// \addtogroup twa_on_the_fly_algorithms TωA on-the-fly algorithms
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1243
  /// \ingroup twa_algorithms
1244

1245
  /// \addtogroup twa_io Input/Output of TωA
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1246
  /// \ingroup twa_algorithms
1247

1248
  /// \addtogroup twa_ltl Translating LTL formulas into TωA
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1249
  /// \ingroup twa_algorithms
1250

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1251
1252
  /// \addtogroup twa_generic Algorithm patterns
  /// \ingroup twa_algorithms
1253

1254
  /// \addtogroup twa_reduction TωA simplifications
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1255
  /// \ingroup twa_algorithms
1256

1257
  /// \addtogroup twa_misc Miscellaneous algorithms on TωA
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1258
  /// \ingroup twa_algorithms
1259
}