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

#ifndef SPOT_GRAPH_GRAPH_HH
# define SPOT_GRAPH_GRAPH_HH

23
#include "misc/common.hh"
24
25
26
#include <vector>
#include <type_traits>
#include <tuple>
27
#include <cassert>
28
#include <iterator>
29
30
#include <algorithm>
#include <iostream>
31
32
33
34

namespace spot
{
  template <typename State_Data, typename Trans_Data, bool Alternating = false>
35
  class SPOT_API digraph;
36
37
38
39
40
41
42
43
44
45
46

  namespace internal
  {
    // The boxed_label class stores Data as an attribute called
    // "label" if boxed is true.  It is an empty class if Data is
    // void, and it simply inherits from Data if boxed is false.
    //
    // The data() method offers an homogeneous access to the Data
    // instance.

    template <typename Data, bool boxed = !std::is_class<Data>::value>
47
    struct SPOT_API boxed_label
48
    {
49
      typedef Data data_t;
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
      Data label;

      template <typename... Args>
      boxed_label(Args&&... args):
	label{std::forward<Args>(args)...}
      {
      }

      // if Data is a POD type, G++ 4.8.2 wants default values for all
      // label fields unless we define this default constructor here.
      explicit boxed_label()
      {
      }

      Data& data()
      {
	return label;
      }

      const Data& data() const
      {
	return label;
      }
73
74
75
76
77

      bool operator<(const boxed_label& other) const
      {
	return label < other.label;
      }
78
79
80
    };

    template <>
81
    struct SPOT_API boxed_label<void, true>: public std::tuple<>
82
    {
83
84
85
86
87
88
89
90
91
92
93
      typedef std::tuple<> data_t;
      std::tuple<>& data()
      {
	return *this;
      }

      const std::tuple<>& data() const
      {
	return *this;
      }

94
95
96
    };

    template <typename Data>
97
    struct SPOT_API boxed_label<Data, false>: public Data
98
    {
99
100
      typedef Data data_t;

101
102
103
104
105
106
      template <typename... Args>
      boxed_label(Args&&... args):
	Data{std::forward<Args>(args)...}
      {
      }

107
      // if Data is a POD type, G++ 4.8.2 wants default values for all
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
      // label fields unless we define this default constructor here.
      explicit boxed_label()
      {
      }

      Data& data()
      {
	return *this;
      }

      const Data& data() const
      {
	return *this;
      }
    };

    //////////////////////////////////////////////////
    // State storage for digraphs
    //////////////////////////////////////////////////

    // We have two implementations, one with attached State_Data, and
    // one without.

    template <typename Transition, typename State_Data>
132
    struct SPOT_API distate_storage: public State_Data
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
    {
      Transition succ; // First outgoing transition (used when iterating)
      Transition succ_tail;	// Last outgoing transition (used for
				// appending new transitions)

      template <typename... Args>
      distate_storage(Args&&... args):
	State_Data{std::forward<Args>(args)...},
	succ(0),
	succ_tail(0)
      {
      }
    };

    //////////////////////////////////////////////////
    // Transition storage
    //////////////////////////////////////////////////

    // Again two implementation: one with label, and one without.

153
154
    template <typename StateIn,
	      typename StateOut, typename Transition, typename Trans_Data>
155
    struct SPOT_API trans_storage: public Trans_Data
156
157
158
    {
      typedef Transition transition;

159
      StateOut dst;		// destination
160
161
      Transition next_succ;	// next outgoing transition with same
				// source, or 0
162
      StateIn src;		// source
163

164
165
166
167
168
169
      explicit trans_storage()
	: Trans_Data{}
      {
      }

      template <typename... Args>
170
171
      trans_storage(StateOut dst, Transition next_succ,
		    StateIn src, Args&&... args)
172
	: Trans_Data{std::forward<Args>(args)...},
173
	dst(dst), next_succ(next_succ), src(src)
174
175
      {
      }
176
177
178
179
180
181
182
183
184
185
186
187
188
189

      bool operator<(const trans_storage& other) const
      {
	if (src < other.src)
	  return true;
	if (src > other.src)
	  return false;
	// This might be costly if the destination is a vector
	if (dst < other.dst)
	  return true;
	if (dst < other.dst)
	  return false;
	return this->data() < other.data();
      }
190
191
192
193
194
195
196
197
198
199
200
    };

