common_aoutput.hh 5.99 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

20
#pragma once
21
22

#include "common_sys.hh"
23
#include "common_file.hh"
24
25

#include <argp.h>
26
#include <memory>
27
#include <spot/misc/timer.hh>
28
29
30
#include <spot/parseaut/public.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/isdet.hh>
31
32
33
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/stats.hh>
#include <spot/twaalgos/word.hh>
34
#include <spot/tl/formula.hh>
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49


// Format for automaton output
enum automaton_format_t {
  Dot,
  Lbtt,
  Spin,
  Stats,
  Hoa,
  Quiet,
  Count,
};

// The format to use in output_automaton()
extern automaton_format_t automaton_format;
50
// Set to the argument of --name, else nullptr.
51
extern const char* opt_name;
52
53
54
55
56
57
58
59
60
61
62
63
64
// Output options
extern const struct argp aoutput_argp;

// help text for %F and %L
extern char F_doc[32];
extern char L_doc[32];

// FORMAT help text
extern const struct argp aoutput_io_format_argp;
extern const struct argp aoutput_o_format_argp;

// Parse output options
int parse_opt_aoutput(int key, char* arg, struct argp_state* state);
65

66
67
68

enum stat_style { no_input, aut_input, ltl_input };

69
70
71
72
73
74
75
76

struct printable_automaton final:
  public spot::printable_value<spot::const_twa_graph_ptr>
{
  using spot::printable_value<spot::const_twa_graph_ptr>::operator=;
  void print(std::ostream& os, const char* pos) const override;
};

77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110

struct process_timer
{
  void start()
  {
    sw.start();
    dt.start();
  }

  void stop()
  {
    // sw.stop() --> It always returns the duration since the last call to
    // start(). Therefore, it wont't stop timing, moreover, it can be called
    // multiple times.
    sw_lap_ = sw.stop();
    dt.stop();
  }
  double get_lap_sw()
  {
    return sw_lap_;
  }

  spot::timer dt;
  spot::stopwatch sw;
  double sw_lap_ = 0;
};

struct printable_timer final:
  public spot::printable_value<spot::timer>
{
  using spot::printable_value<spot::timer>::operator=;
  void print(std::ostream& os, const char* pos) const override;
};

111
112
113
114
115
116
117
118
119
120
121
122
123
struct printable_varset final: public spot::printable
{
protected:
  std::vector<spot::formula> val_;
  void sort()
  {
    std::sort(val_.begin(), val_.end(),
              [](spot::formula f, spot::formula g)
              {
                return strverscmp(f.ap_name().c_str(), g.ap_name().c_str()) < 0;
              });
  }
public:
124
125
126
127
  void clear()
  {
    val_.clear();
  }
128
129
130
131

  template<class T>
  void set(T begin, T end)
  {
132
    clear();
133
134
135
136
137
138
139
140
141
142
143
144
145
146
    val_.insert(val_.end(), begin, end);
    sort();
  }

  printable_varset& operator=(const std::vector<spot::formula>& val)
  {
    val_ = val;
    sort();
    return *this;
  }

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

147
148
149
150
151
152
153
154
/// \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.
class hoa_stat_printer: protected spot::stat_printer
{
public:
155
  hoa_stat_printer(std::ostream& os, const char* format,
156
      stat_style input = no_input);
157

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
158
  using spot::formater::declare;
159
  using spot::formater::set_output;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
160

161
162
163
164
165
  /// \brief print the configured statistics.
  ///
  /// The \a f argument is not needed if the Formula does not need
  /// to be output.
  std::ostream&
166
    print(const spot::const_parsed_aut_ptr& haut,
167
168
        const spot::const_twa_graph_ptr& aut,
        spot::formula f,
169
        const char* filename, int loc, process_timer& ptimer,
170
        const char* csv_prefix, const char* csv_suffix);
171
172
173

private:
  spot::printable_value<const char*> filename_;
174
  spot::printable_value<std::string> location_;
175
176
177
  spot::printable_value<std::string> haut_name_;
  spot::printable_value<std::string> aut_name_;
  spot::printable_value<std::string> aut_word_;
178
  spot::printable_value<std::string> haut_word_;
179
  spot::printable_value<std::string> haut_gen_acc_;
180
181
182
183
  spot::printable_value<unsigned> haut_states_;
  spot::printable_value<unsigned> haut_edges_;
  spot::printable_value<unsigned> haut_trans_;
  spot::printable_value<unsigned> haut_acc_;
184
185
  printable_varset haut_ap_;
  printable_varset aut_ap_;
186
  spot::printable_scc_info haut_scc_;
187
188
189
  spot::printable_value<unsigned> haut_deterministic_;
  spot::printable_value<unsigned> haut_nondetstates_;
  spot::printable_value<unsigned> haut_complete_;
190
191
  spot::printable_value<const char*> csv_prefix_;
  spot::printable_value<const char*> csv_suffix_;
192
  printable_timer timer_;
193
194
  printable_automaton input_aut_;
  printable_automaton output_aut_;
195
196
197
198
199
200
201
202
};


class automaton_printer
{
  hoa_stat_printer statistics;
  std::ostringstream name;
  hoa_stat_printer namer;
203
204
205
  std::ostringstream outputname;
  hoa_stat_printer outputnamer;
  std::map<std::string, std::unique_ptr<output_file>> outputfiles;
206
207

public:
208
  automaton_printer(stat_style input = no_input);
209
  ~automaton_printer();
210
211

  void
212
  print(const spot::twa_graph_ptr& aut,
213
        process_timer& ptimer,
214
215
216
217
218
219
220
221
        spot::formula f = nullptr,
        // Input location for errors and statistics.
        const char* filename = nullptr,
        int loc = -1,
        // Time and input automaton for statistics
        const spot::const_parsed_aut_ptr& haut = nullptr,
        const char* csv_prefix = nullptr,
        const char* csv_suffix = nullptr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
222
223

  void add_stat(char c, const spot::printable* p);
224
};
225
226

void setup_default_output_format();