autfilt.cc 46.3 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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>
25
26
#include <set>
#include <memory>
27
28
#include <sys/stat.h>
#include <unistd.h>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
29
30
31

#include <argp.h>
#include "error.h"
32
#include "argmatch.h"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
33
34
35
36

#include "common_setup.hh"
#include "common_finput.hh"
#include "common_cout.hh"
37
#include "common_aoutput.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
38
#include "common_range.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39
#include "common_post.hh"
40
#include "common_conv.hh"
41
#include "common_hoaread.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
42

43
#include <spot/twaalgos/product.hh>
44
#include <spot/twaalgos/sum.hh>
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/isunamb.hh>
#include <spot/misc/optionmap.hh>
#include <spot/misc/timer.hh>
#include <spot/misc/random.hh>
#include <spot/parseaut/public.hh>
#include <spot/tl/exclusive.hh>
#include <spot/twaalgos/remprop.hh>
#include <spot/twaalgos/randomize.hh>
#include <spot/twaalgos/are_isomorphic.hh>
#include <spot/twaalgos/canonicalize.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/twaalgos/sepsets.hh>
#include <spot/twaalgos/stripacc.hh>
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/cleanacc.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/strength.hh>
65
#include <spot/twaalgos/hoa.hh>
66
67
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
68
#include <spot/twaalgos/gtec/gtec.hh>
69
#include <spot/twaalgos/totgba.hh>
70
#include <spot/twaalgos/langmap.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
71

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
72
static const char argp_program_doc[] ="\
73
Convert, transform, and filter omega-automata.\v\
74
75
76
77
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
78

79
80
// Keep this list sorted
enum {
81
82
  OPT_ACC_SCCS = 256,
  OPT_ACC_SETS,
83
  OPT_ACCEPT_WORD,
84
  OPT_AP_N,
85
86
  OPT_ARE_ISOMORPHIC,
  OPT_CLEAN_ACC,
87
  OPT_CNF_ACC,
88
  OPT_COMPLEMENT,
89
90
  OPT_COMPLEMENT_ACC,
  OPT_COUNT,
91
  OPT_DECOMPOSE_STRENGTH,
92
  OPT_DECOMPOSE_SCC,
93
94
95
  OPT_DESTUT,
  OPT_DNF_ACC,
  OPT_EDGES,
96
  OPT_EQUIVALENT_TO,
97
  OPT_EXCLUSIVE_AP,
98
99
  OPT_GENERALIZED_RABIN,
  OPT_GENERALIZED_STREETT,
100
101
102
  OPT_HIGHLIGHT_NONDET,
  OPT_HIGHLIGHT_NONDET_EDGES,
  OPT_HIGHLIGHT_NONDET_STATES,
103
  OPT_HIGHLIGHT_WORD,
104
  OPT_HIGHLIGHT_LANGUAGES,
105
  OPT_INSTUT,
106
  OPT_INCLUDED_IN,
107
  OPT_INHERENTLY_WEAK_SCCS,
108
  OPT_INTERSECT,
109
  OPT_IS_ALTERNATING,
110
111
112
  OPT_IS_COMPLETE,
  OPT_IS_DETERMINISTIC,
  OPT_IS_EMPTY,
113
  OPT_IS_INHERENTLY_WEAK,
114
  OPT_IS_SEMI_DETERMINISTIC,
115
  OPT_IS_STUTTER_INVARIANT,
116
  OPT_IS_TERMINAL,
117
  OPT_IS_UNAMBIGUOUS,
118
  OPT_IS_VERY_WEAK,
119
  OPT_IS_WEAK,
120
121
122
  OPT_KEEP_STATES,
  OPT_MASK_ACC,
  OPT_MERGE,
123
  OPT_NONDET_STATES,
124
125
  OPT_PRODUCT_AND,
  OPT_PRODUCT_OR,
126
  OPT_RANDOMIZE,
127
  OPT_REJ_SCCS,
128
  OPT_REJECT_WORD,
129
  OPT_REM_AP,
130
131
  OPT_REM_DEAD,
  OPT_REM_UNREACH,
132
  OPT_REM_UNUSED_AP,
133
  OPT_REM_FIN,
134
  OPT_SAT_MINIMIZE,
135
  OPT_SCCS,
136
  OPT_SEED,
137
  OPT_SEP_SETS,
138
  OPT_SIMPLIFY_EXCLUSIVE_AP,
139
140
  OPT_STATES,
  OPT_STRIPACC,
141
142
  OPT_SUM_OR,
  OPT_SUM_AND,
143
144
  OPT_TERMINAL_SCCS,
  OPT_TRIV_SCCS,
145
146
  OPT_USED_AP_N,
  OPT_UNUSED_AP_N,
147
  OPT_WEAK_SCCS,
148
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
149

150
151
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
152
153
154
static const argp_option options[] =
  {
    /**************************************************/
155
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
156
157
158
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
159
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
160
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
161
    /**************************************************/
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
    { nullptr, 0, nullptr, 0, "Filtering options:", 5 },
    { "ap", OPT_AP_N, "RANGE", 0,
      "match automata with a number of (declared) atomic propositions in RANGE",
      0 },
    { "used-ap", OPT_USED_AP_N, "RANGE", 0,
      "match automata with a number of used atomic propositions in RANGE", 0 },
    { "unused-ap", OPT_UNUSED_AP_N, "RANGE", 0,
      "match automata with a number of declared, but unused atomic "
      "propositions in RANGE", 0 },
    { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
      "keep automata that are isomorphic to the automaton in FILENAME", 0 },
    { "isomorphic", 0, nullptr, OPTION_ALIAS | OPTION_HIDDEN, nullptr, 0 },
    { "unique", 'u', nullptr, 0,
      "do not output the same automaton twice (same in the sense that they "\
      "are isomorphic)", 0 },
    { "is-complete", OPT_IS_COMPLETE, nullptr, 0,
      "keep complete automata", 0 },
    { "is-deterministic", OPT_IS_DETERMINISTIC, nullptr, 0,
      "keep deterministic automata", 0 },
181
182
    { "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0,
      "keep semi-deterministic automata", 0 },
183
184
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
      "keep automata with an empty language", 0 },
185
186
    { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
      "keep automata representing stutter-invariant properties", 0 },
187
188
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
189
190
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
      "keep only unambiguous automata", 0 },