    //////////////////////////////////////////////////
    // Transition iterator
    //////////////////////////////////////////////////

    // This holds a graph and a transition number that is the start of
    // a list, and it iterates over all the trans_storage_t elements
    // of that list.

    template <typename Graph>
201
202
203
204
205
206
    class SPOT_API trans_iterator:
      std::iterator<std::forward_iterator_tag,
		    typename
		    std::conditional<std::is_const<Graph>::value,
				     const typename Graph::trans_storage_t,
				     typename Graph::trans_storage_t>::type>
207
    {
208
209
210
211
212
213
214
      typedef
	std::iterator<std::forward_iterator_tag,
		      typename
		      std::conditional<std::is_const<Graph>::value,
				       const typename Graph::trans_storage_t,
				       typename Graph::trans_storage_t>::type>
	super;
215
216
217
    public:
      typedef typename Graph::transition transition;

218
219
220
221
222
223
      trans_iterator()
	: g_(nullptr), t_(0)
      {
      }

      trans_iterator(Graph* g, transition t): g_(g), t_(t)
224
225
226
      {
      }

227
      bool operator==(trans_iterator o) const
228
229
230
231
      {
	return t_ == o.t_;
      }

232
      bool operator!=(trans_iterator o) const
233
234
235
236
      {
	return t_ != o.t_;
      }

237
      typename super::reference
238
239
      operator*()
      {
240
	return g_->trans_storage(t_);
241
242
      }

243
244
245
246
247
248
      typename super::pointer
      operator->()
      {
	return &g_->trans_storage(t_);
      }

249
250
251
252
253
254
255
256
257
258
259
260
261
      trans_iterator operator++()
      {
	t_ = operator*().next_succ;
	return *this;
      }

      trans_iterator operator++(int)
      {
	trans_iterator ti = *this;
	t_ = operator*().next_succ;
	return ti;
      }

262
263
264
265
266
      operator bool() const
      {
	return t_;
      }

267
268
269
270
271
      transition trans() const
      {
	return t_;
      }

272
273
    protected:
      Graph* g_;
274
      transition t_;
275
276
    };

277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
    template <typename Graph>
    class SPOT_API killer_trans_iterator: public trans_iterator<Graph>
    {
      typedef trans_iterator<Graph> super;
    public:
      typedef typename Graph::state_storage_t state_storage_t;
      typedef typename Graph::transition transition;

      killer_trans_iterator(Graph* g, transition t, state_storage_t& src):
	super(g, t), src_(src), prev_(0)
      {
      }

      killer_trans_iterator operator++()
      {
	prev_ = this->t_;
	this->t_ = this->operator*().next_succ;
	return *this;
      }

      killer_trans_iterator operator++(int)
      {
	killer_trans_iterator ti = *this;
300
	++*this;
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
	return ti;
      }

      // Erase the current transition and advance the iterator.
      void erase()
      {
	transition next = this->operator*().next_succ;

	// Update source state and previous transitions
	if (prev_)
	  {
	    this->g_->trans_storage(prev_).next_succ = next;
	  }
	else
	  {
	    if (src_.succ == this->t_)
	      src_.succ = next;
	  }
	if (src_.succ_tail == this->t_)
	  {
	    src_.succ_tail = prev_;
	    assert(next == 0);
	  }

	// Erased transitions have themselves as next_succ.
	this->operator*().next_succ = this->t_;

328
	// Advance iterator to next transition.
329
330
331
332
333
334
335
336
337
338
339
	this->t_ = next;

	++this->g_->killed_trans_;
      }

    protected:
      state_storage_t& src_;
      transition prev_;
    };


340
341
342
343
344
345
346
    //////////////////////////////////////////////////
    // State OUT
    //////////////////////////////////////////////////

    // Fake container listing the outgoing transitions of a state.

    template <typename Graph>
347
    class SPOT_API state_out
348
349
350
351
    {
    public:
      typedef typename Graph::transition transition;
      state_out(Graph* g, transition t):
352
	g_(g), t_(t)
353
354
355
356
357
358
359
360
361
362
      {
      }

      trans_iterator<Graph> begin()
      {
	return {g_, t_};
      }

      trans_iterator<Graph> end()
      {
363
	return {};
364
365
      }

366
367
368
369
370
      void recycle(transition t)
      {
	t_ = t;
      }

371
372
    protected:
      Graph* g_;
373
      transition t_;
374
375
376
377
378
379
380
381
382
383
384
    };

  }

