autfilt.cc 46.8 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
#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>
63
#include <spot/twaalgos/dualize.hh>
64
#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
  OPT_DESTUT,
Thomas Medioni's avatar
Thomas Medioni committed
94
  OPT_DUALIZE,
95
96
  OPT_DNF_ACC,
  OPT_EDGES,
97
  OPT_EQUIVALENT_TO,
98
  OPT_EXCLUSIVE_AP,
99
100
  OPT_GENERALIZED_RABIN,
  OPT_GENERALIZED_STREETT,
101
102
103
  OPT_HIGHLIGHT_NONDET,
  OPT_HIGHLIGHT_NONDET_EDGES,
  OPT_HIGHLIGHT_NONDET_STATES,
104
  OPT_HIGHLIGHT_WORD,
105
  OPT_HIGHLIGHT_LANGUAGES,
106
  OPT_INSTUT,
107
  OPT_INCLUDED_IN,
108
  OPT_INHERENTLY_WEAK_SCCS,
109
  OPT_INTERSECT,
110
  OPT_IS_ALTERNATING,
111
112
113
  OPT_IS_COMPLETE,
  OPT_IS_DETERMINISTIC,
  OPT_IS_EMPTY,
114
  OPT_IS_INHERENTLY_WEAK,
115
  OPT_IS_SEMI_DETERMINISTIC,
116
  OPT_IS_STUTTER_INVARIANT,
117
  OPT_IS_TERMINAL,
118
  OPT_IS_UNAMBIGUOUS,
119
  OPT_IS_VERY_WEAK,
120
  OPT_IS_WEAK,
121
122
123
  OPT_KEEP_STATES,
  OPT_MASK_ACC,
  OPT_MERGE,
124
  OPT_NONDET_STATES,
125
126
  OPT_PRODUCT_AND,
  OPT_PRODUCT_OR,
127
  OPT_RANDOMIZE,
128
  OPT_REJ_SCCS,
129
  OPT_REJECT_WORD,
130
  OPT_REM_AP,
131
132
  OPT_REM_DEAD,
  OPT_REM_UNREACH,
133
  OPT_REM_UNUSED_AP,
134
  OPT_REM_FIN,
135
  OPT_SAT_MINIMIZE,
136
  OPT_SCCS,
137
  OPT_SEED,
138
  OPT_SEP_SETS,
139
  OPT_SIMPLIFY_EXCLUSIVE_AP,
140
141
  OPT_STATES,
  OPT_STRIPACC,
142
143
  OPT_SUM_OR,
  OPT_SUM_AND,
144
145
  OPT_TERMINAL_SCCS,
  OPT_TRIV_SCCS,
146
147
  OPT_USED_AP_N,
  OPT_UNUSED_AP_N,
148
  OPT_WEAK_SCCS,
