autfilt.cc 43.6 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>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
69

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

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
347
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
348
  {
349
    { &hoaread_argp, 0, nullptr, 0 },
350
351
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
352
    { &post_argp_disabled, 0, nullptr, 0 },
353
354
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
355
356
  };

357

358
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
359
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
360
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
361
362
363
364
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
365

366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
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);

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

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

470
static spot::twa_graph_ptr
471
ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
472
{
473
  if (!(nonalt && aut->is_alternating()) && spot::is_deterministic(aut))
474
475
476
477
478
479
480
481
    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
482
483
484
485
486
487
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
488
    case 'c':
489
      automaton_format = Count;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
490
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
491
492
493
    case 'F':
      jobs.emplace_back(arg, true);
      break;
494
495
496
    case 'n':
      opt_max_count = to_pos_int(arg);
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
497
    case 'u':
498
      opt->uniq =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
499
500
        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
      break;
501
502
503
    case 'v':
      opt_invert = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
504
505
    case 'x':
      {
506
507
508
        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
509
510
      }
      break;
511
512
513
    case OPT_AP_N:
      opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
514
515
516
    case OPT_ACC_SETS:
      opt_accsets = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
517
518
519
520
    case OPT_ACC_SCCS:
      opt_acc_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
521
    case OPT_ACCEPT_WORD:
522
      try
523
524
525
526
        {
          opt->acc_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
527
      catch (const spot::parse_error& e)
528
529
530
531
        {
          error(2, 0, "failed to parse the argument of --accept-word:\n%s",
                e.what());
        }
532
      break;
533
    case OPT_ARE_ISOMORPHIC:
534
      opt->are_isomorphic = read_automaton(arg, opt->dict);
535
      break;
536
537
538
    case OPT_CLEAN_ACC:
      opt_clean_acc = true;
      break;
539
540
541
542
    case OPT_CNF_ACC:
      opt_dnf_acc = false;
      opt_cnf_acc = true;
      break;
543
544
545
    case OPT_COMPLEMENT:
      opt_complement = true;
      break;
546
547
548
    case OPT_COMPLEMENT_ACC:
      opt_complement_acc = true;
      break;
549
550
551
    case OPT_DECOMPOSE_STRENGTH:
      opt_decompose_strength = arg;
      break;
552
553
554
555
556
    case OPT_DESTUT:
      opt_destut = true;
      break;
    case OPT_DNF_ACC:
      opt_dnf_acc = true;
557
      opt_cnf_acc = false;
558
      break;
559
560
561
    case OPT_EDGES:
      opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
562
    case OPT_EXCLUSIVE_AP:
563
      opt->excl_ap.add_group(arg);
564
      break;
565
566
    case OPT_EQUIVALENT_TO:
      if (opt->equivalent_pos)
567
        error(2, 0, "only one --equivalent-to option can be given");
568
569
      opt->equivalent_pos = read_automaton(arg, opt->dict);
      opt->equivalent_neg =
570
        spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos, true));
571
      break;
572
573
574
575
576
577
578
579
580
581
582
583
584
585
    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;
586
587
588
589
590
591
592
593
594
595
596
597
    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;
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
    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;

631
    case OPT_INSTUT:
632
      if (!arg || (arg[0] == '1' && arg[1] == 0))
633
        opt_instut = 1;
634
      else if (arg[0] == '2' && arg[1] == 0)
635
        opt_instut = 2;
636
      else
637
        error(2, 0, "unknown argument for --instut: %s", arg);
638
      break;
639
640
    case OPT_INCLUDED_IN:
      {
641
        auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
642
643
644
645
646
        aut = spot::dtwa_complement(aut);
        if (!opt->included_in)
          opt->included_in = aut;
        else
          opt->included_in = spot::product_or(opt->included_in, aut);
647
648
      }
      break;
649
650
651
652
653
    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;
654
    case OPT_INTERSECT:
655
      opt->intersect = read_automaton(arg, opt->dict);
656
      break;
657
658
659
    case OPT_IS_ALTERNATING:
      opt_is_alternating = true;
      break;
660
661
662
663
664
665
    case OPT_IS_COMPLETE:
      opt_is_complete = true;
      break;
    case OPT_IS_DETERMINISTIC:
      opt_is_deterministic = true;
      break;
666
667
668
    case OPT_IS_EMPTY:
      opt_is_empty = true;
      break;
669
670
671
    case OPT_IS_INHERENTLY_WEAK:
      opt_is_inherently_weak = true;
      break;
672
673
674
    case OPT_IS_VERY_WEAK:
      opt_is_very_weak = true;
      break;
675
676
    case OPT_IS_STUTTER_INVARIANT:
      opt_is_stutter_invariant = true;
677
      break;
678
679
680
    case OPT_IS_TERMINAL:
      opt_is_terminal = true;
      break;
681
682
683
    case OPT_IS_UNAMBIGUOUS:
      opt_is_unambiguous = true;
      break;
684
685
686
    case OPT_IS_WEAK:
      opt_is_weak = true;
      break;
687
688
689
690
691
692
    case OPT_KEEP_STATES:
      {
        std::vector<long> values = to_longs(arg);
        if (!values.empty())
          opt_keep_states_initial = values[0];
        for (auto res : values)
693
694
695
696
          {
            if (res < 0)
              error(2, 0, "state ids should be non-negative:"
                    " --mask-acc=%ld", res);
697
698
699
            // 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);
700
701
702
            opt_keep_states[res] = true;
          }
        break;
703
      }
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
    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;
726
    case OPT_PRODUCT_AND:
727
      {
728
729
730
731
732
733
        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));
734
735
736
737
      }
      break;
    case OPT_PRODUCT_OR:
      {
738
739
740
741
742
743
        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));