  // The actual graph implementation

  template <typename State_Data, typename Trans_Data, bool Alternating>
  class digraph
  {
    friend class internal::trans_iterator<digraph>;
    friend class internal::trans_iterator<const digraph>;
385
    friend class internal::killer_trans_iterator<digraph>;
386

387
  public:
388
389
390
    typedef internal::trans_iterator<digraph> iterator;
    typedef internal::trans_iterator<const digraph> const_iterator;

391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
    static constexpr bool alternating()
    {
      return Alternating;
    }

    // Extra data to store on each state or transition.
    typedef State_Data state_data_t;
    typedef Trans_Data trans_data_t;

    // State and transitions are identified by their indices in some
    // vector.
    typedef unsigned state;
    typedef unsigned transition;

    // The type of an output state (when seen from a transition)
    // depends on the kind of graph we build
    typedef typename std::conditional<Alternating,
				      std::vector<state>,
				      state>::type out_state;

    typedef internal::distate_storage<transition,
				      internal::boxed_label<State_Data>>
      state_storage_t;
414
    typedef internal::trans_storage<state, out_state, transition,
415
416
417
418
419
420
421
				    internal::boxed_label<Trans_Data>>
      trans_storage_t;
    typedef std::vector<state_storage_t> state_vector;
    typedef std::vector<trans_storage_t> trans_vector;
  protected:
    state_vector states_;
    trans_vector transitions_;
422
423
    // Number of erased transitions.
    unsigned killed_trans_;
424
425
426
427
428
429
430
431
  public:
    /// \brief construct an empty graph
    ///
    /// Construct an empty graph, and reserve space for \a max_states
    /// states and \a max_trans transitions.  These are not hard
    /// limits, but just hints to pre-allocate a data structure that
    /// may hold that much items.
    digraph(unsigned max_states = 10, unsigned max_trans = 0)
432
      : killed_trans_(0)
433
434
435
436
437
438
439
440
    {
      states_.reserve(max_states);
      if (max_trans == 0)
	max_trans = max_states * 2;
      transitions_.reserve(max_trans + 1);
      // Transition number 0 is not used, because we use this index
      // to mark the absence of a transition.
      transitions_.resize(1);
441
442
      // This causes transition 0 to be considered as dead.
      transitions_[0].next_succ = 0;
443
444
    }

445
446
447
448
449
450
451
    unsigned num_states() const
    {
      return states_.size();
    }

    unsigned num_transitions() const
    {
452
453
454
455
456
457
458
459
460
      return transitions_.size() - killed_trans_ - 1;
    }

    bool valid_trans(transition t) const
    {
      // Erased transitions have their next_succ pointing to
      // themselves.
      return (t < transitions_.size() &&
	      transitions_[t].next_succ != t);
461
462
    }

463
464
465
466
467
468
469
470
    template <typename... Args>
    state new_state(Args&&... args)
    {
      state s = states_.size();
      states_.emplace_back(std::forward<Args>(args)...);
      return s;
    }

471
472
473
474
    template <typename... Args>
    state new_states(unsigned n, Args&&... args)
    {
      state s = states_.size();
475
      states_.reserve(s + n);
476
477
478
479
480
      while (n--)
	states_.emplace_back(std::forward<Args>(args)...);
      return s;
    }

481
482
483
484
485
486
487
488
489
490
491
492
493
494
    state_storage_t&
    state_storage(state s)
    {
      assert(s < states_.size());
      return states_[s];
    }

    const state_storage_t&
    state_storage(state s) const
    {
      assert(s < states_.size());
      return states_[s];
    }

495
496
497
    // Do not use State_Data& as return type, because State_Data might
    // be void.
    typename state_storage_t::data_t&
498
499
    state_data(state s)
    {
500
      assert(s < states_.size());
501
502
503
504
      return states_[s].data();
    }

    // May not be called on states with no data.
505
    const typename state_storage_t::data_t&
506
507
    state_data(state s) const
    {
508
      assert(s < states_.size());
509
510
511
      return states_[s].data();
    }

512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
    trans_storage_t&
    trans_storage(transition s)
    {
      assert(s < transitions_.size());
      return transitions_[s];
    }

    const trans_storage_t&
    trans_storage(transition s) const
    {
      assert(s < transitions_.size());
      return transitions_[s];
    }