191
192
193
194
    { "is-weak", OPT_IS_WEAK, nullptr, 0,
      "keep only weak automata", 0 },
    { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
      "keep only inherently weak automata", 0 },
195
196
    { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
      "keep only very-weak automata", 0 },
197
198
    { "is-alternating", OPT_IS_ALTERNATING, nullptr, 0,
      "keep only automata using universal branching", 0 },
199
200
201
202
203
204
205
206
207
208
209
210
211
212
    { "intersect", OPT_INTERSECT, "FILENAME", 0,
      "keep automata whose languages have an non-empty intersection with"
      " the automaton from FILENAME", 0 },
    { "included-in", OPT_INCLUDED_IN, "FILENAME", 0,
      "keep automata whose languages are included in that of the "
      "automaton from FILENAME", 0 },
    { "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0,
      "keep automata thare are equivalent (language-wise) to the automaton "
      "in FILENAME", 0 },
    { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 },
    { "states", OPT_STATES, "RANGE", 0,
      "keep automata whose number of states is in RANGE", 0 },
    { "edges", OPT_EDGES, "RANGE", 0,
      "keep automata whose number of edges is in RANGE", 0 },
213
214
    { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
      "keep automata whose number of nondeterministic states is in RANGE", 0 },
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
    { "acc-sets", OPT_ACC_SETS, "RANGE", 0,
      "keep automata whose number of acceptance sets is in RANGE", 0 },
    { "sccs", OPT_SCCS, "RANGE", 0,
      "keep automata whose number of SCCs is in RANGE", 0 },
    { "acc-sccs", OPT_ACC_SCCS, "RANGE", 0,
      "keep automata whose number of non-trivial accepting SCCs is in RANGE",
      0 },
    { "accepting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "rej-sccs", OPT_REJ_SCCS, "RANGE", 0,
      "keep automata whose number of non-trivial rejecting SCCs is in RANGE",
      0 },
    { "rejecting-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "triv-sccs", OPT_TRIV_SCCS, "RANGE", 0,
      "keep automata whose number of trivial SCCs is in RANGE", 0 },
    { "trivial-sccs", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "inherently-weak-sccs", OPT_INHERENTLY_WEAK_SCCS, "RANGE", 0,
      "keep automata whose number of accepting inherently-weak SCCs is in "
      "RANGE.  An accepting SCC is inherently weak if it does not have a "
      "rejecting cycle.", 0 },
    { "weak-sccs", OPT_WEAK_SCCS, "RANGE", 0,
      "keep automata whose number of accepting weak SCCs is in RANGE.  "
      "In a weak SCC, all transitions belong to the same acceptance sets.", 0 },
    { "terminal-sccs", OPT_TERMINAL_SCCS, "RANGE", 0,
      "keep automata whose number of accepting terminal SCCs is in RANGE.  "
      "Terminal SCCs are weak and complete.", 0 },
    { "accept-word", OPT_ACCEPT_WORD, "WORD", 0,
      "keep automata that accept WORD", 0 },
    { "reject-word", OPT_REJECT_WORD, "WORD", 0,
      "keep automata that reject WORD", 0 },
    /**************************************************/
    RANGE_DOC_FULL,
    WORD_DOC,
    /**************************************************/
    { nullptr, 0, nullptr, 0, "Transformations:", 7 },
