common_aoutput.cc 23.5 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012-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
21
#include "common_sys.hh"
#include "error.h"
22
#include "argmatch.h"
23
#include "common_output.hh"
24
25
26
27
#include "common_aoutput.hh"
#include "common_post.hh"
#include "common_cout.hh"

28
#include <unistd.h>
29
#include <ctime>
30
31
#include <ctype.h>
#include <spot/misc/escape.hh>
32
33
34
35
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/isunamb.hh>
36
37
#include <spot/twaalgos/lbtt.hh>
#include <spot/twaalgos/neverclaim.hh>
38
#include <spot/twaalgos/strength.hh>
39
#include <spot/twaalgos/stutter.hh>
40
#include <spot/twaalgos/isdet.hh>
41

42
automaton_format_t automaton_format = Hoa;
43
static const char* automaton_format_opt = nullptr;
44
const char* opt_name = nullptr;
45
static const char* opt_output = nullptr;
46
static const char* stats = "";
47
48
enum check_type
  {
49
50
    check_unambiguous = (1 << 0),
    check_stutter = (1 << 1),
51
    check_strength = (1 << 2),
52
    check_semi_determinism = (1 << 3),
53
54
55
56
    check_all = -1U,
  };
static char const *const check_args[] =
  {
57
    "unambiguous",
58
59
60
    "stutter-invariant", "stuttering-invariant",
    "stutter-insensitive", "stuttering-insensitive",
    "stutter-sensitive", "stuttering-sensitive",
61
    "strength", "weak", "terminal",
62
    "semi-determinism", "semi-deterministic",
63
    "all",
64
    nullptr
65
66
67
  };
static check_type const check_types[] =
  {
68
    check_unambiguous,
69
70
71
    check_stutter, check_stutter,
    check_stutter, check_stutter,
    check_stutter, check_stutter,
72
    check_strength, check_strength, check_strength,
73
    check_semi_determinism, check_semi_determinism,
74
75
76
77
    check_all
  };
ARGMATCH_VERIFY(check_args, check_types);
unsigned opt_check = 0U;
78

79
enum {
80
  OPT_LBTT = 1,
81
82
  OPT_NAME,
  OPT_STATS,
83
  OPT_CHECK,
84
};
85
86
87
88

static const argp_option options[] =
  {
    /**************************************************/
89
    { nullptr, 0, nullptr, 0, "Output format:", 3 },
90
    { "dot", 'd',
91
      "1|a|b|B|c|C(COLOR)|e|f(FONT)|h|k|n|N|o|r|R|s|t|v|y|+INT|<INT|#",
92
      OPTION_ARG_OPTIONAL,
93
      "GraphViz's format.  Add letters for "
94
95
      "(1) force numbered states, "
      "(a) acceptance display, (b) acceptance sets as bullets, "
96
      "(B) bullets except for Büchi/co-Büchi automata, "
97
98
99
      "(c) force circular nodes, "
      "(C) color nodes with COLOR, "
      "(e) force elliptic nodes, "
100
      "(f(FONT)) use FONT, (h) horizontal layout, "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
101
102
      "(k) use state labels when possible, "
      "(n) with name, (N) without name, "
103
104
105
      "(o) ordered transitions, "
      "(r) rainbow colors for acceptance sets, "
      "(R) color acceptance sets by Inf/Fin, (s) with SCCs, "
106
      "(t) force transition-based acceptance, "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
107
      "(v) vertical layout, "
108
      "(y) split universal edges by color, "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
      "(+INT) add INT to all set numbers, "
110
111
      "(<INT) display at most INT states, "
      "(#) show internal edge numbers", 0 },
112
    { "hoaf", 'H', "1.1|i|k|l|m|s|t|v", OPTION_ARG_OPTIONAL,
113
      "Output the automaton in HOA format (default).  Add letters to select "
114
      "(1.1) version 1.1 of the format, "
115
      "(i) use implicit labels for complete deterministic automata, "
116
117
118
      "(s) prefer state-based acceptance when possible [default], "
      "(t) force transition-based acceptance, "
      "(m) mix state and transition-based acceptance, "
119
      "(k) use state labels when possible, "
120
121
      "(l) single-line output, "
      "(v) verbose properties", 0 },
122
123
124
    { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
      "LBTT's format (add =t to force transition-based acceptance even"
      " on Büchi automata)", 0 },
125
126
    { "name", OPT_NAME, "FORMAT", 0,
      "set the name of the output automaton", 0 },
127
128
129
130
    { "output", 'o', "FORMAT", 0,
      "send output to a file named FORMAT instead of standard output.  The"
      " first automaton sent to a file truncates it unless FORMAT starts"
      " with '>>'.", 0 },
131
    { "quiet", 'q', nullptr, 0, "suppress all normal output", 0 },
132
133
134
    { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)."
      "  Add letters to select (6) Spin's 6.2.4 style, (c) comments on states",
      0 },
