emptiness_stats.hh 6.05 KB
Newer Older
1
2
3
4
5
6
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie.
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
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
#pragma once
24

25
#include <cassert>
26
#include <map>
27
#include "misc/ltstr.hh"
28

29
30
31
namespace spot
{

32
  /// \addtogroup emptiness_check_stats
33
34
  /// @{

35
  struct unsigned_statistics
36
37
38
39
40
41
42
43
44
  {
    virtual
    ~unsigned_statistics()
    {
    }

    unsigned
    get(const char* str) const
    {
45
      auto i = stats.find(str);
46
      assert(i != stats.end());
47
48
49
      return (this->*i->second)();
    }

50
51
52
    typedef unsigned (unsigned_statistics::*unsigned_fun)() const;
    typedef std::map<const char*, unsigned_fun, char_ptr_less_than> stats_map;
    stats_map stats;
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
  /// \brief comparable statistics
  ///
  /// This must be built from a spot::unsigned_statistics.  But unlike
  /// spot::unsigned_statistics, it supports equality and inequality tests.
  /// (It's the only operations it supports, BTW.)
  class unsigned_statistics_copy
  {
  public:
    unsigned_statistics_copy()
      : set(false)
    {
    }

    unsigned_statistics_copy(const unsigned_statistics& o)
      : set(false)
    {
      seteq(o);
    }

    bool
    seteq(const unsigned_statistics& o)
    {
      if (!set)
	{
79
80
	  for (auto& i: o.stats)
	    stats[i.first] = (o.*i.second)();
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
	  set = true;
	  return true;
	}
      if (*this == o)
	return true;
      return false;
    }

    typedef std::map<const char*, unsigned, char_ptr_less_than> stats_map;
    stats_map stats;


    bool
    operator==(const unsigned_statistics_copy& o) const
    {
96
      for (auto& i: stats)
97
	{
98
	  auto i2 = o.stats.find(i.first);
99
100
	  if (i2 == o.stats.end())
	    return false;
101
	  if (i.second != i2->second)
102
103
104
105
106
107
108
109
110
111
112
113
114
115
	    return false;
	}
      return true;
    }

    bool
    operator!=(const unsigned_statistics_copy& o) const
    {
      return !(*this == o);
    }

    bool set;
  };

116
117
118
119
120
  /// \brief Emptiness-check statistics
  ///
  /// Implementations of spot::emptiness_check may also implement
  /// this interface.  Try to dynamic_cast the spot::emptiness_check
  /// pointer to know whether these statistics are available.
121
  class ec_statistics: public unsigned_statistics
122
123
124
125
  {
  public :
    ec_statistics()
    : states_(0), transitions_(0), depth_(0), max_depth_(0)
126
    {
127
128
129
130
      stats["states"] =
	static_cast<unsigned_statistics::unsigned_fun>(&ec_statistics::states);
      stats["transitions"] =
	static_cast<unsigned_statistics::unsigned_fun>
131
	  (&ec_statistics::transitions);
132
133
      stats["max. depth"] =
	static_cast<unsigned_statistics::unsigned_fun>
134
	  (&ec_statistics::max_depth);
135
136
137
    }

    void
138
    set_states(unsigned n)
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
    {
      states_ = n;
    }

    void
    inc_states()
    {
      ++states_;
    }

    void
    inc_transitions()
    {
      ++transitions_;
    }

    void
156
    inc_depth(unsigned n = 1)
157
    {
158
      depth_ += n;
159
160
161
162
163
      if (depth_ > max_depth_)
	max_depth_ = depth_;
    }

    void
164
    dec_depth(unsigned n = 1)
165
    {
166
      assert(depth_ >= n);
167
      depth_ -= n;
168
169
    }

170
    unsigned
171
172
173
174
175
    states() const
    {
      return states_;
    }

176
    unsigned
177
178
179
180
181
    transitions() const
    {
      return transitions_;
    }

182
    unsigned
183
184
185
186
    max_depth() const
    {
      return max_depth_;
    }
187

188
    unsigned
189
190
191
192
193
    depth() const
    {
      return depth_;
    }

194
  private :
195
196
197
198
    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)
199
200
  };

201
202
203
204
205
  /// \brief Accepting Run Search statistics.
  ///
  /// Implementations of spot::emptiness_check_result may also implement
  /// this interface.  Try to dynamic_cast the spot::emptiness_check_result
  /// pointer to know whether these statistics are available.
206
  class ars_statistics: public unsigned_statistics
207
208
209
  {
  public:
    ars_statistics()
210
      : prefix_states_(0), cycle_states_(0)
211
    {
212
213
      stats["(non unique) states for prefix"] =
	static_cast<unsigned_statistics::unsigned_fun>
214
	  (&ars_statistics::ars_prefix_states);
215
216
      stats["(non unique) states for cycle"] =
	static_cast<unsigned_statistics::unsigned_fun>
217
	  (&ars_statistics::ars_cycle_states);
218
219
220
    }

    void
221
    inc_ars_prefix_states()
222
    {
223
      ++prefix_states_;
224
225
    }

226
    unsigned
227
    ars_prefix_states() const
228
    {
229
230
231
232
233
234
235
236
237
      return prefix_states_;
    }

    void
    inc_ars_cycle_states()
    {
      ++cycle_states_;
    }

238
    unsigned
239
240
241
    ars_cycle_states() const
    {
      return cycle_states_;
242
243
244
    }

  private:
245
246
    unsigned prefix_states_;	/// states visited to construct the prefix
    unsigned cycle_states_;	/// states visited to construct the cycle
247
248
  };

249
250
251
252
253
254
255
256
257
258
  /// \brief Accepting Cycle Search Space statistics
  ///
  /// Implementations of spot::emptiness_check_result may also implement
  /// this interface.  Try to dynamic_cast the spot::emptiness_check_result
  /// pointer to know whether these statistics are available.
  class acss_statistics: public ars_statistics
  {
  public:
    acss_statistics()
    {
259
260
      stats["search space states"] =
	static_cast<unsigned_statistics::unsigned_fun>
261
262
263
264
265
266
267
268
269
270
271
	  (&acss_statistics::acss_states);
    }

    virtual
    ~acss_statistics()
    {
    }

    /// Number of states in the search space for the accepting cycle.
    virtual unsigned acss_states() const = 0;
  };
272
273
  /// @}
}