249
    { "merge-transitions", OPT_MERGE, nullptr, 0,
250
      "merge transitions with same destination and acceptance", 0 },
251
252
253
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
254
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
255
256
257
    { "product-or", OPT_PRODUCT_OR, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to sum languages", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
258
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
259
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
260
      "randomize only states or transitions)", 0 },
261
262
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
263
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
264
265
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
266
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
267
      "remove the acceptance condition and all acceptance sets", 0 },
268
269
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
270
      "initial state.  Implies --remove-unreachable-states.", 0 },
271
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
272
      "put the acceptance condition in Disjunctive Normal Form", 0 },
273
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
274
      "put the acceptance condition in Conjunctive Normal Form", 0 },
275
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
276
      "rewrite the automaton without using Fin acceptance", 0 },
277
278
279
280
281
282
283
284
285
286
287
288
289
290
    { "generalized-rabin", OPT_GENERALIZED_RABIN,
      "unique-inf|share-inf", OPTION_ARG_OPTIONAL,
      "rewrite the acceptance condition as generalized Rabin; the default "
      "\"unique-inf\" option uses the generalized Rabin definition from the "
      "HOA format; the \"share-inf\" option allows clauses to share Inf sets, "
      "therefore reducing the number of sets", 0 },
    { "gra", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "generalized-streett", OPT_GENERALIZED_STREETT,
      "unique-fin|share-fin", OPTION_ARG_OPTIONAL,
      "rewrite the acceptance condition as generalized Streett;"
      " the \"share-fin\" option allows clauses to share Fin sets,"
      " therefore reducing the number of sets; the default"
      " \"unique-fin\" does not", 0 },
    { "gsa", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
291
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
292
      "remove unused acceptance sets from the automaton", 0 },
293
294
295
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
296
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
297
298
      "complement the acceptance condition (without touching the automaton)",
      0 },
299
300
301
    { "decompose-strength", OPT_DECOMPOSE_STRENGTH, "t|w|s", 0,
      "extract the (t) terminal, (w) weak, or (s) strong part of an automaton"
      " (letters may be combined to combine more strengths in the output)", 0 },
302
303
    { "decompose-scc", OPT_DECOMPOSE_SCC, "N", 0, "keep only the Nth accepting"
      " SCC as accepting", 0 },
304
305
306
307
308
    { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
      "if any of those APs occur in the automaton, restrict all edges to "
      "ensure two of them may not be true at the same time.  Use this option "
      "multiple times to declare independent groups of exclusive "
      "propositions.", 0 },
309
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
310
311
312
      "if --exclusive-ap is used, assume those AP groups are actually exclusive"
      " in the system to simplify the expression of transition labels (implies "
      "--merge-transitions)", 0 },
313
314
315
    { "remove-ap", OPT_REM_AP, "AP[=0|=1][,AP...]", 0,
      "remove atomic propositions either by existential quantification, or "
      "by assigning them 0 or 1", 0 },
316
317
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
318
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
319
      "remove states that are unreachable from the initial state", 0 },
320
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
321
322
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
323
324
325
326
327
328
329
    { "sum", OPT_SUM_OR, "FILENAME", 0,
      "build the sum with the automaton in FILENAME "
      "to sum languages", 0 },
    { "sum-or", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
    { "sum-and", OPT_SUM_AND, "FILENAME", 0,
      "build the sum with the automaton in FILENAME "
      "to intersect languages", 0 },
330
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
331
332
      "if both Inf(x) and Fin(x) appear in the acceptance condition, replace "
      "Fin(x) by a new Fin(y) and adjust the automaton", 0 },
333
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
334
      "minimize the automaton using a SAT solver (only works for deterministic"
335
336
337
338
339
340
341
      " automata). Supported options are acc=STRING, states=N, max-states=N, "
      "sat-incr=N, sat-incr-steps=N, sat-langmap, sat-naive, colored, preproc=N"
      ". Spot uses by default its PicoSAT distribution but an external SAT"
      "solver can be set thanks to the SPOT_SATSOLVER environment variable"
      "(see spot-x)."
      , 0 },
    { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 },
342
343
    { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
344
      0 },
345
346
    { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
347
      0 },
348
349
350
    { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
      OPTION_ARG_OPTIONAL,
      "highlight nondeterministic states and edges with color NUM", 0},
351
352
    { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
      "highlight one run matching WORD using color NUM", 0},
353
    { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
354
      "highlight states that recognize identical languages", 0},
