stats.hh 3.48 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2008, 2011-2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6
7
8
9
10
11
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// 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
14
15
16
17
18
19
20
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// 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
30
31

namespace spot
{
32

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
33
  /// \addtogroup twa_misc
34
35
  /// @{

36
  struct SPOT_API twa_statistics
37
  {
38
    unsigned edges;
39
    unsigned states;
40

41
    twa_statistics() { edges = 0; states = 0; }
42
43
44
    std::ostream& dump(std::ostream& out) const;
  };

45
  struct SPOT_API twa_sub_statistics: public twa_statistics
46
  {
47
    unsigned transitions;
48

49
    twa_sub_statistics() { transitions = 0; }
50
    std::ostream& dump(std::ostream& out) const;
51
52
  };

53
  /// \brief Compute statistics for an automaton.
54
  SPOT_API twa_statistics stats_reachable(const const_twa_ptr& g);
55
  /// \brief Compute sub statistics for an automaton.
56
  SPOT_API twa_sub_statistics sub_stats_reachable(const const_twa_ptr& g);
57

58

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
59
  class SPOT_API printable_formula: public printable_value<formula>
60
61
62
  {
  public:
    printable_formula&
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63
    operator=(formula new_val)
64
65
66
67
68
69
    {
      val_ = new_val;
      return *this;
    }

    virtual void
70
    print(std::ostream& os, const char*) const override;
71
72
  };

73
74
75
76
77
78
79
  class SPOT_API printable_scc_info final:
    public spot::printable
  {
    std::unique_ptr<scc_info> val_;
  public:
    void automaton(const const_twa_graph_ptr& aut)
    {
80
      val_ = std::make_unique<scc_info>(aut);
81
82
83
84
85
86
87
88
89
90
    }

    void reset()
    {
      val_ = nullptr;
    }

    void print(std::ostream& os, const char* pos) const override;
  };

91
92
93
94
95
  /// \brief prints various statistics about a TGBA
  ///
  /// This object can be configured to display various statistics
  /// about a TGBA.  Some %-sequence of characters are interpreted in
  /// the format string, and replaced by the corresponding statistics.
96
  class SPOT_API stat_printer: protected formater
97
98
99
100
101
102
103
  {
  public:
    stat_printer(std::ostream& os, const char* format);

    /// \brief print the configured statistics.
    ///
    /// The \a f argument is not needed if the Formula does not need
104
    /// to be output, and so is \a run_time).
105
    std::ostream&
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
106
      print(const const_twa_graph_ptr& aut, formula f = nullptr,
107
            double run_time = -1.);
108
109
110

  private:
    const char* format_;
111
112
113
114
115
116

    printable_formula form_;
    printable_value<unsigned> states_;
    printable_value<unsigned> edges_;
    printable_value<unsigned> trans_;
    printable_value<unsigned> acc_;
117
    printable_scc_info scc_;
118
119
    printable_value<unsigned> nondetstates_;
    printable_value<unsigned> deterministic_;
120
    printable_value<unsigned> complete_;
121
    printable_value<double> run_time_;
122
    printable_value<std::string> gen_acc_;
123
124
  };

125
  /// @}
126
}