spot  2.1.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
emptiness_stats.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
3 // l'Epita (LRDE).
4 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
5 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
6 // Pierre et Marie Curie.
7 //
8 // This file is part of Spot, a model checking library.
9 //
10 // Spot is free software; you can redistribute it and/or modify it
11 // 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 // (at your option) any later version.
14 //
15 // Spot is distributed in the hope that it will be useful, but WITHOUT
16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
18 // License for more details.
19 //
20 // 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 <spot/misc/ltstr.hh>
28 
29 namespace spot
30 {
31 
34 
36  {
37  virtual
39  {
40  }
41 
42  unsigned
43  get(const char* str) const
44  {
45  auto i = stats.find(str);
46  SPOT_ASSERT(i != stats.end());
47  return (this->*i->second)();
48  }
49 
50  typedef unsigned (unsigned_statistics::*unsigned_fun)() const;
51  typedef std::map<const char*, unsigned_fun, char_ptr_less_than> stats_map;
52  stats_map stats;
53  };
54 
61  {
62  public:
64  : set(false)
65  {
66  }
67 
69  : set(false)
70  {
71  seteq(o);
72  }
73 
74  bool
75  seteq(const unsigned_statistics& o)
76  {
77  if (!set)
78  {
79  for (auto& i: o.stats)
80  stats[i.first] = (o.*i.second)();
81  set = true;
82  return true;
83  }
84  if (*this == o)
85  return true;
86  return false;
87  }
88 
89  typedef std::map<const char*, unsigned, char_ptr_less_than> stats_map;
90  stats_map stats;
91 
92 
93  bool
94  operator==(const unsigned_statistics_copy& o) const
95  {
96  for (auto& i: stats)
97  {
98  auto i2 = o.stats.find(i.first);
99  if (i2 == o.stats.end())
100  return false;
101  if (i.second != i2->second)
102  return false;
103  }
104  return true;
105  }
106 
107  bool
108  operator!=(const unsigned_statistics_copy& o) const
109  {
110  return !(*this == o);
111  }
112 
113  bool set;
114  };
115 
122  {
123  public :
124  ec_statistics()
125  : states_(0), transitions_(0), depth_(0), max_depth_(0)
126  {
127  stats["states"] =
128  static_cast<unsigned_statistics::unsigned_fun>(&ec_statistics::states);
129  stats["transitions"] =
130  static_cast<unsigned_statistics::unsigned_fun>
131  (&ec_statistics::transitions);
132  stats["max. depth"] =
133  static_cast<unsigned_statistics::unsigned_fun>
134  (&ec_statistics::max_depth);
135  }
136 
137  void
138  set_states(unsigned n)
139  {
140  states_ = n;
141  }
142 
143  void
144  inc_states()
145  {
146  ++states_;
147  }
148 
149  void
150  inc_transitions()
151  {
152  ++transitions_;
153  }
154 
155  void
156  inc_depth(unsigned n = 1)
157  {
158  depth_ += n;
159  if (depth_ > max_depth_)
160  max_depth_ = depth_;
161  }
162 
163  void
164  dec_depth(unsigned n = 1)
165  {
166  SPOT_ASSERT(depth_ >= n);
167  depth_ -= n;
168  }
169 
170  unsigned
171  states() const
172  {
173  return states_;
174  }
175 
176  unsigned
177  transitions() const
178  {
179  return transitions_;
180  }
181 
182  unsigned
183  max_depth() const
184  {
185  return max_depth_;
186  }
187 
188  unsigned
189  depth() const
190  {
191  return depth_;
192  }
193 
194  private :
195  unsigned states_;
196  unsigned transitions_;
197  unsigned depth_;
198  unsigned max_depth_;
199  };
200 
207  {
208  public:
210  : prefix_states_(0), cycle_states_(0)
211  {
212  stats["(non unique) states for prefix"] =
213  static_cast<unsigned_statistics::unsigned_fun>
214  (&ars_statistics::ars_prefix_states);
215  stats["(non unique) states for cycle"] =
216  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  return prefix_states_;
230  }
231 
232  void
233  inc_ars_cycle_states()
234  {
235  ++cycle_states_;
236  }
237 
238  unsigned
239  ars_cycle_states() const
240  {
241  return cycle_states_;
242  }
243 
244  private:
245  unsigned prefix_states_;
246  unsigned cycle_states_;
247  };
248 
255  {
256  public:
258  {
259  stats["search space states"] =
260  static_cast<unsigned_statistics::unsigned_fun>
262  }
263 
264  virtual
265  ~acss_statistics()
266  {
267  }
268 
270  virtual unsigned acss_states() const = 0;
271  };
273 }
Definition: graph.hh:32
Emptiness-check statistics.
Definition: emptiness_stats.hh:121
virtual unsigned acss_states() const =0
Number of states in the search space for the accepting cycle.
comparable statistics
Definition: emptiness_stats.hh:60
Accepting Cycle Search Space statistics.
Definition: emptiness_stats.hh:254
Accepting Run Search statistics.
Definition: emptiness_stats.hh:206
Definition: emptiness_stats.hh:35

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Tue Sep 20 2016 07:13:02 for spot by doxygen 1.8.8