355
    /**************************************************/
356
357
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
358
      "then the simplification level defaults to --high unless specified "
359
      "otherwise.  If any option among --low, --medium, or --high is given, "
360
      "then the simplification goal defaults to --small unless specified "
361
362
363
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
364
    /**************************************************/
365
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
366
367
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
368
369
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
370
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
371
372
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
373
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
374
  {
375
    { &hoaread_argp, 0, nullptr, 0 },
376
377
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
378
    { &post_argp_disabled, 0, nullptr, 0 },
379
380
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
381
382
  };

383

384
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
385
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
386
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
387
388
389
390
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
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
enum gra_type { GRA_NO = 0, GRA_SHARE_INF = 1, GRA_UNIQUE_INF = 2 };
static gra_type opt_gra = GRA_NO;
static char const *const gra_args[] =
{
  "default", "share-inf", "hoa", "unique-inf", nullptr
};
static gra_type const gra_types[] =
{
  GRA_UNIQUE_INF, GRA_SHARE_INF, GRA_UNIQUE_INF, GRA_UNIQUE_INF
};
ARGMATCH_VERIFY(gra_args, gra_types);

enum gsa_type { GSA_NO = 0, GSA_SHARE_FIN = 1, GSA_UNIQUE_FIN = 2 };
static gsa_type opt_gsa = GSA_NO;
static char const *const gsa_args[] =
{
  "default", "share-fin", "unique-fin", nullptr
};
static gsa_type const gsa_types[] =
{
  GSA_UNIQUE_FIN, GSA_SHARE_FIN, GSA_UNIQUE_FIN
};
ARGMATCH_VERIFY(gsa_args, gsa_types);

416
// We want all these variables to be destroyed when we exit main, to
417
418
419
420
421
422
// make sure it happens before all other global variables (like the
// atomic propositions maps) are destroyed.  Otherwise we risk
// accessing deleted stuff.
static struct opt_t
{
  spot::bdd_dict_ptr dict = spot::make_bdd_dict();
423
424
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
425
426
  spot::twa_graph_ptr sum_and = nullptr;
  spot::twa_graph_ptr sum_or = nullptr;
427
  spot::twa_graph_ptr intersect = nullptr;
428
  spot::twa_graph_ptr included_in = nullptr;
429
430
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
431
  spot::twa_graph_ptr are_isomorphic = nullptr;
432
433
434
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
435
436
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
437
  std::vector<spot::twa_graph_ptr> acc_words;
438
  std::vector<spot::twa_graph_ptr> rej_words;
439
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
440
441
}* opt;

442
static bool opt_merge = false;
443
static bool opt_is_alternating = false;
444
445
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
446
static bool opt_is_semi_deterministic = false;
447
static bool opt_is_unambiguous = false;
448
449
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
450
static bool opt_is_inherently_weak = false;
451
static bool opt_is_very_weak = false;
452
static bool opt_is_stutter_invariant = false;
453
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
454
static range opt_states = { 0, std::numeric_limits<int>::max() };
455
456
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
457
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
458
459
460
static range opt_used_ap_n = { 0, std::numeric_limits<int>::max() };
static range opt_unused_ap_n = { 0, std::numeric_limits<int>::max() };
static bool need_unused_ap_count = false;
461
462
463
464
465
466
467
468
469
470
471
472
static range opt_sccs = { 0, std::numeric_limits<int>::max() };
static range opt_acc_sccs = { 0, std::numeric_limits<int>::max() };
static range opt_rej_sccs = { 0, std::numeric_limits<int>::max() };
static range opt_triv_sccs = { 0, std::numeric_limits<int>::max() };
static bool opt_sccs_set = false;
static bool opt_art_sccs_set = false; // need to classify SCCs as Acc/Rej/Triv.
static range opt_inhweak_sccs = { 0, std::numeric_limits<int>::max() };
static bool opt_inhweak_sccs_set = false;
static range opt_weak_sccs = { 0, std::numeric_limits<int>::max() };
static bool opt_weak_sccs_set = false;
static range opt_terminal_sccs = { 0, std::numeric_limits<int>::max() };
static bool opt_terminal_sccs_set = false;
473
474
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
475
static int opt_max_count = -1;
476
static bool opt_destut = false;
477
static char opt_instut = 0;
478
static bool opt_is_empty = false;
479
static bool opt_stripacc = false;
480
static bool opt_dnf_acc = false;
481
static bool opt_cnf_acc = false;
482
static bool opt_rem_fin = false;
483
static bool opt_clean_acc = false;
484
static bool opt_complement = false;
485
static bool opt_complement_acc = false;
486
static char* opt_decompose_strength = nullptr;
487
static int opt_decompose_scc = -1;
488
static spot::acc_cond::mark_t opt_mask_acc = 0U;
489
490
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
491
static bool opt_simplify_exclusive_ap = false;
492
493
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
494
static bool opt_rem_unused_ap = false;
495
static bool opt_sep_sets = false;
496
static const char* opt_sat_minimize = nullptr;
497
498
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
499
static bool opt_highlight_languages = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
500

