graph.hh 14.8 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
31
32

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

  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>
45
    struct SPOT_API boxed_label
46
    {
47
      typedef Data data_t;
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
      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;
      }
    };

    template <>
74
    struct SPOT_API boxed_label<void, true>: public std::tuple<>
75
    {
76
77
78
79
80
81
82
83
84
85
86
      typedef std::tuple<> data_t;
      std::tuple<>& data()
      {
	return *this;
      }

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

87
88
89
    };

    template <typename Data>
90
    struct SPOT_API boxed_label<Data, false>: public Data
91
    {
92
93
      typedef Data data_t;

94
95
96
97
98
99
      template <typename... Args>
      boxed_label(Args&&... args):
	Data{std::forward<Args>(args)...}
      {
      }

100
      // if Data is a POD type, G++ 4.8.2 wants default values for all
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
      // 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>
125
    struct SPOT_API distate_storage: public State_Data
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
    {
      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.

    template <typename State, typename Transition, typename Trans_Data>
147
    struct SPOT_API trans_storage: public Trans_Data
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
    {
      typedef Transition transition;

      State dst;		// destination
      Transition next_succ;	// next outgoing transition with same
				// source, or 0
      explicit trans_storage()
	: Trans_Data{}
      {
      }

      template <typename... Args>
      trans_storage(State dst, Transition next_succ, Args&&... args)
	: Trans_Data{std::forward<Args>(args)...},
	  dst(dst), next_succ(next_succ)
      {
      }
    };

    //////////////////////////////////////////////////
    // 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>
176
177
178
179
180
181
    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>
182
    {
183
184
185
186
187
188
189
      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;
190
191
192
    public:
      typedef typename Graph::transition transition;

193
194
195
196
197
198
      trans_iterator()
	: g_(nullptr), t_(0)
      {
      }

      trans_iterator(Graph* g, transition t): g_(g), t_(t)
199
200
201
202
203
204
205
206
207
208
209
210
211
      {
      }

      bool operator==(trans_iterator o)
      {
	return t_ == o.t_;
      }

      bool operator!=(trans_iterator o)
      {
	return t_ != o.t_;
      }

212
      typename super::reference
213
214
      operator*()
      {
215
	return g_->trans_storage(t_);
216
217
      }

218
219
220
221
222
223
      typename super::pointer
      operator->()
      {
	return &g_->trans_storage(t_);
      }

224
225
226
227
228
229
230
231
232
233
234
235
236
      trans_iterator operator++()
      {
	t_ = operator*().next_succ;
	return *this;
      }

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

237
238
239
240
241
      operator bool() const
      {
	return t_;
      }

242
243
244
245
246
      transition trans() const
      {
	return t_;
      }

247
248
    protected:
      Graph* g_;
249
      transition t_;
250
251
    };

252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
    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;
	prev_ = this->t_;
	this->t_ = this->operator*().next_succ;
	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_;

	// Advance iterator to next transitions.
	this->t_ = next;

	++this->g_->killed_trans_;
      }

    protected:
      state_storage_t& src_;
      transition prev_;
    };


316
317
318
319
320
321
322
    //////////////////////////////////////////////////
    // State OUT
    //////////////////////////////////////////////////

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

    template <typename Graph>
323
    class SPOT_API state_out
324
325
326
327
    {
    public:
      typedef typename Graph::transition transition;
      state_out(Graph* g, transition t):
328
	g_(g), t_(t)
329
330
331
332
333
334
335
336
337
338
      {
      }

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

      trans_iterator<Graph> end()
      {
339
	return {};
340
341
      }

342
343
344
345
346
      void recycle(transition t)
      {
	t_ = t;
      }

347
348
    protected:
      Graph* g_;
349
      transition t_;
350
351
352
353
354
355
356
357
358
359
360
    };

  }

  // 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>;
361
    friend class internal::killer_trans_iterator<digraph>;
362

363
  public:
364
365
366
    typedef internal::trans_iterator<digraph> iterator;
    typedef internal::trans_iterator<const digraph> const_iterator;

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
    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;
    typedef internal::trans_storage<out_state, transition,
				    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_;
398
399
    // Number of erased transitions.
    unsigned killed_trans_;
