sccstack.cc 1.82 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2014 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
4
// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6
7
8
9
10
11
// et Marie Curie.
//
// 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
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/>.
22
23
24
25
26
27
28
29

#include "sccstack.hh"

namespace spot
{
  scc_stack::connected_component::connected_component(int i)
  {
    index = i;
30
    condition = 0U;
31
32
33
34
35
  }

  scc_stack::connected_component&
  scc_stack::top()
  {
36
37
38
39
40
41
42
    return s.front();
  }

  const scc_stack::connected_component&
  scc_stack::top() const
  {
    return s.front();
43
44
45
46
47
  }

  void
  scc_stack::pop()
  {
48
49
    // assert(rem().empty());
    s.pop_front();
50
51
52
53
54
  }

  void
  scc_stack::push(int index)
  {
55
    s.emplace_front(index);
56
57
58
59
60
61
  }

  std::list<const state*>&
  scc_stack::rem()
  {
    return top().rem;
62
63
  }

64

65
66
67
68
69
70
71
72
73
74
75
  size_t
  scc_stack::size() const
  {
    return s.size();
  }

  bool
  scc_stack::empty() const
  {
    return s.empty();
  }
76
77
78
79
80
81
82
83
84
85
86
87
88
89

  unsigned
  scc_stack::clear_rem()
  {
    unsigned n = 0;
    for (stack_type::iterator i = s.begin(); i != s.end(); ++i)
      {
	n += i->rem.size();
	i->rem.clear();
      }
    return n;
  }


90
}