501
static spot::twa_graph_ptr
502
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
503
{
504
  if ((!nonalt || aut->is_existential()) && spot::is_deterministic(aut))
505
506
507
508
509
510
511
512
    return aut;
  spot::postprocessor p;
  p.set_type(spot::postprocessor::Generic);
  p.set_pref(spot::postprocessor::Deterministic);
  p.set_level(level);
  return p.run(aut);
}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
513
514
515
516
517
518
static int
parse_opt(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
519
    case 'c':
520
      automaton_format = Count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
521
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
522
523
524
    case 'F':
      jobs.emplace_back(arg, true);
      break;
525
526
527
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
528
    case 'u':
529
      opt->uniq =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
530
531
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
532
533
534
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
535
536
    case 'x':
      {
537
538
539
        const char* opt = extra_options.parse_options(arg);
        if (opt)
          error(2, 0, "failed to parse --options near '%s'", opt);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
540
541
      }
      break;
542
543
544
    case OPT_AP_N:
      opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
545
546
547
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
548
549
550
551
    case OPT_ACC_SCCS:
      opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
552
    case OPT_ACCEPT_WORD:
553
      try
554
555
556
557
        {
          opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
558
      catch (const spot::parse_error& e)
559
560
561
562
        {
          error(2, 0, "failed to parse the argument of --accept-word:\n%s",
                e.what());
        }
563
      break;
564
    case OPT_ARE_ISOMORPHIC:
565
      opt->are_isomorphic = read_automaton(arg, opt->dict);
566
      break;
567
568
569
    case OPT_CLEAN_ACC:
      opt_clean_acc = true;
      break;
570
571
572
573
    case OPT_CNF_ACC:
      opt_dnf_acc = false;
      opt_cnf_acc = true;
      break;
574
575
576
    case OPT_COMPLEMENT:
      opt_complement = true;
      break;
577
578
579
    case OPT_COMPLEMENT_ACC:
      opt_complement_acc = true;
      break;
580
581
582
    case OPT_DECOMPOSE_STRENGTH:
      opt_decompose_strength = arg;
      break;
583
584
585
    case OPT_DECOMPOSE_SCC:
      opt_decompose_scc = to_pos_int(arg);
      break;
586
587
588
589
590
    case OPT_DESTUT:
      opt_destut = true;
      break;
    case OPT_DNF_ACC:
      opt_dnf_acc = true;
591
      opt_cnf_acc = false;
592
      break;
593
594
595
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
596
    case OPT_EXCLUSIVE_AP:
597
      opt->excl_ap.add_group(arg);
598
      break;
599
600
    case OPT_EQUIVALENT_TO:
      if (opt->equivalent_pos)
601
        error(2, 0, "only one --equivalent-to option can be given");
602
603
      opt->equivalent_pos = read_automaton(arg, opt->dict);
      opt->equivalent_neg =
604
        spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos, true));
605
      break;
606
607
608
609
610
611
612
613
614
615
616
617
618
619
    case OPT_GENERALIZED_RABIN:
      if (arg)
        opt_gra = XARGMATCH("--generalized-rabin", arg, gra_args, gra_types);
      else
        opt_gra = GRA_UNIQUE_INF;
      opt_gsa = GSA_NO;
      break;
    case OPT_GENERALIZED_STREETT:
      if (arg)
        opt_gsa = XARGMATCH("--generalized-streett", arg, gsa_args, gsa_types);
      else
        opt_gsa = GSA_UNIQUE_FIN;
      opt_gra = GRA_NO;
      break;
620
621
622
623
624
625
626
627
628
629
630
631
    case OPT_HIGHLIGHT_NONDET:
      {
        int v = arg ? to_pos_int(arg) : 1;
        opt_highlight_nondet_edges = opt_highlight_nondet_states = v;
        break;
      }
    case OPT_HIGHLIGHT_NONDET_STATES:
      opt_highlight_nondet_states = arg ? to_pos_int(arg) : 1;
      break;
    case OPT_HIGHLIGHT_NONDET_EDGES:
      opt_highlight_nondet_edges = arg ? to_pos_int(arg) : 1;
      break;
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
    case OPT_HIGHLIGHT_WORD:
      {
        char* endptr;
        int res = strtol(arg, &endptr, 10);
        if (endptr == arg)
          {
            res = 1;
          }
        else
          {
            if (res < 0)
              error(2, 0, "failed to parse the argument of --highlight-word: "
                    "%d is not positive", res);
            while (std::isspace(*endptr))
              ++endptr;
            if (*endptr != ',')
              error(2, 0, "failed to parse the argument of --highlight-word: "
                    "%d should be followed by a comma and WORD", res);
            arg = endptr + 1;
          }
        try
          {
            opt->hl_words.emplace_back(spot::parse_word(arg, opt->dict)
                                       ->as_automaton(), res);
          }
        catch (const spot::parse_error& e)
          {
            error(2, 0, "failed to parse the argument of --highlight-word:\n%s",
                  e.what());
          }
      }
      break;
