spot  2.12.2
emptiness_stats.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <spot/misc/common.hh>
22 #include <spot/misc/ltstr.hh>
23 #include <map>
24 
25 namespace spot
26 {
27 
30 
32  {
33  virtual
35  {
36  }
37 
38  unsigned
39  get(const char* str) const
40  {
41  auto i = stats.find(str);
42  SPOT_ASSERT(i != stats.end());
43  return (this->*i->second)();
44  }
45 
46  typedef unsigned (unsigned_statistics::*unsigned_fun)() const;
47  typedef std::map<const char*, unsigned_fun, char_ptr_less_than> stats_map;
48  stats_map stats;
49  };
50 
57  {
58  public :
60  : states_(0), transitions_(0), depth_(0), max_depth_(0)
61  {
62  stats["states"] =
63  static_cast<unsigned_statistics::unsigned_fun>(&ec_statistics::states);
64  stats["transitions"] =
65  static_cast<unsigned_statistics::unsigned_fun>
66  (&ec_statistics::transitions);
67  stats["max. depth"] =
68  static_cast<unsigned_statistics::unsigned_fun>
69  (&ec_statistics::max_depth);
70  }
71 
72  void
73  set_states(unsigned n)
74  {
75  states_ = n;
76  }
77 
78  void
79  inc_states()
80  {
81  ++states_;
82  }
83 
84  void
85  inc_transitions()
86  {
87  ++transitions_;
88  }
89 
90  void
91  inc_depth(unsigned n = 1)
92  {
93  depth_ += n;
94  if (depth_ > max_depth_)
95  max_depth_ = depth_;
96  }
97 
98  void
99  dec_depth(unsigned n = 1)
100  {
101  SPOT_ASSERT(depth_ >= n);
102  depth_ -= n;
103  }
104 
105  unsigned
106  states() const
107  {
108  return states_;
109  }
110 
111  unsigned
112  transitions() const
113  {
114  return transitions_;
115  }
116 
117  unsigned
118  max_depth() const
119  {
120  return max_depth_;
121  }
122 
123  unsigned
124  depth() const
125  {
126  return depth_;
127  }
128 
129  private :
130  unsigned states_;
131  unsigned transitions_;
132  unsigned depth_;
133  unsigned max_depth_;
134  };
135 
142  {
143  public:
145  : prefix_states_(0), cycle_states_(0)
146  {
147  stats["(non unique) states for prefix"] =
148  static_cast<unsigned_statistics::unsigned_fun>
149  (&ars_statistics::ars_prefix_states);
150  stats["(non unique) states for cycle"] =
151  static_cast<unsigned_statistics::unsigned_fun>
152  (&ars_statistics::ars_cycle_states);
153  }
154 
155  void
156  inc_ars_prefix_states()
157  {
158  ++prefix_states_;
159  }
160 
161  unsigned
162  ars_prefix_states() const
163  {
164  return prefix_states_;
165  }
166 
167  void
168  inc_ars_cycle_states()
169  {
170  ++cycle_states_;
171  }
172 
173  unsigned
174  ars_cycle_states() const
175  {
176  return cycle_states_;
177  }
178 
179  private:
180  unsigned prefix_states_;
181  unsigned cycle_states_;
182  };
183 
190  {
191  public:
193  {
194  stats["search space states"] =
195  static_cast<unsigned_statistics::unsigned_fun>
197  }
198 
199  virtual
200  ~acss_statistics()
201  {
202  }
203 
205  virtual unsigned acss_states() const = 0;
206  };
208 }
Accepting Cycle Search Space statistics.
Definition: emptiness_stats.hh:190
virtual unsigned acss_states() const =0
Number of states in the search space for the accepting cycle.
Accepting Run Search statistics.
Definition: emptiness_stats.hh:142
Emptiness-check statistics.
Definition: emptiness_stats.hh:57
Definition: automata.hh:26
Definition: emptiness_stats.hh:32

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1