    typename trans_storage_t::data_t&
    trans_data(transition s)
    {
      assert(s < transitions_.size());
      return transitions_[s].data();
    }

    const typename trans_storage_t::data_t&
    trans_data(transition s) const
    {
      assert(s < transitions_.size());
      return transitions_[s].data();
    }

540
541
542
543
    template <typename... Args>
    transition
    new_transition(state src, out_state dst, Args&&... args)
    {
544
545
      assert(src < states_.size());

546
      transition t = transitions_.size();
547
      transitions_.emplace_back(dst, 0, src, std::forward<Args>(args)...);
548
549

      transition st = states_[src].succ_tail;
550
      assert(st < t || !st);
551
552
553
554
555
556
557
558
      if (!st)
	states_[src].succ = t;
      else
	transitions_[st].next_succ = t;
      states_[src].succ_tail = t;
      return t;
    }

559
    state index_of_state(const state_storage_t& ss) const
560
561
562
563
564
    {
      assert(!states_.empty());
      return &ss - &states_.front();
    }

565
    transition index_of_transition(const trans_storage_t& tt) const
566
567
568
569
570
    {
      assert(!transitions_.empty());
      return &tt - &transitions_.front();
    }

571
572
573
574
575
576
    internal::state_out<digraph>
    out(state src)
    {
      return {this, states_[src].succ};
    }

577
578
579
580
581
582
    internal::state_out<digraph>
    out(state_storage_t& src)
    {
      return out(index_of_state(src));
    }

583
584
585
586
587
588
    internal::state_out<const digraph>
    out(state src) const
    {
      return {this, states_[src].succ};
    }

589
590
    internal::state_out<const digraph>
    out(state_storage_t& src) const
591
    {
592
      return out(index_of_state(src));
593
594
    }

595
596
    internal::killer_trans_iterator<digraph>
    out_iteraser(state_storage_t& src)
597
    {
598
599
600
601
602
603
604
      return {this, src.succ, src};
    }

    internal::killer_trans_iterator<digraph>
    out_iteraser(state src)
    {
      return out_iteraser(state_storage(src));
605
606
607
608
609
610
611
612
613
614
615
616
    }

    const state_vector& states() const
    {
      return states_;
    }

    state_vector& states()
    {
      return states_;
    }

617
618
619
620
621
622
623
624
625
626
    const trans_vector& transitions() const
    {
      return transitions_;
    }

