autfilt.cc 43 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
105
106
107
  OPT_INTERSECT,
  OPT_IS_COMPLETE,
  OPT_IS_DETERMINISTIC,
  OPT_IS_EMPTY,
108
  OPT_IS_STUTTER_INVARIANT,
109
  OPT_IS_TERMINAL,
110
  OPT_IS_UNAMBIGUOUS,
111
  OPT_IS_WEAK,
112
  OPT_IS_INHERENTLY_WEAK,
113
114
115
  OPT_KEEP_STATES,
  OPT_MASK_ACC,
  OPT_MERGE,
116
  OPT_NONDET_STATES,
117
118
  OPT_PRODUCT_AND,
  OPT_PRODUCT_OR,
119
  OPT_RANDOMIZE,
120
  OPT_REJ_SCCS,
121
  OPT_REJECT_WORD,
122
  OPT_REM_AP,
123
124
  OPT_REM_DEAD,
  OPT_REM_UNREACH,
125
  OPT_REM_UNUSED_AP,
126
  OPT_REM_FIN,
127
  OPT_SAT_MINIMIZE,
128
  OPT_SCCS,
129
  OPT_SEED,
130
  OPT_SEP_SETS,
131
  OPT_SIMPLIFY_EXCLUSIVE_AP,
132
133
  OPT_STATES,
  OPT_STRIPACC,
134
135
  OPT_TERMINAL_SCCS,
  OPT_TRIV_SCCS,
136
137
  OPT_USED_AP_N,
  OPT_UNUSED_AP_N,
138
  OPT_WEAK_SCCS,
139
};
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
140
141
142
143

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
341
static const struct argp_child children[] =
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
342
  {
343
    { &hoaread_argp, 0, nullptr, 0 },
344
345
    { &aoutput_argp, 0, nullptr, 0 },
    { &aoutput_io_format_argp, 0, nullptr, 4 },
346
    { &post_argp_disabled, 0, nullptr, 0 },
347
348
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
349
350
  };

351

352
typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
353
typedef std::set<std::vector<tr_t>> unique_aut_t;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
354
static long int match_count = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
355
356
357
358
static spot::option_map extra_options;
static bool randomize_st = false;
static bool randomize_tr = false;
static int opt_seed = 0;
359

360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
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);

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

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

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

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

    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
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
857
858
859

namespace
{
860
  class hoa_processor final: public job_processor
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
861
  {
862
  private:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
863
    spot::postprocessor& post;
864
    automaton_printer printer;
865
  public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
866
867

    hoa_processor(spot::postprocessor& post)
868
      : post(post), printer(aut_input)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
869
870
871
872
    {
    }

    int
873
    process_formula(spot::formula, const char*, int) override
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
874
875
876
877
    {
      SPOT_UNREACHABLE();
    }

878
879
880
881
882
883
884
885
886
887
888
889
890
891
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
    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
962
    int
963
    process_automaton(const spot::const_parsed_aut_ptr& haut,
964
                      const char* filename)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
965
966
967
    {
      spot::stopwatch sw;
      sw.start();
968

969
970
      // If --stats or --name is used, duplicate the automaton so we
      // never modify the original automaton (e.g. with
971
      // merge_edges()) and the statistics about it make sense.
972
      auto aut = ((automaton_format == Stats) || opt_name)
973
974
        ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all())
        : haut->aut;
975

976
977
      // Preprocessing.

978
      if (opt_stripacc)
979
        spot::strip_acceptance_here(aut);
980
      if (opt_merge)
981
        aut->merge_edges();
982
      if (opt_clean_acc || opt_rem_fin)
983
        cleanup_acceptance_here(aut);
984
      if (opt_sep_sets)
985
        separate_sets_here(aut);
986
      if (opt_complement_acc)
987
988
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().complement());
989
      if (opt_rem_fin)
990
        aut = remove_fin(aut);
991
      if (opt_dnf_acc)
992
993
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_dnf());
994
      if (opt_cnf_acc)
995
996
        aut->set_acceptance(aut->acc().num_sets(),
                            aut->get_acceptance().to_cnf());
997

998
999
1000
1001
      // Filters.

      bool matched = true;

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1002
      matched &= opt_states.contains(aut->num_states());
1003
      matched &= opt_edges.contains(aut->num_edges());
1004
      matched &= opt_accsets.contains(aut->acc().num_sets());
1005
      matched &= opt_ap_n.contains(aut->ap().size());
1006
1007
1008
1009
1010
1011
1012
      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);
        }
      if (matched && opt_is_complete)
1013
        matched &= is_complete(aut);
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
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
      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);
            }
        }
1056
1057
      if (opt_nondet_states_set)
        matched &= opt_nondet_states.contains(spot::count_nondet_states(aut));
1058
      if (opt_is_deterministic)
1059
        matched &= is_deterministic(aut);
1060
      else if (opt_is_unambiguous)
1061
        matched &= is_unambiguous(aut);
1062
      if (opt_is_terminal)
1063
        matched &= is_terminal_automaton(aut);
1064
      else if (opt_is_weak)
1065
        matched &= is_weak_automaton(aut);
1066
      else if (opt_is_inherently_weak)
1067
        matched &= is_inherently_weak_automaton(aut);
1068
1069
      if (opt->are_isomorphic)
        matched &= opt->isomorphism_checker->is_isomorphic(aut);
1070
      if (opt_is_empty)
1071
        matched &= aut->is_empty();
1072
      if (opt->intersect)
1073
        matched &= !spot::product(aut, opt->intersect)->is_empty();
1074
      if (opt->included_in)
1075
        matched &= spot::product(aut, opt->included_in)->is_empty();
1076
      if (opt->equivalent_pos)
1077
1078
1079
        matched &= spot::product(aut, opt->equivalent_neg)->is_empty()
          && spot::product(dtwa_complement(ensure_deterministic(aut)),
                           opt->equivalent_pos)->is_empty();
1080
1081

      if (matched && !opt->acc_words.empty())
1082
1083
1084
1085
1086
1087
        for (auto& word_aut: opt->acc_words)
          if (spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
1088
      if (matched && !opt->rej_words.empty())
1089
1090
1091
1092
1093
1094
        for (auto& word_aut: opt->rej_words)
          if (!spot::product(aut, word_aut)->is_empty())
            {
              matched = false;
              break;
            }
1095
1096
1097
1098
1099
1100
      if (opt_is_stutter_invariant)
        {
          check_stutter_invariance(aut);
          assert(aut->prop_stutter_invariant().is_known());
          matched &= aut->prop_stutter_invariant().is_true();
        }
1101

1102
1103
      // Drop or keep matched automata depending on the --invert option
      if (matched == opt_invert)
1104
1105
        return 0;

1106
1107
      // Postprocessing.

1108
      if (opt_mask_acc)
1109
        aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
1110

1111
      if (!opt->rem_ap.empty())
1112
        aut = opt->rem_ap.strip(aut);
1113

1114
1115
1116
1117
1118
      // opt_simplify_exclusive_ap is handled only after
      // post-processing.
      if (!opt->excl_ap.empty())
        aut = opt->excl_ap.constrain(aut, false);

1119
      if (opt_destut)
1120
        aut = spot::closure(std::move(aut));
1121
      if (opt_instut == 1)
1122
        aut = spot::sl(std::move(aut));
1123
      else if (opt_instut == 2)