common_aoutput.cc 24.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
3
// 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|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
      "(1) force numbered states, "
95
      "(a) show acceptance condition (default), "
96
      "(A) hide acceptance condition, "
97
      "(b) acceptance sets as bullets, "
98
      "(B) bullets except for Büchi/co-Büchi automata, "
99
100
      "(c) force circular nodes, "
      "(C) color nodes with COLOR, "
101
      "(d) show origins when known, "
102
      "(e) force elliptic nodes, "
103
104
      "(f(FONT)) use FONT, "
      "(h) horizontal layout, "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
105
      "(k) use state labels when possible, "
106
107
      "(n) show name, "
      "(N) hide name, "
108
109
      "(o) ordered transitions, "
      "(r) rainbow colors for acceptance sets, "
110
111
      "(R) color acceptance sets by Inf/Fin, "
      "(s) with SCCs, "
112
      "(t) force transition-based acceptance, "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
113
      "(v) vertical layout, "
114
      "(y) split universal edges by color, "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
115
      "(+INT) add INT to all set numbers, "
116
117
      "(<INT) display at most INT states, "
      "(#) show internal edge numbers", 0 },
118
    { "hoaf", 'H', "1.1|i|k|l|m|s|t|v", OPTION_ARG_OPTIONAL,
119
      "Output the automaton in HOA format (default).  Add letters to select "
120
      "(1.1) version 1.1 of the format, "
121
      "(i) use implicit labels for complete deterministic automata, "
122
123
124
      "(s) prefer state-based acceptance when possible [default], "
      "(t) force transition-based acceptance, "
      "(m) mix state and transition-based acceptance, "
125
      "(k) use state labels when possible, "
126
127
      "(l) single-line output, "
      "(v) verbose properties", 0 },
128
129
130
    { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
      "LBTT's format (add =t to force transition-based acceptance even"
      " on Büchi automata)", 0 },
131
132
    { "name", OPT_NAME, "FORMAT", 0,
      "set the name of the output automaton", 0 },