400
401
402
403
404
405
406
407
  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)
408
      : killed_trans_(0)
409
410
411
412
413
414
415
416
417
418
    {
      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);
    }

419
420
421
422
423
424
425
    unsigned num_states() const
    {
      return states_.size();
    }

    unsigned num_transitions() const
    {
426
427
428
429
430
431
432
433
434
      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);
435
436
    }

437
438
439
440
441
442
443
444
    template <typename... Args>
    state new_state(Args&&... args)
    {
      state s = states_.size();
      states_.emplace_back(std::forward<Args>(args)...);
      return s;
    }

445
446
447
448
    template <typename... Args>
    state new_states(unsigned n, Args&&... args)
    {
      state s = states_.size();
449
      states_.reserve(s + n);
450
451
452
453
454
      while (n--)
	states_.emplace_back(std::forward<Args>(args)...);
      return s;
    }

455
456
457
458
459
460
461
462
463
464
465
466
467
468
    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];
    }

469
470
471
    // Do not use State_Data& as return type, because State_Data might
    // be void.
    typename state_storage_t::data_t&
472
473
    state_data(state s)
    {
474
      assert(s < states_.size());
475
476
477
478
      return states_[s].data();
    }

    // May not be called on states with no data.
479
    const typename state_storage_t::data_t&
480
481
    state_data(state s) const
    {
482
      assert(s < states_.size());
483
484
485
      return states_[s].data();
    }

486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
    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();
    }

514
515
516
517
    template <typename... Args>
    transition
    new_transition(state src, out_state dst, Args&&... args)
    {
518
519
      assert(src < states_.size());

520
521
522
523
      transition t = transitions_.size();
      transitions_.emplace_back(dst, 0, std::forward<Args>(args)...);

      transition st = states_[src].succ_tail;
524
      assert(st < t || !st);
525
526
527
528
529
530
531
532
      if (!st)
	states_[src].succ = t;
      else
	transitions_[st].next_succ = t;
      states_[src].succ_tail = t;
      return t;
    }

533
534
535
536
537
538
539
540
541
542
543
544
    state index_of_state(state_storage_t& ss)
    {
      assert(!states_.empty());
      return &ss - &states_.front();
    }

    transition index_of_transition(trans_storage_t& tt)
    {
      assert(!transitions_.empty());
      return &tt - &transitions_.front();
    }

545
546
547
548
549
550
    internal::state_out<digraph>
    out(state src)
    {
      return {this, states_[src].succ};
    }

551
552
553
554
555
556
    internal::state_out<digraph>
    out(state_storage_t& src)
    {
      return out(index_of_state(src));
    }

557
558
559
560
561
562
    internal::state_out<const digraph>
    out(state src) const
    {
      return {this, states_[src].succ};
    }

563
564
    internal::state_out<const digraph>
    out(state_storage_t& src) const
565
    {
566
      return out(index_of_state(src));
567
568
    }

569
570
    internal::killer_trans_iterator<digraph>
    out_iteraser(state_storage_t& src)
571
    {
572
573
574
575
576
577
578
      return {this, src.succ, src};
    }

    internal::killer_trans_iterator<digraph>
    out_iteraser(state src)
    {
      return out_iteraser(state_storage(src));
579
580
581
582
583
584
585
586
587
588
589
590
    }

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

    state_vector& states()
    {
      return states_;
    }

591
592
593
594
595
596
597
598
599
600
    const trans_vector& transitions() const
    {
      return transitions_;
    }

    trans_vector& transitions()
    {
      return transitions_;
    }

601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
    void defrag()
    {
      if (killed_trans_ == 0)	// Nothing to do.
	return;

      // 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 (transitions_[t].next_succ == t)
	    continue;
	  if (t != dest)
	    transitions_[dest] = std::move(transitions_[t]);
	  newidx[t] = dest;
	  ++dest;
	}

      transitions_.resize(dest);
      killed_trans_ = 0;

      // Adjust next_succ pointers in all transitions.
      for (transition t = 1; t < dest; ++t)
	transitions_[t].next_succ = newidx[transitions_[t].next_succ];

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

637
638
639
640
641
  };

}

#endif // SPOT_GRAPH_GRAPH_HH