autfilt.cc 44.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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
#include <spot/twaalgos/product.hh>
#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>
64
#include <spot/twaalgos/hoa.hh>
65
66
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isweakscc.hh>
67
#include <spot/twaalgos/gtec/gtec.hh>
68
#include <spot/twaalgos/totgba.hh>
69
#include <spot/twaalgos/langmap.hh>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
70

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

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

146
147
#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
360
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
361
  {
362
    { &hoaread_argp, 0, nullptr, 0 },
363
364
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
365
    { &post_argp_disabled, 0, nullptr, 0 },
366
367
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
368
369
  };

370

371
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
372
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
373
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
374
375
376
377
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
378

379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
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);

403
// We want all these variables to be destroyed when we exit main, to
404
405
406
407
408
409
// 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();
410
411
  spot::twa_graph_ptr product_and = nullptr;
  spot::twa_graph_ptr product_or = nullptr;
412
  spot::twa_graph_ptr intersect = nullptr;
413
  spot::twa_graph_ptr included_in = nullptr;
414
415
  spot::twa_graph_ptr equivalent_pos = nullptr;
  spot::twa_graph_ptr equivalent_neg = nullptr;
416
  spot::twa_graph_ptr are_isomorphic = nullptr;
417
418
419
  std::unique_ptr<spot::isomorphism_checker>
                         isomorphism_checker = nullptr;
  std::unique_ptr<unique_aut_t> uniq = nullptr;
420
421
  spot::exclusive_ap excl_ap;
  spot::remove_ap rem_ap;
422
  std::vector<spot::twa_graph_ptr> acc_words;
423
  std::vector<spot::twa_graph_ptr> rej_words;
424
  std::vector<std::pair<spot::twa_graph_ptr, unsigned>> hl_words;
425
426
}* opt;

427
static bool opt_merge = false;
428
static bool opt_is_alternating = false;
429
430
static bool opt_is_complete = false;
static bool opt_is_deterministic = false;
431
static bool opt_is_semi_deterministic = false;
432
static bool opt_is_unambiguous = false;
433
434
static bool opt_is_terminal = false;
static bool opt_is_weak = false;
435
static bool opt_is_inherently_weak = false;
436
static bool opt_is_very_weak = false;
437
static bool opt_is_stutter_invariant = false;
438
static bool opt_invert = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
439
static range opt_states = { 0, std::numeric_limits<int>::max() };
440
441
static range opt_edges = { 0, std::numeric_limits<int>::max() };
static range opt_accsets = { 0, std::numeric_limits<int>::max() };
442
static range opt_ap_n = { 0, std::numeric_limits<int>::max() };
443
444
445
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;
446
447
448
449
450
451
452
453
454
455
456
457
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;
458
459
static range opt_nondet_states = { 0, std::numeric_limits<int>::max() };
static bool opt_nondet_states_set = false;
460
static int opt_max_count = -1;
461
static bool opt_destut = false;
462
static char opt_instut = 0;
463
static bool opt_is_empty = false;
464
static bool opt_stripacc = false;
465
static bool opt_dnf_acc = false;
466
static bool opt_cnf_acc = false;
467
static bool opt_rem_fin = false;
468
static bool opt_clean_acc = false;
469
static bool opt_complement = false;
470
static bool opt_complement_acc = false;
471
static char* opt_decompose_strength = nullptr;
472
static spot::acc_cond::mark_t opt_mask_acc = 0U;
473
474
static std::vector<bool> opt_keep_states = {};
static unsigned int opt_keep_states_initial = 0;
475
static bool opt_simplify_exclusive_ap = false;
476
477
static bool opt_rem_dead = false;
static bool opt_rem_unreach = false;
478
static bool opt_rem_unused_ap = false;
479
static bool opt_sep_sets = false;
480
static const char* opt_sat_minimize = nullptr;
481
482
static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1;
483
static bool opt_highlight_languages = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
484

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
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
891
892
893

namespace
{
894
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
895
  {
896
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
897
    spot::postprocessor& post;
898
    automaton_printer printer;
899
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
900
901

    hoa_processor(spot::postprocessor& post)
902
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
903
904
905
906
    {
    }

    int
907
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
908
909
910
911
    {
      SPOT_UNREACHABLE();
    }

912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
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
    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
996
    int
997
    process_automaton(const spot::const_parsed_aut_ptr& haut,
998
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
999
    {
1000
1001
      process_timer timer;
      timer.start();
1002

1003
1004
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
1005
      // merge_edges()) and the statistics about it make sense.
1006
      auto aut = ((automaton_format == Stats) || opt_name)
1007
1008
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
1009

1010
1011
      // Preprocessing.

1012
      if (opt_stripacc)
1013
        spot::strip_acceptance_here(aut);
1014
      if (opt_merge)
1015
        aut->merge_edges();
1016
      if (opt_clean_acc)
1017
        cleanup_acceptance_here(aut);
1018
      if (opt_sep_sets)
1019
        separate_sets_here(aut);
1020
      if (opt_complement_acc)
1021
1022
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
1023
      if (opt_rem_fin)
1024
        aut = remove_fin(aut);
1025
      if (opt_dnf_acc)
1026
1027
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
1028
      if (opt_cnf_acc)
1029
1030
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
1031

1032
1033
1034
1035
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1036
      matched &= opt_states.contains(aut->num_states());
1037
      matched &= opt_edges.contains(aut->num_edges());
1038
      matched &= opt_accsets.contains(aut->acc().num_sets());
1039
      matched &= opt_ap_n.contains(aut->ap().size());
1040
1041
1042
1043
1044
1045
      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);
        }
1046
      if (matched && opt_is_alternating)
1047
        matched &= !aut->is_existential();
1048
      if (matched && opt_is_complete)
1049
        matched &= is_complete(aut);
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
      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);
            }
        }
1092
1093
      if (opt_nondet_states_set)
        matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
1094
      if (opt_is_deterministic)
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
        {
          matched &= is_deterministic(aut);
        }
      else
        {
          if (opt_is_unambiguous)
            matched &= is_unambiguous(aut);
          if (opt_is_semi_deterministic)
            matched &= is_semi_deterministic(aut);
        }
1105
      if (opt_is_terminal)
1106
        matched &= is_terminal_automaton(aut);
1107
1108
      else if (opt_is_very_weak)
        matched &= is_very_weak_automaton(aut);
1109
      else if (opt_is_weak)
1110
        matched &= is_weak_automaton(aut);
1111
      else if (opt_is_inherently_weak)
1112
        matched &= is_inherently_weak_automaton(aut);
1113
1114
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
1115
      if (opt_is_empty)
1116
        matched &= aut->is_empty();
1117
      if (opt->intersect)
1118
        matched &= aut->intersects(opt->intersect);