autfilt.cc 20.3 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// 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/>.

#include "common_sys.hh"

#include <string>
#include <iostream>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
24
#include <limits>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
25
26
27
28
29
30
31

#include <argp.h>
#include "error.h"

#include "common_setup.hh"
#include "common_finput.hh"
#include "common_cout.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
32
#include "common_range.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
33
34
35
36
#include "common_post.hh"

#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
37
#include "tgbaalgos/hoa.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
38
#include "tgbaalgos/neverclaim.hh"
39
#include "tgbaalgos/product.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
40
41
#include "tgbaalgos/save.hh"
#include "tgbaalgos/stats.hh"
42
#include "tgbaalgos/isdet.hh"
43
44
#include "tgbaalgos/stutterize.hh"
#include "tgbaalgos/closure.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
45
46
47
#include "tgba/bddprint.hh"
#include "misc/optionmap.hh"
#include "misc/timer.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
48
#include "misc/random.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
49
50
#include "hoaparse/public.hh"
#include "tgbaalgos/sccinfo.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
51
#include "tgbaalgos/randomize.hh"
52
53
54
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
55
#include "tgbaalgos/are_isomorphic.hh"
56
#include "tgbaalgos/canonicalize.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
57
58


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
59
static const char argp_program_doc[] ="\
60
Convert, transform, and filter Büchi automata.\v\
61
62
63
64
Exit status:\n\
  0  if some automata were output\n\
  1  if no automata were output (no match)\n\
  2  if any error has been reported";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
65
66
67
68
69
70
71


#define OPT_TGBA 1
#define OPT_DOT 2
#define OPT_LBTT 3
#define OPT_SPOT 4
#define OPT_STATS 5
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
72
73
#define OPT_RANDOMIZE 6
#define OPT_SEED 7
74
#define OPT_PRODUCT 8
75
#define OPT_MERGE 9
76
#define OPT_ARE_ISOMORPHIC 10
77
78
#define OPT_IS_COMPLETE 11
#define OPT_IS_DETERMINISTIC 12
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
79
80
#define OPT_STATES 17
#define OPT_COUNT 18
81
#define OPT_NAME 19
82
83
#define OPT_EDGES 20
#define OPT_ACC_SETS 21
84
85
86
#define OPT_DESTUT 22
#define OPT_INSTUT 23
#define OPT_IS_EMPTY 24
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
87
88
89
90
91
92
93
94
95
96
97
98
99

