spot 2.11.6.dev
Loading...
Searching...
No Matches
stats.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2008, 2011-2017, 2020, 2022 Laboratoire de Recherche
3// et Développement de l'Epita (LRDE).
4// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
5// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6// 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/twa/twa.hh>
26#include <spot/twaalgos/sccinfo.hh>
27#include <iosfwd>
28#include <spot/misc/formater.hh>
29
30namespace spot
31{
32
35
36 struct SPOT_API twa_statistics
37 {
38 unsigned edges;
39 unsigned states;
40
41 twa_statistics() { edges = 0; states = 0; }
42 std::ostream& dump(std::ostream& out) const;
43 };
44
45 struct SPOT_API twa_sub_statistics: public twa_statistics
46 {
47 unsigned long long transitions;
48
49 twa_sub_statistics() { transitions = 0; }
50 std::ostream& dump(std::ostream& out) const;
51 };
52
54 SPOT_API twa_statistics stats_reachable(const const_twa_ptr& g);
56 SPOT_API twa_sub_statistics sub_stats_reachable(const const_twa_ptr& g);
57
59 SPOT_API unsigned long long
60 count_all_transitions(const const_twa_graph_ptr& g);
61
62 class SPOT_API printable_formula: public printable_value<formula>
63 {
64 public:
66 operator=(formula new_val)
67 {
68 val_ = new_val;
69 return *this;
70 }
71
72 virtual void
73 print(std::ostream& os, const char*) const override;
74 };
75
76 class SPOT_API printable_acc_cond final: public spot::printable
77 {
78 acc_cond val_;
79 public:
81 operator=(const acc_cond& new_val)
82 {
83 val_ = new_val;
84 return *this;
85 }
86
87 void print(std::ostream& os, const char* pos) const override;
88 };
89
90 class SPOT_API printable_scc_info final:
91 public spot::printable
92 {
93 std::unique_ptr<scc_info> val_;
94 public:
95 void automaton(const const_twa_graph_ptr& aut)
96 {
97 val_ = std::make_unique<scc_info>(aut);
98 }
99
100 void reset()
101 {
102 val_ = nullptr;
103 }
104
105 void print(std::ostream& os, const char* pos) const override;
106 };
107
108 class SPOT_API printable_size final:
109 public spot::printable
110 {
111 unsigned reachable_ = 0;
112 unsigned all_ = 0;
113 public:
114 void set(unsigned reachable, unsigned all)
115 {
116 reachable_ = reachable;
117 all_ = all;
118 }
119
120 void print(std::ostream& os, const char* pos) const override;
121 };
122
123 class SPOT_API printable_long_size final:
124 public spot::printable
125 {
126 unsigned long long reachable_ = 0;
127 unsigned long long all_ = 0;
128 public:
129 void set(unsigned long long reachable, unsigned long long all)
130 {
131 reachable_ = reachable;
132 all_ = all;
133 }
134
135 void print(std::ostream& os, const char* pos) const override;
136 };
137
143 class SPOT_API stat_printer: protected formater
144 {
145 public:
146 stat_printer(std::ostream& os, const char* format);
147
152 std::ostream&
153 print(const const_twa_graph_ptr& aut, formula f = nullptr);
154
155 private:
156 const char* format_;
157
158 printable_formula form_;
159 printable_size states_;
160 printable_size edges_;
161 printable_long_size trans_;
164 printable_value<unsigned> nondetstates_;
165 printable_value<unsigned> deterministic_;
167 printable_acc_cond gen_acc_;
168 };
169
171}
An acceptance condition.
Definition acc.hh:62
Definition formater.hh:113
Main class for temporal logic formula.
Definition formula.hh:733
Definition stats.hh:77
Definition stats.hh:63
Definition stats.hh:125
Definition stats.hh:92
Definition stats.hh:110
Definition formater.hh:44
Definition formater.hh:31
prints various statistics about a TGBA
Definition stats.hh:144
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 transtitions, even unreachable ones.
twa_sub_statistics sub_stats_reachable(const const_twa_ptr &g)
Compute sub statistics for an automaton.
Definition automata.hh:27
Definition stats.hh:37
Definition stats.hh:46

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