135
    { "utf8", '8', nullptr, 0, "enable UTF-8 characters in output "
136
137
138
      "(ignored with --lbtt or --spin)", 0 },
    { "stats", OPT_STATS, "FORMAT", 0,
      "output statistics about the automaton", 0 },
139
140
141
    { "check", OPT_CHECK, "PROP", OPTION_ARG_OPTIONAL,
      "test for the additional property PROP and output the result "
      "in the HOA format (implies -H).  PROP may be any prefix of "
142
143
      "'all' (default), 'unambiguous', 'stutter-invariant', or 'strength'.",
      0 },
144
    { nullptr, 0, nullptr, 0, nullptr, 0 }
145
146
  };

147
const struct argp aoutput_argp = { options, parse_opt_aoutput, nullptr, nullptr,
148
                                   nullptr, nullptr, nullptr };
149
150
151
152
153
154
155
156
157

// Those can be overridden by individual tools. E.g. randaut has no
// notion of input file, so %F and %L represent something else.
char F_doc[32] = "name of the input file";
char L_doc[32] = "location in the input file";

static const argp_option io_options[] =
  {
    /**************************************************/
158
    { nullptr, 0, nullptr, 0, "Any FORMAT string may use "\
159
160
      "the following interpreted sequences (capitals for input,"
      " minuscules for output):", 4 },
161
162
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
163
164
165
    { "%H, %h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "the automaton in HOA format on a single line (use %[opt]H or %[opt]h "
      "to specify additional options as in --hoa=opt)", 0 },
166
    { "%M, %m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
167
      "name of the automaton", 0 },
168
169
170
171
172
    { "%S, %s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "number of states", 0 },
    { "%E, %e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "number of edges", 0 },
    { "%T, %t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
173
      "number of transitions", 0 },
174
    { "%A, %a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
175
      "number of acceptance sets", 0 },
176
    { "%G, %g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
177
      "acceptance condition (in HOA syntax)", 0 },
178
179
180
181
182
183
    { "%C, %c, %[LETTERS]C, %[LETTERS]c", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      "number of SCCs; you may filter the SCCs to count "
      "using the following LETTERS, possibly concatenated: (a) accepting, "
      "(r) rejecting, (v) trivial, (t) terminal, (w) weak, "
      "(iw) inherently weak. Use uppercase letters to negate them.", 0 },
184
185
186
    { "%R, %[LETTERS]R", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      "CPU time (excluding parsing), in seconds; Add LETTERS to restrict to"
187
188
      "(u) user time, (s) system time, (p) parent process, "
      "or (c) children processes.", 0 },
189
190
191
192
193
194
    { "%N, %n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "number of nondeterministic states", 0 },
    { "%D, %d", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the automaton is deterministic, 0 otherwise", 0 },
    { "%P, %p", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the automaton is complete, 0 otherwise", 0 },
195
    { "%r", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
196
      "wall-clock time elapsed in seconds (excluding parsing)", 0 },
197
198
    { "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "one word accepted by the automaton", 0 },
199
200
201
    { "%X, %x, %[LETTERS]X, %[LETTERS]x", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 },
202
203
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
204
205
206
207
208
209
    { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "the part of the line before the automaton if it "
      "comes from a column extracted from a CSV file", 4 },
    { "%>", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "the part of the line after the automaton if it "
      "comes from a column extracted from a CSV file", 4 },
210
    { nullptr, 0, nullptr, 0, nullptr, 0 }
211
212
  };

213
const struct argp aoutput_io_format_argp = { io_options, nullptr, nullptr,
214
215
                                             nullptr, nullptr,
                                             nullptr, nullptr };
216
217
218
219

static const argp_option o_options[] =
  {
    /**************************************************/
220
    { nullptr, 0, nullptr, 0, "Any FORMAT string may use "\
221
      "the following interpreted sequences:", 4 },
222
223
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
224
225
226
    { "%h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "the automaton in HOA format on a single line (use %[opt]h "
      "to specify additional options as in --hoa=opt)", 0 },
227
228
229
230
231
232
233
234
235
    { "%m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "name of the automaton", 0 },
    { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "number of states", 0 },
    { "%e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "number of edges", 0 },
    { "%t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "number of transitions", 0 },
    { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
236
      "number of acceptance sets", 0 },
237
    { "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
238
      "acceptance condition (in HOA syntax)", 0 },
239
240
241
242
243
    { "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "number of SCCs; you may filter the SCCs to count "
      "using the following LETTERS, possibly concatenated: (a) accepting, "
      "(r) rejecting, (v) trivial, (t) terminal, (w) weak, "
      "(iw) inherently weak. Use uppercase letters to negate them.", 0 },
244
245
246
    { "%R, %[LETTERS]R", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      "CPU time (excluding parsing), in seconds; Add LETTERS to restrict to"
247
248
      "(u) user time, (s) system time, (p) parent process, "
      "or (c) children processes.", 0 },
249
    { "%n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
250
      "number of nondeterministic states in output", 0 },
251
    { "%d", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
252
      "1 if the output is deterministic, 0 otherwise", 0 },
253
    { "%p", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
254
      "1 if the output is complete, 0 otherwise", 0 },
255
    { "%r", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
256
      "wall-clock time elapsed in seconds (excluding parsing)", 0 },
257
    { "%w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
258
      "one word accepted by the output automaton", 0 },
259
260
261
    { "%x, %[LETTERS]x", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 },
262
263
264
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
265
266
  };

267
const struct argp aoutput_o_format_argp = { o_options,
268
269
                                            nullptr, nullptr, nullptr,
                                            nullptr, nullptr, nullptr };
270
271
272
273
274
275
276
277
278

int parse_opt_aoutput(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case '8':
      spot::enable_utf8();
      break;
279
280
    case 'd':
      automaton_format = Dot;
281
      automaton_format_opt = arg;
282
      break;
283
284
    case 'H':
      automaton_format = Hoa;
285
      automaton_format_opt = arg;
286
      break;
287
288
289
    case 'o':
      opt_output = arg;
      break;
290
291
292
293
294
295
    case 'q':
      automaton_format = Quiet;
      break;
    case 's':
      automaton_format = Spin;
      if (type != spot::postprocessor::Monitor)
296
        type = spot::postprocessor::BA;
297
      automaton_format_opt = arg;
298
      break;
299
300
301
    case OPT_CHECK:
      automaton_format = Hoa;
      if (arg)
302
        opt_check |= XARGMATCH("--check", arg, check_args, check_types);
303
      else
304
        opt_check |= check_all;
305
      break;
306
    case OPT_LBTT:
307
      automaton_format = Lbtt;
308
      automaton_format_opt = arg;
309
310
311
312
      // This test could be removed when more options are added,
      // because print_lbtt will raise an exception anyway.  The
      // error message is slightly better in the current way.
      if (arg && (arg[0] != 't' || arg[1] != 0))
313
        error(2, 0, "unknown argument for --lbtt: '%s'", arg);
314
315
      break;
    case OPT_NAME:
316
      opt_name = arg;
317
318
319
      break;
    case OPT_STATS:
      if (!*arg)
320
        error(2, 0, "empty format string for --stats");
321
322
323
324
325
326
327
328
329
      stats = arg;
      automaton_format = Stats;
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

330
331
332
333
334
void setup_default_output_format()
{
  if (auto val = getenv("SPOT_DEFAULT_FORMAT"))
    {
      static char const *const args[] =
335
336
337
        {
          "dot", "hoa", "hoaf", nullptr
        };
338
      static automaton_format_t const format[] =
339
340
341
        {
          Dot, Hoa, Hoa
        };
342
343
      auto eq = strchr(val, '=');
      if (eq)
344
345
346
347
        {
          val = strndup(val, eq - val);
          automaton_format_opt = eq + 1;
        }
348
349
350
      ARGMATCH_VERIFY(args, format);
      automaton_format = XARGMATCH("SPOT_DEFAULT_FORMAT", val, args, format);
      if (eq)
351
        free(val);
352
353
    }
}
354

355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format,
                                   stat_style input)
  : spot::stat_printer(os, format)
{
  if (input == aut_input)
    {
      declare('A', &haut_acc_);
      declare('C', &haut_scc_);
      declare('D', &haut_deterministic_);
      declare('E', &haut_edges_);
      declare('G', &haut_gen_acc_);
      declare('H', &input_aut_);
      declare('M', &haut_name_);
      declare('N', &haut_nondetstates_);
      declare('P', &haut_complete_);
      declare('S', &haut_states_);
      declare('T', &haut_trans_);
      declare('W', &haut_word_);
373
      declare('X', &haut_ap_);
374
375
376
377
378
    }
  declare('<', &csv_prefix_);
  declare('>', &csv_suffix_);
  declare('F', &filename_);
  declare('L', &location_);
379
  declare('R', &timer_);
380
381
382
383
384
  if (input != ltl_input)
    declare('f', &filename_);        // Override the formula printer.
  declare('h', &output_aut_);
  declare('m', &aut_name_);
  declare('w', &aut_word_);
385
  declare('x', &aut_ap_);
386
387
388
389
390
391
}

std::ostream&
hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
                        const spot::const_twa_graph_ptr& aut,
                        spot::formula f,
392
                        const char* filename, int loc, process_timer& ptimer,
393
394
                        const char* csv_prefix, const char* csv_suffix)
{
395
396
397
  timer_ = ptimer.dt;
  double run_time = ptimer.get_lap_sw();

398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
  filename_ = filename ? filename : "";
  csv_prefix_ = csv_prefix ? csv_prefix : "";
  csv_suffix_ = csv_suffix ? csv_suffix : "";
  if (loc >= 0 && has('L'))
    {
      std::ostringstream os;
      os << loc;
      location_ = os.str();
    }
  output_aut_ = aut;
  if (haut)
    {
      input_aut_ = haut->aut;
      if (loc < 0 && has('L'))
        {
          std::ostringstream os;
          os << haut->loc;
          location_ = os.str();
        }

      if (has('T'))
        {
          spot::twa_sub_statistics s = sub_stats_reachable(haut->aut);
          haut_states_ = s.states;
          haut_edges_ = s.edges;
          haut_trans_ = s.transitions;
        }
      else if (has('E'))
        {
          spot::twa_sub_statistics s = sub_stats_reachable(haut->aut);
          haut_states_ = s.states;
          haut_edges_ = s.edges;
        }
      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'))
446
        haut_scc_.automaton(haut->aut);
447
448
449
450
451
452
453
454
455
456
457
458

      if (has('N'))
        {
          haut_nondetstates_ = count_nondet_states(haut->aut);
          haut_deterministic_ = (haut_nondetstates_ == 0);
        }
      else if (has('D'))
        {
          // This is more efficient than calling count_nondet_state().
          haut_deterministic_ = is_deterministic(haut->aut);
        }

459
      if (has('P'))
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
        haut_complete_ = is_complete(haut->aut);

      if (has('G'))
        {
          std::ostringstream os;
          os << haut->aut->get_acceptance();
          haut_gen_acc_ = os.str();
        }
      if (has('W'))
        {
          if (auto word = haut->aut->accepting_word())
            {
              std::ostringstream out;
              out << *word;
              haut_word_ = out.str();
            }
          else
            {
              haut_word_.val().clear();
            }
        }
481
      if (has('X'))
482
        haut_ap_ = haut->aut->ap();
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
    }

  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'))
    {
      if (auto word = aut->accepting_word())
        {
          std::ostringstream out;
          out << *word;
          aut_word_ = out.str();
        }
      else
        {
          aut_word_.val().clear();
        }
    }
506
  if (has('x'))
507
    aut_ap_ = aut->ap();
508
509
510
511
512
513
514

  auto& res = this->spot::stat_printer::print(aut, f, run_time);
  // Make sure we do not store the automaton until the next one is
  // printed, as the registered APs will affect how the next
  // automata are built.
  output_aut_ = nullptr;
  input_aut_ = nullptr;
515
  haut_scc_.reset();
516
517
  aut_ap_.clear();
  haut_ap_.clear();
518
519
520
  return res;
}

521
522
automaton_printer::automaton_printer(stat_style input)
  : statistics(std::cout, stats, input),
523
524
    namer(name, opt_name, input),
    outputnamer(outputname, opt_output, input)
525
{
526
527
528
  if (automaton_format == Count && opt_output)
    throw std::runtime_error
      ("options --output and --count are incompatible");
529
}
530
531

void
532
automaton_printer::print(const spot::twa_graph_ptr& aut,
533
534
                         // Time for statistics
                         process_timer& ptimer,
535
536
537
538
                         spot::formula f,
                         // Input location for errors and statistics.
                         const char* filename,
                         int loc,
539
                         // input automaton for statistics
540
541
542
                         const spot::const_parsed_aut_ptr& haut,
                         const char* csv_prefix,
                         const char* csv_suffix)
543
{
544
545
546
  if (opt_check)
    {
      if (opt_check & check_stutter)
547
        spot::check_stutter_invariance(aut, f);
548
      if (opt_check & check_unambiguous)
549
        spot::check_unambiguous(aut);
550
      if (opt_check & check_strength)
551
        spot::check_strength(aut);
552
553
      if (opt_check & check_semi_determinism)
        spot::is_semi_deterministic(aut); // sets the property as a side effect.
554
555
    }

556
557
558
559
  // Name the output automaton.
  if (opt_name)
    {
      name.str("");
560
      namer.print(haut, aut, f, filename, loc, ptimer, csv_prefix, csv_suffix);
561
562
563
      aut->set_named_prop("automaton-name", new std::string(name.str()));
    }

564
565
566
567
  std::ostream* out = &std::cout;
  if (opt_output)
    {
      outputname.str("");
568
      outputnamer.print(haut, aut, f, filename, loc, ptimer,
569
                        csv_prefix, csv_suffix);
570
571
572
      std::string fname = outputname.str();
      auto p = outputfiles.emplace(fname, nullptr);
      if (p.second)
573
        p.first->second.reset(new output_file(fname.c_str()));
574
575
576
      out = &p.first->second->ostream();
    }

577
578
579
580
581
582
583
584
  // Output it.
  switch (automaton_format)
    {
    case Count:
    case Quiet:
      // Do not output anything.
      break;
    case Dot:
585
      spot::print_dot(*out, aut, automaton_format_opt);
586
587
      break;
    case Lbtt:
588
      spot::print_lbtt(*out, aut, automaton_format_opt);
589
590
      break;
    case Hoa:
591
      spot::print_hoa(*out, aut, automaton_format_opt) << '\n';
592
593
      break;
    case Spin:
594
      spot::print_never_claim(*out, aut, automaton_format_opt);
595
596
      break;
    case Stats:
597
      statistics.set_output(*out);
598
      statistics.print(haut, aut, f, filename, loc, ptimer,
599
                       csv_prefix, csv_suffix) << '\n';
600
601
602
603
      break;
    }
  flush_cout();
}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
604
605
606
607
608

void automaton_printer::add_stat(char c, const spot::printable* p)
{
  namer.declare(c, p);
  statistics.declare(c, p);
609
  outputnamer.declare(c, p);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
610
}
611

612
613
614
615
616
617
618
automaton_printer::~automaton_printer()
{
  for (auto& p : outputfiles)
    p.second->close(p.first);
}


619
620
621
622
623
624
625
626
627
628
629
630
631
void printable_automaton::print(std::ostream& os, const char* pos) const
{
  std::string options = "l";
  if (*pos == '[')
    {
      ++pos;
      auto end = strchr(pos, ']');
      options = std::string(pos, end - pos);
      options += 'l';
      pos = end + 1;
    }
  print_hoa(os, val_, options.c_str());
}
632

633
634
635
636
637
638
639
640
641
642
643
644
645

namespace
{
  static void percent_error(const char* beg, const char* pos)
  {
    std::ostringstream tmp;
    const char* end = std::strchr(pos, ']');
    tmp << "unknown option '" << *pos << "' in '%"
        << std::string(beg, end + 2) << '\'';
    throw std::runtime_error(tmp.str());
  }
}

646
647
648
649
void printable_timer::print(std::ostream& os, const char* pos) const
{
  double res = 0;

650
651
652
653
654
655
656
657
658
659
#ifdef _SC_CLK_TCK
  const long clocks_per_sec = sysconf(_SC_CLK_TCK);
#else
#  ifdef CLOCKS_PER_SEC
  const long clocks_per_sec = CLOCKS_PER_SEC;
#  else
  const long clocks_per_sec = 100;
#  endif
#endif

660
661
662
  if (*pos != '[')
  {
    res = val_.get_uscp(true, true, true, true);
663
    os << res / clocks_per_sec;
664
665
666
667
668
669
670
671
672
673
    return;
  }

  bool user = false;
  bool system = false;
  bool parent = false;
  bool children = false;

  const char* beg = pos;
  do
674
675
    switch (*++pos)
      {
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
      case 'u':
        user = true;
        break;
      case 's':
        system = true;
        break;
      case 'p':
        parent = true;
        break;
      case 'c':
        children = true;
        break;
      case ' ':
      case '\t':
      case '\n':
      case ',':
      case ']':
        break;
      default:
695
696
697
        percent_error(beg, pos);
      }
  while (*pos != ']');
698

699
  if (!parent && !children)
700
    parent = children = true;
701
  if (!user && !system)
702
703
704
    user = system = true;

  res = val_.get_uscp(user, system, children, parent);
705
  os << res / clocks_per_sec;
706
}
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771

void printable_varset::print(std::ostream& os, const char* pos) const
{
  if (*pos != '[')
    {
      os << val_.size();
      return;
    }
  char qstyle = 's';            // quote style
  bool parent = false;
  std::string sep;

  const char* beg = pos;
  do
    switch (int c = *++pos)
      {
      case 'p':
        parent = true;
        break;
      case 'c':
      case 'd':
      case 's':
      case 'n':
        qstyle = c;
        break;
      case ']':
        break;
      default:
        if (isalnum(c))
          percent_error(beg, pos);
        sep += c;
      }
  while (*pos != ']');

  if (sep.empty())
    sep = " ";

  bool first = true;
  for (auto f: val_)
    {
      if (first)
        first = false;
      else
        os << sep;
      if (parent)
        os << '(';
      switch (qstyle)
        {
        case 's':
          os << f;
          break;
        case 'n':
          os << f.ap_name();
          break;
        case 'd':
          spot::escape_str(os << '"', f.ap_name()) << '"';
          break;
        case 'c':
          spot::escape_rfc4180(os << '"', f.ap_name()) << '"';
          break;
        }
      if (parent)
        os << ')';
    }
}