744
745
      }
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
746
747
    case OPT_RANDOMIZE:
      if (arg)
748
749
750
751
752
753
754
755
756
757
758
759
760
761
        {
          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
762
      else
763
764
765
766
        {
          randomize_tr = true;
          randomize_st = true;
        }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
767
      break;
768
769
770
771
    case OPT_REJ_SCCS:
      opt_rej_sccs = parse_range(arg, 0, std::numeric_limits<int>::max());
      opt_art_sccs_set = true;
      break;
772
773
    case OPT_REJECT_WORD:
      try
774
775
776
777
        {
          opt->rej_words.push_back(spot::parse_word(arg, opt->dict)
                                   ->as_automaton());
        }
778
      catch (const spot::parse_error& e)
779
780
781
782
        {
          error(2, 0, "failed to parse the argument of --reject-word:\n%s",
                e.what());
        }
783
      break;
784
    case OPT_REM_AP:
785
      opt->rem_ap.add_ap(arg);
786
      break;
787
788
789
    case OPT_REM_DEAD:
      opt_rem_dead = true;
      break;
790
791
792
    case OPT_REM_FIN:
      opt_rem_fin = true;
      break;
793
794
795
    case OPT_REM_UNREACH:
      opt_rem_unreach = true;
      break;
796
797
798
    case OPT_REM_UNUSED_AP:
      opt_rem_unused_ap = true;
      break;
799
800
801
    case OPT_SAT_MINIMIZE:
      opt_sat_minimize = arg ? arg : "";
      break;
802
803
804
805
    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
806
807
808
    case OPT_SEED:
      opt_seed = to_int(arg);
      break;
809
810
811
    case OPT_SEP_SETS:
      opt_sep_sets = true;
      break;
812
813
814
815
    case OPT_SIMPLIFY_EXCLUSIVE_AP:
      opt_simplify_exclusive_ap = true;
      opt_merge = true;
      break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
816
817
818
    case OPT_STATES:
      opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
      break;
819
820
821
    case OPT_STRIPACC:
      opt_stripacc = true;
      break;
822
823
824
825
826
827
828
829
830
    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;
831
832
833
834
835
836
837
838
    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;
839
840
841
842
843
    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
844
845
846
847
848
849
850
851
852
853
    case ARGP_KEY_ARG:
      jobs.emplace_back(arg, true);
      break;

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
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
871
872
873

namespace
{
874
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
875
  {
876
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
877
    spot::postprocessor& post;
878
    automaton_printer printer;
879
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
880
881

    hoa_processor(spot::postprocessor& post)
882
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
883
884
885
886
    {
    }

    int
887
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
888
889
890
891
    {
      SPOT_UNREACHABLE();
    }

892
893
894
895
896
897
898
899
900
901
902
903
904
905
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
    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
976
    int
977
    process_automaton(const spot::const_parsed_aut_ptr& haut,
978
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
979
    {
980
981
      process_timer timer;
      timer.start();
982

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

990
991
      // Preprocessing.

992
      if (opt_stripacc)
993
        spot::strip_acceptance_here(aut);
994
      if (opt_merge)
995
        aut->merge_edges();
996
      if (opt_clean_acc)
997
        cleanup_acceptance_here(aut);
998
      if (opt_sep_sets)
999
        separate_sets_here(aut);
1000
      if (opt_complement_acc)
1001
1002
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
1003
      if (opt_rem_fin)
1004
        aut = remove_fin(aut);
1005
      if (opt_dnf_acc)
1006
1007
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
1008
      if (opt_cnf_acc)
1009
1010
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
1011

1012
1013
1014
1015
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1016
      matched &= opt_states.contains(aut->num_states());
1017
      matched &= opt_edges.contains(aut->num_edges());
1018
      matched &= opt_accsets.contains(aut->acc().num_sets());
1019
      matched &= opt_ap_n.contains(aut->ap().size());
1020
1021
1022
1023
1024
1025
      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);
        }
1026
1027
      if (matched && opt_is_alternating)
        matched &= aut->is_alternating();
1028
      if (matched && opt_is_complete)
1029
        matched &= is_complete(aut);
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
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
      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);
            }
        }
1072
1073
      if (opt_nondet_states_set)
        matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
1074
      if (opt_is_deterministic)
1075
        matched &= is_deterministic(aut);
1076
      else if (opt_is_unambiguous)
1077
        matched &= is_unambiguous(aut);
1078
      if (opt_is_terminal)
1079
        matched &= is_terminal_automaton(aut);
1080
1081
      else if (opt_is_very_weak)
        matched &= is_very_weak_automaton(aut);
1082
      else if (opt_is_weak)
1083
        matched &= is_weak_automaton(aut);
1084
      else if (opt_is_inherently_weak)
1085
        matched &= is_inherently_weak_automaton(aut);
1086
1087
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
1088
      if (opt_is_empty)
1089
        matched &= aut->is_empty();
1090
      if (opt->intersect)
1091
        matched &= aut->intersects(opt->intersect);
1092
      if (opt->included_in)
1093
        matched &= !aut->intersects(opt->included_in);
1094
      if (opt->equivalent_pos)
1095
1096
1097
        matched &= !aut->intersects(opt->equivalent_neg)
          && (!dtwa_complement(ensure_deterministic(aut, true))->
              intersects(opt->equivalent_pos));
1098
1099

      if (matched && !opt->acc_words.empty())
1100
1101
1102
1103
1104
1105
        for (auto& word_aut: opt->acc_words)
          if (spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
1106
      if (matched && !opt->rej_words.empty())
1107
1108
1109
1110
1111
1112
        for (auto& word_aut: opt->rej_words)
          if (!spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
1113
1114
1115
1116
1117
1118
      if (opt_is_stutter_invariant)
        {
          check_stutter_invariance(aut);
          assert(aut