static const argp_option options[] =
  {
    /**************************************************/
    { 0, 0, 0, 0, "Input:", 1 },
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "Output automaton type:", 2 },
    { "tgba", OPT_TGBA, 0, 0,
      "Transition-based Generalized Büchi Automaton (default)", 0 },
    { "ba", 'B', 0, 0, "Büchi Automaton", 0 },
    { "monitor", 'M', 0, 0, "Monitor (accepts all finite prefixes "
100
      "of the given property)", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
101
102
    /**************************************************/
    { 0, 0, 0, 0, "Output format:", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
103
    { "count", 'c', 0, 0, "print only a count of matched automata", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
104
105
106
107
108
109
110
111
    { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
    { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL,
      "Output the automaton in HOA format.  Add letters to select "
      "(s) state-based acceptance, (t) transition-based acceptance, "
      "(m) mixed acceptance, (l) single-line output", 0 },
    { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
      "LBTT's format (add =t to force transition-based acceptance even"
      " on Büchi automata)", 0 },
112
113
    { "max-count", 'n', "NUM", 0,
      "output at most NUM automata", 0 },
114
115
    { "name", OPT_NAME, "FORMAT", OPTION_ARG_OPTIONAL,
      "set the name of the output automaton (default: %M)", 0 },
116
    { "quiet", 'q', 0, 0, "suppress all normal output", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
117
118
119
120
121
122
123
124
125
126
127
128
    { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
    { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
    { "utf8", '8', 0, 0, "enable UTF-8 characters in output "
      "(ignored with --lbtt or --spin)", 0 },
    { "stats", OPT_STATS, "FORMAT", 0,
      "output statistics about the automaton", 0 },
    /**************************************************/
    { 0, 0, 0, 0, "The FORMAT string passed to --stats may use "\
      "the following interpreted sequences (capitals for input,"
      " minuscules for output):", 4 },
    { "%F", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "name of the input file", 0 },
129
130
    { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "location in the input file", 0 },
131
132
    { "%M, %m", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "name of the automaton (as specified in the HOA format)", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
    { "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of states", 0 },
    { "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of edges", 0 },
    { "%T, %t", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of transitions", 0 },
    { "%A, %a", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of acceptance pairs or sets", 0 },
    { "%C, %c", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of SCCs", 0 },
    { "%n", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "number of nondeterministic states in output", 0 },
    { "%d", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the output is deterministic, 0 otherwise", 0 },
    { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "1 if the output is complete, 0 otherwise", 0 },
    { "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
150
      "processing time (excluding parsing) in seconds", 0 },
151
152
    { "%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "one word accepted by the output automaton", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
153
154
155
    { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
    /**************************************************/
156
157
158
    { 0, 0, 0, 0, "Transformations:", 5 },
    { "merge-transitions", OPT_MERGE, 0, 0,
      "merge transitions with same destination and acceptance", 0 },
159
160
    { "product", OPT_PRODUCT, "FILENAME", 0,
      "build the product with FILENAME", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
161
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
162
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
163
      "randomize only states or transitions)", 0 },
164
165
    { "instut", OPT_INSTUT, 0, 0, "allow more stuttering", 0 },
    { "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
166
    /**************************************************/
167
168
    { 0, 0, 0, 0, "Filters:", 6 },
    { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
169
      "keep automata that are isomorphic to the automaton in FILENAME", 0 },
170
    { "isomorphic", 0, 0, OPTION_ALIAS | OPTION_HIDDEN, 0, 0 },
171
172
173
174
    { "is-complete", OPT_IS_COMPLETE, 0, 0,
      "the automaton is complete", 0 },
    { "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0,
      "the automaton is deterministic", 0 },
175
176
    { "is-empty", OPT_IS_EMPTY, 0, 0,
      "keep automata with an empty language", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
177
178
179
    { "invert-match", 'v', 0, 0, "select non-matching automata", 0 },
    { "states", OPT_STATES, "RANGE", 0,
      "keep automata whose number of states are in RANGE", 0 },
180
181
182
183
    { "edges", OPT_EDGES, "RANGE", 0,
      "keep automata whose number of edges are in RANGE", 0 },
    { "acc-sets", OPT_ACC_SETS, "RANGE", 0,
      "keep automata whose number of acceptance sets are in RANGE", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
184
    RANGE_DOC_FULL,
185
    /**************************************************/
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
186
187
188
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
189
190
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
191
192
193
    { 0, 0, 0, 0, 0, 0 }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
194
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
195
196
197
198
199
200
  {
    { &post_argp_disabled, 0, 0, 20 },
    { &misc_argp, 0, 0, -1 },
    { 0, 0, 0, 0 }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
201
202
203
static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa,
			    Quiet, Count } format = Dot;
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
204
205
206
207
208
209
static const char* stats = "";
static const char* hoa_opt = 0;
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
210
211
static auto dict = spot::make_bdd_dict();
static spot::tgba_digraph_ptr opt_product = nullptr;
212
static bool opt_merge = false;
213
static spot::tgba_digraph_ptr opt_are_isomorphic = nullptr;
214
215
216
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
217
static range opt_states = { 0, std::numeric_limits<int>::max() };
218
219
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
220
static const char* opt_name = nullptr;
221
static int opt_max_count = -1;
222
223
224
static bool opt_destut = false;
static bool opt_instut = false;
static bool opt_is_empty = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
225
226
227
228
229
230
231
232
233
234

static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
    error(2, 0, "failed to parse '%s' as an integer.", s);
  return res;
}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
235

236
237
238
239
240
241
242
243
244
static int
to_pos_int(const char* s)
{
  int res = to_int(s);
  if (res < 0)
    error(2, 0, "%d is not positive", res);
  return res;
}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
245
246
247
248
249
250
251
252
253
254
255
256
static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case '8':
      spot::enable_utf8();
      break;
    case 'B':
      type = spot::postprocessor::BA;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
257
258
259
    case 'c':
      format = Count;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
260
261
262
263
264
    case 'F':
      jobs.emplace_back(arg, true);
      break;
    case 'H':
      format = Hoa;
265
      hoa_opt = arg;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
266
267
268
269
      break;
    case 'M':
      type = spot::postprocessor::Monitor;
      break;
270
271
272
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
273
274
275
    case 'q':
      format = Quiet;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
276
277
278
279
280
    case 's':
      format = Spin;
      if (type != spot::postprocessor::Monitor)
	type = spot::postprocessor::BA;
      break;
281
282
283
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
284
285
286
287
288
289
290
291
292
293
    case 'x':
      {
	const char* opt = extra_options.parse_options(arg);
	if (opt)
	  error(2, 0, "failed to parse --options near '%s'", opt);
      }
      break;
    case OPT_DOT:
      format = Dot;
      break;
294
295
296
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
297
298
299
300
301
302
303
304
305
306
    case OPT_ARE_ISOMORPHIC:
      {
	spot::hoa_parse_error_list pel;
	auto p = hoa_parse(arg, pel, dict);
	if (spot::format_hoa_parse_errors(std::cerr, arg, pel)
	    || !p || p->aborted)
	  error(2, 0, "failed to read automaton from %s", arg);
        opt_are_isomorphic = std::move(p->aut);
	break;
      }
307
308
309
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
310
311
312
313
314
315
    case OPT_INSTUT:
      opt_instut = true;
      break;
    case OPT_DESTUT:
      opt_destut = true;
      break;
316
317
318
319
320
321
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
322
323
324
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
325
326
327
328
329
330
331
332
333
334
335
336
337
    case OPT_LBTT:
      if (arg)
	{
	  if (arg[0] == 't' && arg[1] == 0)
	    format = Lbtt_t;
	  else
	    error(2, 0, "unknown argument for --lbtt: '%s'", arg);
	}
      else
	{
	  format = Lbtt;
	}
      break;
338
339
340
341
342
    case OPT_NAME:
      if (arg)
	opt_name = arg;
      else
	opt_name = "%M";
343
344
345
    case OPT_MERGE:
      opt_merge = true;
      break;
346
347
348
349
350
351
352
353
354
355
356
357
358
359
    case OPT_PRODUCT:
      {
	spot::hoa_parse_error_list pel;
	auto p = hoa_parse(arg, pel, dict);
	if (spot::format_hoa_parse_errors(std::cerr, arg, pel)
	    || !p || p->aborted)
	  error(2, 0, "failed to read automaton from %s", arg);
	if (!opt_product)
	  opt_product = std::move(p->aut);
	else
	  opt_product = spot::product(std::move(opt_product),
				      std::move(p->aut));
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
    case OPT_RANDOMIZE:
      if (arg)
	{
	  for (auto p = arg; *p; ++p)
	    switch (*p)
	      {
	      case 's':
		randomize_st = true;
		break;
	      case 't':
		randomize_tr = true;
		break;
	      default:
		error(2, 0, "unknown argument for --randomize: '%c'", *p);
	      }
	}
      else
	{
	  randomize_tr = true;
	  randomize_st = true;
	}
      break;
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
385
386
387
    case OPT_SPOT:
      format = Spot;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
388
389
390
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
391
392
393
394
395
396
397
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
    case OPT_STATS:
      if (!*arg)
	error(2, 0, "empty format string for --stats");
      stats = arg;
      format = Stats;
      break;
    case OPT_TGBA:
      if (format == Spin)
	error(2, 0, "--spin and --tgba are incompatible");
      type = spot::postprocessor::TGBA;
      break;
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}


namespace
{
  /// \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:
    hoa_stat_printer(std::ostream& os, const char* format)
      : spot::stat_printer(os, format)
    {
      declare('A', &haut_acc_);
      declare('C', &haut_scc_);
      declare('E', &haut_edges_);
      declare('F', &filename_);
      declare('f', &filename_);	// Override the formula printer.
431
      declare('L', &haut_loc_);
432
433
      declare('M', &haut_name_);
      declare('m', &aut_name_);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
434
435
      declare('S', &haut_states_);
      declare('T', &haut_trans_);
436
      declare('w', &aut_word_);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
437
438
439
440
441
442
443
444
445
446
447
448
    }

    /// \brief print the configured statistics.
    ///
    /// The \a f argument is not needed if the Formula does not need
    /// to be output.
    std::ostream&
    print(const spot::const_hoa_aut_ptr& haut,
	  const spot::const_tgba_digraph_ptr& aut,
	  const char* filename, double run_time)
    {
      filename_ = filename;
449
      haut_loc_ = haut->loc;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
450
451
452
453
454
455
456
457
458
459
460
461
462
463

      if (has('T'))
	{
	  spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut);
	  haut_states_ = s.states;
	  haut_edges_ = s.transitions;
	  haut_trans_ = s.sub_transitions;
	}
      else if (has('E'))
	{
	  spot::tgba_sub_statistics s = sub_stats_reachable(haut->aut);
	  haut_states_ = s.states;
	  haut_edges_ = s.transitions;
	}
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
      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('m'))
	{
	  auto n = aut->get_named_prop<std::string>("automaton-name");
	  if (n)
	    aut_name_ = *n;
	  else
	    aut_name_.val().clear();
	}
      if (has('S'))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
481
482
483
484
485
486
487
488
489
490
	{
	  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();

491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
      if (has('w'))
	{
	  auto res = spot::couvreur99(aut)->check();
	  if (res)
	    {
	      auto run = res->accepting_run();
	      assert(run);
	      run = reduce_run(aut, run);
	      spot::tgba_word w(run);
	      w.simplify();
	      std::ostringstream out;
	      w.print(out, aut->get_dict());
	      aut_word_ = out.str();
	    }
	  else
	    {
	      aut_word_.val().clear();
	    }
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
511
512
513
514
515
      return this->spot::stat_printer::print(aut, 0, run_time);
    }

  private:
    spot::printable_value<const char*> filename_;
516
517
    spot::printable_value<std::string> haut_name_;
    spot::printable_value<std::string> aut_name_;
518
    spot::printable_value<std::string> aut_word_;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
519
520
521
522
523
    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_;
524
    spot::printable_value<spot::location> haut_loc_;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
525
526
527
528
  };

  class hoa_processor: public job_processor
  {
529
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
530
531
    spot::postprocessor& post;
    hoa_stat_printer statistics;
532
533
534
    std::ostringstream name;
    hoa_stat_printer namer;
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
535
536

    hoa_processor(spot::postprocessor& post)
537
      : post(post), statistics(std::cout, stats), namer(name, opt_name)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
538
539
540
541
542
543
544
545
546
547
    {
    }

    int
    process_formula(const spot::ltl::formula*, const char*, int)
    {
      SPOT_UNREACHABLE();
    }

    int
548
549
    process_automaton(const spot::const_hoa_aut_ptr& haut,
		      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
550
551
552
    {
      spot::stopwatch sw;
      sw.start();
553

554
555
556
557
558
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
      // merge_transitions()) and the statistics about it make sense.
      auto aut = ((format == Stats) || opt_name) ?
	spot::make_tgba_digraph(haut->aut) : haut->aut;
559

560
561
      // Preprocessing.

562
      if (opt_merge)
563
	aut->merge_transitions();
564

565
566
567
568
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
569
      matched &= opt_states.contains(aut->num_states());
570
571
      matched &= opt_edges.contains(aut->num_transitions());
      matched &= opt_accsets.contains(aut->acc().num_sets());
572
573
574
575
      if (opt_is_complete)
	matched &= is_complete(aut);
      if (opt_is_deterministic)
	matched &= is_deterministic(aut);
576
      if (opt_are_isomorphic)
577
578
579
580
        {
          spot::tgba_digraph_ptr tmp = make_tgba_digraph(aut);
          matched &= (*spot::canonicalize(tmp) == *opt_are_isomorphic);
        }
581
582
      if (opt_is_empty)
	matched &= aut->is_empty();
583

584
585
      // Drop or keep matched automata depending on the --invert option
      if (matched == opt_invert)
586
587
        return 0;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
588
      ++match_count;
589

590
591
      // Postprocessing.

592
593
594
595
596
      if (opt_destut)
	aut = spot::closure(std::move(aut));
      if (opt_instut)
	aut = spot::sl(aut);

597
598
599
      if (opt_product)
	aut = spot::product(std::move(aut), opt_product);

600
      aut = post.run(aut, nullptr);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
601

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
602
603
604
      if (randomize_st || randomize_tr)
	spot::randomize(aut, randomize_st, randomize_tr);

605
606
      const double conversion_time = sw.stop();

607
608
609
610
611
612
613
614
615
      // Name the output automaton.
      if (opt_name)
	{
	  name.str("");
	  namer.print(haut, aut, filename, conversion_time);
	  aut->set_named_prop("automaton-name", new std::string(name.str()));
	}

      // Output it.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
616
617
      switch (format)
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
618
619
620
621
	case Count:
	case Quiet:
	  // Do not output anything.
	  break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
622
623
624
625
626
627
628
629
630
631
632
633
	case Dot:
	  spot::dotty_reachable(std::cout, aut,
				(type == spot::postprocessor::BA)
				|| (type == spot::postprocessor::Monitor));
	  break;
	case Lbtt:
	  spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA);
	  break;
	case Lbtt_t:
	  spot::lbtt_reachable(std::cout, aut, false);
	  break;
	case Hoa:
634
	  spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
635
636
637
638
639
640
641
642
643
644
645
646
	  break;
	case Spot:
	  spot::tgba_save_reachable(std::cout, aut);
	  break;
	case Spin:
	  spot::never_claim_reachable(std::cout, aut);
	  break;
	case Stats:
	  statistics.print(haut, aut, filename, conversion_time) << '\n';
	  break;
	}
      flush_cout();
647
648
649
650

      if (opt_max_count >= 0 && match_count >= opt_max_count)
	abort_run = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
651
652
      return 0;
    }
653

654
655
656
657
658
659
    int
    aborted(const spot::const_hoa_aut_ptr& h, const char* filename)
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }
660
661
662
663
664
665
666
667
668

    int
    process_file(const char* filename)
    {
      spot::hoa_parse_error_list pel;
      auto hp = spot::hoa_stream_parser(filename);

      int err = 0;

669
      while (!abort_run)
670
	{
671
	  pel.clear();
672
	  auto haut = hp.parse(pel, dict);
673
674
675
676
677
	  if (!haut && pel.empty())
	    break;
	  if (spot::format_hoa_parse_errors(std::cerr, filename, pel))
	    err = 2;
	  if (!haut)
678
	    error(2, 0, "failed to read automaton from %s", filename);
679
680
	  else if (haut->aborted)
	    err = std::max(err, aborted(haut, filename));
681
	  else
682
            process_automaton(haut, filename);
683
684
685
686
	}

      return err;
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
  };
}

int
main(int argc, char** argv)
{
  setup(argv);

  const argp ap = { options, parse_opt, "[FILENAMES...]",
		    argp_program_doc, children, 0, 0 };

  // Disable post-processing as much as possible by default.
  level = spot::postprocessor::Low;
  pref = spot::postprocessor::Any;
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
    exit(err);

  if (jobs.empty())
    jobs.emplace_back("-", true);

707
708
709
710
711
712
713
  if (opt_are_isomorphic)
    {
      if (opt_merge)
        opt_are_isomorphic->merge_transitions();
      spot::canonicalize(opt_are_isomorphic);
    }

714

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
715
716
  spot::srand(opt_seed);

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
717
718
719
720
721
722
  spot::postprocessor post(&extra_options);
  post.set_pref(pref | comp);
  post.set_type(type);
  post.set_level(level);

  hoa_processor processor(post);
723
724
725
726
727
728
729
730
731
  try
    {
      if (processor.run())
	return 2;
    }
  catch (const std::runtime_error& e)
    {
      error(2, 0, "%s", e.what());
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
732
733
734
735

  if (format == Count)
    std::cout << match_count << std::endl;
  return !match_count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
736
}