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

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

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

155
156
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
393
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
394
  {
395
    { &hoaread_argp, 0, nullptr, 0 },
396
397
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
398
    { &post_argp_disabled, 0, nullptr, 0 },
399
400
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
401
402
  };

403

404
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
405
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
406
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
407
408
409
410
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
411

412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
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);

436
// We want all these variables to be destroyed when we exit main, to
437
438
439
440
441
442
// 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();
443
444
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
445
446
  spot::twa_graph_ptr sum_and = nullptr;
  spot::twa_graph_ptr sum_or = nullptr;
447
  spot::twa_graph_ptr intersect = nullptr;
448
  spot::twa_graph_ptr included_in = nullptr;
449
450
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
451
  spot::twa_graph_ptr are_isomorphic = nullptr;
452
453
454
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
455
456
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
457
  std::vector<spot::twa_graph_ptr> acc_words;
458
  std::vector<spot::twa_graph_ptr> rej_words;
459
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
460
461
}* opt;

462
static bool opt_merge = false;
463
static bool opt_is_alternating = false;
464
465
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
466
static bool opt_is_semi_deterministic = false;
467
static bool opt_is_unambiguous = false;
468
469
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
470
static bool opt_is_inherently_weak = false;
471
static bool opt_is_very_weak = false;
472
static bool opt_is_stutter_invariant = false;
473
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
474
static range opt_states = { 0, std::numeric_limits<int>::max() };
475
476
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
477
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
478
479
480
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;
481
482
483
484
485
486
487
488
489
490
491
492
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;
493
494
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
495
static int opt_max_count = -1;
496
static bool opt_destut = false;
497
static char opt_instut = 0;
498
static bool opt_is_empty = false;
499
static bool opt_stripacc = false;
500
static bool opt_dnf_acc = false;
501
static bool opt_cnf_acc = false;
502
static bool opt_rem_fin = false;
503
static bool opt_clean_acc = false;
504
static bool opt_complement = false;
505
static bool opt_complement_acc = false;
506
static char* opt_decompose_scc = nullptr;
Thomas Medioni's avatar
Thomas Medioni committed
507
static bool opt_dualize = false;
508
static spot::acc_cond::mark_t opt_mask_acc = 0U;
509
510
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
511
static bool opt_simpl_acc = false;
512
static bool opt_simplify_exclusive_ap = false;
513
514
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
515
static bool opt_rem_unused_ap = false;
516
static bool opt_sep_sets = false;
517
static bool opt_split_edges = false;
518
static const char* opt_sat_minimize = nullptr;
519
520
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
521
static bool opt_highlight_languages = false;
522
static bool opt_dca = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
523

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
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
968
969
970

namespace
{
971
972

  struct autfilt_processor: hoa_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
973
  {
974
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
975
    spot::postprocessor& post;
976
    automaton_printer printer;
977
  public:
978
979
    autfilt_processor(spot::postprocessor& post, spot::bdd_dict_ptr dict)
      : hoa_processor(dict), post(post), printer(aut_input)
980
981
982
    {
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
983
    int
984
    process_automaton(const spot::const_parsed_aut_ptr& haut) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
985
    {
986
987
      process_timer timer;
      timer.start();
988

989
990
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
991
      // merge_edges()) and the statistics about it make sense.
992
      auto aut = ((automaton_format == Stats) || opt_name)
993
994
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
995

996
997
      // Preprocessing.

998
      if (opt_stripacc)
999
        spot::strip_acceptance_here(aut);
1000
      if (opt_merge)
1001
        aut->merge_edges();
1002
1003
1004
1005

      if (opt_simpl_acc)
        simplify_acceptance_here(aut);
      else if (opt_clean_acc)
1006
        cleanup_acceptance_here(aut);
1007

1008
      if (opt_sep_sets)
1009
        separate_sets_here(aut);
1010
      if (opt_complement_acc)
1011
1012
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
1013
      if (opt_rem_fin)
1014
        aut = remove_fin(aut);
1015
      if (opt_dnf_acc)
1016
1017
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
1018
      if (opt_cnf_acc)
1019
1020
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
1021

1022
1023
1024
1025
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1026
      matched &= opt_states.contains(aut->num_states());
1027
      matched &= opt_edges.contains(aut->num_edges());
1028
      matched &= opt_accsets.contains(aut->acc().num_sets());
1029
      matched &= opt_ap_n.contains(aut->ap().size());
1030
1031
1032
1033
1034
1035
      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);
        }
1036
      if (matched && opt_is_alternating)
1037
        matched &= !aut->is_existential();
1038
      if (matched && opt_is_complete)
1039
        matched &= is_complete(aut);
1040
1041