spot 2.11.0.dev
stats.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2008, 2011-2017, 2020 Laboratoire de Recherche et
3// 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
58
59 class SPOT_API printable_formula: public printable_value<formula>
60 {
61 public:
63 operator=(formula new_val)
64 {
65 val_ = new_val;
66 return *this;
67 }
68
69 virtual void
70 print(std::ostream& os, const char*) const override;
71 };
72
73 class SPOT_API printable_acc_cond final: public spot::printable
74 {
75 acc_cond val_;
76 public:
78 operator=(const acc_cond& new_val)
79 {
80 val_ = new_val;
81 return *this;
82 }
83
84 void print(std::ostream& os, const char* pos) const override;
85 };
86
87 class SPOT_API printable_scc_info final:
88 public spot::printable
89 {
90 std::unique_ptr<scc_info> val_;
91 public:
92 void automaton(const const_twa_graph_ptr& aut)
93 {
94 val_ = std::make_unique<scc_info>(aut);
95 }
96
97 void reset()
98 {
99 val_ = nullptr;
100 }
101
102 void print(std::ostream& os, const char* pos) const override;
103 };
104
110 class SPOT_API stat_printer: protected formater
111 {
112 public:
113 stat_printer(std::ostream& os, const char* format);
114
119 std::ostream&
120 print(const const_twa_graph_ptr& aut, formula f = nullptr);
121
122 private:
123 const char* format_;
124
125 printable_formula form_;
131 printable_value<unsigned> nondetstates_;
132 printable_value<unsigned> deterministic_;
134 printable_acc_cond gen_acc_;
135 };
136
138}
An acceptance condition.
Definition: acc.hh:62
Definition: formater.hh:113
Main class for temporal logic formula.
Definition: formula.hh:715
Definition: stats.hh:74
Definition: stats.hh:60
Definition: stats.hh:89
Definition: formater.hh:44
Definition: formater.hh:31
prints various statistics about a TGBA
Definition: stats.hh:111
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.
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.4