spot  2.12.1
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/twa/twa.hh>
22 #include <spot/twaalgos/sccinfo.hh>
23 #include <iosfwd>
24 #include <spot/misc/formater.hh>
25 
26 namespace spot
27 {
28 
31 
32  struct SPOT_API twa_statistics
33  {
34  unsigned edges;
35  unsigned states;
36 
37  twa_statistics() { edges = 0; states = 0; }
38  std::ostream& dump(std::ostream& out) const;
39  };
40 
41  struct SPOT_API twa_sub_statistics: public twa_statistics
42  {
43  unsigned long long transitions;
44 
45  twa_sub_statistics() { transitions = 0; }
46  std::ostream& dump(std::ostream& out) const;
47  };
48 
50  SPOT_API twa_statistics stats_reachable(const const_twa_ptr& g);
52  SPOT_API twa_sub_statistics sub_stats_reachable(const const_twa_ptr& g);
53 
55  SPOT_API unsigned long long
56  count_all_transitions(const const_twa_graph_ptr& g);
57 
58  class SPOT_API printable_formula: public printable_value<formula>
59  {
60  public:
62  operator=(formula new_val)
63  {
64  val_ = new_val;
65  return *this;
66  }
67 
68  virtual void
69  print(std::ostream& os, const char*) const override;
70  };
71 
72  class SPOT_API printable_acc_cond final: public spot::printable
73  {
74  acc_cond val_;
75  public:
77  operator=(const acc_cond& new_val)
78  {
79  val_ = new_val;
80  return *this;
81  }
82 
83  void print(std::ostream& os, const char* pos) const override;
84  };
85 
86  class SPOT_API printable_scc_info final:
87  public spot::printable
88  {
89  std::unique_ptr<scc_info> val_;
90  public:
91  void automaton(const const_twa_graph_ptr& aut)
92  {
93  val_ = std::make_unique<scc_info>(aut);
94  }
95 
96  void reset()
97  {
98  val_ = nullptr;
99  }
100 
101  void print(std::ostream& os, const char* pos) const override;
102  };
103 
104  class SPOT_API printable_size final:
105  public spot::printable
106  {
107  unsigned reachable_ = 0;
108  unsigned all_ = 0;
109  public:
110  void set(unsigned reachable, unsigned all)
111  {
112  reachable_ = reachable;
113  all_ = all;
114  }
115 
116  void print(std::ostream& os, const char* pos) const override;
117  };
118 
119  class SPOT_API printable_long_size final:
120  public spot::printable
121  {
122  unsigned long long reachable_ = 0;
123  unsigned long long all_ = 0;
124  public:
125  void set(unsigned long long reachable, unsigned long long all)
126  {
127  reachable_ = reachable;
128  all_ = all;
129  }
130 
131  void print(std::ostream& os, const char* pos) const override;
132  };
133 
139  class SPOT_API stat_printer: protected formater
140  {
141  public:
142  stat_printer(std::ostream& os, const char* format);
143 
148  std::ostream&
149  print(const const_twa_graph_ptr& aut, formula f = nullptr);
150 
151  private:
152  const char* format_;
153 
154  printable_formula form_;
155  printable_size states_;
156  printable_size edges_;
157  printable_long_size trans_;
159  printable_scc_info scc_;
160  printable_value<unsigned> nondetstates_;
161  printable_value<unsigned> deterministic_;
162  printable_value<unsigned> complete_;
163  printable_acc_cond gen_acc_;
164  };
165 
167 }
An acceptance condition.
Definition: acc.hh:61
Definition: formater.hh:112
Main class for temporal logic formula.
Definition: formula.hh:732
Definition: stats.hh:73
Definition: stats.hh:59
Definition: stats.hh:121
Definition: stats.hh:88
Definition: stats.hh:106
Definition: formater.hh:43
Definition: formater.hh:30
prints various statistics about a TGBA
Definition: stats.hh:140
std::ostream & print(const const_twa_graph_ptr &aut, formula f=nullptr)
print the configured statistics.
ta_statistics stats_reachable(const const_ta_ptr &t)
Compute statistics for an automaton.
unsigned long long count_all_transitions(const const_twa_graph_ptr &g)
Count all transitions, even unreachable ones.
twa_sub_statistics sub_stats_reachable(const const_twa_ptr &g)
Compute sub statistics for an automaton.
Definition: automata.hh:26
Definition: stats.hh:33
Definition: stats.hh:42

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