149
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
150

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
153
154
155
static const argp_option options[] =
  {
    /**************************************************/
156
    { nullptr, 0, nullptr, 0, "Input:", 1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
158
159
    { "file", 'F', "FILENAME", 0,
      "process the automaton in FILENAME", 0 },
    /**************************************************/
160
    { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
161
    { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
162
    /**************************************************/
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
    { 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 },
182
183
    { "is-semi-deterministic", OPT_IS_SEMI_DETERMINISTIC, nullptr, 0,
      "keep semi-deterministic automata", 0 },
184
185
    { "is-empty", OPT_IS_EMPTY, nullptr, 0,
      "keep automata with an empty language", 0 },
186
187
    { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
      "keep automata representing stutter-invariant properties", 0 },
188
189
    { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
      "keep only terminal automata", 0 },
190
191
    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
      "keep only unambiguous automata", 0 },
192
193
194
195
    { "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 },
196
197
    { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
      "keep only very-weak automata", 0 },
198
199
    { "is-alternating", OPT_IS_ALTERNATING, nullptr, 0,
      "keep only automata using universal branching", 0 },
200
201
202
203
204
205
206
207
208
209
210
211
212
213
    { "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 },
214
215
    { "nondet-states", OPT_NONDET_STATES, "RANGE", 0,
      "keep automata whose number of nondeterministic states is in RANGE", 0 },
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
249
    { "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 },
250
    { "merge-transitions", OPT_MERGE, nullptr, 0,
251
      "merge transitions with same destination and acceptance", 0 },
252
253
254
    { "product", OPT_PRODUCT_AND, "FILENAME", 0,
      "build the product with the automaton in FILENAME "
      "to intersect languages", 0 },
255
    { "product-and", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
256
257
258
    { "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
259
    { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
260
      "randomize states and transitions (specify 's' or 't' to "
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
261
      "randomize only states or transitions)", 0 },
262
263
    { "instut", OPT_INSTUT, "1|2", OPTION_ARG_OPTIONAL,
      "allow more stuttering (two possible algorithms)", 0 },
264
    { "destut", OPT_DESTUT, nullptr, 0, "allow less stuttering", 0 },
265
266
    { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0,
      "remove all transitions in specified acceptance sets", 0 },
267
    { "strip-acceptance", OPT_STRIPACC, nullptr, 0,
268
      "remove the acceptance condition and all acceptance sets", 0 },
269
270
    { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
      "only keep specified states.  The first state will be the new "\
271
      "initial state.  Implies --remove-unreachable-states.", 0 },
272
    { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
273
      "put the acceptance condition in Disjunctive Normal Form", 0 },
274
    { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0,
275
      "put the acceptance condition in Conjunctive Normal Form", 0 },
276
    { "remove-fin", OPT_REM_FIN, nullptr, 0,
277
      "rewrite the automaton without using Fin acceptance", 0 },
278
279
280
281
282
283
284
285
286
287
288
289
290
291
    { "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 },
292
    { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
293
      "remove unused acceptance sets from the automaton", 0 },
294
295
296
    { "complement", OPT_COMPLEMENT, nullptr, 0,
      "complement each automaton (currently support only deterministic "
      "automata)", 0 },
297
    { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
298
299
      "complement the acceptance condition (without touching the automaton)",
      0 },
300
301
302
    { "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 },
303
304
    { "decompose-scc", OPT_DECOMPOSE_SCC, "N", 0, "keep only the Nth accepting"
      " SCC as accepting", 0 },
Thomas Medioni's avatar
Thomas Medioni committed
305
306
    { "dualize", OPT_DUALIZE, nullptr, 0,
      "dualize each automaton", 0 },
307
308
309
310
311
    { "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 },
312
    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, nullptr, 0,
313
314
315
      "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 },
316
317
318
    { "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 },
319
320
    { "remove-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
      "remove declared atomic propositions that are not used", 0 },
321
    { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
322
      "remove states that are unreachable from the initial state", 0 },
323
    { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
324
325
      "remove states that are unreachable, or that cannot belong to an "
      "infinite path", 0 },
326
327
328
329
330
331
332
    { "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 },
333
    { "separate-sets", OPT_SEP_SETS, nullptr, 0,
334
335
      "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 },
336
    { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL,
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
337
      "minimize the automaton using a SAT solver (only works for deterministic"
338
339
340
341
342
343
344
      " 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 },
345
346
    { "highlight-nondet-states", OPT_HIGHLIGHT_NONDET_STATES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic states with color NUM",
347
      0 },
348
349
    { "highlight-nondet-edges", OPT_HIGHLIGHT_NONDET_EDGES, "NUM",
      OPTION_ARG_OPTIONAL, "highlight nondeterministic edges with color NUM",
350
      0 },
351
352
353
    { "highlight-nondet", OPT_HIGHLIGHT_NONDET, "NUM",
      OPTION_ARG_OPTIONAL,
      "highlight nondeterministic states and edges with color NUM", 0},
354
355
    { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0,
      "highlight one run matching WORD using color NUM", 0},
356
    { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 ,
357
      "highlight states that recognize identical languages", 0},
358
    /**************************************************/
359
360
    { nullptr, 0, nullptr, 0,
      "If any option among --small, --deterministic, or --any is given, "
361
      "then the simplification level defaults to --high unless specified "
362
      "otherwise.  If any option among --low, --medium, or --high is given, "
363
      "then the simplification goal defaults to --small unless specified "
364
365
366
      "otherwise.  If none of those options are specified, then autfilt "
      "acts as is --any --low were given: these actually disable the "
      "simplification routines.", 22 },
367
    /**************************************************/
368
    { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
369
370
    { "extra-options", 'x', "OPTS", 0,
      "fine-tuning options (see spot-x (7))", 0 },
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
371
372
    { "seed", OPT_SEED, "INT", 0,
      "seed for the random number generator (0)", 0 },
373
    { nullptr, 0, nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
374
375
  };

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

386

387
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
388
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
389
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
390
391
392
393
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
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
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);

419
// We want all these variables to be destroyed when we exit main, to
420
421
422
423
424
425
// 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();
426
427
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
428
429
  spot::twa_graph_ptr sum_and = nullptr;
  spot::twa_graph_ptr sum_or = nullptr;
430
  spot::twa_graph_ptr intersect = nullptr;
431
  spot::twa_graph_ptr included_in = nullptr;
432
433
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
434
  spot::twa_graph_ptr are_isomorphic = nullptr;
435
436
437
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
438
439
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
440
  std::vector<spot::twa_graph_ptr> acc_words;
441
  std::vector<spot::twa_graph_ptr> rej_words;
442
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
443
444
}* opt;

445
static bool opt_merge = false;
446
static bool opt_is_alternating = false;
447
448
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
449
static bool opt_is_semi_deterministic = false;
450
static bool opt_is_unambiguous = false;
451
452
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
453
static bool opt_is_inherently_weak = false;
454
static bool opt_is_very_weak = false;
455
static bool opt_is_stutter_invariant = false;
456
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
457
static range opt_states = { 0, std::numeric_limits<int>::max() };
458
459
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
460
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
461
462
463
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;
464
465
466
467
468
469
470
471
472
473
474
475
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;
476
477
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
478
static int opt_max_count = -1;
479
static bool opt_destut = false;
480
static char opt_instut = 0;
481
static bool opt_is_empty = false;
482
static bool opt_stripacc = false;
483
static bool opt_dnf_acc = false;
484
static bool opt_cnf_acc = false;
485
static bool opt_rem_fin = false;
486
static bool opt_clean_acc = false;
487
static bool opt_complement = false;
488
static bool opt_complement_acc = false;
489
static char* opt_decompose_strength = nullptr;
490
static int opt_decompose_scc = -1;
Thomas Medioni's avatar
Thomas Medioni committed
491
static bool opt_dualize = false;
492
static spot::acc_cond::mark_t opt_mask_acc = 0U;
493
494
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
495
static bool opt_simplify_exclusive_ap = false;
496
497
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
498
static bool opt_rem_unused_ap = false;
499
static bool opt_sep_sets = false;
500
static const char* opt_sat_minimize = nullptr;
501
502
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
503
static bool opt_highlight_languages = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
504

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
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
943
944
945

namespace
{
946
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
947
  {
948
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
949
    spot::postprocessor& post;
950
    automaton_printer printer;
951
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
952
953

    hoa_processor(spot::postprocessor& post)
954
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
955
956
957
958
    {
    }

    int
959
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
960
961
962
963
    {
      SPOT_UNREACHABLE();
    }

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
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
    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
1048
    int
1049
    process_automaton(const spot::const_parsed_aut_ptr& haut,
1050
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1051
    {
1052
1053
      process_timer timer;
      timer.start();
1054

1055
1056
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
1057
      // merge_edges()) and the statistics about it make sense.
1058
      auto aut = ((automaton_format == Stats) || opt_name)
1059
1060
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
1061

1062
1063
      // Preprocessing.

1064
      if (opt_stripacc)
1065
        spot::strip_acceptance_here(aut);
1066
      if (opt_merge)
1067
        aut->merge_edges();
1068
      if (opt_clean_acc)
1069
        cleanup_acceptance_here(aut);
1070
      if (opt_sep_sets)
1071
        separate_sets_here(aut);
1072
      if (opt_complement_acc)
1073
1074
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
1075
      if (opt_rem_fin)
1076
        aut = remove_fin(aut);
1077
      if (opt_dnf_acc)
1078
1079
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
1080
      if (opt_cnf_acc)
1081
1082
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
1083

1084
1085
1086
1087
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1088
      matched &= opt_states.contains(aut->num_states());
1089
      matched &= opt_edges.contains(aut->num_edges());
1090
      matched &= opt_accsets.contains(aut->acc().num_sets());
1091
      matched &= opt_ap_n.contains(aut->ap().size());
1092
1093
1094
1095
1096
1097
      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);
        }
1098
      if (matched && opt_is_alternating)
1099
        matched &= !aut->is_existential();
1100
      if (matched && opt_is_complete)
1101
        matched &= is_complete(aut);