spot 2.11.2.dev
emptiness_stats.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2015-2017 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 <spot/misc/common.hh>
26#include <spot/misc/ltstr.hh>
27#include <map>
28
29namespace 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 : states_(0), transitions_(0), depth_(0), max_depth_(0)
65 {
66 stats["states"] =
67 static_cast<unsigned_statistics::unsigned_fun>(&ec_statistics::states);
68 stats["transitions"] =
69 static_cast<unsigned_statistics::unsigned_fun>
70 (&ec_statistics::transitions);
71 stats["max. depth"] =
72 static_cast<unsigned_statistics::unsigned_fun>
73 (&ec_statistics::max_depth);
74 }
75
76 void
77 set_states(unsigned n)
78 {
79 states_ = n;
80 }
81
82 void
83 inc_states()
84 {
85 ++states_;
86 }
87
88 void
89 inc_transitions()
90 {
91 ++transitions_;
92 }
93
94 void
95 inc_depth(unsigned n = 1)
96 {
97 depth_ += n;
98 if (depth_ > max_depth_)
99 max_depth_ = depth_;
100 }
101
102 void
103 dec_depth(unsigned n = 1)
104 {
105 SPOT_ASSERT(depth_ >= n);
106 depth_ -= n;
107 }
108
109 unsigned
110 states() const
111 {
112 return states_;
113 }
114
115 unsigned
116 transitions() const
117 {
118 return transitions_;
119 }
120
121 unsigned
122 max_depth() const
123 {
124 return max_depth_;
125 }
126
127 unsigned
128 depth() const
129 {
130 return depth_;
131 }
132
133 private :
134 unsigned states_;
135 unsigned transitions_;
136 unsigned depth_;
137 unsigned max_depth_;
138 };
139
146 {
147 public:
149 : prefix_states_(0), cycle_states_(0)
150 {
151 stats["(non unique) states for prefix"] =
152 static_cast<unsigned_statistics::unsigned_fun>
153 (&ars_statistics::ars_prefix_states);
154 stats["(non unique) states for cycle"] =
155 static_cast<unsigned_statistics::unsigned_fun>
156 (&ars_statistics::ars_cycle_states);
157 }
158
159 void
160 inc_ars_prefix_states()
161 {
162 ++prefix_states_;
163 }
164
165 unsigned
166 ars_prefix_states() const
167 {
168 return prefix_states_;
169 }
170
171 void
172 inc_ars_cycle_states()
173 {
174 ++cycle_states_;
175 }
176
177 unsigned
178 ars_cycle_states() const
179 {
180 return cycle_states_;
181 }
182
183 private:
184 unsigned prefix_states_;
185 unsigned cycle_states_;
186 };
187
194 {
195 public:
197 {
198 stats["search space states"] =
199 static_cast<unsigned_statistics::unsigned_fun>
201 }
202
203 virtual
205 {
206 }
207
209 virtual unsigned acss_states() const = 0;
210 };
212}
Accepting Cycle Search Space statistics.
Definition: emptiness_stats.hh:194
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:146
Emptiness-check statistics.
Definition: emptiness_stats.hh:61
Definition: automata.hh:27
Definition: emptiness_stats.hh:36

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.4