133
134
135
136
    { "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 },
137
    { "quiet", 'q', nullptr, 0, "suppress all normal output", 0 },
138
139
140
    { "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 },
141
    { "utf8", '8', nullptr, 0, "enable UTF-8 characters in output "
142
143
144
      "(ignored with --lbtt or --spin)", 0 },
    { "stats", OPT_STATS, "FORMAT", 0,
      "output statistics about the automaton", 0 },
145
    { "format", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
146
147
148
    { "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 "
149
150
      "'all' (default), 'unambiguous', 'stutter-invariant', or 'strength'.",
      0 },
151
    { nullptr, 0, nullptr, 0, nullptr, 0 }
152
153
  };

154
const struct argp aoutput_argp = { options, parse_opt_aoutput, nullptr, nullptr,
155
                                   nullptr, nullptr, nullptr };
156
157
158
159
160
161

// 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";

162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
#define doc_g                                                           \
      "acceptance condition (in HOA syntax); add brackets to print "    \
      "an acceptance name instead and LETTERS to tweak the format: "    \
      "(0) no parameters, "                                             \
      "(a) accentuated, "                                               \
      "(b) abbreviated, "                                               \
      "(d) style used in dot output, "                                  \
      "(g) no generalized parameter, "                                  \
      "(l) recognize Street-like and Rabin-like, "                      \
      "(m) no main parameter, "                                         \
      "(p) no parity parameter, "                                       \
      "(o) name unknown acceptance as 'other', "                        \
      "(s) shorthand for 'lo0'."


177
178
179
static const argp_option io_options[] =
  {
    /**************************************************/
180
    { nullptr, 0, nullptr, 0, "Any FORMAT string may use "\
181
182
      "the following interpreted sequences (capitals for input,"
      " minuscules for output):", 4 },
183
184
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
185
186
187
    { "%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 },
188
    { "%M, %m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
189
      "name of the automaton", 0 },
190
    { "%S, %s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
191
      "number of reachable states", 0 },
192
    { "%E, %e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
193
      "number of reachable edges", 0 },
194
    { "%T, %t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
195
      "number of reachable transitions", 0 },
196
    { "%A, %a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
197
      "number of acceptance sets", 0 },
198
199
    { "%G, %g, %[LETTERS]G, %[LETTERS]g", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE, doc_g, 0 },
200
201
202
203
    { "%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, "
204
      "(r) rejecting, (c) complete, (v) trivial, (t) terminal, (w) weak, "
205
      "(iw) inherently weak. Use uppercase letters to negate them.", 0 },
206
207
208
    { "%R, %[LETTERS]R", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      "CPU time (excluding parsing), in seconds; Add LETTERS to restrict to"
209
210
      "(u) user time, (s) system time, (p) parent process, "
      "or (c) children processes.", 0 },
211
212
213
214
215
216
    { "%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 },
217
    { "%r", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
218
      "wall-clock time elapsed in seconds (excluding parsing)", 0 },
219
220
    { "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "one word accepted by the automaton", 0 },
221
222
223
    { "%X, %x, %[LETTERS]X, %[LETTERS]x", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 },
224
225
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
226
227
228
229
230
231
    { "%<", 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 },
232
    { nullptr, 0, nullptr, 0, nullptr, 0 }
233
234
  };

235
const struct argp aoutput_io_format_argp = { io_options, nullptr, nullptr,
236
237
                                             nullptr, nullptr,
                                             nullptr, nullptr };
238
239
240
241

static const argp_option o_options[] =
  {
    /**************************************************/
242
    { nullptr, 0, nullptr, 0, "Any FORMAT string may use "\
243
      "the following interpreted sequences:", 4 },
244
245
    { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
    { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
246
247
248
    { "%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 },
249
250
251
    { "%m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "name of the automaton", 0 },
    { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
252
      "number of reachable states", 0 },
253
    { "%e", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
254
      "number of reachable edges", 0 },
255
    { "%t", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
256
      "number of reachable transitions", 0 },
257
    { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
258
      "number of acceptance sets", 0 },
259
260
    { "%g, %[LETTERS]g", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE, doc_g, 0 },
261
262
263
    { "%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, "
264
      "(r) rejecting, (c) complete, (v) trivial, (t) terminal, (w) weak, "
265
      "(iw) inherently weak. Use uppercase letters to negate them.", 0 },
266
267
268
    { "%R, %[LETTERS]R", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      "CPU time (excluding parsing), in seconds; Add LETTERS to restrict to"
269
270
      "(u) user time, (s) system time, (p) parent process, "
      "or (c) children processes.", 0 },
271
    { "%n", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
272
      "number of nondeterministic states in output", 0 },
273
    { "%d", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
274
      "1 if the output is deterministic, 0 otherwise", 0 },
275
    { "%p", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
276
      "1 if the output is complete, 0 otherwise", 0 },
277
    { "%r", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
278
      "wall-clock time elapsed in seconds (excluding parsing)", 0 },
279
    { "%w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
280
      "one word accepted by the output automaton", 0 },
281
282
283
    { "%x, %[LETTERS]x", 0, nullptr,
      OPTION_DOC | OPTION_NO_USAGE,
      COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 },
284
285
286
    { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
287
288
  };

289
const struct argp aoutput_o_format_argp = { o_options,
290
291
                                            nullptr, nullptr, nullptr,
                                            nullptr, nullptr, nullptr };
292
293
294
295
296
297
298
299
300

int parse_opt_aoutput(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case '8':
      spot::enable_utf8();
      break;
301
302
    case 'd':
      automaton_format = Dot;
303
      automaton_format_opt = arg;
304
      break;
305
306
    case 'H':
      automaton_format = Hoa;
307
      automaton_format_opt = arg;
308
      break;
309
310
311
    case 'o':
      opt_output = arg;
      break;
312
313
314
315
316
317
    case 'q':
      automaton_format = Quiet;
      break;
    case 's':
      automaton_format = Spin;
      if (type != spot::postprocessor::Monitor)
318
        type = spot::postprocessor::BA;
319
      automaton_format_opt = arg;
320
      break;
321
322
323
    case OPT_CHECK:
      automaton_format = Hoa;
      if (arg)
324
        opt_check |= XARGMATCH("--check", arg, check_args, check_types);
325
      else
326
        opt_check |= check_all;
327
      break;
328
    case OPT_LBTT:
329
      automaton_format = Lbtt;
330
      automaton_format_opt = arg;
331
332
333
334
      // 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))
335
        error(2, 0, "unknown argument for --lbtt: '%s'", arg);
336
337
      break;
    case OPT_NAME:
338
      opt_name = arg;
339
340
341
      break;
    case OPT_STATS:
      if (!*arg)
342
        error(2, 0, "empty format string for --stats");
343
344
345
346
347
348
349
350
351
      stats = arg;
      automaton_format = Stats;
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

352
353
354
355
356
void setup_default_output_format()
{
  if (auto val = getenv("SPOT_DEFAULT_FORMAT"))
    {
      static char const *const args[] =
357
358
359
        {
          "dot", "hoa", "hoaf", nullptr
        };
360
      static automaton_format_t const format[] =
361
362
363
        {
          Dot, Hoa, Hoa
        };
364
365
      auto eq = strchr(val, '=');
      if (eq)
366
367
368
369
        {
          val = strndup(val, eq - val);
          automaton_format_opt = eq + 1;
        }
370
371
372
      ARGMATCH_VERIFY(args, format);
      automaton_format = XARGMATCH("SPOT_DEFAULT_FORMAT", val, args, format);
      if (eq)
373
        free(val);
374
375
    }
}
376

377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
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_);
395
      declare('X', &haut_ap_);
396
397
398
399
400
    }
  declare('<', &csv_prefix_);
  declare('>', &csv_suffix_);
  declare('F', &filename_);
  declare('L', &location_);
401
  declare('R', &timer_);
402
  declare('r', &timer_);
403
404
405
406
407
  if (input != ltl_input)
    declare('f', &filename_);        // Override the formula printer.
  declare('h', &output_aut_);
  declare('m', &aut_name_);
  declare('w', &aut_word_);
408
  declare('x', &aut_ap_);
409
410
411
412
413
414
}

std::ostream&
hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut,
                        const spot::const_twa_graph_ptr& aut,
                        spot::formula f,
415
416
                        const char* filename, int loc,
                        spot::process_timer& ptimer,
417
418
                        const char* csv_prefix, const char* csv_suffix)
{
419
  timer_ = ptimer;
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
446
447
  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;
        }
448
      else if (has('E') || has('S'))
449
        {
450
          spot::twa_statistics s = stats_reachable(haut->aut);
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
          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('A'))
        haut_acc_ = haut->aut->acc().num_sets();

      if (has('C'))
467
        haut_scc_.automaton(haut->aut);
468
469
470
471
472
473
474
475
476
477
478
479

      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);
        }

480
      if (has('P'))
481
482
        haut_complete_ = is_complete(haut->aut);
      if (has('G'))
483
484
        haut_gen_acc_ = haut->aut->acc();

485
486
487
488
489
490
491
492
493
494
495
496
497
      if (has('W'))
        {
          if (auto word = haut->aut->accepting_word())
            {
              std::ostringstream out;
              out << *word;
              haut_word_ = out.str();
            }
          else
            {
              haut_word_.val().clear();
            }
        }
498
      if (has('X'))
499
        haut_ap_ = haut->aut->ap();
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
    }

  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();
        }
    }
523
  if (has('x'))
524
    aut_ap_ = aut->ap();
525

526
  auto& res = this->spot::stat_printer::print(aut, f);
527
528
529
530
531
  // 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;
532
  haut_scc_.reset();
533
534
  aut_ap_.clear();
  haut_ap_.clear();
535
536
537
  return res;
}

538
539
automaton_printer::automaton_printer(stat_style input)
  : statistics(std::cout, stats, input),
540
541
    namer(name, opt_name, input),
    outputnamer(outputname, opt_output, input)
542
{
543
544
545
  if (automaton_format == Count && opt_output)
    throw std::runtime_error
      ("options --output and --count are incompatible");
546
}
547
548

void
549
automaton_printer::print(const spot::twa_graph_ptr& aut,
550
                         // Time for statistics
551
                         spot::process_timer& ptimer,
552
553
554
555
                         spot::formula f,
                         // Input location for errors and statistics.
                         const char* filename,
                         int loc,
556
                         // input automaton for statistics
557
558
559
                         const spot::const_parsed_aut_ptr& haut,
                         const char* csv_prefix,
                         const char* csv_suffix)
560
{
561
562
563
  if (opt_check)
    {
      if (opt_check & check_stutter)
564
        spot::check_stutter_invariance(aut, f);
565
      if (opt_check & check_unambiguous)
566
        spot::check_unambiguous(aut);
567
      if (opt_check & check_strength)
568
        spot::check_strength(aut);
569
570
      if (opt_check & check_semi_determinism)
        spot::is_semi_deterministic(aut); // sets the property as a side effect.
571
572
    }

573
574
575
576
  // Name the output automaton.
  if (opt_name)
    {
      name.str("");
577
      namer.print(haut, aut, f, filename, loc, ptimer, csv_prefix, csv_suffix);
578
579
580
      aut->set_named_prop("automaton-name", new std::string(name.str()));
    }

581
582
583
584
  std::ostream* out = &std::cout;
  if (opt_output)
    {
      outputname.str("");
585
      outputnamer.print(haut, aut, f, filename, loc, ptimer,
586
                        csv_prefix, csv_suffix);
587
588
589
      std::string fname = outputname.str();
      auto p = outputfiles.emplace(fname, nullptr);
      if (p.second)
590
        p.first->second.reset(new output_file(fname.c_str()));
591
592
593
      out = &p.first->second->ostream();
    }

594
595
596
597
598
599
600
601
  // Output it.
  switch (automaton_format)
    {
    case Count:
    case Quiet:
      // Do not output anything.
      break;
    case Dot:
602
      spot::print_dot(*out, aut, automaton_format_opt);
603
604
      break;
    case Lbtt:
605
      spot::print_lbtt(*out, aut, automaton_format_opt);
606
607
      break;
    case Hoa:
608
      spot::print_hoa(*out, aut, automaton_format_opt) << '\n';
609
610
      break;
    case Spin:
611
      spot::print_never_claim(*out, aut, automaton_format_opt);
612
613
      break;
    case Stats:
614
      statistics.set_output(*out);
615
      statistics.print(haut, aut, f, filename, loc, ptimer,
616
                       csv_prefix, csv_suffix) << '\n';
617
618
619
620
      break;
    }
  flush_cout();
}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
621
622
623
624
625

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

629
630
631
632
633
634
635
automaton_printer::~automaton_printer()
{
  for (auto& p : outputfiles)
    p.second->close(p.first);
}


636
637
638
639
640
641
642
643
644
645
646
647
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';
    }
  print_hoa(os, val_, options.c_str());
}
648

649
650
651
652
653
654
655
656
657
658
659
660
661

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());
  }
}

662
663
664
665
void printable_timer::print(std::ostream& os, const char* pos) const
{
  double res = 0;

666
667
668
669
670
671
672
673
674
675
#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

676
  if (*pos != '[')
677
678
679
680
681
682
683
684
685
686
687
688
689
    {
      if (*pos == 'r')
        {
          res = val_.walltime();
          os << res;
        }
      else
        {
          res = val_.cputime(true, true, true, true);
          os << res / clocks_per_sec;
        }
      return;
    }
690
691
692
693
694
695
696
697

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

  const char* beg = pos;
  do
698
699
    switch (*++pos)
      {
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
      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:
719
720
721
        percent_error(beg, pos);
      }
  while (*pos != ']');
722

723
724
725
  if (*(pos + 1) == 'r')
    percent_error(beg, pos-1);

726
  if (!parent && !children)
727
    parent = children = true;
728
  if (!user && !system)
729
730
    user = system = true;

731
  res = val_.cputime(user, system, children, parent);
732
  os << res / clocks_per_sec;
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
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798

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 << ')';
    }
}