emptiness_stats.hh 2.15 KB
Newer Older
1
// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// 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
// the Free Software Foundation; either version 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

22
23
#ifndef SPOT_TGBAALGOS_EMPTINESS_STATS_HH
# define SPOT_TGBAALGOS_EMPTINESS_STATS_HH
24
25
26
27
28
29
30
31
32
33
34
35

namespace spot
{

  /// \addtogroup ec_misc
  /// @{

  class ec_statistics
  {
  public :
    ec_statistics()
    : states_(0), transitions_(0), depth_(0), max_depth_(0)
36
37
38
39
40
41
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
84
85
86
87
    {
    }

    void
    set_states(int n)
    {
      states_ = n;
    }

    void
    inc_states()
    {
      ++states_;
    }

    void
    inc_transitions()
    {
      ++transitions_;
    }

    void
    inc_depth()
    {
      ++depth_;
      if (depth_ > max_depth_)
	max_depth_ = depth_;
    }

    void
    dec_depth()
    {
      --depth_;
    }

    int
    states() const
    {
      return states_;
    }

    int
    transitions() const
    {
      return transitions_;
    }

    int
    max_depth() const
    {
      return max_depth_;
    }
88
89
90
91
92
93
94
95

  private :
    unsigned states_; /// number of disctint visited states
    unsigned transitions_; /// number of visited transitions
    unsigned depth_; /// maximal depth of the stack(s)
    unsigned max_depth_; /// maximal depth of the stack(s)
  };

96
97
98
99
100
101
102
  /// Accepting Cycle Search Space statistics
  class acss_statistics
  {
  public:
    virtual int acss_states() const = 0;
  };

103
104
105
  /// @}
}

106
#endif // SPOT_TGBAALGOS_EMPTINESS_STATS_HH