autfilt.cc 44.4 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
typos    
Alexandre Duret-Lutz committed
2
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
3
// 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
148

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
354
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
355
  {
356
    { &hoaread_argp, 0, nullptr, 0 },
357
358
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
359
    { &post_argp_disabled, 0, nullptr, 0 },
360
361
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
362
363
  };

364

365
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
366
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
367
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
368
369
370
371
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
372

373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
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);

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

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

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
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
885
886
887

namespace
{
888
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
889
  {
890
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
891
    spot::postprocessor& post;
892
    automaton_printer printer;
893
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
894
895

    hoa_processor(spot::postprocessor& post)
896
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
897
898
899
900
    {
    }

    int
901
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
902
903
904
905
    {
      SPOT_UNREACHABLE();
    }

906
907
908
909
910
911
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
    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
990
    int
991
    process_automaton(const spot::const_parsed_aut_ptr& haut,
992
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
993
    {
994
995
      process_timer timer;
      timer.start();
996

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

1004
1005
      // Preprocessing.

1006
      if (opt_stripacc)
1007
        spot::strip_acceptance_here(aut);
1008
      if (opt_merge)
1009
        aut->merge_edges();
1010
      if (opt_clean_acc)
1011
        cleanup_acceptance_here(aut);
1012
      if (opt_sep_sets)
1013
        separate_sets_here(aut);
1014
      if (opt_complement_acc)
1015
1016
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
1017
      if (opt_rem_fin)
1018
        aut = remove_fin(aut);
1019
      if (opt_dnf_acc)
1020
1021
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
1022
      if (opt_cnf_acc)
1023
1024
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
1025

1026
1027
1028
1029
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1030
      matched &= opt_states.contains(aut->num_states());
1031
      matched &= opt_edges.contains(aut->num_edges());
1032
      matched &= opt_accsets.contains(aut->acc().num_sets());
1033
      matched &= opt_ap_n.contains(aut->ap().size());
1034
1035
1036
1037
1038
1039
      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);
        }
1040
1041
      if (matched && opt_is_alternating)
        matched &= aut->is_alternating();
1042
      if (matched && opt_is_complete)
1043
        matched &= is_complete(aut);
1044
1045
1046
1047
1048
1049
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
      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);
            }
        }
1086
1087
      if (opt_nondet_states_set)
        matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
1088
      if (opt_is_deterministic)
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
        {
          matched &= is_deterministic(aut);
        }
      else
        {
          if (opt_is_unambiguous)
            matched &= is_unambiguous(aut);
          if (opt_is_semi_deterministic)
            matched &= is_semi_deterministic(aut);
        }
1099
      if (opt_is_terminal)
1100
        matched &= is_terminal_automaton(aut);
1101
1102
      else if (opt_is_very_weak)
        matched &= is_very_weak_automaton(aut);
1103
      else if (opt_is_weak)
1104
        matched &= is_weak_automaton(aut);
1105
      else if (opt_is_inherently_weak)
1106
        matched &= is_inherently_weak_automaton(aut);
1107
1108
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
1109
      if (opt_is_empty)
1110
        matched &= aut->is_empty();
1111
      if (opt->intersect)
1112
        matched &= aut->intersects(opt->intersect);
1113
      if (opt->included_in)