664
665
666
    case OPT_HIGHLIGHT_LANGUAGES:
      opt_highlight_languages = true;
      break;
667
    case OPT_INSTUT:
668
      if (!arg || (arg[0] == '1' && arg[1] == 0))
669
        opt_instut = 1;
670
      else if (arg[0] == '2' && arg[1] == 0)
671
        opt_instut = 2;
672
      else
673
        error(2, 0, "unknown argument for --instut: %s", arg);
674
      break;
675
676
    case OPT_INCLUDED_IN:
      {
677
        auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
678
679
680
681
682
        aut = spot::dtwa_complement(aut);
        if (!opt->included_in)
          opt->included_in = aut;
        else
          opt->included_in = spot::product_or(opt->included_in, aut);
683
684
      }
      break;
685
686
687
688
689
    case OPT_INHERENTLY_WEAK_SCCS:
      opt_inhweak_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_inhweak_sccs_set = true;
      opt_art_sccs_set = true;
      break;
690
    case OPT_INTERSECT:
691
      opt->intersect = read_automaton(arg, opt->dict);
692
      break;
693
694
695
    case OPT_IS_ALTERNATING:
      opt_is_alternating = true;
      break;
696
697
698
699
700
701
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
702
703
704
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
705
706
707
    case OPT_IS_INHERENTLY_WEAK:
      opt_is_inherently_weak = true;
      break;
708
709
710
    case OPT_IS_VERY_WEAK:
      opt_is_very_weak = true;
      break;
711
712
713
    case OPT_IS_SEMI_DETERMINISTIC:
      opt_is_semi_deterministic = true;
      break;
714
715
    case OPT_IS_STUTTER_INVARIANT:
      opt_is_stutter_invariant = true;
716
      break;
717
718
719
    case OPT_IS_TERMINAL:
      opt_is_terminal = true;
      break;
720
721
722
    case OPT_IS_UNAMBIGUOUS:
      opt_is_unambiguous = true;
      break;
723
724
725
    case OPT_IS_WEAK:
      opt_is_weak = true;
      break;
726
727
728
729
730
731
    case OPT_KEEP_STATES:
      {
        std::vector<long> values = to_longs(arg);
        if (!values.empty())
          opt_keep_states_initial = values[0];
        for (auto res : values)
732
733
734
735
          {
            if (res < 0)
              error(2, 0, "state ids should be non-negative:"
                    " --mask-acc=%ld", res);
736
737
738
            // We don't know yet how many states the automata contain.
            if (opt_keep_states.size() <= static_cast<unsigned long>(res))
              opt_keep_states.resize(res + 1, false);
739
740
741
            opt_keep_states[res] = true;
          }
        break;
742
      }
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
    case OPT_MERGE:
      opt_merge = true;
      break;
    case OPT_MASK_ACC:
      {
        for (auto res : to_longs(arg))
          {
            if (res < 0)
              error(2, 0, "acceptance sets should be non-negative:"
                    " --mask-acc=%ld", res);
            if (static_cast<unsigned long>(res)
                > sizeof(spot::acc_cond::mark_t::value_t))
              error(2, 0, "this implementation does not support that many"
                    " acceptance sets: --mask-acc=%ld", res);
            opt_mask_acc.set(res);
          }
        break;
      }
    case OPT_NONDET_STATES:
      opt_nondet_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_nondet_states_set = true;
      break;
765
    case OPT_PRODUCT_AND:
766
      {
767
768
769
770
771
772
        auto a = read_automaton(arg, opt->dict);
        if (!opt->product_and)
          opt->product_and = std::move(a);
        else
          opt->product_and = spot::product(std::move(opt->product_and),
                                           std::move(a));
773
774
775
776
      }
      break;
    case OPT_PRODUCT_OR:
      {
777
778
779
780
781
782
        auto a = read_automaton(arg, opt->dict);
        if (!opt->product_or)
          opt->product_or = std::move(a);
        else
          opt->product_or = spot::product_or(std::move(opt->product_or),
                                             std::move(a));
783
784
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
785
786
    case OPT_RANDOMIZE:
      if (arg)
787
788
789
790
791
792
793
794
795
796
797
798
799
800
        {
          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);
              }
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
801
      else
