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

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

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

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

373

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

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

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

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

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
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
898
899
900

namespace
{
901
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
902
  {
903
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
904
    spot::postprocessor& post;
905
    automaton_printer printer;
906
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
907
908

    hoa_processor(spot::postprocessor& post)
909
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
910
911
912
913
    {
    }

    int
914
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
915
916
917
918
    {
      SPOT_UNREACHABLE();
    }

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
996
997
998
999
1000
1001
1002
    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
1003
    int
1004
    process_automaton(const spot::const_parsed_aut_ptr& haut,
1005
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1006
    {
1007
1008
      process_timer timer;
      timer.start();
1009

1010
1011
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
1012
      // merge_edges()) and the statistics about it make sense.
1013
      auto aut = ((automaton_format == Stats) || opt_name)
1014
1015
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
1016

1017
1018
      // Preprocessing.

1019
      if (opt_stripacc)
1020
        spot::strip_acceptance_here(aut);
1021
      if (opt_merge)
1022
        aut->merge_edges();
1023
      if (opt_clean_acc)
1024
        cleanup_acceptance_here(aut);
1025
      if (opt_sep_sets)
1026
        separate_sets_here(aut);
1027
      if (opt_complement_acc)
1028
1029
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
1030
      if (opt_rem_fin)
1031
        aut = remove_fin(aut);
1032
      if (opt_dnf_acc)
1033
1034
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
1035
      if (opt_cnf_acc)
1036
1037
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
1038

1039
1040
1041
1042
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1043
      matched &= opt_states.contains(aut->num_states());
1044
      matched &= opt_edges.contains(aut->num_edges());
1045
      matched &= opt_accsets.contains(aut->acc().num_sets());
1046
      matched &= opt_ap_n.contains(aut->ap().size());
1047
1048
1049
1050
1051
1052
      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);
        }
1053
      if (matched && opt_is_alternating)
1054
        matched &= !aut->is_existential();
1055
      if (matched && opt_is_complete)
1056
        matched &= is_complete(aut);
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
1092
1093
1094
1095
1096
1097
1098
      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);
            }
        }
1099
1100
      if (opt_nondet_states_set)
        matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
1101
      if (opt_is_deterministic)
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
        {
          matched &= is_deterministic(aut);
        }
      else
        {
          if (opt_is_unambiguous)
            matched &= is_unambiguous(aut);
          if (opt_is_semi_deterministic)
            matched &= is_semi_deterministic(aut);
        }
1112
      if (opt_is_terminal)
1113
        matched &= is_terminal_automaton(aut);
1114
1115
      else if (opt_is_very_weak)
        matched &= is_very_weak_automaton(aut);
1116
      else if (opt_is_weak)
1117
        matched &= is_weak_automaton(aut);
1118
      else if (opt_is_inherently_weak)
1119
        matched &= is_inherently_weak_automaton(aut);
1120
1121
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
Alexandre Duret-Lutz's avatar