common_aoutput.hh 5.81 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// de l'Epita (LRDE).
//
// 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
23
24

#include "common_sys.hh"

#include <argp.h>
25
#include <memory>
26

27
#include "parseaut/public.hh"
28

29
30
31
32
33
#include "twaalgos/stats.hh"
#include "twaalgos/sccinfo.hh"
#include "twaalgos/gtec/gtec.hh"
#include "twaalgos/word.hh"
#include "twaalgos/isdet.hh"
34
#include "common_file.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
/// \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:
77
  hoa_stat_printer(std::ostream& os, const char* format,
78
		   stat_style input = no_input)
79
80
    : spot::stat_printer(os, format)
  {
81
    if (input == aut_input)
82
83
84
85
      {
	declare('A', &haut_acc_);
	declare('C', &haut_scc_);
	declare('E', &haut_edges_);
86
	declare('G', &haut_gen_acc_);
87
88
89
90
	declare('M', &haut_name_);
	declare('S', &haut_states_);
	declare('T', &haut_trans_);
      }
91
    declare('F', &filename_);
92
    declare('L', &location_);
93
94
    if (input != ltl_input)
      declare('f', &filename_);	// Override the formula printer.
95
96
97
98
    declare('m', &aut_name_);
    declare('w', &aut_word_);
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
99
  using spot::formater::declare;
100
  using spot::formater::set_output;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
101

102
103
104
105
106
  /// \brief print the configured statistics.
  ///
  /// The \a f argument is not needed if the Formula does not need
  /// to be output.
  std::ostream&
107
  print(const spot::const_parsed_aut_ptr& haut,
108
	const spot::const_twa_graph_ptr& aut,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
	spot::formula f,
110
	const char* filename, int loc, double run_time)
111
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
112
    filename_ = filename ? filename : "";
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
    if (loc >= 0 && has('L'))
      {
	std::ostringstream os;
	os << loc;
	location_ = os.str();
      }
    if (haut)
      {
	if (loc < 0 && has('L'))
	  {
	    std::ostringstream os;
	    os << haut->loc;
	    location_ = os.str();
	  }

	if (has('T'))
	  {
130
	    spot::twa_sub_statistics s = sub_stats_reachable(haut->aut);
131
	    haut_states_ = s.states;
132
133
	    haut_edges_ = s.edges;
	    haut_trans_ = s.transitions;
134
135
136
	  }
	else if (has('E'))
	  {
137
	    spot::twa_sub_statistics s = sub_stats_reachable(haut->aut);
138
	    haut_states_ = s.states;
139
	    haut_edges_ = s.edges;
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
	  }
	if (has('M'))
	  {
	    auto n = haut->aut->get_named_prop<std::string>("automaton-name");
	    if (n)
	      haut_name_ = *n;
	    else
	      haut_name_.val().clear();
	  }
	if (has('S'))
	  haut_states_ = haut->aut->num_states();

	if (has('A'))
	  haut_acc_ = haut->aut->acc().num_sets();

	if (has('C'))
	  haut_scc_ = spot::scc_info(haut->aut).scc_count();
157
158
159
160
161
162
163

	if (has('G'))
	  {
	    std::ostringstream os;
	    os << haut->aut->get_acceptance();
	    haut_gen_acc_ = os.str();
	  }
164
      }
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180

    if (has('m'))
	{
	  auto n = aut->get_named_prop<std::string>("automaton-name");
	  if (n)
	    aut_name_ = *n;
	  else
	    aut_name_.val().clear();
	}
    if (has('w'))
	{
	  auto res = spot::couvreur99(aut)->check();
	  if (res)
	    {
	      auto run = res->accepting_run();
	      assert(run);
181
	      spot::twa_word w(run->reduce());
182
183
	      w.simplify();
	      std::ostringstream out;
184
	      out << w;
185
186
187
188
189
190
191
192
	      aut_word_ = out.str();
	    }
	  else
	    {
	      aut_word_.val().clear();
	    }
	}

193
    return this->spot::stat_printer::print(aut, f, run_time);
194
195
196
197
  }

private:
  spot::printable_value<const char*> filename_;
198
  spot::printable_value<std::string> location_;
199
200
201
  spot::printable_value<std::string> haut_name_;
  spot::printable_value<std::string> aut_name_;
  spot::printable_value<std::string> aut_word_;
202
  spot::printable_value<std::string> haut_gen_acc_;
203
204
205
206
207
208
209
210
211
212
213
214
215
  spot::printable_value<unsigned> haut_states_;
  spot::printable_value<unsigned> haut_edges_;
  spot::printable_value<unsigned> haut_trans_;
  spot::printable_value<unsigned> haut_acc_;
  spot::printable_value<unsigned> haut_scc_;
};


class automaton_printer
{
  hoa_stat_printer statistics;
  std::ostringstream name;
  hoa_stat_printer namer;
216
217
218
  std::ostringstream outputname;
  hoa_stat_printer outputnamer;
  std::map<std::string, std::unique_ptr<output_file>> outputfiles;
219
220
221

public:

222
  automaton_printer(stat_style input = no_input);
223
224

  void
225
  print(const spot::twa_graph_ptr& aut,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
226
	spot::formula f = nullptr,
227
228
	// Input location for errors and statistics.
	const char* filename = nullptr,
229
	int loc = -1,
230
231
	// Time and input automaton for statistics
	double time = 0.0,
232
	const spot::const_parsed_aut_ptr& haut = nullptr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
233
234

  void add_stat(char c, const spot::printable* p);
235
};