802
803
804
805
        {
          randomize_tr = true;
          randomize_st = true;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
806
      break;
807
808
809
810
    case OPT_REJ_SCCS:
      opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
811
812
    case OPT_REJECT_WORD:
      try
813
814
815
816
        {
          opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
817
      catch (const spot::parse_error& e)
818
819
820
821
        {
          error(2, 0, "failed to parse the argument of --reject-word:\n%s",
                e.what());
        }
822
      break;
823
    case OPT_REM_AP:
824
      opt->rem_ap.add_ap(arg);
825
      break;
826
827
828
    case OPT_REM_DEAD:
      opt_rem_dead = true;
      break;
829
830
831
    case OPT_REM_FIN:
      opt_rem_fin = true;
      break;
832
833
834
    case OPT_REM_UNREACH:
      opt_rem_unreach = true;
      break;
835
836
837
    case OPT_REM_UNUSED_AP:
      opt_rem_unused_ap = true;
      break;
838
839
840
    case OPT_SAT_MINIMIZE:
      opt_sat_minimize = arg ? arg : "";
      break;
841
842
843
844
    case OPT_SCCS:
      opt_sccs_set = true;
      opt_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
845
846
847
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
848
849
850
    case OPT_SEP_SETS:
      opt_sep_sets = true;
      break;
851
852
853
854
    case OPT_SIMPLIFY_EXCLUSIVE_AP:
      opt_simplify_exclusive_ap = true;
      opt_merge = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
855
856
857
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
858
859
860
    case OPT_STRIPACC:
      opt_stripacc = true;
      break;
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
    case OPT_SUM_OR:
      {
        auto a = read_automaton(arg, opt->dict);
        if (!opt->sum_or)
          opt->sum_or = std::move(a);
        else
          opt->sum_or = spot::sum(std::move(opt->sum_or),
                                  std::move(a));
      }
      break;
    case OPT_SUM_AND:
      {
        auto a = read_automaton(arg, opt->dict);
        if (!opt->sum_and)
          opt->sum_and = std::move(a);
        else
          opt->sum_and = spot::sum_and(std::move(opt->sum_and),
                                       std::move(a));
      }
      break;
881
882
883
884
885
886
887
888
889
    case OPT_TERMINAL_SCCS:
      opt_terminal_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_terminal_sccs_set = true;
      opt_art_sccs_set = true;
      break;
    case OPT_TRIV_SCCS:
      opt_triv_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
890
891
892
893
894
895
896
897
    case OPT_USED_AP_N:
      opt_used_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      need_unused_ap_count = true;
      break;
    case OPT_UNUSED_AP_N:
      opt_unused_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      need_unused_ap_count = true;
      break;
898
899
900
901
902
    case OPT_WEAK_SCCS:
      opt_weak_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_weak_sccs_set = true;
      opt_art_sccs_set = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
903
904
905
906
907
908
909
910
911
912
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
static int unused_ap(const spot::const_twa_graph_ptr& aut)
{
  bdd all = aut->ap_vars();
  for (auto& e: aut->edges())
    {
      all = bdd_exist(all, bdd_support(e.cond));
      if (all == bddtrue)    // All APs are used.
        return 0;
    }
  int count = 0;
  while (all != bddtrue)
    {
      ++count;
      all = bdd_high(all);
    }
  return count;
}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
930
931
932

namespace
{
933
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
934
  {
935
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
936
    spot::postprocessor& post;
937
    automaton_printer printer;
938
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
939
940

    hoa_processor(spot::postprocessor& post)
941
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
942
943
944
945
    {
    }

    int
946
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
947
948
949
950
    {
      SPOT_UNREACHABLE();
    }

951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
    int process_string(const std::string& input, const char* filename,
                       int linenum) override
    {
      std::ostringstream loc;
      loc << filename << ':' << linenum;
      std::string locstr = loc.str();
      return process_automaton_stream
        (spot::automaton_stream_parser(input.c_str(), locstr, opt_parse),
         locstr.c_str());
    }

    int
    aborted(const spot::const_parsed_aut_ptr& h, const char* filename)
    {
      std::cerr << filename << ':' << h->loc << ": aborted input automaton\n";
      return 2;
    }

    int
    process_file(const char* filename) override
    {
      // If we have a filename like "foo/NN" such
      // that:
      // ① foo/NN is not a file,
      // ② NN is a number,
      // ③ foo is a file,
      // then it means we want to open foo as
      // a CSV file and process column NN.
      if (const char* slash = strrchr(filename, '/'))
        {
          char* end;
          errno = 0;
          long int col = strtol(slash + 1, &end, 10);
          if (errno == 0 && !*end && col != 0)
            {
              struct stat buf;
              if (stat(filename, &buf) != 0)
                {
                  col_to_read = col;
                  if (real_filename)
                    free(real_filename);
                  real_filename = strndup(filename, slash - filename);

                  // Special case for stdin.
                  if (real_filename[0] == '-' && real_filename[1] == 0)
                    return process_stream(std::cin, real_filename);

                  std::ifstream input(real_filename);
                  if (input)
                    return process_stream(input, real_filename);

                  error(2, errno, "cannot open '%s' nor '%s'",
                        filename, real_filename);
                }
            }
        }

      return process_automaton_stream(spot::automaton_stream_parser(filename,
                                                                    opt_parse),
                                      filename);
    }

    int process_automaton_stream(spot::automaton_stream_parser&& hp,
                                 const char* filename)
    {
      int err = 0;
      while (!abort_run)
        {
          auto haut = hp.parse(opt->dict);
          if (!haut->aut && haut->errors.empty())
            break;
          if (haut->format_errors(std::cerr))
            err = 2;
          if (!haut->aut)
            error(2, 0, "failed to read automaton from %s", filename);
          else if (haut->aborted)
            err = std::max(err, aborted(haut, filename));
          else
            process_automaton(haut, filename);
        }
      return err;
    }


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1035
    int
1036
    process_automaton(const spot::const_parsed_aut_ptr& haut,
1037
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1038
    {
1039
1040
      process_timer timer;
      timer.start();
1041

1042
1043
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
1044
      // merge_edges()) and the statistics about it make sense.
1045
      auto aut = ((automaton_format == Stats) || opt_name)
1046
1047
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
1048

1049
1050
      // Preprocessing.

1051
      if (opt_stripacc)
1052
        spot::strip_acceptance_here(aut);
1053
      if (opt_merge)
1054
        aut->merge_edges();
1055
      if (opt_clean_acc)
1056
        cleanup_acceptance_here(aut);
1057
      if (opt_sep_sets)
1058
        separate_sets_here(aut);
1059
      if (opt_complement_acc)
1060
1061
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
1062
      if (opt_rem_fin)
1063
        aut = remove_fin(aut);
1064
      if (opt_dnf_acc)
1065
1066
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
1067
      if (opt_cnf_acc)
1068
1069
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
1070

1071
1072
1073
1074
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1075
      matched &= opt_states.contains(aut->num_states());
1076
      matched &= opt_edges.contains(aut->num_edges());
1077
      matched &= opt_accsets.contains(aut->acc().num_sets());
1078
      matched &= opt_ap_n.contains(aut->ap().size());
1079
1080
1081
1082
1083
1084
      if (matched && need_unused_ap_count)
        {
          int unused = unused_ap(aut);
          matched &= opt_unused_ap_n.contains(unused);
          matched &= opt_used_ap_n.contains(aut->ap().size() - unused);
        }
1085
      if (matched && opt_is_alternating)
1086
        matched &= !aut->is_existential();
1087
      if (matched && opt_is_complete)
1088
        matched &= is_complete(aut);
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
      if (matched && (opt_sccs_set | opt_art_sccs_set))
        {
          spot::scc_info si(aut);
          unsigned n = si.scc_count();
          matched = opt_sccs.contains(n);

          if (opt_art_sccs_set && matched)
            {
              si.determine_unknown_acceptance();
              unsigned triv = 0;
              unsigned acc = 0;
              unsigned rej = 0;
              unsigned inhweak = 0;
              unsigned weak = 0;
              unsigned terminal = 0;
              for (unsigned s = 0; s < n; ++s)
                if (si.is_trivial(s))
                  {
                    ++triv;
                  }
                else if (si.is_rejecting_scc(s))
                  {
                    ++rej;
                  }
                else
                  {
                    ++acc;
                    if (opt_inhweak_sccs_set)
                      inhweak += is_inherently_weak_scc(si, s);
                    if (opt_weak_sccs_set)
                      weak += is_weak_scc(si, s);
                    if (opt_terminal_sccs_set)
                      terminal += is_terminal_scc(si, s);
                  }
              matched &= opt_acc_sccs.contains(acc);
              matched &= opt_rej_sccs.contains(rej);
              matched &= opt_triv_sccs.contains(triv);
              matched &= opt_inhweak_sccs.contains(inhweak);
              matched &= opt_weak_sccs.contains(weak);
              matched &= opt_terminal_sccs.contains(terminal);
            }
        }
1131
1132
      if (opt_nondet_states_set)
        matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
1133
      if (opt_