    trans_vector& transitions()
    {
      return transitions_;
    }

627
628
629
630
631
    bool is_dead_transition(unsigned t) const
    {
      return transitions_[t].next_succ == t;
    }

632
    bool is_dead_transition(const trans_storage_t& t) const
633
634
635
636
    {
      return t.next_succ == index_of_transition(t);
    }

637

638
639
640
    // To help debugging
    void dump_storage(std::ostream& o) const
    {
641
      unsigned tend = transitions_.size();
642
      for (unsigned t = 1; t < tend; ++t)
643
	{
644
645
646
647
648
649
650
651
652
653
654
	  o << 't' << t << ": (s"
	    << transitions_[t].src << ", s"
	    << transitions_[t].dst << ") t"
	    << transitions_[t].next_succ << '\n';
	}
      unsigned send = states_.size();
      for (unsigned s = 0; s < send; ++s)
	{
	  o << 's' << s << ": t"
	    << states_[s].succ << " t"
	    << states_[s].succ_tail << '\n';
655
	}
656
    }
657

658
659
660
661
662
663
664
665
666
667
668
669
670
    // Remove all dead transitions.  The transitions_ vector is left
    // in a state that is incorrect and should eventually be fixed by
    // a call to chain_transitions_() before any iteration on the
    // successor of a state is performed.
    void remove_dead_transitions_()
    {
      if (killed_trans_ == 0)
	return;
      auto i = std::remove_if(transitions_.begin() + 1, transitions_.end(),
			      [this](const trans_storage_t& t) {
				return this->is_dead_transition(t);
			      });
      transitions_.erase(i, transitions_.end());
671
      killed_trans_ = 0;
672
    }
673

674
675
676
677
678
679
680
681
682
683
    // This will invalidate all iterators, and also destroy transition
    // chains.  Call chain_transitions_() immediately afterwards
    // unless you know what you are doing.
    template<class Predicate = std::less<trans_storage_t>>
    void sort_transitions_(Predicate p = Predicate())
    {
      //std::cerr << "\nbefore\n";
      //dump_storage(std::cerr);
      std::sort(transitions_.begin() + 1, transitions_.end(), p);
    }
684

685
686
687
688
689
690
691
    // Should be called only when it is known that all transitions
    // with the same destination are consecutive in the vector.
    void chain_transitions_()
    {
      state last_src = -1U;
      transition tend = transitions_.size();
      for (transition t = 1; t < tend; ++t)
692
	{
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
	  state src = transitions_[t].src;
	  if (src != last_src)
	    {
	      states_[src].succ = t;
	      if (last_src != -1U)
		{
		  states_[last_src].succ_tail = t - 1;
		  transitions_[t - 1].next_succ = 0;
		}
	      while (++last_src != src)
		{
		  states_[last_src].succ = 0;
		  states_[last_src].succ_tail = 0;
		}
	    }
	  else
	    {
	      transitions_[t - 1].next_succ = t;
	    }
	}
      if (last_src != -1U)
	{
	  states_[last_src].succ_tail = tend - 1;
	  transitions_[tend - 1].next_succ = 0;
	}
      unsigned send = states_.size();
      while (++last_src != send)
	{
	  states_[last_src].succ = 0;
	  states_[last_src].succ_tail = 0;
723
	}
724
725
      //std::cerr << "\nafter\n";
      //dump_storage(std::cerr);
726
727
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
    // Rename all the states in the transition vector.  The
    // transitions_ vector is left in a state that is incorrect and
    // should eventually be fixed by a call to chain_transitions_()
    // before any iteration on the successor of a state is performed.
    void rename_states_(const std::vector<unsigned>& newst)
    {
      assert(newst.size() == states_.size());
      unsigned tend = transitions_.size();
      for (unsigned t = 1; t < tend; t++)
	{
	  transitions_[t].dst = newst[transitions_[t].dst];
	  transitions_[t].src = newst[transitions_[t].src];
	}
    }

743
744
745
746
747
    void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
    {
      assert(newst.size() == states_.size());
      assert(used_states > 0);

748
749
750
      //std::cerr << "\nbefore defrag\n";
      //dump_storage(std::cerr);

751
752
753
754
755
      // Shift all states in states_, as indicated by newst.
      unsigned send = states_.size();
      for (state s = 0; s < send; ++s)
	{
	  state dst = newst[s];
756
	  if (dst == s)
757
	    continue;
758
759
760
761
762
763
764
765
766
767
	  if (dst == -1U)
	    {
	      // This is an erased state.  Mark all its transitions as
	      // dead (i.e., t.next_succ should point to t for each of
	      // them).
	      auto t = states_[s].succ;
	      while (t)
		std::swap(t, transitions_[t].next_succ);
	      continue;
	    }
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
	  states_[dst] = std::move(states_[s]);
	}
      states_.resize(used_states);

      // Shift all transitions in transitions_.  The algorithm is
      // similar to remove_if, but it also keeps the correspondence
      // between the old and new index as newidx[old] = new.
      unsigned tend = transitions_.size();
      std::vector<transition> newidx(tend);
      unsigned dest = 1;
      for (transition t = 1; t < tend; ++t)
	{
	  if (is_dead_transition(t))
	    continue;
	  if (t != dest)
	    transitions_[dest] = std::move(transitions_[t]);
	  newidx[t] = dest;
	  ++dest;
	}
      transitions_.resize(dest);
      killed_trans_ = 0;

      // Adjust next_succ and dst pointers in all transitions.
      for (transition t = 1; t < dest; ++t)
	{
	  auto& tr = transitions_[t];
	  tr.next_succ = newidx[tr.next_succ];
	  tr.dst = newst[tr.dst];
796
	  tr.src = newst[tr.src];
797
798
799
800
801
802
803
804
805
	  assert(tr.dst != -1U);
	}

      // Adjust succ and succ_tails pointers in all states.
      for (auto& s: states_)
	{
	  s.succ = newidx[s.succ];
	  s.succ_tail = newidx[s.succ_tail];
	}
806
807
808

      //std::cerr << "\nafter defrag\n";
      //dump_storage(std::cerr);
809
810
    }

811
812
813
814
815
  };

}

#endif // SPOT_GRAPH_GRAPH_HH